Improve robustness of :let command (#2297)

* Improve robustness of `:let` command

Fixes #2296

The root cause of the above bug was that the old parser for `:let`
commands was too lenient.  In particular, given a command like:

```
:let x : T = e
```

… the old parser would silently ignore the `: T` part of the command.

This change fixes that by adding support for type annotations and
fixing the `:let` command to exactly match the standard parser in
terms of what expressions it permits.

* Use `NamedFieldPuns`

… as suggested by @sjakobi

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

dhall/src/Dhall/Parser/Expression.hs

@@ -107,6 +107,7 @@ importExpression embedded = importExpression_
 data Parsers a = Parsers
     { completeExpression_ :: Parser (Expr Src a)
     , importExpression_   :: Parser (Expr Src a)
+    , letBinding          :: Parser (Binding Src a)
     }
 
 {-| Parse a numeric `TimeZone`
@@ -237,7 +238,7 @@ temporalLiteral =
 
 -- | Given a parser for imports,
 parsers :: forall a. Parser a -> Parsers a
-parsers embedded = Parsers {..}
+parsers embedded = Parsers{..}
   where
     completeExpression_ =
         many shebang *> whitespace *> expression <* whitespace
@@ -251,6 +252,34 @@ parsers embedded = Parsers {..}
 
         endOfLine
 
+    letBinding = do
+        src0 <- try (_let *> src nonemptyWhitespace)
+
+        c <- label
+
+        src1 <- src whitespace
+
+        d <- optional (do
+            _colon
+
+            src2 <- src nonemptyWhitespace
+
+            e <- expression
+
+            whitespace
+
+            return (Just src2, e) )
+
+        _equal
+
+        src3 <- src whitespace
+
+        f <- expression
+
+        whitespace
+
+        return (Binding (Just src0) c (Just src1) d (Just src3) f)
+
     expression =
         noted
             ( choice
@@ -293,35 +322,7 @@ parsers embedded = Parsers {..}
             return (BoolIf a b c)
 
         alternative2 = do
-            let binding = do
-                    src0 <- try (_let *> src nonemptyWhitespace)
-
-                    c <- label
-
-                    src1 <- src whitespace
-
-                    d <- optional (do
-                        _colon
-
-                        src2 <- src nonemptyWhitespace
-
-                        e <- expression
-
-                        whitespace
-
-                        return (Just src2, e) )
-
-                    _equal
-
-                    src3 <- src whitespace
-
-                    f <- expression
-
-                    whitespace
-
-                    return (Binding (Just src0) c (Just src1) d (Just src3) f)
-
-            as <- NonEmpty.some1 binding
+            as <- NonEmpty.some1 letBinding
 
             try (_in *> nonemptyWhitespace)
 

dhall/src/Dhall/Repl.hs

@@ -62,9 +62,10 @@ import qualified Dhall.Core                          as Expr (Expr (..))
 import qualified Dhall.Import                        as Dhall
 import qualified Dhall.Map                           as Map
 import qualified Dhall.Parser                        as Dhall
-import qualified Dhall.Parser.Token                  as Parser.Token
+import qualified Dhall.Parser.Expression             as Parser.Expression
 import qualified Dhall.Pretty
 import qualified Dhall.Pretty.Internal
+import qualified Dhall.Syntax                        as Syntax
 import qualified Dhall.TypeCheck                     as Dhall
 import qualified Dhall.Version                       as Meta
 import qualified Prettyprinter                       as Pretty
@@ -234,31 +235,51 @@ parseAssignment str
   | otherwise
   = Left (trim str)
 
-addBinding :: ( MonadFail m, MonadIO m, MonadState Env m ) => Either String (String, String) -> m ()
-addBinding (Right (k, src)) = do
-  varName <- case Megaparsec.parse (unParser Parser.Token.label) "(input)" (Text.pack k) of
-      Left   _      -> Fail.fail "Invalid variable name"
-      Right varName -> return varName
+addBinding :: ( MonadFail m, MonadIO m, MonadState Env m ) => String -> m ()
+addBinding string = do
+  let parseBinding =
+          Parser.Expression.letBinding
+              (Parser.Expression.parsers
+                  (Megaparsec.try Parser.Expression.import_)
+              )
 
-  loaded <- parseAndLoad src
+  let input = "let " <> Text.pack string
 
-  t <- typeCheck loaded
+  Syntax.Binding{ variable, annotation, value } <- case Megaparsec.parse (unParser parseBinding) "(input)" input of
+      Left  _       -> Fail.fail ":let should be of the form `:let x [: T] = y`"
+      Right binding -> return binding
 
-  expr <- normalize loaded
+  (resolved, bindingType) <- case annotation of
+      Just (_, unresolvedType) -> do
+          let annotated = Syntax.Annot value unresolvedType
+
+          resolved <- liftIO (Dhall.load annotated)
+
+          _ <- typeCheck resolved
+
+          bindingType <- liftIO (Dhall.load unresolvedType)
+
+          return (resolved, bindingType)
+      _ -> do
+          resolved <- liftIO (Dhall.load value)
+
+          bindingType <- typeCheck resolved
+
+          return (resolved, bindingType)
+
+  bindingExpr <- normalize resolved
 
   modify
     ( \e ->
         e { envBindings =
               Dhall.Context.insert
-                varName
-                Binding { bindingType = t, bindingExpr = expr }
+                variable
+                Binding{ bindingType, bindingExpr }
                 ( envBindings e )
           }
     )
 
-  output ( Expr.Annot ( Expr.Var ( Dhall.V varName 0 ) ) t )
-
-addBinding _ = Fail.fail ":let should be of the form `:let x = y`"
+  output (Expr.Annot (Expr.Var (Dhall.V variable 0)) bindingType)
 
 clearBindings :: (MonadFail m, MonadState Env m) => String -> m ()
 clearBindings _ = modify adapt
@@ -476,7 +497,7 @@ helpOptions =
       "let"
       "IDENTIFIER = EXPRESSION"
       "Assign an expression to a variable"
-      (dontCrash . addBinding . parseAssignment)
+      (dontCrash . addBinding)
   , HelpOption
       "clear"
       ""