Refactor the desugaring of multi-argument functions.

Multi-argument functions are now desuguared into nested lambdas
in the `NoPat` phase instead of during typechecking.  This gives
more sensible results when the same variable is shadowed in the argument
list.  In particular, extra "where" bindings that are added for pattern
desugaring now have a scope that is outside patterns and variables
occuring further to the right.

Some programs that used to produce "overlapping symbols" errors are
now accepted with a shadowing warning instead.

The main downside of this refactoring is that the `checkFun` operation
no longer has access to function name or argument numbers for definitions,
as all functions have become single-argument lambdas by typechecking time.
This can be fixed by recording this information in the AST during the
NoPat desugaring instead.

src/Cryptol/Parser/NoPat.hs

@@ -162,8 +162,7 @@ noPatE expr =
     EWhere e ds   -> EWhere <$> noPatE e <*> noPatDs ds
     ETyped e t    -> ETyped <$> noPatE e <*> return t
     ETypeVal {}   -> return expr
-    EFun ps e     -> do (ps1,e1) <- noPatFun ps e
-                        return (EFun ps1 e1)
+    EFun ps e     -> noPatFun ps e
     ELocated e r1 -> ELocated <$> inRange r1 (noPatE e) <*> return r1
 
     ESplit e      -> ESplit  <$> noPatE e
@@ -174,15 +173,25 @@ noPatE expr =
 noPatUF :: UpdField PName -> NoPatM (UpdField PName)
 noPatUF (UpdField h ls e) = UpdField h ls <$> noPatE e
 
-noPatFun :: [Pattern PName] -> Expr PName -> NoPatM ([Pattern PName], Expr PName)
-noPatFun ps e =
-  do (xs,bs) <- unzip <$> mapM noPat ps
-     e1 <- noPatE e
-     let body = case concat bs of
-                        [] -> e1
-                        ds -> EWhere e1 $ map DBind ds
-     return (xs, body)
-
+-- Desugar lambdas with multiple patterns into a sequence of
+-- lambdas with a single, simple pattern each.  Bindings required
+-- to simplify patterns are placed inside "where" blocks that are
+-- interspersed into the lambdas to ensure that the lexical
+-- structure is reliable, with names on the right shadowing names
+-- on the left.
+noPatFun :: [Pattern PName] -> Expr PName -> NoPatM (Expr PName)
+noPatFun [] e = noPatE e
+noPatFun (p:ps) e =
+  do (p',ds) <- noPat p
+     e' <- noPatFun ps e
+     let body = case ds of
+                  [] -> e'
+                  _  -> EWhere e' $ map DBind (reverse ds)
+                           --                  ^
+                           -- This reverse isn't strictly necessary, but yields more sensible
+                           -- variable ordering results from type inference.  I'm not entirely
+                           -- sure why.
+     return (EFun [p'] body)
 
 noPatArm :: [Match PName] -> NoPatM [Match PName]
 noPatArm ms = concat <$> mapM noPatM ms
@@ -203,8 +212,8 @@ noMatchB b =
                                               , show b ]
 
     DExpr e ->
-      do (ps,e') <- noPatFun (bParams b) e
-         return b { bParams = ps, bDef = DExpr e' <$ bDef b }
+      do e' <- noPatFun (bParams b) e
+         return b { bParams = [], bDef = DExpr e' <$ bDef b }
 
 noMatchD :: Decl PName -> NoPatM [Decl PName]
 noMatchD decl =

tests/issues/issue567.icry.stdout

@@ -2,28 +2,26 @@ Loading module Cryptol
 [warning] at issue567.icry:1:7--1:8
     This binding for `x` shadows the existing binding at
     issue567.icry:1:5--1:6
-(\x x -> x : [8]) : {a} [8] -> a -> [8]
+(\x x -> x : [8]) : {a} a -> [8] -> [8]
 [warning] at issue567.icry:2:11--2:12
     This binding for `x` shadows the existing binding at
     issue567.icry:2:5--2:6
 (\x -> \x -> x : [8]) : {a} a -> [8] -> [8]
-[warning] at issue567.icry:3:6--3:7
+[warning] at issue567.icry:3:12--3:13
     This binding for `x` shadows the existing binding at
-    issue567.icry:3:12--3:13
-(\(x, y) x -> x) : {a, b, c} (c, b) -> a -> c
-
-[error]
-    Overlapping symbols defined:
-    (at issue567.icry:4:6--4:7, x)
-    (at issue567.icry:4:13--4:14, x)
-[error]
-    Overlapping symbols defined:
-    (at issue567.icry:4:9--4:10, y)
-    (at issue567.icry:4:16--4:17, y)
-[warning] at issue567.icry:5:11--5:12
+    issue567.icry:3:6--3:7
+(\(x, y) x -> x) : {a, b, c} (a, b) -> c -> c
+[warning] at issue567.icry:4:16--4:17
+    This binding for `y` shadows the existing binding at
+    issue567.icry:4:9--4:10
+[warning] at issue567.icry:4:13--4:14
     This binding for `x` shadows the existing binding at
-    issue567.icry:5:5--5:6
+    issue567.icry:4:6--4:7
+(\(x, y) (x, y) -> x) : {a, b, c, d} (a, b) -> (c, d) -> c
 [warning] at issue567.icry:5:8--5:9
     This binding for `x` shadows the existing binding at
     issue567.icry:5:5--5:6
-(\x [x] x -> x) : {a, b, c} a -> [1]c -> b -> c
+[warning] at issue567.icry:5:11--5:12
+    This binding for `x` shadows the existing binding at
+    issue567.icry:5:8--5:9
+(\x [x] x -> x) : {a, b, c} a -> [1]b -> c -> c