diff --git a/libs/base/Language/Reflection.idr b/libs/base/Language/Reflection.idr
index 1b320cfb5..5138be954 100644
--- a/libs/base/Language/Reflection.idr
+++ b/libs/base/Language/Reflection.idr
@@ -14,8 +14,8 @@ data Elab : Type -> Type where
      LogMsg : Nat -> String -> Elab ()
      LogTerm : Nat -> String -> TTImp -> Elab ()
 
-     -- Check a TTImp term against the current goal type
-     Check : TTImp -> Elab TT
+     -- Elaborate a TTImp term to a concrete value
+     Check : {expected : Type} -> TTImp -> Elab expected
      -- Get the current goal type, if known 
      -- (it might need to be inferred from the solution)
      Goal : Elab (Maybe TTImp)
@@ -73,9 +73,8 @@ logGoal n msg
               Nothing => pure ()
               Just t => logTerm n msg t
 
--- Check a TTImp term against the current goal type
 export
-check : TTImp -> Elab TT
+check : {expected : Type} -> TTImp -> Elab expected
 check = Check
 
 export
diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr
index 520b6866a..5203ca318 100644
--- a/src/TTImp/Elab/RunElab.idr
+++ b/src/TTImp/Elab/RunElab.idr
@@ -75,7 +75,16 @@ elabScript fc nest env (NDCon nfc nm t ar args) exp
                      pure $ !(reify defs str') ++ ": " ++
                              show (the RawImp !(reify defs tm'))
              scriptRet ()
-    elabCon defs "Check" [ttimp] = evalClosure defs ttimp -- to be reified
+    elabCon defs "Check" [exp, ttimp]
+        = do exp' <- evalClosure defs exp
+             ttimp' <- evalClosure defs ttimp
+             tidx <- resolveName (UN "[elaborator script]")
+             e <- newRef EST (initEState tidx env)
+             (checktm, _) <- runDelays 0 $
+                     check top (initElabInfo InExpr) nest env !(reify defs ttimp')
+                           (Just (glueBack defs env exp'))
+             empty <- clearDefs defs
+             nf empty env checktm
     elabCon defs "Goal" []
         = do let Just gty = exp
                  | Nothing => nfOpts withAll defs env
@@ -138,17 +147,23 @@ checkRunElab : {vars : _} ->
                FC -> RawImp -> Maybe (Glued vars) ->
                Core (Term vars, Glued vars)
 checkRunElab rig elabinfo nest env fc script exp
-    = do defs <- get Ctxt
+    = do expected <- mkExpected exp
+         defs <- get Ctxt
          when (not (isExtension ElabReflection defs)) $
              throw (GenericMsg fc "%language ElabReflection not enabled")
          let n = NS ["Reflection", "Language"] (UN "Elab")
          let ttn = reflectiontt "TT"
-         tt <- getCon fc defs ttn
-         elabtt <- appCon fc defs n [tt]
+         elabtt <- appCon fc defs n [expected]
          (stm, sty) <- runDelays 0 $
                            check rig elabinfo nest env script (Just (gnf env elabtt))
          defs <- get Ctxt -- checking might have resolved some holes
          ntm <- elabScript fc nest env
-                           !(nfOpts withAll defs env stm) exp
+                           !(nfOpts withAll defs env stm) (Just (gnf env expected))
          defs <- get Ctxt -- might have updated as part of the script
-         check rig elabinfo nest env !(reify defs ntm) exp
+         pure (!(quote defs env ntm), gnf env expected)
+  where
+    mkExpected : Maybe (Glued vars) -> Core (Term vars)
+    mkExpected (Just ty) = pure !(getTerm ty)
+    mkExpected Nothing
+        = do nm <- genName "scriptTy"
+             metaVar fc erased env nm (TType fc)
diff --git a/tests/idris2/reflection002/expected b/tests/idris2/reflection002/expected
index d573613f7..f00c46366 100644
--- a/tests/idris2/reflection002/expected
+++ b/tests/idris2/reflection002/expected
@@ -1,5 +1,5 @@
 1/1: Building power (power.idr)
 Main> Main.cube : Nat -> Nat
-cube = \x => mult x (mult x (mult x (const (fromInteger 1) x)))
+cube = \x => mult x (mult x (mult x 1))
 Main> 27
 Main> Bye for now!
diff --git a/tests/idris2/reflection002/power.idr b/tests/idris2/reflection002/power.idr
index 7807612e5..ee62478df 100644
--- a/tests/idris2/reflection002/power.idr
+++ b/tests/idris2/reflection002/power.idr
@@ -7,7 +7,7 @@ powerFn Z = `(const 1)
 powerFn (S k) = `(\x => mult x (~(powerFn k) x))
 
 %macro
-power : Nat -> Elab TT
+power : Nat -> Elab (Nat -> Nat)
 power n = check (powerFn n)
 
 cube : Nat -> Nat
diff --git a/tests/idris2/reflection003/expected b/tests/idris2/reflection003/expected
index f48ec40b1..583a49727 100644
--- a/tests/idris2/reflection003/expected
+++ b/tests/idris2/reflection003/expected
@@ -12,4 +12,4 @@ Error during reflection: Still not trying
 refprims.idr:43:10--45:1:While processing right hand side of dummy3 at refprims.idr:43:1--45:1:
 Error during reflection: Undefined name
 refprims.idr:46:10--48:1:While processing right hand side of dummy4 at refprims.idr:46:1--48:1:
-Error during reflection: failed after generating Main.{plus:5817}
+Error during reflection: failed after generating Main.{plus:5841}
diff --git a/tests/idris2/reflection003/refprims.idr b/tests/idris2/reflection003/refprims.idr
index 3648a2556..952258575 100644
--- a/tests/idris2/reflection003/refprims.idr
+++ b/tests/idris2/reflection003/refprims.idr
@@ -2,7 +2,7 @@ import Language.Reflection
 
 %language ElabReflection
 
-logPrims : Elab TT
+logPrims : Elab a
 logPrims
     = do ns <- getType `{{ (++) }} 
          traverse (\ (n, ty) =>
@@ -10,7 +10,7 @@ logPrims
                            logTerm 0 "Type" ty) ns
          fail "Not really trying"
 
-logDataCons : Elab TT
+logDataCons : Elab a
 logDataCons
     = do [(n, _)] <- getType `{{ Nat }}
              | _ => fail "Ambiguous name"
@@ -18,7 +18,7 @@ logDataCons
          logMsg 0 ("Constructors: " ++ show !(getCons n))
          fail "Still not trying"
 
-logBad : Elab TT
+logBad : Elab a
 logBad
     = do [(n, _)] <- getType `{{ DoesntExist }}
              | [] => fail "Undefined name"
@@ -27,7 +27,7 @@ logBad
          logMsg 0 ("Constructors: " ++ show !(getCons n))
          fail "Still not trying"
 
-tryGenSym : Elab TT
+tryGenSym : Elab a
 tryGenSym
    = do n <- genSym "plus"
         ns <- inCurrentNS n
diff --git a/tests/idris2/reflection004/refdecl.idr b/tests/idris2/reflection004/refdecl.idr
index d4bd1a8b1..58c6bbc1a 100644
--- a/tests/idris2/reflection004/refdecl.idr
+++ b/tests/idris2/reflection004/refdecl.idr
@@ -2,7 +2,7 @@ import Language.Reflection
 
 %language ElabReflection
 
-logDecls : TTImp -> Elab TT
+logDecls : TTImp -> Elab (Int -> Int)
 logDecls v
     = do declare [IClaim EmptyFC MW Public []
                  (MkTy EmptyFC `{{ Main.foo }}
diff --git a/tests/idris2/reflection005/expected b/tests/idris2/reflection005/expected
index 64dacceb4..12df87bd9 100644
--- a/tests/idris2/reflection005/expected
+++ b/tests/idris2/reflection005/expected
@@ -1,9 +1,9 @@
 1/1: Building refdecl (refdecl.idr)
 refdecl.idr:13:16--14:1:While processing right hand side of bad at refdecl.idr:13:1--14:1:
-When unifying Elab () and Elab TT
+When unifying Elab () and Elab a
 Mismatch between:
 	()
 and
-	TT
+	a
 Main> 9400
 Main> Bye for now!
diff --git a/tests/idris2/reflection006/refleq.idr b/tests/idris2/reflection006/refleq.idr
index 8c3accae2..96b14400c 100644
--- a/tests/idris2/reflection006/refleq.idr
+++ b/tests/idris2/reflection006/refleq.idr
@@ -2,7 +2,7 @@ import Language.Reflection
 
 %language ElabReflection
 
-solveReflected : TTImp -> Elab TT
+solveReflected : TTImp -> Elab any
 solveReflected `(Builtin.Equal {a=_} {b=_} ~(left) ~(right))
     = do logTerm 0 "Left" left
          logTerm 0 "Right" right
@@ -12,7 +12,7 @@ solveReflected g
          fail "I don't know how to prove this"
 
 %macro
-prove : Elab TT
+prove : Elab any
 prove
     = do env <- localVars
          Just g <- goal