Extract PmTypes module from PmExpr and PmOraclewip/pmcheck-types

Apparently ghc-lib-parser's API blew up because the newly induced cyclic
dependency between TcRnTypes and PmOracle pulled in the other half of
GHC into the relevant strongly-connected component.

This patch arranges it so that PmTypes exposes mostly data type
definitions and type class instances to be used within PmOracle, without
importing the any of the possibly offending modules DsMonad, TcSimplify
and FamInst.

8 files changed, 264 insertions, 270 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 3a1515d0cc..1c9493bbca 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -26,7 +26,7 @@ module Check (
 
 import GhcPrelude
 
-import PmExpr
+import PmTypes
 import PmOracle
 import PmPpr
 import BasicTypes (Origin, isGenerated)
@@ -817,7 +817,7 @@ below is the *right thing to do*:
 The case with literals is a bit different. a literal @l@ should be translated
 to @x (True <- x == from l)@. Since we want to have better warnings for
 overloaded literals as it is a very common feature, we treat them differently.
-They are mainly covered in Note [Undecidable Equality for PmAltCons] in PmExpr.
+They are mainly covered in Note [Undecidable Equality for PmAltCons] in PmTypes.
 
 4. N+K Patterns & Pattern Synonyms
 ----------------------------------
@@ -949,7 +949,7 @@ additional features added to the coverage checker which are not described in
 the paper. This Note serves as a reference for these new features.
 
 * Value abstractions are severely simplified to the point where they are just
-  variables. The information about the PmExpr shape of a variable is encoded in
+  variables. The information about the shape of a variable is encoded in
   the oracle state 'Delta' instead.
 * Handling of uninhabited fields like `!Void`.
   See Note [Strict argument type constraints] in PmOracle.
@@ -1397,9 +1397,6 @@ addPatTmCs ps xs k = do
   pv <- concat <$> translatePatVec fam_insts ps
   locallyExtendPmDelta (\delta -> addVarPatVecCt delta xs pv) k
 
--- ----------------------------------------------------------------------------
--- * Converting between Value Abstractions, Patterns and PmExpr
-
 -- | Add a constraint equating a variable to a 'PatVec'. Picks out the single
 -- 'PmPat' of arity 1 and equates x to it. Returns the original Delta if that
 -- fails. Otherwise it returns Nothing when the resulting Delta would be
@@ -1422,7 +1419,7 @@ addVarPatVecCt delta (x:xs) (pat:pv)
 addVarPatVecCt delta []     pv = ASSERT( patVecArity pv == 0 ) pure (Just delta)
 addVarPatVecCt _     (_:_)  [] = panic "More match vars than patterns"
 
--- | Convert a pattern to a 'PmExpr' (will be either 'Nothing' if the pattern is
+-- | Convert a pattern to a 'PmTypes' (will be either 'Nothing' if the pattern is
 -- a guard pattern, or 'Just' an expression in all other cases) by dropping the
 -- guards
 addVarPatCt :: Delta -> Id -> PmPat -> DsM (Maybe Delta)
diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs
index d937b3b134..1bfa25324a 100644
--- a/compiler/deSugar/DsMonad.hs
+++ b/compiler/deSugar/DsMonad.hs
@@ -70,7 +70,7 @@ import BasicTypes ( Origin )
 import DataCon
 import ConLike
 import TyCon
-import {-# SOURCE #-} PmOracle
+import PmTypes
 import Id
 import Module
 import Outputable
diff --git a/compiler/deSugar/PmOracle.hs b/compiler/deSugar/PmOracle.hs
index 93c4d1d959..f9abae481c 100644
--- a/compiler/deSugar/PmOracle.hs
+++ b/compiler/deSugar/PmOracle.hs
@@ -31,7 +31,7 @@ module PmOracle (
 
 import GhcPrelude
 
-import PmExpr
+import PmTypes
 
 import DynFlags
 import Outputable
@@ -77,7 +77,6 @@ import Control.Monad.Trans.State.Strict
 import Data.Bifunctor (second)
 import Data.Foldable (foldlM)
 import Data.List     (find)
-import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.NonEmpty as NonEmpty
 import qualified Data.Semigroup as Semigroup
 
@@ -100,22 +99,6 @@ mkPmId ty = getUniqueM >>= \unique ->
 -----------------------------------------------
 -- * Caching possible matches of a COMPLETE set
 
-type ConLikeSet = UniqDSet ConLike
-
--- | A data type caching the results of 'completeMatchConLikes' with support for
--- deletion of contructors that were already matched on.
-data PossibleMatches
-  = PM TyCon (NonEmpty ConLikeSet)
-  -- ^ Each ConLikeSet is a (subset of) the constructors in a COMPLETE pragma
-  -- 'NonEmpty' because the empty case would mean that the type has no COMPLETE
-  -- set at all, for which we have 'NoPM'
-  | NoPM
-  -- ^ No COMPLETE set for this type (yet). Think of overloaded literals.
-
-instance Outputable PossibleMatches where
-  ppr (PM _tc cs) = ppr (NonEmpty.toList cs)
-  ppr NoPM = text "<NoPM>"
-
 initIM :: Type -> DsM (Maybe PossibleMatches)
 initIM ty = case splitTyConApp_maybe ty of
   Nothing -> pure Nothing
@@ -235,26 +218,6 @@ equateTyVars ex_tvs1 ex_tvs2
 -- * Pattern match oracle
 
 
--- | Term and type constraints to accompany each value vector abstraction.
--- For efficiency, we store the term oracle state instead of the term
--- constraints.
-data Delta = MkDelta { delta_ty_cs :: Bag EvVar  -- Type oracle; things like a~Int
-                     , delta_tm_cs :: TmState }  -- Term oracle; things like x~Nothing
-
--- | An initial delta that is always satisfiable
-initDelta :: Delta
-initDelta = MkDelta emptyBag initTmState
-
-instance Outputable Delta where
-  ppr delta = vcat [
-      -- intentionally formatted this way enable the dev to comment in only
-      -- the info she needs
-      ppr (delta_tm_cs delta),
-      ppr (pprEvVarWithType <$> delta_ty_cs delta)
-      --ppr (delta_ty_cs delta)
-    ]
-
-
 {- Note [Recovering from unsatisfiable pattern-matching constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider the following code (see #12957 and #15450):
@@ -603,68 +566,10 @@ tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \delta -> do
 
 {- *********************************************************************
 *                                                                      *
-                 SharedIdEnv
               DIdEnv with sharing
 *                                                                      *
 ********************************************************************* -}
 
--- | Either @Indirect x@, meaning the value is represented by that of @x@, or
--- an @Entry@ containing containing the actual value it represents.
-data Shared a
-  = Indirect Id
-  | Entry a
-
--- | A 'DIdEnv' in which entries can be shared by multiple 'Id's.
--- Merge equivalence classes of two Ids by 'setIndirectSDIE' and set the entry
--- of an Id with 'setEntrySDIE'.
-newtype SharedDIdEnv a
-  = SDIE { unSDIE :: DIdEnv (Shared a) }
-
-emptySDIE :: SharedDIdEnv a
-emptySDIE = SDIE emptyDVarEnv
-
-lookupReprAndEntrySDIE :: SharedDIdEnv a -> Id -> (Id, Maybe a)
-lookupReprAndEntrySDIE sdie@(SDIE env) x = case lookupDVarEnv env x of
-  Nothing           -> (x, Nothing)
-  Just (Indirect y) -> lookupReprAndEntrySDIE sdie y
-  Just (Entry a)    -> (x, Just a)
-
--- | @lookupSDIE env x@ looks up an entry for @x@, looking through all
--- 'Indirect's until it finds a shared 'Entry'.
-lookupSDIE :: SharedDIdEnv a -> Id -> Maybe a
-lookupSDIE sdie x = snd (lookupReprAndEntrySDIE sdie x)
-
--- | Check if two variables are part of the same equivalence class.
-sameRepresentative :: SharedDIdEnv a -> Id -> Id -> Bool
-sameRepresentative sdie x y =
-  fst (lookupReprAndEntrySDIE sdie x) == fst (lookupReprAndEntrySDIE sdie y)
-
--- | @setIndirectSDIE env x y@ sets @x@'s 'Entry' to @Indirect y@, thereby
--- merging @x@'s equivalence class into @y@'s. This will discard all info on
--- @x@!
-setIndirectSDIE :: SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a
-setIndirectSDIE sdie@(SDIE env) x y =
-  SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Indirect y)
-
--- | @setEntrySDIE env x a@ sets the 'Entry' @x@ is associated with to @a@,
--- thereby modifying its whole equivalence class.
-setEntrySDIE :: SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
-setEntrySDIE sdie@(SDIE env) x a =
-  SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Entry a)
-
-traverseSharedIdEnv :: Applicative f => (a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b)
-traverseSharedIdEnv f = fmap (SDIE . listToUDFM) . traverse g . udfmToList . unSDIE
-  where
-    g (u, Indirect y) = pure (u,Indirect y)
-    g (u, Entry a)    = (u,) . Entry <$> f a
-
-instance Outputable a => Outputable (Shared a) where
-  ppr (Indirect x) = ppr x
-  ppr (Entry a)    = ppr a
-
-instance Outputable a => Outputable (SharedDIdEnv a) where
-  ppr (SDIE env) = ppr env
-
 
 {- *********************************************************************
 *                                                                      *
@@ -673,66 +578,6 @@ instance Outputable a => Outputable (SharedDIdEnv a) where
 *                                                                      *
 ********************************************************************* -}
 
--- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These
--- entries are possibly shared when we figure out that two variables must be
--- equal, thus represent the same set of values.
---
--- See Note [TmState invariants].
-newtype TmState = TS (SharedDIdEnv VarInfo)
-  -- Deterministic so that we generate deterministic error messages
-
--- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
--- and negative ('vi_neg') facts, like "x is not (:)".
--- Also caches the type ('vi_ty'), the 'PossibleMatches' of a COMPLETE set
--- ('vi_cache') and the number of times each variable was refined
--- ('vi_n_refines').
---
--- Subject to Note [The Pos/Neg invariant].
-data VarInfo
-  = VI
-  { vi_ty  :: !Type
-  -- ^ The type of the variable. Important for rejecting possible GADT
-  -- constructors or incompatible pattern synonyms (@Just42 :: Maybe Int@).
-
-  , vi_pos :: [(PmAltCon, [Id])]
-  -- ^ Positive info: 'PmExprCon's it is (i.e. @x ~ [Just y, PatSyn z]@), all
-  -- at the same time (i.e. conjunctive).  We need a list because of nested
-  -- pattern matches involving pattern synonym
-  --    case x of { Just y -> case x of PatSyn z -> ... }
-  -- However, no more than one RealDataCon in the list, otherwise contradiction
-  -- because of generativity.
-
-  , vi_neg :: ![PmAltCon]
-  -- ^ Negative info: A list of 'PmAltCon's that it cannot match.
-  -- Example, assuming
-  --
-  -- @
-  --     data T = Leaf Int | Branch T T | Node Int T
-  -- @
-  --
-  -- then @x /~ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
-  -- and hence can only match @Branch@. Is orthogonal to anything from 'vi_pos',
-  -- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing
-  -- between 'vi_pos' and 'vi_neg'.
-
-  -- See Note [Why record both positive and negative info?]
-
-  , vi_cache :: !PossibleMatches
-  -- ^ A cache of the associated COMPLETE sets. At any time a superset of
-  -- possible constructors of each COMPLETE set. So, if it's not in here, we
-  -- can't possibly match on it. Complementary to 'vi_neg'. We still need it
-  -- to recognise completion of a COMPLETE set efficiently for large enums.
-
-  , vi_n_refines :: !Int
-  -- ^ Purely for Check performance reasons. The number of times this
-  -- representative was refined ('refineToAltCon') in the Check's ConVar split.
-  -- Sadly, we can't store this info in the Check module, as it's tightly coupled
-  -- to the particular 'Delta' and also is per *representative*, not per
-  -- syntactic variable. Note that this number does not always correspond to the
-  -- length of solutions: 'addVarConCt' might add a solution without
-  -- incurring the potential exponential blowup by ConVar.
-  }
-
 {- Note [The Pos/Neg invariant]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Invariant applying to each VarInfo: Whenever we have @(C, [y,z])@ in 'vi_pos',
@@ -830,19 +675,6 @@ The "list" option is far simpler, but incurs some overhead in representation and
 warning messages (which can be alleviated by someone with enough dedication).
 -}
 
--- | Not user-facing.
-instance Outputable TmState where
-  ppr (TS state) = ppr state
-
--- | Not user-facing.
-instance Outputable VarInfo where
-  ppr (VI ty pos neg cache n)
-    = braces (hcat (punctuate comma [ppr ty, ppr pos, ppr neg, ppr cache, ppr n]))
-
--- | Initial state of the oracle.
-initTmState :: TmState
-initTmState = TS emptySDIE
-
 -- | A 'SatisfiabilityCheck' based on new term-level constraints.
 -- Returns a new 'Delta' if the new constraints are compatible with existing
 -- ones.
@@ -1098,15 +930,15 @@ ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This wo
 -- impossible matches.
 ensureAllPossibleMatchesInhabited :: Delta -> DsM (Maybe Delta)
 ensureAllPossibleMatchesInhabited delta@MkDelta{ delta_tm_cs = TS env }
-  = runMaybeT (set_tm_cs_env delta <$> traverseSharedIdEnv go env)
+  = runMaybeT (set_tm_cs_env delta <$> traverseSDIE go env)
   where
     set_tm_cs_env delta env = delta{ delta_tm_cs = TS env }
     go vi = MaybeT (ensureInhabited delta vi)
 
 -- | @refineToAltCon delta x con arg_tys ex_tyvars@ instantiates @con@ at
 -- @arg_tys@ with fresh variables (equating existentials to @ex_tyvars@).
--- It adds a new term equality equating @x@ is to the resulting 'PmExprCon' and
--- new type equalities arising from GADT matches.
+-- It adds a new term equality equating @x@ is to the resulting 'PmAltCon' app
+-- and new type equalities arising from GADT matches.
 -- If successful, returns the new @delta@ and the fresh term variables, or
 -- @Nothing@ otherwise.
 refineToAltCon :: Delta -> Id -> PmAltCon -> [Type] -> [TyVar] -> DsM (Maybe (Delta, [Id]))
@@ -1286,19 +1118,19 @@ addVarVarCt delta@MkDelta{ delta_tm_cs = TS env } (x, y)
   -- class, otherwise we might get cyclic substitutions.
   -- Cf. 'extendSubstAndSolve' and
   -- @testsuite/tests/pmcheck/should_compile/CyclicSubst.hs@.
-  | sameRepresentative env x y = pure delta
-  | otherwise                  = equate delta x y
+  | sameRepresentativeSDIE env x y = pure delta
+  | otherwise                      = equate delta x y
 
 -- | @equate ts@(TS env) x y@ merges the equivalence classes of @x@ and @y@ by
 -- adding an indirection to the environment.
 -- Makes sure that the positive and negative facts of @x@ and @y@ are
 -- compatible.
--- Preconditions: @not (sameRepresentative env x y)@
+-- Preconditions: @not (sameRepresentativeSDIE env x y)@
 --
 -- See Note [TmState invariants].
 equate :: Delta -> Id -> Id -> MaybeT DsM Delta
 equate delta@MkDelta{ delta_tm_cs = TS env } x y
-  = ASSERT( not (sameRepresentative env x y) )
+  = ASSERT( not (sameRepresentativeSDIE env x y) )
     case (lookupSDIE env x, lookupSDIE env y) of
       (Nothing, _) -> pure (delta{ delta_tm_cs = TS (setIndirectSDIE env x y) })
       (_, Nothing) -> pure (delta{ delta_tm_cs = TS (setIndirectSDIE env y x) })
@@ -1323,9 +1155,9 @@ equate delta@MkDelta{ delta_tm_cs = TS env } x y
         -- go!
         pure delta_neg
 
--- | @addVarConCt x alt args ts@ extends the substitution with a mapping @x: ->
--- PmExprCon alt args@ if compatible with refutable shapes of @x@ and its
--- solution, reject (@Nothing@) otherwise.
+-- | @addVarConCt x alt args ts@ extends the substitution with a solution
+-- @x :-> (alt, args)@ if compatible with refutable shapes of @x@ and its
+-- other solutions, reject (@Nothing@) otherwise.
 --
 -- See Note [TmState invariants].
 addVarConCt :: Delta -> Id -> PmAltCon -> [Id] -> MaybeT DsM Delta
diff --git a/compiler/deSugar/PmPpr.hs b/compiler/deSugar/PmPpr.hs
index bee38ed46b..82e6d0f0a0 100644
--- a/compiler/deSugar/PmPpr.hs
+++ b/compiler/deSugar/PmPpr.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE CPP, ViewPatterns #-}
 
--- | Provides factilities for pretty-printing 'PmExpr's in a way approriate for
+-- | Provides factilities for pretty-printing 'Delta's in a way appropriate for
 -- user facing pattern match warnings.
 module PmPpr (
         pprUncovered
@@ -22,7 +22,7 @@ import Util
 import Maybes
 import Data.List.NonEmpty (NonEmpty, nonEmpty, toList)
 
-import PmExpr
+import PmTypes
 import PmOracle
 
 -- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its
@@ -44,7 +44,7 @@ pprUncovered delta vas
   | otherwise         = hang (fsep vec) 4 $
                           text "where" <+> vcat (map (pprRefutableShapes . snd) (udfmToList refuts))
   where
-    ppr_action       = mapM (pprPmExprVar 2) vas
+    ppr_action       = mapM (pprPmVar 2) vas
     (vec, renamings) = runPmPpr delta ppr_action
     refuts           = prettifyRefuts delta renamings
 
@@ -128,16 +128,16 @@ checkRefuts x = do
 -- | Pretty print a variable, but remember to prettify the names of the variables
 -- that refer to neg-literals. The ones that cannot be shown are printed as
 -- underscores.
-pprPmExprVar :: Int -> Id -> PmPprM SDoc
-pprPmExprVar prec x = do
+pprPmVar :: Int -> Id -> PmPprM SDoc
+pprPmVar prec x = do
   delta <- ask
   case lookupSolution delta x of
-    Just (alt, args) -> pprPmExprCon prec alt args
+    Just (alt, args) -> pprPmAltCon prec alt args
     Nothing          -> fromMaybe underscore <$> checkRefuts x
 
-pprPmExprCon :: Int -> PmAltCon -> [Id] -> PmPprM SDoc
-pprPmExprCon _prec (PmAltLit l)      _    = pure (ppr l)
-pprPmExprCon prec  (PmAltConLike cl) args = do
+pprPmAltCon :: Int -> PmAltCon -> [Id] -> PmPprM SDoc
+pprPmAltCon _prec (PmAltLit l)      _    = pure (ppr l)
+pprPmAltCon prec  (PmAltConLike cl) args = do
   delta <- ask
   pprConLike delta prec cl args
 
@@ -146,24 +146,24 @@ pprConLike delta _prec cl args
   | Just pm_expr_list <- pmExprAsList delta (PmAltConLike cl) args
   = case pm_expr_list of
       NilTerminated list ->
-        brackets . fsep . punctuate comma <$> mapM (pprPmExprVar 0) list
+        brackets . fsep . punctuate comma <$> mapM (pprPmVar 0) list
       WcVarTerminated pref x ->
-        parens   . fcat . punctuate colon <$> mapM (pprPmExprVar 0) (toList pref ++ [x])
+        parens   . fcat . punctuate colon <$> mapM (pprPmVar 0) (toList pref ++ [x])
 pprConLike _delta _prec (RealDataCon con) args
   | isUnboxedTupleCon con
   , let hash_parens doc = text "(#" <+> doc <+> text "#)"
-  = hash_parens . fsep . punctuate comma <$> mapM (pprPmExprVar 0) args
+  = hash_parens . fsep . punctuate comma <$> mapM (pprPmVar 0) args
   | isTupleDataCon con
-  = parens . fsep . punctuate comma <$> mapM (pprPmExprVar 0) args
+  = parens . fsep . punctuate comma <$> mapM (pprPmVar 0) args
 pprConLike _delta prec cl args
   | conLikeIsInfix cl = case args of
-      [x, y] -> do x' <- pprPmExprVar 1 x
-                   y' <- pprPmExprVar 1 y
+      [x, y] -> do x' <- pprPmVar 1 x
+                   y' <- pprPmVar 1 y
                    return (cparen (prec > 0) (x' <+> ppr cl <+> y'))
       -- can it be infix but have more than two arguments?
-      list   -> pprPanic "pprPmExprCon:" (ppr list)
+      list   -> pprPanic "pprConLike:" (ppr list)
   | null args = return (ppr cl)
-  | otherwise = do args' <- mapM (pprPmExprVar 2) args
+  | otherwise = do args' <- mapM (pprPmVar 2) args
                    return (cparen (prec > 1) (fsep (ppr cl : args')))
 
 -- | The result of 'pmExprAsList'.
@@ -171,7 +171,7 @@ data PmExprList
   = NilTerminated [Id]
   | WcVarTerminated (NonEmpty Id) Id
 
--- | Extract a list of 'PmExpr's out of a sequence of cons cells, optionally
+-- | Extract a list of 'Id's out of a sequence of cons cells, optionally
 -- terminated by a wildcard variable instead of @[]@. Some examples:
 --
 -- * @pmExprAsList (1:2:[]) == Just ('NilTerminated' [1,2])@, a regular,
diff --git a/compiler/deSugar/PmExpr.hs b/compiler/deSugar/PmTypes.hs
index f83c63e4fd..fc97f636a7 100644
--- a/compiler/deSugar/PmExpr.hs
+++ b/compiler/deSugar/PmTypes.hs
@@ -1,17 +1,35 @@
 {-
 Author: George Karachalias <george.karachalias@cs.kuleuven.be>
-
-Haskell expressions (as used by the pattern matching checker) and utilities.
+        Sebastian Graf <sgraf1337@gmail.com>
 -}
 
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TupleSections #-}
+
+-- | Types used through-out pattern match checking. This module is mostly there
+-- to be imported from "TcRnTypes". The exposed API is that of "PmOracle" and
+-- "Check".
+module PmTypes (
+        -- * Representations for Literals and AltCons
+        PmLit(..), PmLitValue(..), PmAltCon(..), pmLitType, pmAltConType,
+
+        -- ** Equality on 'PmAltCon's
+        PmEquality(..), eqPmAltCon,
+
+        -- ** Operations on 'PmLit'
+        literalToPmLit, negatePmLit, overloadPmLit,
+        pmLitAsStringLit, coreExprAsPmLit,
+
+        -- * Caching partially matched COMPLETE sets
+        ConLikeSet, PossibleMatches(..),
 
-module PmExpr (
-        PmLit(..), PmLitValue(..), PmAltCon(..),
-        pmAltConType, PmEquality(..), eqPmAltCon,
-        pmLitType, literalToPmLit, negatePmLit, overloadPmLit,
-        pmLitAsStringLit, coreExprAsPmLit
+        -- * A 'DIdEnv' where entries may be shared
+        Shared(..), SharedDIdEnv(..), emptySDIE, lookupSDIE, sameRepresentativeSDIE,
+        setIndirectSDIE, setEntrySDIE, traverseSDIE,
+
+        -- * The pattern match oracle
+        VarInfo(..), TmState(..), Delta(..), initDelta,
     ) where
 
 #include "HsVersions.h"
@@ -19,8 +37,13 @@ module PmExpr (
 import GhcPrelude
 
 import Util
+import Bag
 import FastString
+import Var (EvVar)
 import Id
+import VarEnv
+import UniqDSet
+import UniqDFM
 import Name
 import DataCon
 import ConLike
@@ -34,22 +57,13 @@ import CoreUtils (exprType)
 import PrelNames
 import TysWiredIn
 import TysPrim
+import TcRnTypes (pprEvVarWithType)
 
 import Numeric (fromRat)
 import Data.Foldable (find)
+import qualified Data.List.NonEmpty as NonEmpty
 import Data.Ratio
 
-{-
-%************************************************************************
-%*                                                                      *
-                         Lifted Expressions
-%*                                                                      *
-%************************************************************************
--}
-
--- ----------------------------------------------------------------------------
--- ** Types
-
 -- | Literals (simple and overloaded ones) for pattern match checking.
 --
 -- See Note [Undecidable Equality for PmAltCons]
@@ -118,6 +132,39 @@ pmAltConType :: PmAltCon -> [Type] -> Type
 pmAltConType (PmAltLit lit)     _arg_tys = ASSERT( null _arg_tys ) pmLitType lit
 pmAltConType (PmAltConLike con) arg_tys  = conLikeResTy con arg_tys
 
+instance Outputable PmLitValue where
+  ppr (PmLitInt i)        = ppr i
+  ppr (PmLitRat r)        = ppr (double (fromRat r)) -- good enough
+  ppr (PmLitChar c)       = pprHsChar c
+  ppr (PmLitString s)     = pprHsString s
+  ppr (PmLitOverInt n i)  = minuses n (ppr i)
+  ppr (PmLitOverRat n r)  = minuses n (ppr (double (fromRat r)))
+  ppr (PmLitOverString s) = pprHsString s
+
+-- Take care of negated literals
+minuses :: Int -> SDoc -> SDoc
+minuses n sdoc = iterate (\sdoc -> parens (char '-' <> sdoc)) sdoc !! n
+
+instance Outputable PmLit where
+  ppr (PmLit ty v) = ppr v <> suffix
+    where
+      -- Some ad-hoc hackery for displaying proper lit suffixes based on type
+      tbl = [ (intPrimTy, primIntSuffix)
+            , (int64PrimTy, primInt64Suffix)
+            , (wordPrimTy, primWordSuffix)
+            , (word64PrimTy, primWord64Suffix)
+            , (charPrimTy, primCharSuffix)
+            , (floatPrimTy, primFloatSuffix)
+            , (doublePrimTy, primDoubleSuffix) ]
+      suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl)
+
+instance Outputable PmAltCon where
+  ppr (PmAltConLike cl) = ppr cl
+  ppr (PmAltLit l)      = ppr l
+
+instance Outputable PmEquality where
+  ppr = text . show
+
 -- | Undecidable equality for values represented by 'ConLike's.
 -- See Note [Undecidable Equality for PmAltCons].
 -- 'PatSynCon's aren't enforced to be generative, so two syntactically different
@@ -265,12 +312,6 @@ pmLitAsStringLit :: PmLit -> Maybe FastString
 pmLitAsStringLit (PmLit _ (PmLitString s)) = Just s
 pmLitAsStringLit _                         = Nothing
 
--- ----------------------------------------------------------------------------
--- ** Predicates on PmExpr
-
--- -----------------------------------------------------------------------
--- ** Lift source expressions (HsExpr Id) to PmExpr
-
 coreExprAsPmLit :: CoreExpr -> Maybe PmLit
 -- coreExprAsPmLit e | pprTrace "coreExprAsPmLit" (ppr e) False = undefined
 coreExprAsPmLit (Tick _t e) = coreExprAsPmLit e
@@ -322,43 +363,167 @@ coreExprAsPmLit e = case collectArgs e of
       | otherwise
       = False
 
-{-
-%************************************************************************
-%*                                                                      *
-                            Pretty printing
-%*                                                                      *
-%************************************************************************
--}
-
-instance Outputable PmLitValue where
-  ppr (PmLitInt i)        = ppr i
-  ppr (PmLitRat r)        = ppr (double (fromRat r)) -- good enough
-  ppr (PmLitChar c)       = pprHsChar c
-  ppr (PmLitString s)     = pprHsString s
-  ppr (PmLitOverInt n i)  = minuses n (ppr i)
-  ppr (PmLitOverRat n r)  = minuses n (ppr (double (fromRat r)))
-  ppr (PmLitOverString s) = pprHsString s
-
--- Take care of negated literals
-minuses :: Int -> SDoc -> SDoc
-minuses n sdoc = iterate (\sdoc -> parens (char '-' <> sdoc)) sdoc !! n
+type ConLikeSet = UniqDSet ConLike
+
+-- | A data type caching the results of 'completeMatchConLikes' with support for
+-- deletion of contructors that were already matched on.
+data PossibleMatches
+  = PM TyCon (NonEmpty.NonEmpty ConLikeSet)
+  -- ^ Each ConLikeSet is a (subset of) the constructors in a COMPLETE pragma
+  -- 'NonEmpty' because the empty case would mean that the type has no COMPLETE
+  -- set at all, for which we have 'NoPM'
+  | NoPM
+  -- ^ No COMPLETE set for this type (yet). Think of overloaded literals.
+
+instance Outputable PossibleMatches where
+  ppr (PM _tc cs) = ppr (NonEmpty.toList cs)
+  ppr NoPM = text "<NoPM>"
+
+-- | Either @Indirect x@, meaning the value is represented by that of @x@, or
+-- an @Entry@ containing containing the actual value it represents.
+data Shared a
+  = Indirect Id
+  | Entry a
+
+-- | A 'DIdEnv' in which entries can be shared by multiple 'Id's.
+-- Merge equivalence classes of two Ids by 'setIndirectSDIE' and set the entry
+-- of an Id with 'setEntrySDIE'.
+newtype SharedDIdEnv a
+  = SDIE { unSDIE :: DIdEnv (Shared a) }
+
+emptySDIE :: SharedDIdEnv a
+emptySDIE = SDIE emptyDVarEnv
+
+lookupReprAndEntrySDIE :: SharedDIdEnv a -> Id -> (Id, Maybe a)
+lookupReprAndEntrySDIE sdie@(SDIE env) x = case lookupDVarEnv env x of
+  Nothing           -> (x, Nothing)
+  Just (Indirect y) -> lookupReprAndEntrySDIE sdie y
+  Just (Entry a)    -> (x, Just a)
+
+-- | @lookupSDIE env x@ looks up an entry for @x@, looking through all
+-- 'Indirect's until it finds a shared 'Entry'.
+lookupSDIE :: SharedDIdEnv a -> Id -> Maybe a
+lookupSDIE sdie x = snd (lookupReprAndEntrySDIE sdie x)
+
+-- | Check if two variables are part of the same equivalence class.
+sameRepresentativeSDIE :: SharedDIdEnv a -> Id -> Id -> Bool
+sameRepresentativeSDIE sdie x y =
+  fst (lookupReprAndEntrySDIE sdie x) == fst (lookupReprAndEntrySDIE sdie y)
+
+-- | @setIndirectSDIE env x y@ sets @x@'s 'Entry' to @Indirect y@, thereby
+-- merging @x@'s equivalence class into @y@'s. This will discard all info on
+-- @x@!
+setIndirectSDIE :: SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a
+setIndirectSDIE sdie@(SDIE env) x y =
+  SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Indirect y)
+
+-- | @setEntrySDIE env x a@ sets the 'Entry' @x@ is associated with to @a@,
+-- thereby modifying its whole equivalence class.
+setEntrySDIE :: SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
+setEntrySDIE sdie@(SDIE env) x a =
+  SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Entry a)
+
+traverseSDIE :: Applicative f => (a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b)
+traverseSDIE f = fmap (SDIE . listToUDFM) . traverse g . udfmToList . unSDIE
+  where
+    g (u, Indirect y) = pure (u,Indirect y)
+    g (u, Entry a)    = (u,) . Entry <$> f a
 
-instance Outputable PmLit where
-  ppr (PmLit ty v) = ppr v <> suffix
-    where
-      -- Some ad-hoc hackery for displaying proper lit suffixes based on type
-      tbl = [ (intPrimTy, primIntSuffix)
-            , (int64PrimTy, primInt64Suffix)
-            , (wordPrimTy, primWordSuffix)
-            , (word64PrimTy, primWord64Suffix)
-            , (charPrimTy, primCharSuffix)
-            , (floatPrimTy, primFloatSuffix)
-            , (doublePrimTy, primDoubleSuffix) ]
-      suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl)
+instance Outputable a => Outputable (Shared a) where
+  ppr (Indirect x) = ppr x
+  ppr (Entry a)    = ppr a
 
-instance Outputable PmAltCon where
-  ppr (PmAltConLike cl) = ppr cl
-  ppr (PmAltLit l)      = ppr l
+instance Outputable a => Outputable (SharedDIdEnv a) where
+  ppr (SDIE env) = ppr env
 
-instance Outputable PmEquality where
-  ppr = text . show
+-- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These
+-- entries are possibly shared when we figure out that two variables must be
+-- equal, thus represent the same set of values.
+--
+-- See Note [TmState invariants].
+newtype TmState = TS (SharedDIdEnv VarInfo)
+  -- Deterministic so that we generate deterministic error messages
+
+-- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
+-- and negative ('vi_neg') facts, like "x is not (:)".
+-- Also caches the type ('vi_ty'), the 'PossibleMatches' of a COMPLETE set
+-- ('vi_cache') and the number of times each variable was refined
+-- ('vi_n_refines').
+--
+-- Subject to Note [The Pos/Neg invariant].
+data VarInfo
+  = VI
+  { vi_ty  :: !Type
+  -- ^ The type of the variable. Important for rejecting possible GADT
+  -- constructors or incompatible pattern synonyms (@Just42 :: Maybe Int@).
+
+  , vi_pos :: [(PmAltCon, [Id])]
+  -- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all
+  -- at the same time (i.e. conjunctive).  We need a list because of nested
+  -- pattern matches involving pattern synonym
+  --    case x of { Just y -> case x of PatSyn z -> ... }
+  -- However, no more than one RealDataCon in the list, otherwise contradiction
+  -- because of generativity.
+
+  , vi_neg :: ![PmAltCon]
+  -- ^ Negative info: A list of 'PmAltCon's that it cannot match.
+  -- Example, assuming
+  --
+  -- @
+  --     data T = Leaf Int | Branch T T | Node Int T
+  -- @
+  --
+  -- then @x /~ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
+  -- and hence can only match @Branch@. Is orthogonal to anything from 'vi_pos',
+  -- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing
+  -- between 'vi_pos' and 'vi_neg'.
+
+  -- See Note [Why record both positive and negative info?]
+
+  , vi_cache :: !PossibleMatches
+  -- ^ A cache of the associated COMPLETE sets. At any time a superset of
+  -- possible constructors of each COMPLETE set. So, if it's not in here, we
+  -- can't possibly match on it. Complementary to 'vi_neg'. We still need it
+  -- to recognise completion of a COMPLETE set efficiently for large enums.
+
+  , vi_n_refines :: !Int
+  -- ^ Purely for Check performance reasons. The number of times this
+  -- representative was refined ('refineToAltCon') in the Check's ConVar split.
+  -- Sadly, we can't store this info in the Check module, as it's tightly coupled
+  -- to the particular 'Delta' and also is per *representative*, not per
+  -- syntactic variable. Note that this number does not always correspond to the
+  -- length of solutions: 'addVarConCt' might add a solution without
+  -- incurring the potential exponential blowup by ConVar.
+  }
+
+-- | Not user-facing.
+instance Outputable TmState where
+  ppr (TS state) = ppr state
+
+-- | Not user-facing.
+instance Outputable VarInfo where
+  ppr (VI ty pos neg cache n)
+    = braces (hcat (punctuate comma [ppr ty, ppr pos, ppr neg, ppr cache, ppr n]))
+
+-- | Initial state of the oracle.
+initTmState :: TmState
+initTmState = TS emptySDIE
+
+-- | Term and type constraints to accompany each value vector abstraction.
+-- For efficiency, we store the term oracle state instead of the term
+-- constraints.
+data Delta = MkDelta { delta_ty_cs :: Bag EvVar  -- Type oracle; things like a~Int
+                     , delta_tm_cs :: TmState }  -- Term oracle; things like x~Nothing
+
+-- | An initial delta that is always satisfiable
+initDelta :: Delta
+initDelta = MkDelta emptyBag initTmState
+
+instance Outputable Delta where
+  ppr delta = vcat [
+      -- intentionally formatted this way enable the dev to comment in only
+      -- the info she needs
+      ppr (delta_tm_cs delta),
+      ppr (pprEvVarWithType <$> delta_ty_cs delta)
+      --ppr (delta_ty_cs delta)
+    ]
diff --git a/compiler/deSugar/PmOracle.hs-boot b/compiler/deSugar/PmTypes.hs-boot
index e099fe78a6..f6e3a7ec5b 100644
--- a/compiler/deSugar/PmOracle.hs-boot
+++ b/compiler/deSugar/PmTypes.hs-boot
@@ -1,4 +1,4 @@
-module PmOracle where
+module PmTypes where
 
 import GhcPrelude ()
 
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index 884006b487..fc5f581a4d 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -334,9 +334,9 @@ Library
         CoreStats
         MkCore
         PprCore
-        PmExpr
-        PmPpr
         PmOracle
+        PmPpr
+        PmTypes
         Check
         Coverage
         Desugar
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 0a2db75a2d..05eb56d6f7 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -167,7 +167,7 @@ import TcType
 import Annotations
 import InstEnv
 import FamInstEnv
-import {-# SOURCE #-} PmOracle (Delta)
+import {-# SOURCE #-} PmTypes (Delta)
 import IOEnv
 import RdrName
 import Name