@@ -1746,6 +1746,11 @@ runTactical ist fc env tm = do tm' <- eval tm
1746 updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}
1746 updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}
1747 return ()
1747 return ()
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)
1749 -- | Do a step in the reflected elaborator monad. The input is the
1754 -- | Do a step in the reflected elaborator monad. The input is the
1750 -- step, the output is the (reflected) term returned.
1755 -- step, the output is the (reflected) term returned.
1751 runTacTm :: Term -> ElabD Term
1756 runTacTm :: Term -> ElabD Term
@@ -1756,12 +1761,12 @@ runTactical ist fc env tm = do tm' <- eval tm
1756 | n == tacN "prim__Goal", [] <- args
1761 | n == tacN "prim__Goal", [] <- args
1757 = do (h:_) <- get_holes
1762 = do (h:_) <- get_holes
1758 t <- goal
1763 t <- goal
1759− fmap fst . get_type_val $
1764+ fmap fst . checkClosed $
1760 rawPair (Var (reflm "TTName"), Var (reflm "TT"))
1765 rawPair (Var (reflm "TTName"), Var (reflm "TT"))
1761 (reflectName h, reflect t)
1766 (reflectName h, reflect t)
1762 | n == tacN "prim__Holes", [] <- args
1767 | n == tacN "prim__Holes", [] <- args
1763 = do hs <- get_holes
1768 = do hs <- get_holes
1764− fmap fst . get_type_val $
1769+ fmap fst . checkClosed $
1765 mkList (Var $ reflm "TTName") (map reflectName hs)
1770 mkList (Var $ reflm "TTName") (map reflectName hs)
1766 | n == tacN "prim__Guess", [] <- args
1771 | n == tacN "prim__Guess", [] <- args
1767 = do ok <- is_guess
1772 = do ok <- is_guess
@@ -1771,7 +1776,7 @@ runTactical ist fc env tm = do tm' <- eval tm
1771 RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))
1776 RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))
1772 (Var (reflm "TT")))
1777 (Var (reflm "TT")))
1774− else fmap fst . get_type_val $
1779+ else fmap fst . checkClosed $
1775 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1780 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1776 (Var (reflm "TT"))
1781 (Var (reflm "TT"))
1777 | n == tacN "prim__LookupTy", [n] <- args
1782 | n == tacN "prim__LookupTy", [n] <- args
@@ -1791,7 +1796,7 @@ runTactical ist fc env tm = do tm' <- eval tm
1791 let defs = [ reflectTriple (reflectName n, reflectNameType nt, reflect ty)
1796 let defs = [ reflectTriple (reflectName n, reflectNameType nt, reflect ty)
1792 | (n, def) <- lookupNameDef n' ctxt
1797 | (n, def) <- lookupNameDef n' ctxt
1793 , let (nt, ty) = getNameTypeAndType def ]
1798 , let (nt, ty) = getNameTypeAndType def ]
1794− fmap fst . get_type_val $
1799+ fmap fst . checkClosed $
1795 rawList (raw_apply (Var pairTy) [ Var (reflm "TTName")
1800 rawList (raw_apply (Var pairTy) [ Var (reflm "TTName")
1796 , raw_apply (Var pairTy) [ Var (reflm "NameType")
1801 , raw_apply (Var pairTy) [ Var (reflm "NameType")
1797 , Var (reflm "TT")]])
1802 , Var (reflm "TT")]])
@@ -1800,15 +1805,15 @@ runTactical ist fc env tm = do tm' <- eval tm
1800 = do n' <- reifyTTName name
1805 = do n' <- reifyTTName name
1801 datatypes <- get_datatypes
1806 datatypes <- get_datatypes
1802 ctxt <- get_context
1807 ctxt <- get_context
1803− fmap fst . get_type_val $
1808+ fmap fst . checkClosed $
1804 rawList (Var (tacN "Datatype"))
1809 rawList (Var (tacN "Datatype"))
1805 (map reflectDatatype (buildDatatypes ctxt datatypes n'))
1810 (map reflectDatatype (buildDatatypes ctxt datatypes n'))
1806 | n == tacN "prim__SourceLocation", [] <- args
1811 | n == tacN "prim__SourceLocation", [] <- args
1807− = fmap fst . get_type_val $
1812+ = fmap fst . checkClosed $
1808 reflectFC fc
1813 reflectFC fc
1809 | n == tacN "prim__Env", [] <- args
1814 | n == tacN "prim__Env", [] <- args
1810 = do env <- get_env
1815 = do env <- get_env
1811− fmap fst . get_type_val $ reflectEnv env
1816+ fmap fst . checkClosed $ reflectEnv env
1812 | n == tacN "prim__Fail", [_a, errs] <- args
1817 | n == tacN "prim__Fail", [_a, errs] <- args
1813 = do errs' <- eval errs
1818 = do errs' <- eval errs
1814 parts <- reifyReportParts errs'
1819 parts <- reifyReportParts errs'
@@ -1849,12 +1854,12 @@ runTactical ist fc env tm = do tm' <- eval tm
1849 ctxt <- get_context
1854 ctxt <- get_context
1850 env <- get_env
1855 env <- get_env
1851 (tm, ty) <- lift $ check ctxt env raw'
1856 (tm, ty) <- lift $ check ctxt env raw'
1852− fmap fst . get_type_val $
1857+ fmap fst . checkClosed $
1853 rawPair (Var (reflm "TT"), Var (reflm "TT"))
1858 rawPair (Var (reflm "TT"), Var (reflm "TT"))
1854 (reflect tm, reflect ty)
1859 (reflect tm, reflect ty)
1855 | n == tacN "prim__Forget", [tt] <- args
1860 | n == tacN "prim__Forget", [tt] <- args
1856 = do tt' <- reifyTT tt
1861 = do tt' <- reifyTT tt
1857− fmap fst . get_type_val . reflectRaw $ forget tt'
1862+ fmap fst . checkClosed . reflectRaw $ forget tt'
1858 | n == tacN "prim__Attack", [] <- args
1863 | n == tacN "prim__Attack", [] <- args
1859 = do attack
1864 = do attack
1860 returnUnit
1865 returnUnit
@@ -1961,7 +1966,7 @@ runTactical ist fc env tm = do tm' <- eval tm
1961 env' <- get_env
1966 env' <- get_env
1962 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out
1967 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out
1963 let (tm', ty') = (reflect tm, reflect ty)
1968 let (tm', ty') = (reflect tm, reflect ty)
1964− fmap fst . get_type_val $
1969+ fmap fst . checkClosed $
1965 rawPair (Var $ reflm "TT", Var $ reflm "TT")
1970 rawPair (Var $ reflm "TT", Var $ reflm "TT")
1966 (tm', ty')
1971 (tm', ty')
1967 | n == tacN "prim__Debug", [ty, msg] <- args
1972 | n == tacN "prim__Debug", [ty, msg] <- args