[ fix #2088 ] Make %runElab expression propagate its rig to check

src/TTImp/Elab/RunElab.idr

@@ -53,10 +53,10 @@ elabScript : {vars : _} ->
              {auto u : Ref UST UState} ->
              {auto s : Ref Syn SyntaxInfo} ->
              {auto o : Ref ROpts REPLOpts} ->
-             FC -> NestedNames vars ->
+             RigCount -> FC -> NestedNames vars ->
              Env Term vars -> NF vars -> Maybe (Glued vars) ->
              Core (NF vars)
-elabScript fc nest env script@(NDCon nfc nm t ar args) exp
+elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp
     = do defs <- get Ctxt
          fnm <- toFullNames nm
          case fnm of
@@ -91,12 +91,12 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp
         -- 2) Evaluate the resulting act
         -- 3) apply k to the result of (2)
         -- 4) Run elabScript on the result stripping off Elab
-        = do act <- elabScript fc nest env
+        = do act <- elabScript rig fc nest env
                                 !(evalClosure defs act) exp
              act <- quote defs env act
              k <- evalClosure defs k
              r <- applyToStack defs withAll env k [(getLoc act, toClosure withAll env act)]
-             elabScript fc nest env r exp
+             elabScript rig fc nest env r exp
     elabCon defs "Fail" [_, mbfc, msg]
         = do msg' <- evalClosure defs msg
              let customFC = case !(evalClosure defs mbfc >>= reify defs) of
@@ -105,13 +105,13 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp
              throw $ RunElabFail $ GenericMsg customFC !(reify defs msg')
     elabCon defs "Try" [_, elab1, elab2]
         = tryUnify (do constart <- getNextEntry
-                       res <- elabScript fc nest env !(evalClosure defs elab1) exp
+                       res <- elabScript rig fc nest env !(evalClosure defs elab1) exp
                        -- We ensure that all of the constraints introduced during the elab script
                        -- have been solved. This guarantees that we do not mistakenly succeed even
                        -- though e.g. a proof search got delayed.
                        solveConstraintsAfter constart inTerm LastChance
                        pure res)
-                   (elabScript fc nest env !(evalClosure defs elab2) exp)
+                   (elabScript rig fc nest env !(evalClosure defs elab2) exp)
     elabCon defs "LogMsg" [topic, verb, str]
         = do topic' <- evalClosure defs topic
              verb' <- evalClosure defs verb
@@ -143,7 +143,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp
              tidx <- resolveName (UN $ Basic "[elaborator script]")
              e <- newRef EST (initEState tidx env)
              (checktm, _) <- runDelays (const True) $
-                     check top (initElabInfo InExpr) nest env !(reify defs ttimp')
+                     check rig (initElabInfo InExpr) nest env !(reify defs ttimp')
                            (Just (glueBack defs env exp'))
              empty <- clearDefs defs
              nf empty env checktm
@@ -164,7 +164,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp
              qty <- quote empty env ty
              let env' = Lam fc' c qp qty :: env
 
-             runsc <- elabScript fc (weaken nest) env'
+             runsc <- elabScript rig fc (weaken nest) env'
                                  !(nf defs env' lamsc) Nothing -- (map weaken exp)
              nf empty env (Bind bfc x (Lam fc' c qp qty) !(quote empty env' runsc))
        where
@@ -224,7 +224,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp
              scriptRet ()
     elabCon defs n args = failWith defs $ "unexpected Elab constructor " ++ n ++
                                           ", or incorrect count of arguments: " ++ show (length args)
-elabScript fc nest env script exp
+elabScript rig fc nest env script exp
     = do defs <- get Ctxt
          empty <- clearDefs defs
          throw (BadRunElab fc env !(quote empty env script) "script is not a data value")
@@ -252,7 +252,7 @@ checkRunElab rig elabinfo nest env fc script exp
                            check rig elabinfo nest env script (Just (gnf env elabtt))
          solveConstraints inTerm Normal
          defs <- get Ctxt -- checking might have resolved some holes
-         ntm <- elabScript fc nest env
+         ntm <- elabScript rig fc nest env
                            !(nfOpts withAll defs env stm) (Just (gnf env expected))
          defs <- get Ctxt -- might have updated as part of the script
          empty <- clearDefs defs

src/TTImp/ProcessRunElab.idr

@@ -39,4 +39,4 @@ processRunElab eopts nest env fc tm
          exp <- appCon fc defs n [unit]
 
          stm <- checkTerm tidx InExpr eopts nest env tm (gnf env exp)
-         ignore $ elabScript fc nest env !(nfOpts withAll defs env stm) Nothing
+         ignore $ elabScript top fc nest env !(nfOpts withAll defs env stm) Nothing

tests/Main.idr

@@ -231,7 +231,8 @@ idrisTestsReflection = MkTestPool "Quotation and Reflection" [] Nothing
       ["reflection001", "reflection002", "reflection003", "reflection004",
        "reflection005", "reflection006", "reflection007", "reflection008",
        "reflection009", "reflection010", "reflection011", "reflection012",
-       "reflection013", "reflection014", "reflection015", "reflection016"]
+       "reflection013", "reflection014", "reflection015", "reflection016",
+       "reflection017"]
 
 idrisTestsWith : TestPool
 idrisTestsWith = MkTestPool "With abstraction" [] Nothing

tests/idris2/reflection017/CanElabType.idr

@@ -0,0 +1,36 @@
+module CanElabType
+
+import Data.Vect
+
+import Language.Reflection
+
+%language ElabReflection
+
+0 T : Nat -> Type
+T n = Vect n Nat
+
+desiredType : TTImp
+desiredType = IApp EmptyFC (IVar EmptyFC `{CanElabType.T}) `(3)
+
+elabDecl : Name -> Elab Unit
+elabDecl n = declare [
+    IClaim EmptyFC MW Public [] $ MkTy EmptyFC EmptyFC n desiredType
+  ]
+
+%runElab elabDecl `{x1}
+x1 = [1, 2, 3]
+
+export
+elabExpr : Elab Type
+elabExpr = check desiredType
+
+-- should typecheck because the rig of calling is zero
+
+x2 : %runElab elabExpr
+x2 = [1, 2, 3]
+
+-- Check that zero can't escape
+failing "CanElabType.T is not accessible in this context"
+
+  T' : Type
+  T' = %runElab elabExpr

tests/idris2/reflection017/StillCantEscape.idr

@@ -0,0 +1,13 @@
+module StillCantEscape
+
+import CanElabType
+
+import Language.Reflection
+
+%language ElabReflection
+
+-- check that zero does not leak, should not typecheck
+failing "CanElabType.T is private"
+
+  T' : Type
+  T' = %runElab elabExpr

tests/idris2/reflection017/expected

@@ -0,0 +1,2 @@
+1/1: Building CanElabType (CanElabType.idr)
+2/2: Building StillCantEscape (StillCantEscape.idr)

tests/idris2/reflection017/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check CanElabType.idr
+$1 --no-color --console-width 0 --no-banner --check StillCantEscape.idr