From 8d8d281fb4742f1e9ad258bee65fb2d4bae65e0c Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sat, 1 Feb 2020 13:54:10 +0000
Subject: [PATCH] Lift ! out of 'let' in do blocks

---
 src/Idris/Desugar.idr | 7 +++++--
 src/Idris/Parser.idr  | 3 ++-
 2 files changed, 7 insertions(+), 3 deletions(-)

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"