Fixes #1696

CHANGES.md

@@ -10,6 +10,10 @@
 
 * Fix #1685, which caused Cryptol to panic when given a local definition without
   a type signature that uses numeric constraint guards.
+
+* Fix #1696, which corrected an incorrect simplification rule, leading to
+  panics.
+
 # 3.1.0 -- 2024-02-05
 
 ## Language changes

src/Cryptol/TypeCheck/Solver/Numeric.hs

@@ -46,8 +46,8 @@ cryIsEqual ctxt t1 t2 =
     <|> tryEqAddInf ctxt t1 t2
     <|> tryAddConst (=#=) t1 t2
     <|> tryCancelVar ctxt (=#=) t1 t2
-    <|> tryLinearSolution t1 t2
-    <|> tryLinearSolution t2 t1
+    <|> tryLinearSolution ctxt t1 t2
+    <|> tryLinearSolution ctxt t2 t1
 
 -- | Try to solve @t1 /= t2@
 cryIsNotEqual :: Ctxt -> Type -> Type -> Solved
@@ -423,14 +423,15 @@ tryAddConst rel l r =
 -- | Check for situations where a unification variable is involved in
 --   a sum of terms not containing additional unification variables,
 --   and replace it with a solution and an inequality.
---   @s1 = ?a + s2 ~~> (?a = s1 - s2, s1 >= s2)@
-tryLinearSolution :: Type -> Type -> Match Solved
-tryLinearSolution s1 t =
+--   @s1 = ?a + s2 ~~> (?a = s1 - s2, s1 >= s2, fin s2)@
+tryLinearSolution :: Ctxt -> Type -> Type -> Match Solved
+tryLinearSolution ctxt s1 t =
   do (a,xs) <- matchLinearUnifier t
-     guard (noFreeVariables s1)
+     guard (noFreeVariables s1) 
 
      -- NB: matchLinearUnifier only matches if xs is nonempty
      let s2 = foldr1 Simp.tAdd xs
+     guard (iIsFin (typeInterval (intervals ctxt) s2))
      return (SolvedIf [ TVar a =#= (Simp.tSub s1 s2), s1 >== s2 ])
 
 

tests/issues/issue_1696.cry

@@ -0,0 +1,5 @@
+
+f : {m,n} (m >= n) => [m] -> [n]
+f = take`{n}
+
+

tests/issues/issue_1696.icry

@@ -0,0 +1 @@
+:load issue_1696.cry

tests/issues/issue_1696.icry.stdout

@@ -0,0 +1,18 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+
+[error] at issue_1696.cry:3:1--3:13:
+  Failed to infer the following types:
+    • ?m, type argument 'back' of 'take' at issue_1696.cry:3:5--3:9
+  while validating user-specified signature
+    in the definition of 'Main::f', at issue_1696.cry:3:1--3:2,
+    we need to show that
+      for any type m, n
+      assuming
+        • m >= n
+      the following constraints hold:
+        • m == ?m + n
+            arising from
+            matching types
+            at issue_1696.cry:3:5--3:9