From abbce5405c2ff3e29ba027c0f39a2a2e88a3cd1f Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Thu, 19 Jul 2018 18:01:12 -0700
Subject: [PATCH] Tweak fix for #494: it should never say an equation is
 unsolvable.

---
 src/Cryptol/TypeCheck/Solver/Numeric.hs | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/src/Cryptol/TypeCheck/Solver/Numeric.hs b/src/Cryptol/TypeCheck/Solver/Numeric.hs
index e67e459b..b5864c67 100644
--- a/src/Cryptol/TypeCheck/Solver/Numeric.hs
+++ b/src/Cryptol/TypeCheck/Solver/Numeric.hs
@@ -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 =