Improve performance for PM check on literals (Fixes #11160 and #11161)

Two changes:

1. Instead of generating constraints of the form (x ~ e) (as we do in
the paper), generate constraints of the form (e ~ e). The term oracle
(`tmOracle` in deSugar/TmOracle.hs) is not really efficient and in the
presence of many (x ~ e) constraints behaves quadratically. For
literals, constraints of the form (False ~ (x ~ lit)) are pretty common,
so if we start with { y ~ False, y ~ (x ~ lit) } we end up givng to the
solver (a) twice as many constraints as we need and (b) half of them
trigger the solver's weakness. This fixes #11160.

2. Treat two overloaded literals that look different as different. This
is not entirely correct but it is what both the previous and the current
check did. I had the ambitious plan to do the *right thing* (equality
between overloaded literals is undecidable in the general case) and just
use this assumption when issuing the warnings. It seems to generate much
more constraints than I expected (breaks #11161) so I just do it
immediately now instead of generating everything and filtering
afterwards.

Even if it is not (strictly speaking) correct, we have the following:
  * Gives the "expected" warnings (the ones Ocaml or the previous
    algorithm would give) and,
  * Most importantly, it is safe. Unless a catch-all clause exists, a
    match against literals is always non-exhaustive. So, effectively
    this affects only what is shown to the user (and, evidently,
    performance!).

3 files changed, 70 insertions, 329 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 382112c951..55dcfc224e 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -71,7 +71,7 @@ The algorithm used is described in the paper:
 
 type PmM a = DsM a
 
-data PmConstraint = TmConstraint Id PmExpr -- ^ Term equalities: x ~ e
+data PmConstraint = TmConstraint PmExpr PmExpr -- ^ Term equalities: e ~ e
                   | TyConstraint [EvVar]   -- ^ Type equalities
                   | BtConstraint Id        -- ^ Strictness constraints: x ~ _|_
 
@@ -174,10 +174,12 @@ checkMatches vars matches
 initial_uncovered :: [Id] -> DsM ValSetAbs
 initial_uncovered vars = do
   ty_cs <- TyConstraint . bagToList <$> getDictsDs
-  tm_cs <- map (uncurry TmConstraint) . bagToList <$> getTmCsDs
+  tm_cs <- map simpleToTmCs . bagToList <$> getTmCsDs
   let vsa = map (VA . PmVar) vars
   return $ mkConstraint (ty_cs:tm_cs) (foldr Cons Singleton vsa)
-
+  where
+    simpleToTmCs :: (Id, PmExpr) -> PmConstraint
+    simpleToTmCs (x,e) = TmConstraint (PmExprVar x) e
 {-
 %************************************************************************
 %*                                                                      *
@@ -670,8 +672,8 @@ mkOneConFull x usupply con = (con_abs, constraints)
                        , pm_con_args    = arguments }
 
     constraints -- term and type constraints
-      | null evvars = [ TmConstraint x (pmPatToPmExpr con_abs) ]
-      | otherwise   = [ TmConstraint x (pmPatToPmExpr con_abs)
+      | null evvars = [ TmConstraint (PmExprVar x) (pmPatToPmExpr con_abs) ]
+      | otherwise   = [ TmConstraint (PmExprVar x) (pmPatToPmExpr con_abs)
                       , TyConstraint evvars ]
 
 mkConVars :: UniqSupply -> [Type] -> [ValAbs] -- ys, fresh with the given type
@@ -818,14 +820,14 @@ nameType name usupply ty = newEvVar idname ty
     idname  = mkInternalName unique occname noSrcSpan
 
 -- | Partition the constraints to type cs, term cs and forced variables
-splitConstraints :: [PmConstraint] -> ([EvVar], [(Id, PmExpr)], Maybe Id)
+splitConstraints :: [PmConstraint] -> ([EvVar], [(PmExpr, PmExpr)], Maybe Id)
 splitConstraints [] = ([],[],Nothing)
 splitConstraints (c : rest)
   = case c of
-      TyConstraint cs  -> (cs ++ ty_cs, tm_cs, bot_cs)
-      TmConstraint x e -> (ty_cs, (x,e):tm_cs, bot_cs)
-      BtConstraint cs  -> ASSERT (isNothing bot_cs) -- NB: Only one x ~ _|_
-                                 (ty_cs, tm_cs, Just cs)
+      TyConstraint cs    -> (cs ++ ty_cs, tm_cs, bot_cs)
+      TmConstraint e1 e2 -> (ty_cs, (e1,e2):tm_cs, bot_cs)
+      BtConstraint cs    -> ASSERT (isNothing bot_cs) -- NB: Only one x ~ _|_
+                                   (ty_cs, tm_cs, Just cs)
   where
     (ty_cs, tm_cs, bot_cs) = splitConstraints rest
 
@@ -883,20 +885,14 @@ pruneVSABound n v = go n init_cs emptylist v
             vecs1 <- go n                  all_cs vec vsa1
             vecs2 <- go (n - length vecs1) all_cs vec vsa2
             return (vecs1 ++ vecs2)
-          Singleton ->
-            -- Have another go at the term oracle state, for strange
-            -- equalities between overloaded literals. See
-            -- Note [Undecidable Equality on Overloaded Literals] in TmOracle
-            if containsEqLits tm_env
-              then return [] -- not on the safe side
-              else do
-                -- TODO: Provide an incremental interface for the type oracle
-                sat <- tyOracle (listToBag ty_cs)
-                return $ case sat of
-                  True  -> let (residual_eqs, subst) = wrapUpTmState tm_env
-                               vector = substInValVecAbs subst (toList vec)
-                           in  [(vector, residual_eqs)]
-                  False -> []
+          Singleton -> do
+            -- TODO: Provide an incremental interface for the type oracle
+            sat <- tyOracle (listToBag ty_cs)
+            return $ case sat of
+              True  -> let (residual_eqs, subst) = wrapUpTmState tm_env
+                           vector = substInValVecAbs subst (toList vec)
+                       in  [(vector, residual_eqs)]
+              False -> []
 
           Constraint cs vsa -> case splitConstraints cs of
             (new_ty_cs, new_tm_cs, new_bot_ct) ->
@@ -1000,7 +996,7 @@ pmTraverse us gvsa rec (p:ps) vsa =
     PmGuard pv e ->
       let (us1, us2) = splitUniqSupply us
           y  = mkPmId us1 (patternType p)
-          cs = [TmConstraint y e]
+          cs = [TmConstraint (PmExprVar y) e]
       in  mkConstraint cs $ tailVSA $
             pmTraverse us2 gvsa rec (pv++ps) (VA (PmVar y) `mkCons` vsa)
 
@@ -1023,16 +1019,12 @@ cMatcher, uMatcher, dMatcher :: PmMatcher
 -- CVar
 cMatcher us gvsa (PmVar x) ps va vsa
   = VA va `mkCons` (cs `mkConstraint` covered us gvsa ps vsa)
-  where cs = [TmConstraint x (pmPatToPmExpr va)]
+  where cs = [TmConstraint (PmExprVar x) (pmPatToPmExpr va)]
 
 -- CLitCon
 cMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa
-  = VA va `mkCons` (cs `mkConstraint` covered us2 gvsa ps vsa)
-  where
-    (us1, us2) = splitUniqSupply us
-    y  = mkPmId us1 (pmPatType va)
-    cs = [ TmConstraint y (PmExprLit l)
-         , TmConstraint y (pmPatToPmExpr va) ]
+  = VA va `mkCons` (cs `mkConstraint` covered us gvsa ps vsa)
+  where cs = [ TmConstraint (PmExprLit l) (pmPatToPmExpr va) ]
 
 -- CConLit
 cMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa
@@ -1041,7 +1033,7 @@ cMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa
     (us1, us2, us3)   = splitUniqSupply3 us
     y                 = mkPmId us1 (pmPatType p)
     (con_abs, all_cs) = mkOneConFull y us2 (pm_con_con p)
-    cs = TmConstraint y (PmExprLit l) : all_cs
+    cs = TmConstraint (PmExprVar y) (PmExprLit l) : all_cs
 
 -- CConCon
 cMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
@@ -1055,15 +1047,8 @@ cMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
 
 -- CLitLit
 cMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of
-  Just True  -> VA va `mkCons` covered us gvsa ps vsa -- match
-  Just False -> Empty                                 -- mismatch
-  Nothing    -> VA va `mkCons` (cs `mkConstraint` covered us2 gvsa ps vsa)
-  -- See Note [Undecidable Equality on Overloaded Literals] in TmOracle
-  where
-    (us1, us2) = splitUniqSupply us
-    y          = mkPmId us1 (pmPatType va)
-    cs         = [ TmConstraint y (PmExprLit l1)
-                 , TmConstraint y (PmExprLit l2) ]
+  True  -> VA va `mkCons` covered us gvsa ps vsa -- match
+  False -> Empty                                 -- mismatch
 
 -- CConVar
 cMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa
@@ -1077,7 +1062,7 @@ cMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa
   = cMatcher us gvsa p ps lit_abs (mkConstraint cs vsa)
   where
     lit_abs = PmLit l
-    cs      = [TmConstraint x (PmExprLit l)]
+    cs      = [TmConstraint (PmExprVar x) (PmExprLit l)]
 
 -- uMatcher
 -- ----------------------------------------------------------------------------
@@ -1085,7 +1070,7 @@ cMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa
 -- UVar
 uMatcher us gvsa (PmVar x) ps va vsa
   = VA va `mkCons` (cs `mkConstraint` uncovered us gvsa ps vsa)
-  where cs = [TmConstraint x (pmPatToPmExpr va)]
+  where cs = [TmConstraint (PmExprVar x) (pmPatToPmExpr va)]
 
 -- ULitCon
 uMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa
@@ -1093,7 +1078,7 @@ uMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa
   where
     (us1, us2) = splitUniqSupply us
     y  = mkPmId us1 (pmPatType va)
-    cs = [TmConstraint y (PmExprLit l)]
+    cs = [TmConstraint (PmExprVar y) (PmExprLit l)]
 
 -- UConLit
 uMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa
@@ -1101,7 +1086,7 @@ uMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa
   where
     (us1, us2) = splitUniqSupply us
     y  = mkPmId us1 (pmPatType p)
-    cs = [TmConstraint y (PmExprLit l)]
+    cs = [TmConstraint (PmExprVar y) (PmExprLit l)]
 
 -- UConCon
 uMatcher us gvsa ( p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
@@ -1115,20 +1100,8 @@ uMatcher us gvsa ( p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
 
 -- ULitLit
 uMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of
-  Just True  -> VA va `mkCons` uncovered us gvsa ps vsa -- match
-  Just False -> VA va `mkCons` vsa                      -- mismatch
-  Nothing    -> mkUnion (VA va `mkCons`
-                            (match_cs `mkConstraint` uncovered us3 gvsa ps vsa))
-                        (non_match_cs `mkConstraint` (VA va `mkCons` vsa))
-  -- See Note [Undecidable Equality on Overloaded Literals] in TmOracle
-  where
-    (us1, us2, us3) = splitUniqSupply3 us
-    y               = mkPmId us1 (pmPatType va)
-    z               = mkPmId us2 boolTy
-    match_cs        = [ TmConstraint y (PmExprLit l1)
-                      , TmConstraint y (PmExprLit l2) ]
-    non_match_cs    = [ TmConstraint z falsePmExpr
-                      , TmConstraint z (PmExprEq (PmExprLit l1) (PmExprLit l2))]
+  True  -> VA va `mkCons` uncovered us gvsa ps vsa -- match
+  False -> VA va `mkCons` vsa                      -- mismatch
 
 -- UConVar
 uMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa
@@ -1145,14 +1118,12 @@ uMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa
 
 -- ULitVar
 uMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa
-  = mkUnion (uMatcher us2 gvsa p ps (PmLit l) (mkConstraint match_cs vsa))
+  = mkUnion (uMatcher us gvsa p ps (PmLit l) (mkConstraint match_cs vsa))
             (non_match_cs `mkConstraint` (VA (PmVar x) `mkCons` vsa))
   where
-    (us1, us2) = splitUniqSupply us
-    y  = mkPmId us1 (pmPatType p)
-    match_cs     = [ TmConstraint x (PmExprLit l)]
-    non_match_cs = [ TmConstraint y falsePmExpr
-                   , TmConstraint y (PmExprEq (PmExprVar x) (PmExprLit l)) ]
+    match_cs     = [ TmConstraint (PmExprVar x) (PmExprLit l)]
+    non_match_cs = [ TmConstraint falsePmExpr
+                                  (PmExprEq (PmExprVar x) (PmExprLit l)) ]
 
 -- dMatcher
 -- ----------------------------------------------------------------------------
@@ -1160,16 +1131,12 @@ uMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa
 -- DVar
 dMatcher us gvsa (PmVar x) ps va vsa
   = VA va `mkCons` (cs `mkConstraint` divergent us gvsa ps vsa)
-  where cs = [TmConstraint x (pmPatToPmExpr va)]
+  where cs = [TmConstraint (PmExprVar x) (pmPatToPmExpr va)]
 
 -- DLitCon
 dMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa
-  = VA va  `mkCons` (cs `mkConstraint` divergent us2 gvsa ps vsa)
-  where
-    (us1, us2) = splitUniqSupply us
-    y  = mkPmId us1 (pmPatType va)
-    cs = [ TmConstraint y (PmExprLit l)
-         , TmConstraint y (pmPatToPmExpr va) ]
+  = VA va `mkCons` (cs `mkConstraint` divergent us gvsa ps vsa)
+  where cs = [ TmConstraint (PmExprLit l) (pmPatToPmExpr va) ]
 
 -- DConLit
 dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmLit l) vsa
@@ -1178,7 +1145,7 @@ dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmLit l) vsa
     (us1, us2, us3)   = splitUniqSupply3 us
     y                 = mkPmId us1 (pmPatType p)
     (con_abs, all_cs) = mkOneConFull y us2 con
-    cs = TmConstraint y (PmExprLit l) : all_cs
+    cs = TmConstraint (PmExprVar y) (PmExprLit l) : all_cs
 
 -- DConCon
 dMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
@@ -1192,15 +1159,8 @@ dMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
 
 -- DLitLit
 dMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of
-  Just True  -> VA va `mkCons` divergent us gvsa ps vsa -- we know: match
-  Just False -> Empty                                   -- we know: no match
-  Nothing    -> VA va `mkCons` (cs `mkConstraint` divergent us2 gvsa ps vsa)
-  -- See Note [Undecidable Equality on Overloaded Literals] in TmOracle
-  where
-    (us1, us2) = splitUniqSupply us
-    y          = mkPmId us1 (pmPatType va)
-    cs         = [ TmConstraint y (PmExprLit l1)
-                 , TmConstraint y (PmExprLit l2) ]
+  True  -> VA va `mkCons` divergent us gvsa ps vsa -- match
+  False -> Empty                                   -- mismatch
 
 -- DConVar
 dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa
@@ -1215,7 +1175,7 @@ dMatcher us gvsa (PmLit l) ps (PmVar x) vsa
   = mkUnion (VA (PmVar x) `mkCons` mkConstraint [BtConstraint x] vsa)
             (dMatcher us gvsa (PmLit l) ps (PmLit l) (mkConstraint cs vsa))
   where
-    cs = [TmConstraint x (PmExprLit l)]
+    cs = [TmConstraint (PmExprVar x) (PmExprLit l)]
 
 -- ----------------------------------------------------------------------------
 -- * Propagation of term constraints inwards when checking nested matches
diff --git a/compiler/deSugar/PmExpr.hs b/compiler/deSugar/PmExpr.hs
index c28e95d90d..f426bb4d19 100644
--- a/compiler/deSugar/PmExpr.hs
+++ b/compiler/deSugar/PmExpr.hs
@@ -27,7 +27,7 @@ import VarSet
 
 import Data.Functor ((<$>))
 import Data.Maybe (mapMaybe)
-import Data.List (groupBy, sortBy)
+import Data.List (groupBy, sortBy, nubBy)
 import Control.Monad.Trans.State.Lazy
 
 {-
@@ -66,21 +66,16 @@ data PmLit = PmSLit HsLit                                    -- simple
 -- inconclusive. Since an overloaded PmLit represents a function application
 -- (e.g.  fromInteger 5), if two literals look the same they are the same but
 -- if they don't, whether they are depends on the implementation of the
--- from-function.
-eqPmLit :: PmLit -> PmLit -> Maybe Bool
-eqPmLit (PmSLit    l1) (PmSLit l2   ) = Just (l1 == l2)
-eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = if res then Just True else Nothing
-  where res = b1 == b2 && l1 == l2
-eqPmLit _ _ = Just False -- this should not even happen I think
+-- from-function. Yet, for the purposes of the check, we check syntactically
+-- only (it is safe anyway, since literals always need a catch-all to be
+-- considered to be exhaustive).
+eqPmLit :: PmLit -> PmLit -> Bool
+eqPmLit (PmSLit    l1) (PmSLit    l2) = l1 == l2
+eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = b1 == b2 && l1 == l2
+eqPmLit _              _              = False
 
 nubPmLit :: [PmLit] -> [PmLit]
-nubPmLit []     = []
-nubPmLit [x]    = [x]
-nubPmLit (x:xs) = x : nubPmLit (filter (neqPmLit x) xs)
-  where neqPmLit l1 l2 = case eqPmLit l1 l2 of
-          Just True  -> False
-          Just False -> True
-          Nothing    -> True
+nubPmLit = nubBy eqPmLit
 
 -- | Term equalities
 type SimpleEq  = (Id, PmExpr) -- We always use this orientation
@@ -374,4 +369,3 @@ instance Outputable PmLit where
 -- not really useful for pmexprs per se
 instance Outputable PmExpr where
   ppr e = fst $ runPmPprM (pprPmExpr e) []
-
diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs
index 8babc2ebdc..3731f801d3 100644
--- a/compiler/deSugar/TmOracle.hs
+++ b/compiler/deSugar/TmOracle.hs
@@ -14,7 +14,7 @@ module TmOracle (
         pprPmExprWithParens, lhsExprToPmExpr, hsExprToPmExpr,
 
         -- the term oracle
-        tmOracle, TmState, initialTmState, containsEqLits,
+        tmOracle, TmState, initialTmState,
 
         -- misc.
         exprDeepLookup, pmLitType, flattenPmVarEnv
@@ -91,12 +91,12 @@ type TmState = ([ComplexEq], TmOracleEnv)
 initialTmState :: TmState
 initialTmState = ([], (False, Map.empty))
 
--- | Solve a simple equality.
-solveSimpleEq :: TmState -> SimpleEq -> Maybe TmState
-solveSimpleEq solver_env@(_,(_,env)) simple
+-- | Solve a complex equality (top-level).
+solveOneEq :: TmState -> ComplexEq -> Maybe TmState
+solveOneEq solver_env@(_,(_,env)) complex
   = solveComplexEq solver_env -- do the actual *merging* with existing state
-  $ simplifyComplexEq             -- simplify as much as you can
-  $ applySubstSimpleEq env simple -- replace everything we already know
+  $ simplifyComplexEq               -- simplify as much as you can
+  $ applySubstComplexEq env complex -- replace everything we already know
 
 -- | Solve a complex equality.
 solveComplexEq :: TmState -> ComplexEq -> Maybe TmState
@@ -106,9 +106,8 @@ solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
   (_,PmExprOther _)            -> Just (standby, (True, env))
 
   (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
-    Just True  -> Just solver_state           -- we are sure: equal
-    Just False -> Nothing                     -- we are sure: not equal
-    Nothing    -> Just (eq:standby, (unhandled, env)) -- no clue
+    True  -> Just solver_state
+    False -> Nothing
 
   (PmExprCon c1 ts1, PmExprCon c2 ts2)
     | c1 == c2  -> foldlM solveComplexEq solver_state (zip ts1 ts2)
@@ -166,9 +165,8 @@ simplifyEqExpr e1 e2 = case (e1, e2) of
 
   -- Literals
   (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
-    Just True  -> (truePmExpr,  True)
-    Just False -> (falsePmExpr, True)
-    Nothing    -> (original,   False)
+    True  -> (truePmExpr,  True)
+    False -> (falsePmExpr, True)
 
   -- Can potentially be simplified
   (PmExprEq {}, _) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
@@ -199,18 +197,18 @@ simplifyEqExpr e1 e2 = case (e1, e2) of
   where
     original = PmExprEq e1 e2 -- reconstruct equality
 
--- | Apply an (un-flattened) substitution on a simple equality.
-applySubstSimpleEq :: PmVarEnv -> SimpleEq -> ComplexEq
-applySubstSimpleEq env (x, e) = (varDeepLookup env x, exprDeepLookup env e)
+-- | Apply an (un-flattened) substitution to a simple equality.
+applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq
+applySubstComplexEq env (e1,e2) = (exprDeepLookup env e1, exprDeepLookup env e2)
 
--- | Apply an (un-flattened) substitution on a variable.
+-- | Apply an (un-flattened) substitution to a variable.
 varDeepLookup :: PmVarEnv -> Id -> PmExpr
 varDeepLookup env x
   | Just e <- Map.lookup x env = exprDeepLookup env e -- go deeper
   | otherwise                  = PmExprVar x          -- terminal
 {-# INLINE varDeepLookup #-}
 
--- | Apply an (un-flattened) substitution on an expression.
+-- | Apply an (un-flattened) substitution to an expression.
 exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
 exprDeepLookup env (PmExprVar x)    = varDeepLookup env x
 exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es)
@@ -219,8 +217,8 @@ exprDeepLookup env (PmExprEq e1 e2) = PmExprEq (exprDeepLookup env e1)
 exprDeepLookup _   other_expr       = other_expr -- PmExprLit, PmExprOther
 
 -- | External interface to the term oracle.
-tmOracle :: TmState -> [SimpleEq] -> Maybe TmState
-tmOracle tm_state eqs = foldlM solveSimpleEq tm_state eqs
+tmOracle :: TmState -> [ComplexEq] -> Maybe TmState
+tmOracle tm_state eqs = foldlM solveOneEq tm_state eqs
 
 -- | Type of a PmLit
 pmLitType :: PmLit -> Type -- should be in PmExpr but gives cyclic imports :(
@@ -241,215 +239,4 @@ is the following:
     truePmExpr, falsePmExpr or (e1' ~ e2') in case it is uncertain. Note
     that it is not e but rather e', since it may perform some
     simplifications deeper.
-
-Note [Undecidable Equality on Overloaded Literals]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Overloaded literals do not offer equality like constructors do. A literal @lit@
-is used to actually represent @from lit@. For example, we can have the
-following:
-
-  instance Num Bool where
-    ...
-    fromInteger 0 = False
-    fromInteger _ = True
-
-  g :: Bool -> Bool
-  g 4 = ...          -- clause A
-  g 2 = ...          -- clause B
-
-Both clauses A and B will match argunent @True@ so we have an overlap. Yet, we
-cannot detect this unless we unfold the @fromInteger@ function. So @eqPmLit@
-from deSugar/PmExpr.hs returns @Nothing@ in this case. This complexes things a
-lot. Consider the following (similar to test ds022 in deSugar/should_compile):
-
-  f l1 l2 = ...      -- clause A
-  f l3 l4 = ...      -- clause B
-  f l1 l2 = ...      -- clause C
-
-Assuming that the @from@ function is side-effect-free (and total), clauses C
-and D are redundant, independently of the implementation of @from@:
-
-  l1 == l2     ===>    from l1 == from l2
-  l1 /= l2     =/=>    from l1 /= from l2
-
-Now consider what we should generate for @f@ (covered and uncovered only):
-
-U0 = { [x y |> {}] }
-
-Clause A: l1 l2
--------------------------------------------------------------------------------
-CA = { [l1 l2 |> { x ~ l1, y ~ l2 }] }
-
-UA = { [x  y  |> { False ~ (x ~ l1) }]
-     , [l1 y  |> { x ~ l1, False ~ (y ~ l2) }] }
-
-Clause B: l3 l4
--------------------------------------------------------------------------------
-
-CB = { [l3 l4 |> { False ~ (x ~ l1), x ~ l3, y ~ l4}]
-         ..reduces to: False ~ (l3 ~ l1), y ~ l4
-
-     , [l1 l4 |> { x ~ l1, False ~ (y ~ l2), l3 ~ z, z ~ l1, y ~ l4}] }
-         ..reduces to: x ~ l1, False ~ (l4 ~ l2), l1 ~ l3
-
-UB = { [x  y  |> { False ~ (x ~ l1), False ~ (x ~ l3) }]
-     , [l3 y  |> { False ~ (x ~ l1), x ~ l3, False ~ (y ~ l4) }]
-         ..reduces to: False ~ (l1 ~ l3), False ~ (y ~ l4)
-     , [l1 y  |> { x ~ l1, False ~ (y ~ l2), False ~ (l1 ~ l3) }]
-     , [l1 y  |> { x ~ l1, False ~ (y ~ l2), l1 ~ l3, False ~ (y ~ l4) }] }
-
-Clause C: l1 l2
--------------------------------------------------------------------------------
-
-CC = { [l1 l2 |> { False ~ (x ~ l1), False ~ (x ~ l3), x ~ l1, y ~ l2 }]
-         ..reduces to: False ~ (l1 ~ l1), False ~ (l1 ~ l3), x ~ l1
-                       False ~ True, False ~ (l1 ~ l3), x ~ l1
-                       INCONSISTENT
-     , [l3 l2 |> { False ~ (l1 ~ l3), False ~ (y ~ l4), l1 ~ l3, y ~ l2 }]
-         ..reduces to: False ~ (l1 ~ l3), False ~ (l2 ~ l4), l1 ~ l3
-     , [l1 l2 |> { x ~ l1, False ~ (y ~ l2), False ~ (l1 ~ l3), y ~ l2 }]
-         ..reduces to: x ~ l1, False ~ (l2 ~ l2), False ~ (l1 ~ l3)
-                       x ~ l1, False ~ True, False ~ (l1 ~ l3)
-                       INCONSISTENT
-     , [l1 l2 |> { x ~ l1,False ~ (y ~ l2),l1 ~ l3,False ~ (y ~ l4),y ~ l2 }] }
-         ..reduces to: x ~ l1, False ~ (l2 ~ l2), l1 ~ l3, False ~ (l2 ~ l4)
-                       x ~ l1, False ~ True, l1 ~ l3, False ~ (l2 ~ l4)
-                       INCONSISTENT
--------------------------------------------------------------------------------
-
-PROBLEM 1:
-~~~~~~~~~~
-Now the first problem shows itself: Our basic unification-based term oracle
-cannot detect that constraint:
-
-    False ~ (l1 ~ l3), False ~ (l2 ~ l4), l1 ~ l3
-
-is inconsistent. That's what function @tryLitEqs@ (in comments) tries to do:
-use the equality l1 ~ l3 to replace False ~ (l1 ~ l3) with False ~ (l1 ~ l1)
-and expose the inconsistency.
-
-PROBLEM 2:
-~~~~~~~~~~
-Let's turn back to UB and assume we had only clauses A and B. UB is as follows:
-
-  UB = { [x  y  |> { False ~ (x ~ l1), False ~ (x ~ l3) }]
-       , [l3 y  |> { False ~ (l1 ~ l3), False ~ (y ~ l4) }]
-       , [l1 y  |> { x ~ l1, False ~ (y ~ l2), False ~ (l1 ~ l3) }]
-       , [l1 y  |> { x ~ l1, False ~ (y ~ l2), l1 ~ l3, False ~ (y ~ l4) }] }
-
-So we would get:
-
-    Pattern match(es) are non-exhaustive
-    In an equation for f:
-        Patterns not matched:
-          x y    where x not one of {l1, l3}
-          l3 y   where y not one of {l4}
-          l1 y   where y not one of {l2}
-          l1 y   where y not one of {l2, l4} -- (*)
-
-What about the last warning? It holds UNDER THE ASSUMPTION that l1 == l2. It is
-quite unintuitive for the user so at the moment we drop such cases (see
-function @pruneVSABound@ in deSugar/Check.hs). I (gkaracha) would prefer to
-issue a warning like:
-
-    Pattern match(es) are non-exhaustive
-    In an equation for f:
-        Patterns not matched:
-          ...
-          l1 y   where y not one of {l2, l4}
-                 under the assumption that l1 ~ l3
-
-It may be more complex but I would prefer to play on the safe side and (safely)
-issue all warnings and leave it up to the user to decide whether the assumption
-holds or not.
-
-At the moment, we use @containsEqLits@ and consider all constraints that
-include literal equalities inconsistent. We could achieve the same by replacing
-this clause of @eqPmLit@:
-
-  eqPmLit (PmOLit b1 l1) (PmOLit b2 l2)
-    | b1 == b2 && l1 == l2 = Just True
-    | otherwise            = Nothing
-
-with this:
-
-  eqPmLit (PmOLit b1 l1) (PmOLit b2 l2)
-    | b1 == b2 && l1 == l2 = Just True
-    | otherwise            = Just False
-
-which approximates on the unsafe side. Hopefully, literals always need a
-catch-all case to be considered exhaustive so in practice it makes small
-difference. I hate this but it gives the warnings the users are used to.
 -}
-
-{- Not Enabled at the moment
-
--- | Check whether overloaded literal constraints exist in the state and if
--- they can be used to detect further inconsistencies.
-tryLitEqs :: TmState -> Maybe Bool
-tryLitEqs tm_state@(stb,_) = do
-  ans <- exploitLitEqs (Just tm_state)
-  -- Three possible results:
-  --   Nothing    : Inconsistency found.
-  --   Just True  : Literal constraints exist but no inconsistency found.
-  --   Just False : There are no literal constraints in the state.
-  return (isJust $ exists isLitEq_mb stb)
-
--- | Exploit overloaded literal constraints
--- @lit1 ~ lit2@ to improve the term oracle's expressivity.
-exploitLitEqs :: Maybe TmState -> Maybe TmState
-exploitLitEqs tm_state = case tm_state of
-  -- The oracle did not find any inconsistency. Try and exploit
-  -- residual literal equalities for a more precise result.
-  Just st@(standby, (unhandled, env)) ->
-    case exists isLitEq_mb standby of
-      -- Such an equality exists. This means that we are under the assumption
-      -- that two overloaded literals reduce to the same value (for all we know
-      -- they do). Replace the one with the other in the rest residual
-      -- constraints and run the solver once more, looking for an inconsistency.
-      Just ((l1, l2), rest) ->
-        let new_env = Map.map (replaceLit l1 l2) env
-            new_stb = map (replaceLitSimplifyComplexEq l1 l2) rest
-        in  exploitLitEqs
-              (foldlM solveComplexEq ([], (unhandled, new_env)) new_stb)
-      -- We don't have anything. Just return what you had..
-      Nothing -> Just st
-  -- The oracle has already found an inconsistency.
-  -- No need to search further.
-  Nothing -> Nothing
-  where
-    replaceLitSimplifyComplexEq :: PmLit -> PmLit -> ComplexEq -> ComplexEq
-    replaceLitSimplifyComplexEq l1 l2 (e1,e2) =
-      simplifyComplexEq (replaceLit l1 l2 e1, replaceLit l1 l2 e2)
-
--- | Replace a literal with another in an expression
--- See Note [Undecidable Equality on Overloaded Literals]
-replaceLit :: PmLit -> PmLit -> PmExpr -> PmExpr
-replaceLit l1 l2 e = case e of
-  PmExprVar {}   -> e
-  PmExprCon c es -> PmExprCon c (map (replaceLit l1 l2) es)
-  PmExprLit l    -> case eqPmLit l l1 of
-                      Just True  -> PmExprLit l2
-                      Just False -> e
-                      Nothing    -> e
-  PmExprEq e1 e2 -> PmExprEq (replaceLit l1 l2 e1) (replaceLit l1 l2 e2)
-  PmExprOther {} -> e -- do nothing
--}
-
--- | Check whether the term oracle state
--- contains any equalities between literals.
-containsEqLits :: TmState -> Bool
-containsEqLits (stb, _) = isJust (exists isLitEq_mb stb)
-
-exists :: (a -> Maybe b) -> [a] -> Maybe (b, [a])
-exists _ []     = Nothing
-exists p (x:xs) = case p x of
-  Just y  -> Just (y, xs)
-  Nothing -> do
-    (y, ys) <- exists p xs
-    return (y, x:ys)
-
--- | Check whether a complex equality refers to literals only
-isLitEq_mb :: ComplexEq -> Maybe (PmLit, PmLit)
-isLitEq_mb (PmExprLit l1, PmExprLit l2) = Just (l1, l2)
-isLitEq_mb _other_eq                    = Nothing