diff --git a/src/Algebra/Preorder.idr b/src/Algebra/Preorder.idr
index 385c5861a22..ed9176c526f 100644
--- a/src/Algebra/Preorder.idr
+++ b/src/Algebra/Preorder.idr
@@ -29,3 +29,9 @@ public export
 interface Preorder a => Top a where
   top : a
   topAbs : {x : a} -> x <= top = True
+
+||| The least bound of a bounded lattice
+public export
+interface Preorder a => Bot a where
+  bot : a
+  botAbs : {x : a} -> bot <= x = True
diff --git a/src/Algebra/ZeroOneOmega.idr b/src/Algebra/ZeroOneOmega.idr
index d50a5b4d659..e18e51e319d 100644
--- a/src/Algebra/ZeroOneOmega.idr
+++ b/src/Algebra/ZeroOneOmega.idr
@@ -72,6 +72,14 @@ Top ZeroOneOmega where
   topAbs {x = Rig1} = Refl
   topAbs {x = RigW} = Refl
 
+||| The bottom value of a lattice
+export
+Bot ZeroOneOmega where
+  bot = Rig0
+  botAbs {x = Rig0} = Refl
+  botAbs {x = Rig1} = Refl
+  botAbs {x = RigW} = Refl
+
 ----------------------------------------
 
 rigPlusAssociative : (x, y, z : ZeroOneOmega) ->
diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr
index 9b709b73e6a..813f541315e 100644
--- a/src/TTImp/Elab/RunElab.idr
+++ b/src/TTImp/Elab/RunElab.idr
@@ -353,8 +353,8 @@ checkRunElab rig elabinfo nest env fc reqExt script exp
              throw (GenericMsg fc "%language ElabReflection not enabled")
          let n = NS reflectionNS (UN $ Basic "Elab")
          elabtt <- appCon fc defs n [expected]
-         (stm, sty) <- runDelays (const True) $
-                           check rig elabinfo nest env script (Just (gnf env elabtt))
+         (stm, _) <- runDelays (const True) $
+                           check bot elabinfo nest env script (Just (gnf env elabtt))
          solveConstraints inTerm Normal
          defs <- get Ctxt -- checking might have resolved some holes
          ntm <- elabScript rig fc nest env
diff --git a/src/TTImp/ProcessRunElab.idr b/src/TTImp/ProcessRunElab.idr
index 12e84e4525e..786f20eae7a 100644
--- a/src/TTImp/ProcessRunElab.idr
+++ b/src/TTImp/ProcessRunElab.idr
@@ -38,5 +38,6 @@ processRunElab eopts nest env fc tm
          unit <- getCon fc defs (builtin "Unit")
          exp <- appCon fc defs n [unit]
 
-         stm <- checkTerm tidx InExpr eopts nest env tm (gnf env exp)
+         e <- newRef EST $ initEStateSub tidx env SubRefl
+         (stm, _) <- check bot (initElabInfo InExpr) nest env tm $ Just $ gnf env exp
          ignore $ elabScript top fc nest env !(nfOpts withAll defs env stm) Nothing
diff --git a/tests/idris2/reflection/reflection027/NoEscape.idr b/tests/idris2/reflection/reflection027/NoEscape.idr
new file mode 100644
index 00000000000..3a5b50c33a9
--- /dev/null
+++ b/tests/idris2/reflection/reflection027/NoEscape.idr
@@ -0,0 +1,16 @@
+module NoEscape
+
+import Language.Reflection
+
+%language ElabReflection
+
+0 n : Nat
+n = 3
+
+0 elabScript : Elab Nat
+elabScript = pure n
+
+failing "n is not accessible in this context"
+
+  m : Nat
+  m = %runElab elabScript
diff --git a/tests/idris2/reflection/reflection027/NoEscapePar.idr b/tests/idris2/reflection/reflection027/NoEscapePar.idr
new file mode 100644
index 00000000000..1f37d7de66f
--- /dev/null
+++ b/tests/idris2/reflection/reflection027/NoEscapePar.idr
@@ -0,0 +1,35 @@
+||| Check that we cannot implement function illegally escaping zero quantity using elaboration reflection
+module NoEscapePar
+
+import Language.Reflection
+
+%language ElabReflection
+
+escScr : Elab $ (0 _ : a) -> a
+escScr = check $ ILam EmptyFC M0 ExplicitArg (Just `{x}) `(a) `(x)
+
+failing "x is not accessible in this context"
+
+  esc : (0 _ : a) -> a
+  esc = %runElab escScr
+
+escd : (0 _ : a) -> a
+
+0 escd' : (0 _ : a) -> a
+
+escDecl : Name -> Elab Unit
+escDecl name = declare [
+                 IDef EmptyFC name [
+                   PatClause EmptyFC
+                     -- lhs
+                     (IApp EmptyFC (IVar EmptyFC name) (IBindVar EmptyFC "x"))
+                     -- rhs
+                     `(x)
+                 ]
+               ]
+
+%runElab escDecl `{escd'}
+
+failing "x is not accessible in this context"
+
+  %runElab escDecl `{escd}
diff --git a/tests/idris2/reflection/reflection027/RunElab0.idr b/tests/idris2/reflection/reflection027/RunElab0.idr
new file mode 100644
index 00000000000..c72996546bc
--- /dev/null
+++ b/tests/idris2/reflection/reflection027/RunElab0.idr
@@ -0,0 +1,13 @@
+module RunElab0
+
+import Language.Reflection
+
+%language ElabReflection
+
+0 elabScript : Elab Unit
+elabScript = pure ()
+
+x : Unit
+x = %runElab elabScript
+
+%runElab elabScript
diff --git a/tests/idris2/reflection/reflection027/expected b/tests/idris2/reflection/reflection027/expected
new file mode 100644
index 00000000000..28bf1ab381a
--- /dev/null
+++ b/tests/idris2/reflection/reflection027/expected
@@ -0,0 +1,3 @@
+1/1: Building RunElab0 (RunElab0.idr)
+1/1: Building NoEscape (NoEscape.idr)
+1/1: Building NoEscapePar (NoEscapePar.idr)
diff --git a/tests/idris2/reflection/reflection027/run b/tests/idris2/reflection/reflection027/run
new file mode 100755
index 00000000000..d08d68d0627
--- /dev/null
+++ b/tests/idris2/reflection/reflection027/run
@@ -0,0 +1,5 @@
+. ../../../testutils.sh
+
+check RunElab0.idr
+check NoEscape.idr
+check NoEscapePar.idr