Merge pull request #598 from HigherOrderCO/return-term-do-check

Use the term from 'check' to check for unfilled metas
HigherOrderCO · Oct 29, 2024 · 8e701ae · 8e701ae
2 parents 9ab334f + 8af8097
commit 8e701ae
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/Kind/API.hs b/src/Kind/API.hs
@@ -96,9 +96,9 @@ apiCheck bookPath (book, defs, _) defName defPath = do
         case M.lookup fileDefName book of
           Just term -> do
             case envRun (doCheck term) book of
-              Done state _ -> do
+              Done state chkTerm -> do
                 apiPrintLogs state
-                apiPrintWarn term state
+                apiPrintWarn chkTerm state
                 putStrLn $ "\x1b[32m✓ " ++ fileDefName ++ "\x1b[0m"
                 return $ Right ()
               Fail state -> do

diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs
@@ -417,7 +417,7 @@ checkUnreachable src cNam term dep = go src cNam term dep where
 
 checkLater :: Bool -> Maybe Cod -> Term -> Term -> Int -> Env Term
 checkLater False src term typx dep = check False src term typx dep
-checkLater True  src term typx dep = envSusp (Check src term typx dep) >> return (Met 0 [])
+checkLater True  src term typx dep = envSusp (Check src term typx dep) >> return term
 
 doCheckMode :: Bool -> Term -> Env Term
 doCheckMode sus (Ann _ val typ) = do