From 97d99072a0ce0e04d5f5ca967e2a02102b93f219 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 14 May 2020 09:18:30 -0700 Subject: [PATCH] Fix the solver code for `Integral`. It was previously failing too early if sequence element type is a variable. --- src/Cryptol/TypeCheck/Solver/Class.hs | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/Cryptol/TypeCheck/Solver/Class.hs b/src/Cryptol/TypeCheck/Solver/Class.hs index 5d054936..b8af8498 100644 --- a/src/Cryptol/TypeCheck/Solver/Class.hs +++ b/src/Cryptol/TypeCheck/Solver/Class.hs @@ -148,15 +148,20 @@ solveIntegralInst ty = case tNoUser ty of TCon (TC TCBit) [] -> Unsolvable $ TCErrorMessage "Arithmetic cannot be done on individual bits." - -- fin n => Integral [n] - TCon (TC TCSeq) [n, TCon (TC TCBit) []] -> SolvedIf [ pFin n ] - -- Integral Integer TCon (TC TCInteger) [] -> SolvedIf [] -- Integral (Z n) TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne ] + -- fin n => Integral [n] + TCon (TC TCSeq) [n, elTy] -> + case tNoUser elTy of + TCon (TC TCBit) [] -> SolvedIf [ pFin n ] + TVar _ -> Unsolved + _ -> Unsolvable $ TCErrorMessage $ show + $ "Type" <+> quotes (pp ty) <+> "is not an intergral type." + TVar _ -> Unsolved _ -> Unsolvable $ TCErrorMessage $ show