Errata for the final accepted version of Type Inference, Haskell and Dependent Types Adam Michael Gundry PhD thesis, 2013 9th August 2014 Please report any further errors to adam (at) well (dash) typed (dot) com. 1. Pruning is not most general In the description of higher-order pattern unification, the final rule for pruning given on page 72, prune V Δ ts ↦ Δ' fv^rig(s) ⊄ V ---------------------------------- prune V (Δ,x:S) (ts,s) ↦ Δ' does not lead to most general solutions. For example, consider α : 𝔹, β : ((𝔹 → 𝔹) → 𝔹) → 𝔹 | x : 𝔹 ⊢ α ≈ β (λ f. f x) : 𝔹 Then pruning 𝔹 is successful and the rule allows the derivation of prune ∅ (x:𝔹) (λ f. f x) ↦ . since fv^rig(λ f. f x) = {x}, but this loses the solution β = λ k. k (λ _. α). Similarly, the problem α ≅ β (tt, x) is erroneously pruned, despite having the solution β = λ z. if z HD then tt else z TL. Instead, the side condition should be strengthened to require not only that fv^rig(s) ⊄ V, but that one of the variables not in V occurs in a "non-eliminateable" position (i.e. a position such that no instance of the metavariable can project away the bad variable). Lemma D.8 (Generality of pruning, page 248) is false as stated. It makes the assumption that fv^rig(t) ⊈ V implies fv^rig(θ t) ⊈ V, which is not the case for β-normal forms, because rigid free variables may be eliminated by the combination of substitution for metavariables and β-reduction (as in the above examples). Thanks to Andreas Abel for pointing out this problem. See also the errata for "Higher-Order Dynamic Pattern Unification for Dependent Types and Records" by Andreas Abel and Brigitte Pientka (2011) [1] and a related bug in Agda [2]. [1] http://www.cse.chalmers.se/~abela/errata-tlca11.txt [2] https://code.google.com/p/agda/issues/detail?id=458