On Wed, Jul 10, 2013 at 3:08 AM, Andreas Abel <andreas.abel@ifi.lmu.de> wrote:

Another instance (cut-down) are let-guards like

let Just x | x > 0 = e in x

The "x > 0" is understood as an assertion here, documenting an invariant. However, Haskell reads this as

let Just x = case () of { () | x > 0 -> e } in x

leading to non-termination. A non-recursive version

let' Just x | x > 0 = e in x

could be interpreted as

case e of { Just x | x > 0 -> x }

instead, which is meaningful (in contrast to the current interpretation).

I still don't understand how this is supposed to work. It is a completely different interpretation of guarded definitions that can only apply to certain special cases.

Specifically, you have a let with one definition with one guard. This lets you permute the pieces into a case, because there is one of everything. But, if we instead have two guards, then we have two possible bodies of the definition, and only one body of the let. But, the case has only one discriminee (which comes from the definition body), and two branches (which are supposed to come from the let body). We have the wrong number of pieces to shuffle everything around.

The only general desugaring is the one in the report, but keeping the non-recursive let. This means that the x in the guard refers to an outer scope. But it is still equivalent to:

let' Just x = case x > 0 of True -> e in x

let' x = case (case x > 0 of True -> e) of ~(Just y) -> y in x

not:

case e of Just x | x > 0 -> x

case e of Just x -> case x > 0 of True -> x