Add an extra rule for Arith when the lenght of the sequence is inf

Fixes #596
GaloisInc · May 28, 2019 · 4ce64e9 · 4ce64e9
1 parent 56cb58a
commit 4ce64e9
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/src/Cryptol/TypeCheck/Solver/Class.hs b/src/Cryptol/TypeCheck/Solver/Class.hs
@@ -129,7 +129,12 @@ solveArithSeq n ty = case tNoUser ty of
   TCon (TC TCBit) [] -> SolvedIf [ pFin n ]
 
   -- variables are not solvable.
-  TVar {} -> Unsolved
+  TVar {} -> case tNoUser n of
+                {- We are sure that the lenght is not `fin`, so the
+                special case for `Bit` does not apply.
+                Arith ty => Arith [n]ty -}
+                TCon (TC TCInf) [] -> SolvedIf [ pArith ty ]
+                _                  -> Unsolved
 
   -- Arith ty => Arith [n]ty
   _ -> SolvedIf [ pArith ty ]