[ elab ] Treat (>>) specially in elaborator scripts

libs/base/Language/Reflection.idr

@@ -37,6 +37,7 @@ data Elab : Type -> Type where
      Map  : (a -> b) -> Elab a -> Elab b
      Ap   : Elab (a -> b) -> Elab a -> Elab b
      Bind : Elab a -> (a -> Elab b) -> Elab b
+     Seq  : Elab () -> Elab b -> Elab b
      Fail : FC -> String -> Elab a
      Warn : FC -> String -> Elab ()
 
@@ -122,6 +123,7 @@ Alternative Elab where
 export
 Monad Elab where
   (>>=) = Bind
+  l >> r = Seq l r
 
 -----------------------------
 --- Elaboration interface ---

src/TTImp/Elab/RunElab.idr

@@ -187,6 +187,11 @@ elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp
              k <- evalClosure defs k
              r <- applyToStack defs withAll env k [(getLoc act, toClosure withAll env act)]
              elabScript rig fc nest env r exp
+    elabCon defs "Seq" [_,l,r]
+        -- l : Elab ()
+        -- r : Elab A
+        = do ignore $ elabScript rig fc nest env !(evalClosure defs l) exp
+             elabScript rig fc nest env !(evalClosure defs r) exp
     elabCon defs "Fail" [_, mbfc, msg]
         = do msg' <- evalClosure defs msg
              throw $ RunElabFail $ GenericMsg !(reifyFC defs mbfc) !(reify defs msg')