Respect DontCare in termination checker (#6639)

agda · May 15, 2023 · 3058179 · 3058179
1 parent dbf25c7
commit 3058179
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/src/full/Agda/Termination/TermCheck.hs b/src/full/Agda/Termination/TermCheck.hs
@@ -1313,7 +1313,7 @@ instance StripAllProjections Term where
         -- c <- fromRightM (\ err -> return c) $ getConForm (conName c)
         Con c ci <$> stripAllProjections ts
       Def d es   -> Def d <$> stripAllProjections es
-      DontCare t -> stripAllProjections t
+      DontCare t -> DontCare <$> stripAllProjections t
       _ -> return t
 
 -- | Normalize outermost constructor name in a pattern.
@@ -1340,8 +1340,7 @@ compareTerm' v mp@(Masked m p) = do
     (Var i es, _) | Just{} <- allApplyElims es ->
       compareVar i mp
 
-    (DontCare t, _) ->
-      compareTerm' t mp
+    (DontCare t, _) -> pure Order.unknown
 
     -- Andreas, 2014-09-22, issue 1281:
     -- For metas, termination checking should be optimistic.