mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-30 23:45:23 +03:00
Tweak fix for #494: it should never say an equation is unsolvable.
This commit is contained in:
parent
af6b830162
commit
abbce5405c
@ -219,13 +219,10 @@ tryEqMins x y =
|
||||
do (a, b) <- aMin y
|
||||
let ys = splitMin a ++ splitMin b
|
||||
let ys' = filter (not . isGt) ys
|
||||
return $ case ys' of
|
||||
[] -> Unsolvable
|
||||
$ TCErrorMessage
|
||||
$ "Unsolvable constraint: " ++
|
||||
show (pp (x =#= y))
|
||||
_ | length ys' < length ys -> SolvedIf [x =#= foldr1 Simp.tMin ys']
|
||||
| otherwise -> Unsolved
|
||||
let y' = if null ys' then tInf else foldr1 Simp.tMin ys'
|
||||
return $ if length ys' < length ys
|
||||
then SolvedIf [x =#= y']
|
||||
else Unsolved
|
||||
where
|
||||
splitMin :: Type -> [Type]
|
||||
splitMin ty =
|
||||
|
Loading…
Reference in New Issue
Block a user