Don't get rid of constraints when we print

plclub · Sep 18, 2023 · 485aacb · 485aacb
1 parent 8eadf7d
commit 485aacb
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/src/Environment.hs b/src/Environment.hs
@@ -29,6 +29,7 @@ module Environment
     extendSourceLocation,
     extendLevelConstraint,
     simplify,
+    getConstraints,
     dumpConstraints,
     getSourceLocation,
     err,
@@ -410,6 +411,9 @@ extendLevelConstraint c = do
   -- if c `elem` cs then return () else
     put $ TcState { constraints = (head locs,c) : cs }
 
+getConstraints :: (MonadState TcState m) => m [(SourceLocation,LevelConstraint)]
+getConstraints = gets constraints
+
 dumpConstraints :: (MonadState TcState m) => m [(SourceLocation,LevelConstraint)]
 dumpConstraints = do
   st <- get

diff --git a/src/TypeCheck.hs b/src/TypeCheck.hs
@@ -338,7 +338,7 @@ tcTerm LetPair{} _ k =  Env.err [DS "The parser for 'full' expands Sigmas into d
 
 tcTerm PrintMe (Just ty) mk = do
   gamma <- Env.getLocalCtx
-  cs <- Env.dumpConstraints
+  cs <- Env.getConstraints
   let dcs = displayConstraints (Env.simplify cs)
   Env.warn $ [DS "Unmet obligation.\nContext:", DD gamma,
         DS "\nGoal:", DD ty, DS " @ ", DD mk,