Parsing of lambda and where

[brianhuffman]

Currently, the cryptol parser doesn't extend the scope of lambdas over where clauses. For example:

Cryptol> (\(x:[8]) -> y+y where y = x + 2)

[error] at <interactive>:1:28--1:29 Value not in scope: x

It might be considered less surprising if we changed the parser so that the scope of the lambda extended over the where clause, so that this would be accepted.

[brianhuffman]

A related question is how should where interact with if/then/else.
Should if a then b else c where d = e parse as

• (if a then b else c) where d = e, or as
• if a then b else (c where d = e)?

[robdockins]

I think where should extend left as far as possible, even across lambdas and if/then/else, etc. For example, the following program currently works (and I think it should), where as the proposed change would break it.

asdf : Integer -> Integer
asdf x = f \y -> x+y
  where
    f g = g (g 0)

[robdockins]

I get the impression that we have not arrived at a strong consensus that this should be changed, and I'm going to suggest we break the tie in favor of not changing things.

If you disagree and think this deserves more discussion, feel free to reopen.