@@ -1746,6 +1746,11 @@ runTactical ist fc env tm = do tm' <- eval tm
17461746 updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}
17471747 return ()
17481748
1749+ checkClosed :: Raw -> Elab' aux (Term, Type)
1750+ checkClosed tm = do ctxt <- get_context
1751+ (val, ty) <- lift $ check ctxt [] tm
1752+ return $! (finalise val, finalise ty)
1753+
17491754 -- | Do a step in the reflected elaborator monad. The input is the
17501755 -- step, the output is the (reflected) term returned.
17511756 runTacTm :: Term -> ElabD Term
@@ -1756,12 +1761,12 @@ runTactical ist fc env tm = do tm' <- eval tm
17561761 | n == tacN "prim__Goal", [] <- args
17571762 = do (h:_) <- get_holes
17581763 t <- goal
1759− fmap fst . get_type_val $
1764+ fmap fst . checkClosed $
17601765 rawPair (Var (reflm "TTName"), Var (reflm "TT"))
17611766 (reflectName h, reflect t)
17621767 | n == tacN "prim__Holes", [] <- args
17631768 = do hs <- get_holes
1764− fmap fst . get_type_val $
1769+ fmap fst . checkClosed $
17651770 mkList (Var $ reflm "TTName") (map reflectName hs)
17661771 | n == tacN "prim__Guess", [] <- args
17671772 = do ok <- is_guess
@@ -1771,7 +1776,7 @@ runTactical ist fc env tm = do tm' <- eval tm
17711776 RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))
17721777 (Var (reflm "TT")))
17731778 guess
1774− else fmap fst . get_type_val $
1779+ else fmap fst . checkClosed $
17751780 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
17761781 (Var (reflm "TT"))
17771782 | n == tacN "prim__LookupTy", [n] <- args
@@ -1791,7 +1796,7 @@ runTactical ist fc env tm = do tm' <- eval tm
17911796 let defs = [ reflectTriple (reflectName n, reflectNameType nt, reflect ty)
17921797 | (n, def) <- lookupNameDef n' ctxt
17931798 , let (nt, ty) = getNameTypeAndType def ]
1794− fmap fst . get_type_val $
1799+ fmap fst . checkClosed $
17951800 rawList (raw_apply (Var pairTy) [ Var (reflm "TTName")
17961801 , raw_apply (Var pairTy) [ Var (reflm "NameType")
17971802 , Var (reflm "TT")]])
@@ -1800,15 +1805,15 @@ runTactical ist fc env tm = do tm' <- eval tm
18001805 = do n' <- reifyTTName name
18011806 datatypes <- get_datatypes
18021807 ctxt <- get_context
1803− fmap fst . get_type_val $
1808+ fmap fst . checkClosed $
18041809 rawList (Var (tacN "Datatype"))
18051810 (map reflectDatatype (buildDatatypes ctxt datatypes n'))
18061811 | n == tacN "prim__SourceLocation", [] <- args
1807− = fmap fst . get_type_val $
1812+ = fmap fst . checkClosed $
18081813 reflectFC fc
18091814 | n == tacN "prim__Env", [] <- args
18101815 = do env <- get_env
1811− fmap fst . get_type_val $ reflectEnv env
1816+ fmap fst . checkClosed $ reflectEnv env
18121817 | n == tacN "prim__Fail", [_a, errs] <- args
18131818 = do errs' <- eval errs
18141819 parts <- reifyReportParts errs'
@@ -1849,12 +1854,12 @@ runTactical ist fc env tm = do tm' <- eval tm
18491854 ctxt <- get_context
18501855 env <- get_env
18511856 (tm, ty) <- lift $ check ctxt env raw'
1852− fmap fst . get_type_val $
1857+ fmap fst . checkClosed $
18531858 rawPair (Var (reflm "TT"), Var (reflm "TT"))
18541859 (reflect tm, reflect ty)
18551860 | n == tacN "prim__Forget", [tt] <- args
18561861 = do tt' <- reifyTT tt
1857− fmap fst . get_type_val . reflectRaw $ forget tt'
1862+ fmap fst . checkClosed . reflectRaw $ forget tt'
18581863 | n == tacN "prim__Attack", [] <- args
18591864 = do attack
18601865 returnUnit
@@ -1961,7 +1966,7 @@ runTactical ist fc env tm = do tm' <- eval tm
19611966 env' <- get_env
19621967 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out
19631968 let (tm', ty') = (reflect tm, reflect ty)
1964− fmap fst . get_type_val $
1969+ fmap fst . checkClosed $
19651970 rawPair (Var $ reflm "TT", Var $ reflm "TT")
19661971 (tm', ty')
19671972 | n == tacN "prim__Debug", [ty, msg] <- args