In section 3.17 Pattern Matching, there are some inconsistencies between the informal and formal semantics: (1) Section 3.17.2 Informal Semantics of Pattern Matching needs an extra rule (before rule 2): Matching _|_ against the pattern con pat, where con is a constructor defined by newtype, is equivalent to matching _|_ against the pattern pat. (2) Rule 3 "Matching _|_ against a refutable pattern always diverges" is untrue, because rules 4(b) and (c) (numeric literals and n+k patterns) are also applicable to _|_, and it is possible to define the Eq, Ord and Num classes so that pattern matching is non-strict:
data Foo = Foo instance Eq Foo where _ == _ = True instance Ord Foo where _ > _ = False instance Show Foo instance Num Foo
f :: Foo -> Int f 0 = 20
g :: Foo -> Int g (n+1) = 20 -- Hugs incorrectly requires the Integral class
so f undefined = g undefined = 20. Other definitions could be hyperstrict, so _|_/non-_|_ distinction isn't relevant. I'd suggest changing rule 3 to Matching _|_ against a pattern whose outermost component is a constructor defined by data always diverges. deleting rule 4 and promoting the subrules, removing "non-_|_" from (c) and changing "if x < k" to "otherwise". You might wish to say it diverges if x >= k does, but maybe that's too formal. (3) Section 3.17.3 Formal Semantics of Pattern Matching needs an extra equation: case _|_ of { K x1 ... xn -> e; _ -> e' } = _|_ where K is a data constructor of arity n (4) Equation (r) uses let, suggesting the possibility of polymorphism -- I'd suggest changing the rhs to if v >= k then case v-k of { x -> e } else e'