diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 06148c14de..12faf9801a 100644 --- a/CHANGELOG_NEXT.md +++ b/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 diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 8985d4d7e2..02b41723e1 100644 --- a/src/Idris/Desugar.idr +++ b/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' diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 05c4ef67e8..0b8cfdeb2c 100644 --- a/src/Idris/Parser.idr +++ b/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 diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr index ee44d85cda..b324c4b656 100644 --- a/src/Idris/Pretty.idr +++ b/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 diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 7c712d5e39..3973b1cb4e 100644 --- a/src/Idris/Syntax.idr +++ b/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) diff --git a/src/Idris/Syntax/Traversals.idr b/src/Idris/Syntax/Traversals.idr index f442309736..c2d45212cd 100644 --- a/src/Idris/Syntax/Traversals.idr +++ b/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) diff --git a/tests/idris2/basic/basic072/Issue3327.idr b/tests/idris2/basic/basic072/Issue3327.idr new file mode 100644 index 0000000000..5f390eef4b --- /dev/null +++ b/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 + + diff --git a/tests/idris2/basic/basic072/expected b/tests/idris2/basic/basic072/expected new file mode 100644 index 0000000000..b986a5fd07 --- /dev/null +++ b/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 + ^ + diff --git a/tests/idris2/basic/basic072/run b/tests/idris2/basic/basic072/run new file mode 100755 index 0000000000..7e140a1b22 --- /dev/null +++ b/tests/idris2/basic/basic072/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Issue3327.idr