TmOracle: Replace negative term equalities by refutable PmAltConswip/pmcheck-refuts

The `PmExprEq` business was a huge hack and was at the same time vastly
too powerful and not powerful enough to encode negative term equalities,
i.e. facts of the form "forall y. x ≁ Just y".

This patch introduces the concept of 'refutable shapes': What matters
for the pattern match checker is being able to encode knowledge of the
kind "x can no longer be the literal 5". We encode this knowledge in a
`PmRefutEnv`, mapping a set of newly introduced `PmAltCon`s (which are
just `PmLit`s at the moment) to each variable denoting above
inequalities.

So, say we have `x ≁ 42 ∈ refuts` in the term oracle context and
try to solve an equality like `x ~ 42`. The entry in the refutable
environment will immediately lead to a contradiction.

This machinery renders the whole `PmExprEq` and `ComplexEq` business
unnecessary, getting rid of a lot of (mostly dead) code.

See the Note [Refutable shapes] in TmOracle for a place to start.

Metric Decrease:
    T11195

1 files changed, 283 insertions, 186 deletions

diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs
index 87e5f0a268..db3ce6d770 100644
--- a/compiler/deSugar/TmOracle.hs
+++ b/compiler/deSugar/TmOracle.hs
@@ -1,23 +1,27 @@
 {-
 Author: George Karachalias <george.karachalias@cs.kuleuven.be>
-
-The term equality oracle. The main export of the module is function `tmOracle'.
 -}
 
 {-# LANGUAGE CPP, MultiWayIf #-}
 
+-- | The term equality oracle. The main export of the module are the functions
+-- 'tmOracle', 'solveOneEq' and 'addSolveRefutableAltCon'.
+--
+-- If you are looking for an oracle that can solve type-level constraints, look
+-- at 'TcSimplify.tcCheckSatisfiability'.
 module TmOracle (
 
         -- re-exported from PmExpr
-        PmExpr(..), PmLit(..), SimpleEq, ComplexEq, PmVarEnv, falsePmExpr,
-        eqPmLit, filterComplex, isNotPmExprOther, runPmPprM, lhsExprToPmExpr,
-        hsExprToPmExpr, pprPmExprWithParens,
+        PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..), TmVarCtEnv,
+        PmRefutEnv, eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr,
 
         -- the term oracle
-        tmOracle, TmState, initialTmState, solveOneEq, extendSubst, canDiverge,
+        tmOracle, TmState, initialTmState, wrapUpTmState, solveOneEq,
+        extendSubst, canDiverge, isRigid,
+        addSolveRefutableAltCon, lookupRefutableAltCons,
 
         -- misc.
-        toComplex, exprDeepLookup, pmLitType, flattenPmVarEnv
+        exprDeepLookup, pmLitType
     ) where
 
 #include "HsVersions.h"
@@ -26,16 +30,19 @@ import GhcPrelude
 
 import PmExpr
 
+import Util
 import Id
 import Name
 import Type
 import HsLit
 import TcHsSyn
 import MonadUtils
-import Util
+import ListSetOps (insertNoDup, unionLists)
+import Maybes
 import Outputable
-
 import NameEnv
+import UniqFM
+import UniqDFM
 
 {-
 %************************************************************************
@@ -45,202 +52,261 @@ import NameEnv
 %************************************************************************
 -}
 
--- | The type of substitutions.
-type PmVarEnv = NameEnv PmExpr
+-- | Pretty much a @['TmVarCt']@ association list where the domain is 'Name'
+-- instead of 'Id'. This is the type of 'tm_pos', where we store solutions for
+-- rigid pattern match variables.
+type TmVarCtEnv = NameEnv PmExpr
+
+-- | An environment assigning shapes to variables that immediately lead to a
+-- refutation. So, if this maps @x :-> [3]@, then trying to solve a 'TmVarCt'
+-- like @x ~ 3@ immediately leads to a contradiction.
+-- Determinism is important since we use this for warning messages in
+-- 'PmPpr.pprUncovered'. We don't do the same for 'TmVarCtEnv', so that is a plain
+-- 'NameEnv'.
+--
+-- See also Note [Refutable shapes] in TmOracle.
+type PmRefutEnv = DNameEnv [PmAltCon]
+
+-- | The state of the term oracle. Tracks all term-level facts of the form "x is
+-- @True@" ('tm_pos') and "x is not @5@" ('tm_neg').
+--
+-- Subject to Note [The Pos/Neg invariant].
+data TmState = TmS
+  { tm_pos :: !TmVarCtEnv
+  -- ^ A substitution with solutions we extend with every step and return as a
+  -- result. The substitution is in /triangular form/: It might map @x@ to @y@
+  -- where @y@ itself occurs in the domain of 'tm_pos', rendering lookup
+  -- non-idempotent. This means that 'varDeepLookup' potentially has to walk
+  -- along a chain of var-to-var mappings until we find the solution but has the
+  -- advantage that when we update the solution for @y@ above, we automatically
+  -- update the solution for @x@ in a union-find-like fashion.
+  -- Invariant: Only maps to other variables ('PmExprVar') or to WHNFs
+  -- ('PmExprLit', 'PmExprCon'). Ergo, never maps to a 'PmExprOther'.
+  , tm_neg :: !PmRefutEnv
+  -- ^ Maps each variable @x@ to a list of 'PmAltCon's that @x@ definitely
+  -- cannot match. Example, @x :-> [3, 4]@ means that @x@ cannot match a literal
+  -- 3 or 4. Should we later solve @x@ to a variable @y@
+  -- ('extendSubstAndSolve'), we merge the refutable shapes of @x@ into those of
+  -- @y@. See also Note [The Pos/Neg invariant].
+  }
+
+{- Note [The Pos/Neg invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Invariant: In any 'TmState', The domains of 'tm_pos' and 'tm_neg' are disjoint.
+
+For example, it would make no sense to say both
+    tm_pos = [...x :-> 3 ...]
+    tm_neg = [...x :-> [4,42]... ]
+The positive information is strictly more informative than the negative.
+
+Suppose we are adding the (positive) fact @x :-> e@ to 'tm_pos'. Then we must
+delete any binding for @x@ from 'tm_neg', to uphold the invariant.
+
+But there is more! Suppose we are adding @x :-> y@ to 'tm_pos', and 'tm_neg'
+contains @x :-> cs, y :-> ds@. Then we want to update 'tm_neg' to
+@y :-> (cs ++ ds)@, to make use of the negative information we have about @x@.
+-}
+
+instance Outputable TmState where
+  ppr state = braces (fsep (punctuate comma (pos ++ neg)))
+    where
+      pos   = map pos_eq (nonDetUFMToList (tm_pos state))
+      neg   = map neg_eq (udfmToList (tm_neg state))
+      pos_eq (l, r) = ppr l <+> char '~' <+> ppr r
+      neg_eq (l, r) = ppr l <+> char '≁' <+> ppr r
+
+-- | Initial state of the oracle.
+initialTmState :: TmState
+initialTmState = TmS emptyNameEnv emptyDNameEnv
+
+-- | Wrap up the term oracle's state once solving is complete. Return the
+-- flattened 'tm_pos' and 'tm_neg'.
+wrapUpTmState :: TmState -> (TmVarCtEnv, PmRefutEnv)
+wrapUpTmState solver_state
+  = (flattenTmVarCtEnv (tm_pos solver_state), tm_neg solver_state)
 
--- | The environment of the oracle contains
---     1. A Bool (are there any constraints we cannot handle? (PmExprOther)).
---     2. A substitution we extend with every step and return as a result.
-type TmOracleEnv = (Bool, PmVarEnv)
+-- | Flatten the triangular subsitution.
+flattenTmVarCtEnv :: TmVarCtEnv -> TmVarCtEnv
+flattenTmVarCtEnv env = mapNameEnv (exprDeepLookup env) env
 
 -- | Check whether a constraint (x ~ BOT) can succeed,
 -- given the resulting state of the term oracle.
 canDiverge :: Name -> TmState -> Bool
-canDiverge x (standby, (_unhandled, env))
+canDiverge x TmS{ tm_pos = pos, tm_neg = neg }
   -- If the variable seems not evaluated, there is a possibility for
-  -- constraint x ~ BOT to be satisfiable.
-  | PmExprVar y <- varDeepLookup env x -- seems not forced
-  -- If it is involved (directly or indirectly) in any equality in the
-  -- worklist, we can assume that it is already indirectly evaluated,
-  -- as a side-effect of equality checking. If not, then we can assume
-  -- that the constraint is satisfiable.
-  = not $ any (isForcedByEq x) standby || any (isForcedByEq y) standby
-  -- Variable x is already in WHNF so the constraint is non-satisfiable
+  -- constraint x ~ BOT to be satisfiable. That's the case when we haven't found
+  -- a solution (i.e. some equivalent literal or constructor) for it yet.
+  | (_, PmExprVar y) <- varDeepLookup pos x -- seems not forced
+  -- Even if we don't have a solution yet, it might be involved in a negative
+  -- constraint, in which case we must already have evaluated it earlier.
+  , Nothing <- lookupDNameEnv neg y
+  = True
+  -- Variable x is already in WHNF or we know some refutable shape, so the
+  -- constraint is non-satisfiable
   | otherwise = False
 
-  where
-    isForcedByEq :: Name -> ComplexEq -> Bool
-    isForcedByEq y (e1, e2) = varIn y e1 || varIn y e2
-
--- | Check whether a variable is in the free variables of an expression
-varIn :: Name -> PmExpr -> Bool
-varIn x e = case e of
-  PmExprVar y    -> x == y
-  PmExprCon _ es -> any (x `varIn`) es
-  PmExprLit _    -> False
-  PmExprEq e1 e2 -> (x `varIn` e1) || (x `varIn` e2)
-  PmExprOther _  -> False
-
--- | Flatten the DAG (Could be improved in terms of performance.).
-flattenPmVarEnv :: PmVarEnv -> PmVarEnv
-flattenPmVarEnv env = mapNameEnv (exprDeepLookup env) env
-
--- | The state of the term oracle (includes complex constraints that cannot
--- progress unless we get more information).
-type TmState = ([ComplexEq], TmOracleEnv)
-
--- | Initial state of the oracle.
-initialTmState :: TmState
-initialTmState = ([], (False, emptyNameEnv))
-
--- | 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
-  $ applySubstComplexEq env complex -- replace everything we already know
-
--- | Solve a complex equality.
--- Nothing => definitely unsatisfiable
--- Just tms => I have added the complex equality and added
---             it to the tmstate; the result may or may not be
---             satisfiable
-solveComplexEq :: TmState -> ComplexEq -> Maybe TmState
-solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
+-- | Check whether the equality @x ~ e@ leads to a refutation. Make sure that
+-- @x@ and @e@ are completely substituted before!
+isRefutable :: Name -> PmExpr -> PmRefutEnv -> Bool
+isRefutable x e env
+  = fromMaybe False $ elem <$> exprToAlt e <*> lookupDNameEnv env x
+
+-- | Solve an equality (top-level).
+solveOneEq :: TmState -> TmVarCt -> Maybe TmState
+solveOneEq solver_env (TVC x e) = unify solver_env (PmExprVar (idName x), e)
+
+exprToAlt :: PmExpr -> Maybe PmAltCon
+exprToAlt (PmExprLit l)    = Just (PmAltLit l)
+exprToAlt _                = Nothing
+
+-- | Record that a particular 'Id' can't take the shape of a 'PmAltCon' in the
+-- 'TmState' and return @Nothing@ if that leads to a contradiction.
+addSolveRefutableAltCon :: TmState -> Id -> PmAltCon -> Maybe TmState
+addSolveRefutableAltCon original@TmS{ tm_pos = pos, tm_neg = neg } x nalt
+  = case exprToAlt e of
+      -- We have to take care to preserve Note [The Pos/Neg invariant]
+      Nothing         -> Just extended -- Not solved yet
+      Just alt                         -- We have a solution
+        | alt == nalt -> Nothing       -- ... which is contradictory
+        | otherwise   -> Just original -- ... which is compatible, rendering the
+  where                                --     refutation redundant
+    (y, e) = varDeepLookup pos (idName x)
+    extended = original { tm_neg = neg' }
+    neg' = alterDNameEnv (delNulls (insertNoDup nalt)) neg y
+
+-- | When updating 'tm_neg', we want to delete any 'null' entries. This adapter
+-- intends to provide a suitable interface for 'alterDNameEnv'.
+delNulls :: ([a] -> [a]) -> Maybe [a] -> Maybe [a]
+delNulls f mb_entry
+  | ret@(_:_) <- f (fromMaybe [] mb_entry) = Just ret
+  | otherwise                              = Nothing
+
+-- | Return all 'PmAltCon' shapes that are impossible for 'Id' to take, i.e.
+-- would immediately lead to a refutation by the term oracle.
+lookupRefutableAltCons :: Id -> TmState -> [PmAltCon]
+lookupRefutableAltCons x TmS { tm_neg = neg }
+  = fromMaybe [] (lookupDNameEnv neg (idName x))
+
+-- | Is the given variable /rigid/ (i.e., we have a solution for it) or
+-- /flexible/ (i.e., no solution)? Returns the solution if /rigid/. A
+-- semantically helpful alias for 'lookupNameEnv'.
+isRigid :: TmState -> Name -> Maybe PmExpr
+isRigid TmS{ tm_pos = pos } x = lookupNameEnv pos x
+
+-- | @isFlexible tms = isNothing . 'isRigid' tms@
+isFlexible :: TmState -> Name -> Bool
+isFlexible tms = isNothing . isRigid tms
+
+-- | Try to unify two 'PmExpr's and record the gained knowledge in the
+-- 'TmState'.
+--
+-- Returns @Nothing@ when there's a contradiction. Returns @Just tms@
+-- when the constraint was compatible with prior facts, in which case @tms@ has
+-- integrated the knowledge from the equality constraint.
+unify :: TmState -> (PmExpr, PmExpr) -> Maybe TmState
+unify tms eq@(e1, e2) = case eq of
   -- We cannot do a thing about these cases
-  (PmExprOther _,_)            -> Just (standby, (True, env))
-  (_,PmExprOther _)            -> Just (standby, (True, env))
+  (PmExprOther _,_)            -> boring
+  (_,PmExprOther _)            -> boring
 
   (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
     -- See Note [Undecidable Equality for Overloaded Literals]
-    True  -> Just solver_state
-    False -> Nothing
+    True  -> boring
+    False -> unsat
 
   (PmExprCon c1 ts1, PmExprCon c2 ts2)
-    | c1 == c2  -> foldlM solveComplexEq solver_state (zip ts1 ts2)
-    | otherwise -> Nothing
-  (PmExprCon _ [], PmExprEq t1 t2)
-    | isTruePmExpr e1  -> solveComplexEq solver_state (t1, t2)
-    | isFalsePmExpr e1 -> Just (eq:standby, (unhandled, env))
-  (PmExprEq t1 t2, PmExprCon _ [])
-    | isTruePmExpr e2   -> solveComplexEq solver_state (t1, t2)
-    | isFalsePmExpr e2  -> Just (eq:standby, (unhandled, env))
+    | c1 == c2  -> foldlM unify tms (zip ts1 ts2)
+    | otherwise -> unsat
 
   (PmExprVar x, PmExprVar y)
-    | x == y    -> Just solver_state
-    | otherwise -> extendSubstAndSolve x e2 solver_state
-
-  (PmExprVar x, _) -> extendSubstAndSolve x e2 solver_state
-  (_, PmExprVar x) -> extendSubstAndSolve x e1 solver_state
-
-  (PmExprEq _ _, PmExprEq _ _) -> Just (eq:standby, (unhandled, env))
-
-  _ -> WARN( True, text "solveComplexEq: Catch all" <+> ppr eq )
-       Just (standby, (True, env)) -- I HATE CATCH-ALLS
-
--- | Extend the substitution and solve the (possibly updated) constraints.
-extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState
-extendSubstAndSolve x e (standby, (unhandled, env))
-  = foldlM solveComplexEq new_incr_state (map simplifyComplexEq changed)
+    | x == y    -> boring
+
+  -- It's important to handle both rigid cases first, otherwise we get cyclic
+  -- substitutions. Cf. 'extendSubstAndSolve' and
+  -- @testsuite/tests/pmcheck/should_compile/CyclicSubst.hs@.
+  (PmExprVar x, _)
+    | Just e1' <- isRigid tms x -> unify tms (e1', e2)
+  (_, PmExprVar y)
+    | Just e2' <- isRigid tms y -> unify tms (e1, e2')
+  (PmExprVar x, PmExprVar y)    -> Just (equate x y tms)
+  (PmExprVar x, _)              -> trySolve x e2 tms
+  (_, PmExprVar y)              -> trySolve y e1 tms
+
+  _ -> WARN( True, text "unify: Catch all" <+> ppr eq)
+       boring -- I HATE CATCH-ALLS
+  where
+    boring    = Just tms
+    unsat     = Nothing
+
+-- | Merges the equivalence classes of @x@ and @y@ by extending the substitution
+-- with @x :-> y@.
+-- Preconditions: @x /= y@ and both @x@ and @y@ are flexible (cf.
+-- 'isFlexible'/'isRigid').
+equate :: Name -> Name -> TmState -> TmState
+equate x y tms@TmS{ tm_pos = pos, tm_neg = neg }
+  = ASSERT( x /= y )
+    ASSERT( isFlexible tms x )
+    ASSERT( isFlexible tms y )
+    tms'
   where
-    -- Apply the substitution to the worklist and partition them to the ones
-    -- that had some progress and the rest. Then, recurse over the ones that
-    -- had some progress. Careful about performance:
-    -- See Note [Representation of Term Equalities] in deSugar/Check.hs
-    (changed, unchanged) = partitionWith (substComplexEq x e) standby
-    new_incr_state       = (unchanged, (unhandled, extendNameEnv env x e))
+    pos' = extendNameEnv pos x (PmExprVar y)
+    -- Be careful to uphold Note [The Pos/Neg invariant] by merging the refuts
+    -- of x into those of y
+    nalts = fromMaybe [] (lookupDNameEnv neg x)
+    neg'  = alterDNameEnv (delNulls (unionLists nalts)) neg y
+              `delFromDNameEnv` x
+    tms'  = TmS { tm_pos = pos', tm_neg = neg' }
+
+-- | Extend the substitution with a mapping @x: -> e@ if compatible with
+-- refutable shapes of @x@ and its solution, reject (@Nothing@) otherwise.
+--
+-- Precondition: @x@ is flexible (cf. 'isFlexible'/'isRigid').
+-- Precondition: @e@ is a 'PmExprCon' or 'PmExprLit'
+trySolve:: Name -> PmExpr -> TmState -> Maybe TmState
+trySolve x e _tms@TmS{ tm_pos = pos, tm_neg = neg }
+  | ASSERT( isFlexible _tms x )
+    ASSERT( _is_whnf e )
+    isRefutable x e neg
+  = Nothing
+  | otherwise
+  = Just (TmS (extendNameEnv pos x e) (delFromDNameEnv neg x))
+  where
+    _is_whnf PmExprCon{} = True
+    _is_whnf PmExprLit{} = True
+    _is_whnf _           = False
 
 -- | When we know that a variable is fresh, we do not actually have to
 -- check whether anything changes, we know that nothing does. Hence,
--- `extendSubst` simply extends the substitution, unlike what
--- `extendSubstAndSolve` does.
+-- @extendSubst@ simply extends the substitution, unlike what
+-- 'extendSubstAndSolve' does.
 extendSubst :: Id -> PmExpr -> TmState -> TmState
-extendSubst y e (standby, (unhandled, env))
+extendSubst y e solver_state@TmS{ tm_pos = pos }
   | isNotPmExprOther simpl_e
-  = (standby, (unhandled, extendNameEnv env x simpl_e))
-  | otherwise = (standby, (True, env))
+  = solver_state { tm_pos = extendNameEnv pos x simpl_e }
+  | otherwise = solver_state
   where
     x = idName y
-    simpl_e = fst $ simplifyPmExpr $ exprDeepLookup env e
-
--- | Simplify a complex equality.
-simplifyComplexEq :: ComplexEq -> ComplexEq
-simplifyComplexEq (e1, e2) = (fst $ simplifyPmExpr e1, fst $ simplifyPmExpr e2)
-
--- | Simplify an expression. The boolean indicates if there has been any
--- simplification or if the operation was a no-op.
-simplifyPmExpr :: PmExpr -> (PmExpr, Bool)
--- See Note [Deep equalities]
-simplifyPmExpr e = case e of
-  PmExprCon c ts -> case mapAndUnzip simplifyPmExpr ts of
-                      (ts', bs) -> (PmExprCon c ts', or bs)
-  PmExprEq t1 t2 -> simplifyEqExpr t1 t2
-  _other_expr    -> (e, False) -- the others are terminals
-
--- | Simplify an equality expression. The equality is given in parts.
-simplifyEqExpr :: PmExpr -> PmExpr -> (PmExpr, Bool)
--- See Note [Deep equalities]
-simplifyEqExpr e1 e2 = case (e1, e2) of
-  -- Varables
-  (PmExprVar x, PmExprVar y)
-    | x == y -> (truePmExpr, True)
-
-  -- Literals
-  (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
-    -- See Note [Undecidable Equality for Overloaded Literals]
-    True  -> (truePmExpr,  True)
-    False -> (falsePmExpr, True)
-
-  -- Can potentially be simplified
-  (PmExprEq {}, _) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
-    ((e1', True ), (e2', _    )) -> simplifyEqExpr e1' e2'
-    ((e1', _    ), (e2', True )) -> simplifyEqExpr e1' e2'
-    ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
-  (_, PmExprEq {}) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
-    ((e1', True ), (e2', _    )) -> simplifyEqExpr e1' e2'
-    ((e1', _    ), (e2', True )) -> simplifyEqExpr e1' e2'
-    ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
-
-  -- Constructors
-  (PmExprCon c1 ts1, PmExprCon c2 ts2)
-    | c1 == c2 ->
-        let (ts1', bs1) = mapAndUnzip simplifyPmExpr ts1
-            (ts2', bs2) = mapAndUnzip simplifyPmExpr ts2
-            (tss, _bss) = zipWithAndUnzip simplifyEqExpr ts1' ts2'
-            worst_case  = PmExprEq (PmExprCon c1 ts1') (PmExprCon c2 ts2')
-        in  if | not (or bs1 || or bs2) -> (worst_case, False) -- no progress
-               | all isTruePmExpr  tss  -> (truePmExpr, True)
-               | any isFalsePmExpr tss  -> (falsePmExpr, True)
-               | otherwise              -> (worst_case, False)
-    | otherwise -> (falsePmExpr, True)
-
-  -- We cannot do anything about the rest..
-  _other_equality -> (original, False)
-
-  where
-    original = PmExprEq e1 e2 -- reconstruct equality
-
--- | 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 to a variable.
-varDeepLookup :: PmVarEnv -> Name -> PmExpr
-varDeepLookup env x
-  | Just e <- lookupNameEnv env x = exprDeepLookup env e -- go deeper
-  | otherwise                  = PmExprVar x          -- terminal
+    simpl_e = exprDeepLookup pos e
+
+-- | Apply an (un-flattened) substitution to a variable and return its
+-- representative in the triangular substitution @env@ and the completely
+-- substituted expression. The latter may just be the representative wrapped
+-- with 'PmExprVar' if we haven't found a solution for it yet.
+varDeepLookup :: TmVarCtEnv -> Name -> (Name, PmExpr)
+varDeepLookup env x = case lookupNameEnv env x of
+  Just (PmExprVar y) -> varDeepLookup env y
+  Just e             -> (x, exprDeepLookup env e) -- go deeper
+  Nothing            -> (x, PmExprVar x)          -- terminal
 {-# INLINE varDeepLookup #-}
 
 -- | Apply an (un-flattened) substitution to an expression.
-exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
-exprDeepLookup env (PmExprVar x)    = varDeepLookup env x
+exprDeepLookup :: TmVarCtEnv -> PmExpr -> PmExpr
+exprDeepLookup env (PmExprVar x)    = snd (varDeepLookup env x)
 exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es)
-exprDeepLookup env (PmExprEq e1 e2) = PmExprEq (exprDeepLookup env e1)
-                                               (exprDeepLookup env e2)
 exprDeepLookup _   other_expr       = other_expr -- PmExprLit, PmExprOther
 
 -- | External interface to the term oracle.
-tmOracle :: TmState -> [ComplexEq] -> Maybe TmState
+tmOracle :: TmState -> [TmVarCt] -> Maybe TmState
 tmOracle tm_state eqs = foldlM solveOneEq tm_state eqs
 
 -- | Type of a PmLit
@@ -248,18 +314,49 @@ pmLitType :: PmLit -> Type -- should be in PmExpr but gives cyclic imports :(
 pmLitType (PmSLit   lit) = hsLitType   lit
 pmLitType (PmOLit _ lit) = overLitType lit
 
-{- Note [Deep equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Solving nested equalities is the most difficult part. The general strategy
-is the following:
+{- Note [Refutable shapes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Consider a pattern match like
+
+    foo x
+      | 0 <- x = 42
+      | 0 <- x = 43
+      | 1 <- x = 44
+      | otherwise = 45
+
+This will result in the following initial matching problem:
+
+    PatVec: x     (0 <- x)
+    ValVec: $tm_y
+
+Where the first line is the pattern vector and the second line is the value
+vector abstraction. When we handle the first pattern guard in Check, it will be
+desugared to a match of the form
+
+    PatVec: x     0
+    ValVec: $tm_y x
+
+In LitVar, this will split the value vector abstraction for `x` into a positive
+`PmLit 0` and a negative `PmLit x [0]` value abstraction. While the former is
+immediately matched against the pattern vector, the latter (vector value
+abstraction `~[0] $tm_y`) is completely uncovered by the clause.
+
+`pmcheck` proceeds by *discarding* the the value vector abstraction involving
+the guard to accomodate for the desugaring. But this also discards the valuable
+information that `x` certainly is not the literal 0! Consequently, we wouldn't
+be able to report the second clause as redundant.
 
-  * Equalities of the form (True ~ (e1 ~ e2)) are transformed to just
-    (e1 ~ e2) and then treated recursively.
+That's a typical example of why we need the term oracle, and in this specific
+case, the ability to encode that `x` certainly is not the literal 0. Now the
+term oracle can immediately refute the constraint `x ~ 0` generated by the
+second clause and report the clause as redundant. After the third clause, the
+set of such *refutable* literals is again extended to `[0, 1]`.
 
-  * Equalities of the form (False ~ (e1 ~ e2)) cannot be analyzed unless
-    we know more about the inner equality (e1 ~ e2). That's exactly what
-    `simplifyEqExpr' tries to do: It takes e1 and e2 and either returns
-    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.
+In general, we want to store a set of refutable shapes (`PmAltCon`) for each
+variable. That's the purpose of the `PmRefutEnv`. `addSolveRefutableAltCon` will
+add such a refutable mapping to the `PmRefutEnv` in the term oracles state and
+check if causes any immediate contradiction. Whenever we record a solution in
+the substitution via `extendSubstAndSolve`, the refutable environment is checked
+for any matching refutable `PmAltCon`.
 -}