diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index d48e19f..2e38cc5 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -388,10 +388,13 @@ mutual (PatClause fc bpat rest' :: alts'))) expandDo side ps topfc (DoLet fc n rig ty tm :: rest) - = do tm' <- desugar side ps tm + = do b <- newRef Bang initBangs + tm' <- desugarB side ps tm ty' <- desugar side ps ty rest' <- expandDo side ps topfc rest - pure $ ILet fc rig n ty' tm' rest' + let bind = ILet fc rig n ty' tm' rest' + bd <- get Bang + pure $ bindBangs (bangNames bd) bind expandDo side ps topfc (DoLetPat fc pat ty tm alts :: rest) = do pat' <- desugar LHS ps pat ty' <- desugar side ps ty diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 77b3e03..3afb649 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -159,7 +159,8 @@ mutual arg <- implicitArg fname indents pure (ImpArg (fst arg) (snd arg)) <|> if withOK q - then do symbol "|" + then do continue indents + symbol "|" arg <- expr (record { withOK = False} q) fname indents pure (WithArg arg) else fail "| not allowed here"