Add type annotations to monadic bind #3327 (#3329)

* [ new ] Support type annotations on monadic bind

* don't parse quantites on patbind

* Update changelog

CHANGELOG_NEXT.md

@@ -55,6 +55,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * The language now has a ``%foreign_impl`` pragma to add additional languages
   to a ``%foreign`` function.
 
+* Bind expressions in `do` blocks can now have a type ascription.
+  See [#3327](https://github.com/idris-lang/Idris2/issues/3327).
+
 ### Compiler changes
 
 * The compiler now differentiates between "package search path" and "package

src/Idris/Desugar.idr

@@ -735,14 +735,15 @@ mutual
       = do tm' <- desugarDo side ps ns tm
            rest' <- expandDo side ps topfc ns rest
            pure $ seqFun fc ns tm' rest'
-  expandDo side ps topfc ns (DoBind fc nameFC n tm :: rest)
+  expandDo side ps topfc ns (DoBind fc nameFC n rig ty tm :: rest)
       = do tm' <- desugarDo side ps ns tm
            rest' <- expandDo side ps topfc ns rest
            whenJust (isConcreteFC nameFC) $ \nfc => addSemanticDecorations [(nfc, Bound, Just n)]
+           ty' <- maybe (pure $ Implicit (virtualiseFC fc) False)
+                        (\ty => desugarDo side ps ns ty) ty
            pure $ bindFun fc ns tm'
-                $ ILam nameFC top Explicit (Just n)
-                       (Implicit (virtualiseFC fc) False) rest'
-  expandDo side ps topfc ns (DoBindPat fc pat exp alts :: rest)
+                $ ILam nameFC rig Explicit (Just n) ty' rest'
+  expandDo side ps topfc ns (DoBindPat fc pat ty exp alts :: rest)
       = do pat' <- desugarDo LHS ps ns pat
            (newps, bpat) <- bindNames False pat'
            exp' <- desugarDo side ps ns exp
@@ -752,9 +753,11 @@ mutual
            let fcOriginal = fc
            let fc = virtualiseFC fc
            let patFC = virtualiseFC (getFC bpat)
+           ty' <- maybe (pure $ Implicit fc False)
+                        (\ty => desugarDo side ps ns ty) ty
            pure $ bindFun fc ns exp'
                 $ ILam EmptyFC top Explicit (Just (MN "_" 0))
-                          (Implicit fc False)
+                          ty'
                           (ICase fc [] (IVar patFC (MN "_" 0))
                                (Implicit fc False)
                                (PatClause fcOriginal bpat rest'

src/Idris/Parser.idr

@@ -977,16 +977,18 @@ mutual
 
   doAct : OriginDesc -> IndentInfo -> Rule (List PDo)
   doAct fname indents
-      = do b <- bounds (do n <- bounds (name <|> UN Underscore <$ symbol "_")
+      = do b <- bounds (do rig <- multiplicity fname
+                           n <- bounds (name <|> UN Underscore <$ symbol "_")
                            -- If the name doesn't begin with a lower case letter, we should
                            -- treat this as a pattern, so fail
                            validPatternVar n.val
+                           ty <- optional (decoratedSymbol fname ":" *> typeExpr (pnoeq pdef) fname indents)
                            decoratedSymbol fname "<-"
                            val <- expr pdef fname indents
-                           pure (n, val))
+                           pure (n, rig, ty, val))
            atEnd indents
-           let (n, val) = b.val
-           pure [DoBind (boundToFC fname b) (boundToFC fname n) n.val val]
+           let (n, rig, ty, val) = b.val
+           pure [DoBind (boundToFC fname b) (boundToFC fname n) n.val rig ty val]
     <|> do decoratedKeyword fname "let"
            commit
            res <- nonEmptyBlock (letBlock fname)
@@ -1000,11 +1002,12 @@ mutual
            pure [DoRewrite (boundToFC fname b) b.val]
     <|> do e <- bounds (expr plhs fname indents)
            (atEnd indents $> [DoExp (virtualiseFC $ boundToFC fname e) e.val])
-             <|> (do b <- bounds $ decoratedSymbol fname "<-" *> [| (expr pnowith fname indents, block (patAlt fname)) |]
+             <|> (do ty <- optional (decoratedSymbol fname ":" *> typeExpr (pnoeq pdef) fname indents)
+                     b <- bounds $ decoratedSymbol fname "<-" *> [| (expr pnowith fname indents, block (patAlt fname)) |]
                      atEnd indents
                      let (v, alts) = b.val
                      let fc = virtualiseFC $ boundToFC fname (mergeBounds e b)
-                     pure [DoBindPat fc e.val v alts])
+                     pure [DoBindPat fc e.val ty v alts])
 
   patAlt : OriginDesc -> IndentInfo -> Rule PClause
   patAlt fname indents

src/Idris/Pretty.idr

@@ -133,8 +133,13 @@ mutual
 
   prettyPDo : PDo' KindedName -> Doc IdrisSyntax
   prettyPDo (DoExp _ tm) = pretty tm
-  prettyPDo (DoBind _ _ n tm) = pretty0 n <++> keyword "<-" <++> pretty tm
-  prettyPDo (DoBindPat _ l tm alts) =
+  prettyPDo (DoBind _ _ n rig (Just ty) tm) =
+      prettyRig rig <+> pretty0 n <++> colon <++> pretty ty <++> keyword "<-" <++> pretty tm
+  prettyPDo (DoBind _ _ n rig Nothing tm) =
+      prettyRig rig <+> pretty0 n <++> keyword "<-" <++> pretty tm
+  prettyPDo (DoBindPat _ l (Just ty) tm alts) =
+      pretty l <++> colon <++> keyword "<-" <++> pretty tm <+> hang 4 (fillSep $ prettyAlt <$> alts)
+  prettyPDo (DoBindPat _ l Nothing tm alts) =
       pretty l <++> keyword "<-" <++> pretty tm <+> hang 4 (fillSep $ prettyAlt <$> alts)
   prettyPDo (DoLet _ _ l rig _ tm) =
       let_ <++> prettyRig rig <+> pretty0 l <++> equals <++> pretty tm

src/Idris/Syntax.idr

@@ -239,8 +239,8 @@ mutual
   public export
   data PDo' : Type -> Type where
        DoExp : FC -> PTerm' nm -> PDo' nm
-       DoBind : FC -> (nameFC : FC) -> Name -> PTerm' nm -> PDo' nm
-       DoBindPat : FC -> PTerm' nm -> PTerm' nm -> List (PClause' nm) -> PDo' nm
+       DoBind : FC -> (nameFC : FC) -> Name -> RigCount -> Maybe (PTerm' nm) -> PTerm' nm -> PDo' nm
+       DoBindPat : FC -> PTerm' nm -> Maybe (PTerm' nm) -> PTerm' nm -> List (PClause' nm) -> PDo' nm
        DoLet : FC -> (lhs : FC) -> Name -> RigCount -> PTerm' nm -> PTerm' nm -> PDo' nm
        DoLetPat : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm -> List (PClause' nm) -> PDo' nm
        DoLetLocal : FC -> List (PDecl' nm) -> PDo' nm
@@ -258,8 +258,8 @@ mutual
   export
   getLoc : PDo' nm -> FC
   getLoc (DoExp fc _) = fc
-  getLoc (DoBind fc _ _ _) = fc
-  getLoc (DoBindPat fc _ _ _) = fc
+  getLoc (DoBind fc _ _ _ _ _) = fc
+  getLoc (DoBindPat fc _ _ _ _) = fc
   getLoc (DoLet fc _ _ _ _ _) = fc
   getLoc (DoLetPat fc _ _ _ _) = fc
   getLoc (DoLetLocal fc _) = fc
@@ -710,8 +710,11 @@ parameters {0 nm : Type} (toName : nm -> Name)
   showAlt (MkImpossible _ lhs) = " | " ++ showPTerm lhs ++ " impossible;"
 
   showDo (DoExp _ tm) = showPTerm tm
-  showDo (DoBind _ _ n tm) = show n ++ " <- " ++ showPTerm tm
-  showDo (DoBindPat _ l tm alts)
+  showDo (DoBind _ _ n rig (Just ty) tm) = showCount rig ++ show n ++ " : " ++ showPTerm ty ++ " <- " ++ showPTerm tm
+  showDo (DoBind _ _ n rig _ tm) = showCount rig ++ show n ++ " <- " ++ showPTerm tm
+  showDo (DoBindPat _ l (Just ty) tm alts)
+      = showPTerm l ++ " : " ++ showPTerm ty ++ " <- " ++ showPTerm tm ++ concatMap showAlt alts
+  showDo (DoBindPat _ l _ tm alts)
       = showPTerm l ++ " <- " ++ showPTerm tm ++ concatMap showAlt alts
   showDo (DoLet _ _ l rig _ tm) = "let " ++ show l ++ " = " ++ showPTerm tm
   showDo (DoLetPat _ l _ tm alts)

src/Idris/Syntax/Traversals.idr

@@ -216,9 +216,10 @@ mapPTermM f = goPTerm where
 
     goPDo : PDo' nm -> Core (PDo' nm)
     goPDo (DoExp fc t) = DoExp fc <$> goPTerm t
-    goPDo (DoBind fc nameFC n t) = DoBind fc nameFC n <$> goPTerm t
-    goPDo (DoBindPat fc t u cls) =
+    goPDo (DoBind fc nameFC n c ty t) = DoBind fc nameFC n c <$> goMPTerm ty <*> goPTerm t
+    goPDo (DoBindPat fc t ty u cls) =
       DoBindPat fc <$> goPTerm t
+                   <*> goMPTerm ty
                    <*> goPTerm u
                    <*> goPClauses cls
     goPDo (DoLet fc lhsFC n c t scope) =
@@ -513,9 +514,9 @@ mapPTerm f = goPTerm where
 
     goPDo : PDo' nm -> PDo' nm
     goPDo (DoExp fc t) = DoExp fc $ goPTerm t
-    goPDo (DoBind fc nameFC n t) = DoBind fc nameFC n $ goPTerm t
-    goPDo (DoBindPat fc t u cls)
-      = DoBindPat fc (goPTerm t) (goPTerm u) (goPClause <$> cls)
+    goPDo (DoBind fc nameFC n c ty t) = DoBind fc nameFC n c (goPTerm <$> ty) (goPTerm t)
+    goPDo (DoBindPat fc t ty u cls)
+      = DoBindPat fc (goPTerm t) (goPTerm <$> ty) (goPTerm u) (goPClause <$> cls)
     goPDo (DoLet fc lhsFC n c t scope)
       = DoLet fc lhsFC n c (goPTerm t) (goPTerm scope)
     goPDo (DoLetPat fc pat t scope cls)

tests/idris2/basic/basic072/Issue3327.idr

@@ -0,0 +1,36 @@
+foo : IO Nat
+
+test1 : IO ()
+test1 = do
+  x : Nat <- foo
+  printLn x
+
+test2 : IO ()
+test2 = do
+  1 x : Nat <- foo
+  printLn x
+
+test3 : IO ()
+test3 = do
+  0 x : Nat <- foo
+  printLn x
+
+test4 : IO ()
+test4 = do
+  1 x <- foo
+  printLn x
+
+test5 : IO ()
+test5 = do
+  0 x <- foo
+  printLn x
+
+bar : IO (Maybe Nat)
+
+test6 : IO ()
+test6 = do
+  Just x : Maybe Nat <- bar
+    | Nothing => pure ()
+  printLn x
+
+

tests/idris2/basic/basic072/expected

@@ -0,0 +1,41 @@
+1/1: Building Issue3327 (Issue3327.idr)
+Error: While processing right hand side of test2. Trying to use linear name x in non-linear context.
+
+Issue3327:11:11--11:12
+ 07 | 
+ 08 | test2 : IO ()
+ 09 | test2 = do
+ 10 |   1 x : Nat <- foo
+ 11 |   printLn x
+                ^
+
+Error: While processing right hand side of test3. x is not accessible in this context.
+
+Issue3327:16:11--16:12
+ 12 | 
+ 13 | test3 : IO ()
+ 14 | test3 = do
+ 15 |   0 x : Nat <- foo
+ 16 |   printLn x
+                ^
+
+Error: While processing right hand side of test4. Trying to use linear name x in non-linear context.
+
+Issue3327:21:11--21:12
+ 17 | 
+ 18 | test4 : IO ()
+ 19 | test4 = do
+ 20 |   1 x <- foo
+ 21 |   printLn x
+                ^
+
+Error: While processing right hand side of test5. x is not accessible in this context.
+
+Issue3327:26:11--26:12
+ 22 | 
+ 23 | test5 : IO ()
+ 24 | test5 = do
+ 25 |   0 x <- foo
+ 26 |   printLn x
+                ^
+

tests/idris2/basic/basic072/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Issue3327.idr