Part of Lemma 4.8 (completeness of type inference for pattern matching) seems incorrect. A counter example by Stijn Vansummeren is: T = ab | abb P = (x as (ab | a)) (b | \eps) Although it does not affect soundness, the problem is important and not easy to fix.