Michael, (Sorry for duplicates; I sent this from the wrong address initially.)

(m) case v of { K { f1 = p1 , f2 = p2 , ... } -> e ; _ -> e' } = case e' of { y -> case v of { K { f1 = p1 } -> case v of { K { f2 = p2 , ... } -> e ; _ -> y }; _ -> y }} where f1, f2, ... are fields of constructor K; y is a new variable [...] I'm totally confused with this identity. Especialy with " = case e'". Can anyone explain a little what does this rule stand, please? It is better to see some example.

You got me curious, so I looked over this. The table you reference lists identities that should hold for all implementations of case expressions. (m) is about how case matches against constructors with named fields, and it shows that a case expression that matches against multiple fields (f1, f2, etc.) can be broken into nested case expressions which each match a single field (eg. f1). It looks like "case e' of { y -> ..." was introduced solely to give e' a name that can be used in two places, since the nested form may fail to match at each level. It seems to me that without this, you could get code explosion from duplicating the expression e' below; with this you get sharing. Here it is with a interim step added: -- Match v against a constructor with multiple fields case v of { K { f1 = p1 , f2 = p2 , ... } -> e ; _ -> e' } -- Same, but introduce y to represent e' without loss of sharing case e' of { y -> case v of { K { f1 = p1 , f2 = p2 , ... } -> e ; _ -> y }} -- Same, but match first field of K independent of the rest case e' of { y -> case v of { K { f1 = p1 } -> case v of { K { f2 = p2 , ... } -> e ; _ -> y }; _ -> y }} I hope this helps. Regards, John