compiler: Introduce and use RoughMap for instance environmentswip/roughmap-mp

Here we introduce a new data structure, RoughMap, inspired by the
previous `RoughTc` matching mechanism for checking instance matches.
This allows [Fam]InstEnv to be implemented as a trie indexed by these
RoughTc signatures, reducing the complexity of instance lookup and
FamInstEnv merging (done during the family instance conflict test)
from O(n) to O(log n).

The critical performance improvement currently realised by this patch is
in instance matching. In particular the RoughMap mechanism allows us to
discount many potential instances which will never match for constraints
involving type variables (see Note [Matching a RoughMap]). In realistic
code bases matchInstEnv was accounting for 50% of typechecker time due
to redundant work checking instances when simplifying instance contexts
when deriving instances. With this patch the cost is significantly
reduced.

The larger constants in InstEnv creation do mean that a few small
tests regress in allocations slightly. However, the runtime of T19703 is
reduced by a factor of 4. Moreover, the compilation time of the Cabal
library is slightly improved.

A couple of test cases are included which demonstrate significant
improvements in compile time with this patch.

This unfortunately does not fix the testcase provided in #19703 but does
fix #20933

-------------------------
Metric Decrease:
    T12425
Metric Increase:
    T13719
    T9872a
    T9872d
    hard_hole_fits
-------------------------

Co-authored-by: Matthew Pickering <matthewtpickering@gmail.com>

6 files changed, 687 insertions, 203 deletions

diff --git a/compiler/GHC/Core/Coercion/Axiom.hs b/compiler/GHC/Core/Coercion/Axiom.hs
index 5db9f17161..2476cfd7cc 100644
--- a/compiler/GHC/Core/Coercion/Axiom.hs
+++ b/compiler/GHC/Core/Coercion/Axiom.hs
@@ -455,6 +455,7 @@ See also:
   type; but it too is eta-reduced.
 * Note [Implementing eta reduction for data families] in "GHC.Tc.TyCl.Instance". This
   describes the implementation details of this eta reduction happen.
+* Note [RoughMap and rm_empty] for how this complicates the RoughMap implementation slightly.
 -}
 
 instance Eq (CoAxiom br) where
diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs
index c0981ac9e1..78ed3a104c 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -15,7 +15,7 @@ module GHC.Core.FamInstEnv (
         mkImportedFamInst,
 
         FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs,
-        extendFamInstEnv, extendFamInstEnvList,
+        unionFamInstEnv, extendFamInstEnv, extendFamInstEnvList,
         famInstEnvElts, famInstEnvSize, familyInstances,
 
         -- * CoAxioms
@@ -46,10 +46,10 @@ import GHC.Core.TyCon
 import GHC.Core.Coercion
 import GHC.Core.Coercion.Axiom
 import GHC.Core.Reduction
+import GHC.Core.RoughMap
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
 import GHC.Types.Name
-import GHC.Types.Unique.DFM
 import GHC.Data.Maybe
 import GHC.Types.Var
 import GHC.Types.SrcLoc
@@ -61,6 +61,7 @@ import GHC.Utils.Misc
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
+import GHC.Data.Bag
 
 {-
 ************************************************************************
@@ -302,7 +303,17 @@ mkImportedFamInst fam mb_tcs axiom
 
 Note [FamInstEnv]
 ~~~~~~~~~~~~~~~~~
-A FamInstEnv maps a family name to the list of known instances for that family.
+A FamInstEnv is a RoughMap of instance heads. Specifically, the keys are formed
+by the family name and the instance arguments. That is, an instance:
+
+    type instance Fam (Maybe Int) a
+
+would insert into the instance environment an instance with a key of the form
+
+  [RM_KnownTc Fam, RM_KnownTc Maybe, RM_WildCard]
+
+See Note [RoughMap] in GHC.Core.RoughMap.
+
 
 The same FamInstEnv includes both 'data family' and 'type family' instances.
 Type families are reduced during type inference, but not data families;
@@ -350,30 +361,24 @@ UniqFM and UniqDFM.
 See Note [Deterministic UniqFM].
 -}
 
--- Internally we sometimes index by Name instead of TyCon despite
--- of what the type says. This is safe since
--- getUnique (tyCon) == getUniqe (tcName tyCon)
-type FamInstEnv = UniqDFM TyCon FamilyInstEnv  -- Maps a family to its instances
-     -- See Note [FamInstEnv]
-     -- See Note [FamInstEnv determinism]
-
 type FamInstEnvs = (FamInstEnv, FamInstEnv)
      -- External package inst-env, Home-package inst-env
 
-newtype FamilyInstEnv
-  = FamIE [FamInst]     -- The instances for a particular family, in any order
+data FamInstEnv
+  = FamIE !Int -- The number of instances, used to choose the smaller environment
+               -- when checking type family consistnecy of home modules.
+          !(RoughMap FamInst)
+     -- See Note [FamInstEnv]
+     -- See Note [FamInstEnv determinism]
 
-instance Outputable FamilyInstEnv where
-  ppr (FamIE fs) = text "FamIE" <+> vcat (map ppr fs)
 
--- | Index a FamInstEnv by the tyCons name.
-toNameInstEnv :: FamInstEnv -> UniqDFM Name FamilyInstEnv
-toNameInstEnv = unsafeCastUDFMKey
+instance Outputable FamInstEnv where
+  ppr (FamIE _ fs) = text "FamIE" <+> vcat (map ppr $ elemsRM fs)
 
--- | Create a FamInstEnv from Name indices.
-fromNameInstEnv :: UniqDFM Name FamilyInstEnv -> FamInstEnv
-fromNameInstEnv = unsafeCastUDFMKey
+famInstEnvSize :: FamInstEnv -> Int
+famInstEnvSize (FamIE sz _) = sz
 
+-- | Create a 'FamInstEnv' from 'Name' indices.
 -- INVARIANTS:
 --  * The fs_tvs are distinct in each FamInst
 --      of a range value of the map (so we can safely unify them)
@@ -382,14 +387,12 @@ emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
 
 emptyFamInstEnv :: FamInstEnv
-emptyFamInstEnv = emptyUDFM
+emptyFamInstEnv = FamIE 0 emptyRM
 
 famInstEnvElts :: FamInstEnv -> [FamInst]
-famInstEnvElts fi = [elt | FamIE elts <- eltsUDFM fi, elt <- elts]
+famInstEnvElts (FamIE _ rm) = elemsRM rm
   -- See Note [FamInstEnv determinism]
 
-famInstEnvSize :: FamInstEnv -> Int
-famInstEnvSize = nonDetStrictFoldUDFM (\(FamIE elt) sum -> sum + length elt) 0
   -- It's OK to use nonDetStrictFoldUDFM here since we're just computing the
   -- size.
 
@@ -397,19 +400,23 @@ familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
 familyInstances (pkg_fie, home_fie) fam
   = get home_fie ++ get pkg_fie
   where
-    get env = case lookupUDFM env fam of
-                Just (FamIE insts) -> insts
-                Nothing                      -> []
+    get :: FamInstEnv -> [FamInst]
+    get (FamIE _ env) = lookupRM [RML_KnownTc (tyConName fam)] env
+
+
+-- | Makes no particular effort to detect conflicts.
+unionFamInstEnv :: FamInstEnv -> FamInstEnv -> FamInstEnv
+unionFamInstEnv (FamIE sa a) (FamIE sb b) = FamIE (sa + sb) (a `unionRM` b)
 
 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
 extendFamInstEnvList inst_env fis = foldl' extendFamInstEnv inst_env fis
 
 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
-extendFamInstEnv inst_env
+extendFamInstEnv (FamIE s inst_env)
                  ins_item@(FamInst {fi_fam = cls_nm})
-  = fromNameInstEnv $ addToUDFM_C add (toNameInstEnv inst_env) cls_nm (FamIE [ins_item])
+  = FamIE (s+1) $ insertRM rough_tmpl ins_item inst_env
   where
-    add (FamIE items) _ = FamIE (ins_item:items)
+    rough_tmpl = RM_KnownTc cls_nm : fi_tcs ins_item
 
 {-
 ************************************************************************
@@ -774,9 +781,7 @@ lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst]
 lookupFamInstEnvByTyCon (pkg_ie, home_ie) fam_tc
   = get pkg_ie ++ get home_ie
   where
-    get ie = case lookupUDFM ie fam_tc of
-               Nothing          -> []
-               Just (FamIE fis) -> fis
+    get (FamIE _ rm) = lookupRM [RML_KnownTc (tyConName fam_tc)] rm
 
 lookupFamInstEnv
     :: FamInstEnvs
@@ -785,14 +790,12 @@ lookupFamInstEnv
 -- Precondition: the tycon is saturated (or over-saturated)
 
 lookupFamInstEnv
-   = lookup_fam_inst_env match
-   where
-     match _ _ tpl_tys tys = tcMatchTys tpl_tys tys
+   = lookup_fam_inst_env WantMatches
 
 lookupFamInstEnvConflicts
     :: FamInstEnvs
     -> FamInst          -- Putative new instance
-    -> [FamInstMatch]   -- Conflicting matches (don't look at the fim_tys field)
+    -> [FamInst]   -- Conflicting matches (don't look at the fim_tys field)
 -- E.g. when we are about to add
 --    f : type instance F [a] = a->a
 -- we do (lookupFamInstConflicts f [b])
@@ -800,25 +803,10 @@ lookupFamInstEnvConflicts
 --
 -- Precondition: the tycon is saturated (or over-saturated)
 
-lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom })
-  = lookup_fam_inst_env my_unify envs fam tys
+lookupFamInstEnvConflicts envs fam_inst
+  = lookup_fam_inst_env (WantConflicts fam_inst) envs fam tys
   where
     (fam, tys) = famInstSplitLHS fam_inst
-        -- In example above,   fam tys' = F [b]
-
-    my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _
-       = assertPpr (tyCoVarsOfTypes tys `disjointVarSet` tpl_tvs)
-                   ((ppr fam <+> ppr tys) $$
-                    (ppr tpl_tvs <+> ppr tpl_tys)) $
-                -- Unification will break badly if the variables overlap
-                -- They shouldn't because we allocate separate uniques for them
-         if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch
-           then Nothing
-           else Just noSubst
-      -- See Note [Family instance overlap conflicts]
-
-    noSubst = panic "lookupFamInstEnvConflicts noSubst"
-    new_branch = coAxiomSingleBranch new_axiom
 
 --------------------------------------------------------------------------------
 --                 Type family injectivity checking bits                      --
@@ -927,11 +915,17 @@ lookupFamInstEnvInjectivityConflicts
     ->  FamInstEnvs   -- all type instances seens so far
     ->  FamInst       -- new type instance that we're checking
     -> [CoAxBranch]   -- conflicting instance declarations
-lookupFamInstEnvInjectivityConflicts injList (pkg_ie, home_ie)
+lookupFamInstEnvInjectivityConflicts injList fam_inst_envs
                              fam_inst@(FamInst { fi_axiom = new_axiom })
+  | not $ isOpenFamilyTyCon fam
+  = []
+
+  | otherwise
   -- See Note [Verifying injectivity annotation]. This function implements
   -- check (1.B1) for open type families described there.
-  = lookup_inj_fam_conflicts home_ie ++ lookup_inj_fam_conflicts pkg_ie
+  = map (coAxiomSingleBranch . fi_axiom) $
+    filter isInjConflict $
+    familyInstances fam_inst_envs fam
     where
       fam        = famInstTyCon fam_inst
       new_branch = coAxiomSingleBranch new_axiom
@@ -944,12 +938,6 @@ lookupFamInstEnvInjectivityConflicts injList (pkg_ie, home_ie)
           = False -- no conflict
           | otherwise = True
 
-      lookup_inj_fam_conflicts ie
-          | isOpenFamilyTyCon fam, Just (FamIE insts) <- lookupUDFM ie fam
-          = map (coAxiomSingleBranch . fi_axiom) $
-            filter isInjConflict insts
-          | otherwise = []
-
 
 --------------------------------------------------------------------------------
 --                    Type family overlap checking bits                       --
@@ -973,46 +961,61 @@ Note [Family instance overlap conflicts]
 
 ------------------------------------------------------------
 -- Might be a one-way match or a unifier
-type MatchFun =  FamInst                -- The FamInst template
-              -> TyVarSet -> [Type]     --   fi_tvs, fi_tys of that FamInst
-              -> [Type]                 -- Target to match against
-              -> Maybe TCvSubst
+data FamInstLookupMode a where
+  -- The FamInst we are trying to find conflicts against
+  WantConflicts :: FamInst -> FamInstLookupMode FamInst
+  WantMatches  :: FamInstLookupMode FamInstMatch
 
 lookup_fam_inst_env'          -- The worker, local to this module
-    :: MatchFun
+    :: forall a . FamInstLookupMode a
     -> FamInstEnv
     -> TyCon -> [Type]        -- What we are looking for
-    -> [FamInstMatch]
-lookup_fam_inst_env' match_fun ie fam match_tys
+    -> [a]
+lookup_fam_inst_env' lookup_mode (FamIE _ ie) fam match_tys
   | isOpenFamilyTyCon fam
-  , Just (FamIE insts) <- lookupUDFM ie fam
-  = find insts    -- The common case
+  , let xs = rm_fun (lookupRM' rough_tmpl ie)   -- The common case
+    -- Avoid doing any of the allocation below if there are no instances to look at.
+  , not $ null xs
+  = mapMaybe' check_fun xs
   | otherwise = []
   where
+    rough_tmpl :: [RoughMatchLookupTc]
+    rough_tmpl = RML_KnownTc (tyConName fam) : map typeToRoughMatchLookupTc match_tys
 
-    find [] = []
-    find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, fi_cvs = tpl_cvs
-                        , fi_tys = tpl_tys }) : rest)
-        -- Fast check for no match, uses the "rough match" fields
-      | instanceCantMatch rough_tcs mb_tcs
-      = find rest
-
-        -- Proper check
-      | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1
-      = (FamInstMatch { fim_instance = item
-                      , fim_tys      = substTyVars subst tpl_tvs `chkAppend` match_tys2
-                      , fim_cos      = assert (all (isJust . lookupCoVar subst) tpl_cvs) $
-                                       substCoVars subst tpl_cvs
-                      })
-        : find rest
-
-        -- No match => try next
-      | otherwise
-      = find rest
-      where
-        (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys
+    rm_fun :: (Bag FamInst, [FamInst]) -> [FamInst]
+    (rm_fun, check_fun) = case lookup_mode of
+                            WantConflicts fam_inst -> (snd, unify_fun fam_inst)
+                            WantMatches -> (bagToList . fst, match_fun)
 
-      -- Precondition: the tycon is saturated (or over-saturated)
+    -- Function used for finding unifiers
+    unify_fun orig_fam_inst item@(FamInst { fi_axiom = old_axiom, fi_tys = tpl_tys, fi_tvs = tpl_tvs })
+
+       = assertPpr (tyCoVarsOfTypes tys `disjointVarSet` mkVarSet tpl_tvs)
+                   ((ppr fam <+> ppr tys) $$
+                    (ppr tpl_tvs <+> ppr tpl_tys)) $
+                -- Unification will break badly if the variables overlap
+                -- They shouldn't because we allocate separate uniques for them
+         if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch
+           then Nothing
+           else Just item
+      -- See Note [Family instance overlap conflicts]
+      where
+        new_branch = coAxiomSingleBranch (famInstAxiom orig_fam_inst)
+        (fam, tys) = famInstSplitLHS orig_fam_inst
+
+    -- Function used for checking matches
+    match_fun item@(FamInst { fi_tvs = tpl_tvs, fi_cvs = tpl_cvs
+                            , fi_tys = tpl_tys }) =  do
+      subst <- tcMatchTys tpl_tys match_tys1
+      return (FamInstMatch { fim_instance = item
+                             , fim_tys      = substTyVars subst tpl_tvs `chkAppend` match_tys2
+                             , fim_cos      = assert (all (isJust . lookupCoVar subst) tpl_cvs) $
+                                               substCoVars subst tpl_cvs
+                             })
+        where
+          (match_tys1, match_tys2) = split_tys tpl_tys
+
+    -- Precondition: the tycon is saturated (or over-saturated)
 
     -- Deal with over-saturation
     -- See Note [Over-saturated matches]
@@ -1022,18 +1025,17 @@ lookup_fam_inst_env' match_fun ie fam match_tys
 
       | otherwise
       = let (match_tys1, match_tys2) = splitAtList tpl_tys match_tys
-            rough_tcs = roughMatchTcs match_tys1
-        in (rough_tcs, match_tys1, match_tys2)
+        in (match_tys1, match_tys2)
 
     (pre_match_tys1, pre_match_tys2) = splitAt (tyConArity fam) match_tys
     pre_rough_split_tys
-      = (roughMatchTcs pre_match_tys1, pre_match_tys1, pre_match_tys2)
+      = (pre_match_tys1, pre_match_tys2)
 
 lookup_fam_inst_env           -- The worker, local to this module
-    :: MatchFun
+    :: FamInstLookupMode a
     -> FamInstEnvs
     -> TyCon -> [Type]        -- What we are looking for
-    -> [FamInstMatch]         -- Successful matches
+    -> [a]         -- Successful matches
 
 -- Precondition: the tycon is saturated (or over-saturated)
 
diff --git a/compiler/GHC/Core/InstEnv.hs b/compiler/GHC/Core/InstEnv.hs
index ab23fcae2c..e223a7cd87 100644
--- a/compiler/GHC/Core/InstEnv.hs
+++ b/compiler/GHC/Core/InstEnv.hs
@@ -11,17 +11,19 @@ The bits common to GHC.Tc.TyCl.Instance and GHC.Tc.Deriv.
 
 module GHC.Core.InstEnv (
         DFunId, InstMatch, ClsInstLookupResult,
+        PotentialUnifiers(..), getPotentialUnifiers, nullUnifiers,
         OverlapFlag(..), OverlapMode(..), setOverlapModeMaybe,
         ClsInst(..), DFunInstType, pprInstance, pprInstanceHdr, pprInstances,
         instanceHead, instanceSig, mkLocalInstance, mkImportedInstance,
-        instanceDFunId, updateClsInstDFun, instanceRoughTcs,
+        instanceDFunId, updateClsInstDFuns, updateClsInstDFun,
         fuzzyClsInstCmp, orphNamesOfClsInst,
 
         InstEnvs(..), VisibleOrphanModules, InstEnv,
-        emptyInstEnv, extendInstEnv,
-        deleteFromInstEnv, deleteDFunFromInstEnv,
+        mkInstEnv, emptyInstEnv, unionInstEnv, extendInstEnv,
+        filterInstEnv, deleteFromInstEnv, deleteDFunFromInstEnv,
+        anyInstEnv,
         identicalClsInstHead,
-        extendInstEnvList, lookupUniqueInstEnv, lookupInstEnv, instEnvElts, instEnvClasses,
+        extendInstEnvList, lookupUniqueInstEnv, lookupInstEnv, instEnvElts, instEnvClasses, mapInstEnv,
         memberInstEnv,
         instIsVisible,
         classInstances, instanceBindFun,
@@ -34,25 +36,25 @@ import GHC.Prelude
 import GHC.Tc.Utils.TcType -- InstEnv is really part of the type checker,
               -- and depends on TcType in many ways
 import GHC.Core ( IsOrphan(..), isOrphan, chooseOrphanAnchor )
+import GHC.Core.RoughMap
 import GHC.Unit.Module.Env
 import GHC.Unit.Types
 import GHC.Core.Class
 import GHC.Types.Var
+import GHC.Types.Unique.DSet
 import GHC.Types.Var.Set
 import GHC.Types.Name
 import GHC.Types.Name.Set
-import GHC.Types.Unique (getUnique)
 import GHC.Core.Unify
 import GHC.Types.Basic
-import GHC.Types.Unique.DFM
 import GHC.Types.Id
 import Data.Data        ( Data )
 import Data.Maybe       ( isJust )
 
-import GHC.Utils.Misc
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
+import Data.Semigroup
 
 {-
 ************************************************************************
@@ -68,9 +70,12 @@ import GHC.Utils.Panic.Plain
 data ClsInst
   = ClsInst {   -- Used for "rough matching"; see
                 -- Note [ClsInst laziness and the rough-match fields]
-                -- INVARIANT: is_tcs = roughMatchTcs is_tys
+                -- INVARIANT: is_tcs = KnownTc is_cls_nm : roughMatchTcs is_tys
                is_cls_nm :: Name          -- ^ Class name
+
              , is_tcs  :: [RoughMatchTc]  -- ^ Top of type args
+                          -- The class itself is always
+                          -- the first element of this list
 
                -- | @is_dfun_name = idName . is_dfun@.
                --
@@ -103,13 +108,12 @@ data ClsInst
 -- instances before displaying them to the user.
 fuzzyClsInstCmp :: ClsInst -> ClsInst -> Ordering
 fuzzyClsInstCmp x y =
-    stableNameCmp (is_cls_nm x) (is_cls_nm y) `mappend`
-    mconcat (map cmp (zip (is_tcs x) (is_tcs y)))
+    foldMap cmp (zip (is_tcs x) (is_tcs y))
   where
-    cmp (OtherTc,   OtherTc)   = EQ
-    cmp (OtherTc,   KnownTc _) = LT
-    cmp (KnownTc _, OtherTc)   = GT
-    cmp (KnownTc x, KnownTc y) = stableNameCmp x y
+    cmp (RM_WildCard,  RM_WildCard)   = EQ
+    cmp (RM_WildCard,  RM_KnownTc _) = LT
+    cmp (RM_KnownTc _, RM_WildCard)   = GT
+    cmp (RM_KnownTc x, RM_KnownTc y) = stableNameCmp x y
 
 isOverlappable, isOverlapping, isIncoherent :: ClsInst -> Bool
 isOverlappable i = hasOverlappableFlag (overlapMode (is_flag i))
@@ -196,8 +200,9 @@ updateClsInstDFun :: (DFunId -> DFunId) -> ClsInst -> ClsInst
 updateClsInstDFun tidy_dfun ispec
   = ispec { is_dfun = tidy_dfun (is_dfun ispec) }
 
-instanceRoughTcs :: ClsInst -> [RoughMatchTc]
-instanceRoughTcs = is_tcs
+updateClsInstDFuns :: (DFunId -> DFunId) -> InstEnv -> InstEnv
+updateClsInstDFuns tidy_dfun (InstEnv rm)
+  = InstEnv $ fmap (updateClsInstDFun tidy_dfun) rm
 
 instance NamedThing ClsInst where
    getName ispec = getName (is_dfun ispec)
@@ -259,7 +264,7 @@ mkLocalInstance dfun oflag tvs cls tys
             , is_tvs = tvs
             , is_dfun_name = dfun_name
             , is_cls = cls, is_cls_nm = cls_name
-            , is_tys = tys, is_tcs = roughMatchTcs tys
+            , is_tys = tys, is_tcs = RM_KnownTc cls_name : roughMatchTcs tys
             , is_orphan = orph
             }
   where
@@ -290,7 +295,7 @@ mkLocalInstance dfun oflag tvs cls tys
     choose_one nss = chooseOrphanAnchor (unionNameSets nss)
 
 mkImportedInstance :: Name           -- ^ the name of the class
-                   -> [RoughMatchTc] -- ^ the types which the class was applied to
+                   -> [RoughMatchTc] -- ^ the rough match signature of the instance
                    -> Name           -- ^ the 'Name' of the dictionary binding
                    -> DFunId         -- ^ the 'Id' of the dictionary.
                    -> OverlapFlag    -- ^ may this instance overlap?
@@ -304,7 +309,8 @@ mkImportedInstance cls_nm mb_tcs dfun_name dfun oflag orphan
   = ClsInst { is_flag = oflag, is_dfun = dfun
             , is_tvs = tvs, is_tys = tys
             , is_dfun_name = dfun_name
-            , is_cls_nm = cls_nm, is_cls = cls, is_tcs = mb_tcs
+            , is_cls_nm = cls_nm, is_cls = cls
+            , is_tcs = RM_KnownTc cls_nm : mb_tcs
             , is_orphan = orphan }
   where
     (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun)
@@ -386,9 +392,12 @@ UniqDFM. See also Note [Deterministic UniqFM]
 -- We still use Class as key type as it's both the common case
 -- and conveys the meaning better. But the implementation of
 --InstEnv is a bit more lax internally.
-type InstEnv = UniqDFM Class ClsInstEnv      -- Maps Class to instances for that class
+newtype InstEnv = InstEnv (RoughMap ClsInst)      -- Maps Class to instances for that class
   -- See Note [InstEnv determinism]
 
+instance Outputable InstEnv where
+  ppr (InstEnv rm) = pprInstances $ elemsRM rm
+
 -- | 'InstEnvs' represents the combination of the global type class instance
 -- environment, the local type class instance environment, and the set of
 -- transitively reachable orphan modules (according to what modules have been
@@ -406,30 +415,32 @@ data InstEnvs = InstEnvs {
 -- transitively reachable orphan modules (modules that define orphan instances).
 type VisibleOrphanModules = ModuleSet
 
-newtype ClsInstEnv
-  = ClsIE [ClsInst]    -- The instances for a particular class, in any order
-
-instance Outputable ClsInstEnv where
-  ppr (ClsIE is) = pprInstances is
 
 -- INVARIANTS:
 --  * The is_tvs are distinct in each ClsInst
 --      of a ClsInstEnv (so we can safely unify them)
 
--- Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
+-- Thus, the @ClsInstEnv@ for @Eq@ might contain the following entry:
 --      [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
 -- The "a" in the pattern must be one of the forall'd variables in
 -- the dfun type.
 
 emptyInstEnv :: InstEnv
-emptyInstEnv = emptyUDFM
+emptyInstEnv = InstEnv emptyRM
+
+mkInstEnv :: [ClsInst] -> InstEnv
+mkInstEnv = extendInstEnvList emptyInstEnv
 
 instEnvElts :: InstEnv -> [ClsInst]
-instEnvElts ie = [elt | ClsIE elts <- eltsUDFM ie, elt <- elts]
+instEnvElts (InstEnv rm) = elemsRM rm
   -- See Note [InstEnv determinism]
 
-instEnvClasses :: InstEnv -> [Class]
-instEnvClasses ie = [is_cls e | ClsIE (e : _) <- eltsUDFM ie]
+instEnvEltsForClass :: InstEnv -> Class -> [ClsInst]
+instEnvEltsForClass (InstEnv rm) cls = lookupRM [RML_KnownTc (className cls)] rm
+
+-- N.B. this is not particularly efficient but used only by GHCi.
+instEnvClasses :: InstEnv -> UniqDSet Class
+instEnvClasses ie = mkUniqDSet $ map is_cls (instEnvElts ie)
 
 -- | Test if an instance is visible, by checking that its origin module
 -- is in 'VisibleOrphanModules'.
@@ -449,42 +460,50 @@ classInstances :: InstEnvs -> Class -> [ClsInst]
 classInstances (InstEnvs { ie_global = pkg_ie, ie_local = home_ie, ie_visible = vis_mods }) cls
   = get home_ie ++ get pkg_ie
   where
-    get env = case lookupUDFM env cls of
-                Just (ClsIE insts) -> filter (instIsVisible vis_mods) insts
-                Nothing            -> []
+    get :: InstEnv -> [ClsInst]
+    get ie = filter (instIsVisible vis_mods) (instEnvEltsForClass ie cls)
 
 -- | Checks for an exact match of ClsInst in the instance environment.
 -- We use this when we do signature checking in "GHC.Tc.Module"
 memberInstEnv :: InstEnv -> ClsInst -> Bool
-memberInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm } ) =
-    maybe False (\(ClsIE items) -> any (identicalDFunType ins_item) items)
-          (lookupUDFM_Directly inst_env (getUnique cls_nm))
+memberInstEnv (InstEnv rm) ins_item@(ClsInst { is_tcs = tcs } ) =
+    any (identicalDFunType ins_item) (fst $ lookupRM' (map roughMatchTcToLookup tcs) rm)
  where
   identicalDFunType cls1 cls2 =
     eqType (varType (is_dfun cls1)) (varType (is_dfun cls2))
 
+-- | Makes no particular effort to detect conflicts.
+unionInstEnv :: InstEnv -> InstEnv -> InstEnv
+unionInstEnv (InstEnv a) (InstEnv b) = InstEnv (a `unionRM` b)
+
 extendInstEnvList :: InstEnv -> [ClsInst] -> InstEnv
 extendInstEnvList inst_env ispecs = foldl' extendInstEnv inst_env ispecs
 
 extendInstEnv :: InstEnv -> ClsInst -> InstEnv
-extendInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm })
-  = addToUDFM_C_Directly add inst_env (getUnique cls_nm) (ClsIE [ins_item])
-  where
-    add (ClsIE cur_insts) _ = ClsIE (ins_item : cur_insts)
+extendInstEnv (InstEnv rm) ins_item@(ClsInst { is_tcs = tcs })
+  = InstEnv $ insertRM tcs ins_item rm
+
+filterInstEnv :: (ClsInst -> Bool) -> InstEnv -> InstEnv
+filterInstEnv pred (InstEnv rm)
+  = InstEnv $ filterRM pred rm
+
+anyInstEnv :: (ClsInst -> Bool) -> InstEnv -> Bool
+anyInstEnv pred (InstEnv rm)
+  = foldRM (\x rest -> pred x || rest) False rm
+
+mapInstEnv :: (ClsInst -> ClsInst) -> InstEnv -> InstEnv
+mapInstEnv f (InstEnv rm) = InstEnv (f <$> rm)
 
 deleteFromInstEnv :: InstEnv -> ClsInst -> InstEnv
-deleteFromInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm })
-  = adjustUDFM_Directly adjust inst_env (getUnique cls_nm)
-  where
-    adjust (ClsIE items) = ClsIE (filterOut (identicalClsInstHead ins_item) items)
+deleteFromInstEnv (InstEnv rm) ins_item@(ClsInst { is_tcs = tcs })
+  = InstEnv $ filterMatchingRM (not . identicalClsInstHead ins_item) tcs rm
 
 deleteDFunFromInstEnv :: InstEnv -> DFunId -> InstEnv
 -- Delete a specific instance fron an InstEnv
-deleteDFunFromInstEnv inst_env dfun
-  = adjustUDFM adjust inst_env cls
+deleteDFunFromInstEnv (InstEnv rm) dfun
+  = InstEnv $ filterMatchingRM (not . same_dfun) [RM_KnownTc (className cls)] rm
   where
     (_, _, cls, _) = tcSplitDFunTy (idType dfun)
-    adjust (ClsIE items) = ClsIE (filterOut same_dfun items)
     same_dfun (ClsInst { is_dfun = dfun' }) = dfun == dfun'
 
 identicalClsInstHead :: ClsInst -> ClsInst -> Bool
@@ -492,10 +511,10 @@ identicalClsInstHead :: ClsInst -> ClsInst -> Bool
 -- e.g.  both are   Eq [(a,b)]
 -- Used for overriding in GHCi
 -- Obviously should be insensitive to alpha-renaming
-identicalClsInstHead (ClsInst { is_cls_nm = cls_nm1, is_tcs = rough1, is_tys = tys1 })
-                     (ClsInst { is_cls_nm = cls_nm2, is_tcs = rough2, is_tys = tys2 })
-  =  cls_nm1 == cls_nm2
-  && not (instanceCantMatch rough1 rough2)  -- Fast check for no match, uses the "rough match" fields
+identicalClsInstHead (ClsInst { is_tcs = rough1, is_tys = tys1 })
+                     (ClsInst { is_tcs = rough2, is_tys = tys2 })
+  =  not (instanceCantMatch rough1 rough2)  -- Fast check for no match, uses the "rough match" fields;
+                                            -- also accounts for class name.
   && isJust (tcMatchTys tys1 tys2)
   && isJust (tcMatchTys tys2 tys1)
 
@@ -730,7 +749,7 @@ type InstMatch = (ClsInst, [DFunInstType])
 
 type ClsInstLookupResult
      = ( [InstMatch]     -- Successful matches
-       , [ClsInst]       -- These don't match but do unify
+       , PotentialUnifiers  -- These don't match but do unify
        , [InstMatch] )   -- Unsafe overlapped instances under Safe Haskell
                          -- (see Note [Safe Haskell Overlapping Instances] in
                          -- GHC.Tc.Solver).
@@ -811,11 +830,38 @@ lookupUniqueInstEnv instEnv cls tys
       _other -> Left $ text "instance not found" <+>
                        (ppr $ mkTyConApp (classTyCon cls) tys)
 
+data PotentialUnifiers = NoUnifiers
+                       | OneOrMoreUnifiers [ClsInst]
+                       -- This list is lazy as we only look at all the unifiers when
+                       -- printing an error message. It can be expensive to compute all
+                       -- the unifiers because if you are matching something like C a[sk] then
+                       -- all instances will unify.
+
+instance Outputable PotentialUnifiers where
+  ppr NoUnifiers = text "NoUnifiers"
+  ppr xs = ppr (getPotentialUnifiers xs)
+
+instance Semigroup PotentialUnifiers where
+  NoUnifiers <> u = u
+  u <> NoUnifiers = u
+  u1 <> u2 = OneOrMoreUnifiers (getPotentialUnifiers u1 ++ getPotentialUnifiers u2)
+
+instance Monoid PotentialUnifiers where
+  mempty = NoUnifiers
+
+getPotentialUnifiers :: PotentialUnifiers -> [ClsInst]
+getPotentialUnifiers NoUnifiers = []
+getPotentialUnifiers (OneOrMoreUnifiers cls) = cls
+
+nullUnifiers :: PotentialUnifiers -> Bool
+nullUnifiers NoUnifiers = True
+nullUnifiers _ = False
+
 lookupInstEnv' :: InstEnv          -- InstEnv to look in
                -> VisibleOrphanModules   -- But filter against this
                -> Class -> [Type]  -- What we are looking for
                -> ([InstMatch],    -- Successful matches
-                   [ClsInst])      -- These don't match but do unify
+                   PotentialUnifiers)      -- These don't match but do unify
                                    -- (no incoherent ones in here)
 -- The second component of the result pair happens when we look up
 --      Foo [a]
@@ -827,35 +873,35 @@ lookupInstEnv' :: InstEnv          -- InstEnv to look in
 -- but Foo [Int] is a unifier.  This gives the caller a better chance of
 -- giving a suitable error message
 
-lookupInstEnv' ie vis_mods cls tys
-  = lookup ie
+lookupInstEnv' (InstEnv rm) vis_mods cls tys
+  = (foldr check_match [] rough_matches, check_unifier rough_unifiers)
   where
-    rough_tcs  = roughMatchTcs tys
-
-    --------------
-    lookup env = case lookupUDFM env cls of
-                   Nothing -> ([],[])   -- No instances for this class
-                   Just (ClsIE insts) -> find [] [] insts
+    (rough_matches, rough_unifiers) = lookupRM' rough_tcs rm
+    rough_tcs  = RML_KnownTc (className cls) : roughMatchTcsLookup tys
 
     --------------
-    find ms us [] = (ms, us)
-    find ms us (item@(ClsInst { is_tcs = mb_tcs, is_tvs = tpl_tvs
-                              , is_tys = tpl_tys }) : rest)
+    check_match :: ClsInst -> [InstMatch] -> [InstMatch]
+    check_match item@(ClsInst { is_tvs = tpl_tvs, is_tys = tpl_tys }) acc
       | not (instIsVisible vis_mods item)
-      = find ms us rest  -- See Note [Instance lookup and orphan instances]
-
-        -- Fast check for no match, uses the "rough match" fields
-      | instanceCantMatch rough_tcs mb_tcs
-      = find ms us rest
+      = acc  -- See Note [Instance lookup and orphan instances]
 
       | Just subst <- tcMatchTys tpl_tys tys
-      = find ((item, map (lookupTyVar subst) tpl_tvs) : ms) us rest
+      = ((item, map (lookupTyVar subst) tpl_tvs) : acc)
+      | otherwise
+      = acc
 
+
+    check_unifier :: [ClsInst] -> PotentialUnifiers
+    check_unifier [] = NoUnifiers
+    check_unifier (item@ClsInst { is_tvs = tpl_tvs, is_tys = tpl_tys }:items)
+      | not (instIsVisible vis_mods item)
+      = check_unifier items  -- See Note [Instance lookup and orphan instances]
+      | Just {} <- tcMatchTys tpl_tys tys = check_unifier items
         -- Does not match, so next check whether the things unify
         -- See Note [Overlapping instances]
         -- Ignore ones that are incoherent: Note [Incoherent instances]
       | isIncoherent item
-      = find ms us rest
+      = check_unifier items
 
       | otherwise
       = assertPpr (tys_tv_set `disjointVarSet` tpl_tv_set)
@@ -868,10 +914,12 @@ lookupInstEnv' ie vis_mods cls tys
           -- We consider MaybeApart to be a case where the instance might
           -- apply in the future. This covers an instance like C Int and
           -- a target like [W] C (F a), where F is a type family.
-            SurelyApart              -> find ms us        rest
+            SurelyApart              -> check_unifier items
               -- See Note [Infinitary substitution in lookup]
-            MaybeApart MARInfinite _ -> find ms us        rest
-            _                        -> find ms (item:us) rest
+            MaybeApart MARInfinite _ -> check_unifier items
+            _                        ->
+              OneOrMoreUnifiers (item: getPotentialUnifiers (check_unifier items))
+
       where
         tpl_tv_set = mkVarSet tpl_tvs
         tys_tv_set = tyCoVarsOfTypes tys
@@ -891,13 +939,12 @@ lookupInstEnv check_overlap_safe
                         , ie_visible = vis_mods })
               cls
               tys
-  = -- pprTrace "lookupInstEnv" (ppr cls <+> ppr tys $$ ppr home_ie) $
-    (final_matches, final_unifs, unsafe_overlapped)
+  = (final_matches, final_unifs, unsafe_overlapped)
   where
     (home_matches, home_unifs) = lookupInstEnv' home_ie vis_mods cls tys
     (pkg_matches,  pkg_unifs)  = lookupInstEnv' pkg_ie  vis_mods cls tys
     all_matches = home_matches ++ pkg_matches
-    all_unifs   = home_unifs   ++ pkg_unifs
+    all_unifs   = home_unifs   `mappend` pkg_unifs
     final_matches = pruneOverlappedMatches all_matches
         -- Even if the unifs is non-empty (an error situation)
         -- we still prune the matches, so that the error message isn't
@@ -911,7 +958,7 @@ lookupInstEnv check_overlap_safe
 
     -- If the selected match is incoherent, discard all unifiers
     final_unifs = case final_matches of
-                    (m:_) | isIncoherent (fst m) -> []
+                    (m:_) | isIncoherent (fst m) -> NoUnifiers
                     _                            -> all_unifs
 
     -- NOTE [Safe Haskell isSafeOverlap]
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index ec9b024fc5..c79ce8be1d 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -52,7 +52,7 @@ import GHC.Core.TyCo.Ppr ( pprTyVar, pprTyVars )
 import GHC.Core.TyCon as TyCon
 import GHC.Core.Coercion.Axiom
 import GHC.Core.Unify
-import GHC.Core.InstEnv      ( instanceDFunId )
+import GHC.Core.InstEnv      ( instanceDFunId, instEnvElts )
 import GHC.Core.Coercion.Opt ( checkAxInstCo )
 import GHC.Core.Opt.Arity    ( typeArity )
 
@@ -448,7 +448,7 @@ interactiveInScope ictxt
     -- C.f. GHC.Tc.Module.setInteractiveContext, Desugar.deSugarExpr
     (cls_insts, _fam_insts) = ic_instances ictxt
     te1    = mkTypeEnvWithImplicits (ic_tythings ictxt)
-    te     = extendTypeEnvWithIds te1 (map instanceDFunId cls_insts)
+    te     = extendTypeEnvWithIds te1 (map instanceDFunId $ instEnvElts cls_insts)
     ids    = typeEnvIds te
     tyvars = tyCoVarsOfTypesList $ map idType ids
               -- Why the type variables?  How can the top level envt have free tyvars?
diff --git a/compiler/GHC/Core/RoughMap.hs b/compiler/GHC/Core/RoughMap.hs
new file mode 100644
index 0000000000..cc64e96149
--- /dev/null
+++ b/compiler/GHC/Core/RoughMap.hs
@@ -0,0 +1,451 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE BangPatterns #-}
+
+-- | 'RoughMap' is an approximate finite map data structure keyed on
+-- @['RoughMatchTc']@. This is useful when keying maps on lists of 'Type's
+-- (e.g. an instance head).
+module GHC.Core.RoughMap
+  ( -- * RoughMatchTc
+    RoughMatchTc(..)
+  , isRoughWildcard
+  , typeToRoughMatchTc
+  , RoughMatchLookupTc(..)
+  , typeToRoughMatchLookupTc
+  , roughMatchTcToLookup
+
+    -- * RoughMap
+  , RoughMap
+  , emptyRM
+  , lookupRM
+  , lookupRM'
+  , insertRM
+  , filterRM
+  , filterMatchingRM
+  , elemsRM
+  , sizeRM
+  , foldRM
+  , unionRM
+  ) where
+
+import GHC.Prelude
+
+import GHC.Data.Bag
+import GHC.Core.TyCon
+import GHC.Core.TyCo.Rep
+import GHC.Core.Type
+import GHC.Utils.Outputable
+import GHC.Types.Name
+import GHC.Types.Name.Env
+
+import Control.Monad (join)
+import Data.Data (Data)
+import GHC.Utils.Misc
+import Data.Bifunctor
+import GHC.Utils.Panic
+
+{-
+Note [RoughMap]
+~~~~~~~~~~~~~~~
+We often want to compute whether one type matches another. That is, given
+`ty1` and `ty2`, we want to know whether `ty1` is a substitution instance of `ty2`.
+
+We can bail out early by taking advantage of the following observation:
+
+  If `ty2` is headed by a generative type constructor, say `tc`,
+  but `ty1` is not headed by that same type constructor,
+  then `ty1` does not match `ty2`.
+
+The idea is that we can use a `RoughMap` as a pre-filter, to produce a
+short-list of candidates to examine more closely.
+
+This means we can avoid computing a full substitution if we represent types
+as applications of known generative type constructors. So, after type synonym
+expansion, we classify application heads into two categories ('RoughMatchTc')
+
+  - `RM_KnownTc tc`: the head is the generative type constructor `tc`,
+  - `RM_Wildcard`: anything else.
+
+A (RoughMap val) is semantically a list of (key,[val]) pairs, where
+   key :: [RoughMatchTc]
+So, writing # for `OtherTc`, and Int for `KnownTc "Int"`, we might have
+    [ ([#, Int, Maybe, #, Int], v1)
+    , ([Int, #, List], v2 ]
+
+This map is stored as a trie, so looking up a key is very fast.
+See Note [Matching a RoughMap] and Note [Simple Matching Semantics] for details on
+lookup.
+
+We lookup a key of type [RoughMatchLookupTc], and return the list of all values whose
+keys "match":
+
+Given the above map, here are the results of some lookups:
+   Lookup key       Result
+   -------------------------
+   [Int, Int]       [v1,v2] -- Matches because the prefix of both entries matches
+   [Int,Int,List]   [v2]
+   [Bool]           []
+
+Notice that a single key can map to /multiple/ values.  E.g. if we started
+with (Maybe Int, val1) and (Maybe Bool, val2), we'd generate a RoughMap
+that is semantically the list   [( Maybe, [val1,val2] )]
+
+Note [RoughMap and beta reduction]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There is one tricky case we have to account for when matching a rough map due
+to Note [Eta reduction for data families] in `GHC.Core.Coercion.Axiom`:
+Consider that the user has written a program containing a data family:
+
+> data family Fam a b
+> data instance Fam Int a = SomeType  -- known henceforth as FamIntInst
+
+The LHS of this instance will be eta reduced, as described in Note [Eta
+reduction for data families]. Consequently, we will end up with a `FamInst`
+with `fi_tcs = [KnownTc Int]`. Naturally, we need RoughMap to return this
+instance when queried for an instance with template, e.g., `[KnownTc Fam,
+KnownTc Int, KnownTc Char]`.
+
+This explains the third clause of the mightMatch specification in Note [Simple Matching Semantics].
+As soon as the the lookup key runs out, the remaining instances might match.
+
+Note [Matching a RoughMap]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+The /lookup key/ into a rough map (RoughMatchLookupTc) is slightly
+different to the /insertion key/ (RoughMatchTc).  Like the insertion
+key each lookup argument is classified to a simpler key which
+describes what could match that position. There are three
+possibilities:
+
+* RML_KnownTc Name: The argument is headed by a known type
+  constructor.  Example: 'Bool' is classified as 'RML_KnownTc Bool'
+  and '[Int]' is classified as `RML_KnownTc []`
+
+* RML_NoKnownTc: The argument is definitely not headed by any known
+  type constructor.  Example: For instance matching 'a[sk], a[tau]' and 'F a[sk], F a[tau]'
+  are classified as 'RML_NoKnownTc', for family instance matching no examples.
+
+* RML_WildCard: The argument could match anything, we don't know
+  enough about it. For instance matching no examples, for type family matching,
+  things to do with variables.
+
+The interesting case for instance matching is the second case, because it does not appear in
+an insertion key. The second case arises in two situations:
+
+1. The head of the application is a type variable. The type variable definitely
+   doesn't match with any of the KnownTC instances so we can discard them all. For example:
+    Show a[sk] or Show (a[sk] b[sk]). One place constraints like this arise is when
+    typechecking derived instances.
+2. The head of the application is a known type family.
+   For example: F a[sk]. The application of F is stuck, and because
+   F is a type family it won't match any KnownTC instance so it's safe to discard
+   all these instances.
+
+Of course, these two cases can still match instances of the form `forall a . Show a =>`,
+and those instances are retained as they are classified as RM_WildCard instances.
+
+Note [Matches vs Unifiers]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+The lookupRM' function returns a pair of potential /matches/ and potential /unifiers/.
+The potential matches is likely to be much smaller than the bag of potential unifiers due
+to the reasoning about rigid type variables described in Note [Matching a RoughMap].
+On the other hand, the instances captured by the RML_NoKnownTC case can still potentially unify
+with any instance (depending on the substituion of said rigid variable) so they can't be discounted
+from the list of potential unifiers. This is achieved by the RML_NoKnownTC case continuing
+the lookup for unifiers by replacing RML_NoKnownTC with RML_LookupOtherTC.
+
+This distinction between matches and unifiers is also important for type families.
+During normal type family lookup, we care about matches and when checking for consistency
+we care about the unifiers. This is evident in the code as `lookup_fam_inst_env` is
+parameterised over a lookup function which either performs matching checking or unification
+checking.
+
+In addition to this, we only care whether there are zero or non-zero potential
+unifiers, even if we have many candidates, the search can stop before consulting
+each candidate. We only need the full list of unifiers when displaying error messages.
+Therefore the list is computed lazily so much work can be avoided constructing the
+list in the first place.
+
+Note [Simple Matching Semantics]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose `rm` is a RoughMap representing a set of (key,vals) pairs,
+  where key::[RoughMapTc] and val::a.
+Suppose I look up a key lk :: [RoughMapLookupTc] in `rm`
+Then I get back (matches, unifiers) where
+   matches  = [ vals | (key,vals) <- rm, key `mightMatch` lk ]
+   unifiers = [ vals | (key,vals) <- rm, key `mightUnify` lk ]
+
+Where mightMatch is defined like this:
+
+  mightMatch :: [RoughMapTc] -> [RoughMapLookupTc] -> Bool
+  mightMatch []  []    = True   -- A perfectly sized match might match
+  mightMatch key []    = True   -- A shorter lookup key matches everything
+  mightMatch []  (_:_) = True   -- If the lookup key is longer, then still might match
+                                -- Note [RoughMatch and beta reduction]
+  mightMatch (k:ks) (lk:lks) =
+    = case (k,lk) of
+         -- Standard case, matching on a specific known TyCon.
+         (RM_KnownTc n1, RML_KnownTc n2) -> n1==n2 && mightMatch ks lks
+         -- For example, if the key for 'Show Bool' is [RM_KnownTc Show, RM_KnownTc Bool]
+         ---and we match against (Show a[sk]) [RM_KnownTc Show, RML_NoKnownTc]
+         -- then Show Bool can never match Show a[sk] so return False.
+         (RM_KnownTc _, RML_NoKnownTc)   -> False
+         -- Wildcard cases don't inform us anything about the match.
+         (RM_WildCard, _ )    -> mightMatch ks lks
+         (_, RML_WildCard)    -> mightMatch ks lks
+
+  -- Might unify is very similar to mightMatch apart from RML_NoKnownTc may
+  -- unify with any instance.
+  mightUnify :: [RoughMapTc] -> [RoughMapLookupTc] -> Bool
+  mightUnify []  []    = True   -- A perfectly sized match might unify
+  mightUnify key []    = True   -- A shorter lookup key matches everything
+  mightUnify []  (_:_) = True
+  mightUnify (k:ks) (lk:lks) =
+    = case (k,lk) of
+         (RM_KnownTc n1, RML_KnownTc n2) -> n1==n2 && mightUnify ks lks
+         (RM_KnownTc _, RML_NoKnownTc)   -> mightUnify (k:ks) (RML_WildCard:lks)
+         (RM_WildCard, _ )    -> mightUnify ks lks
+         (_, RML_WildCard)    -> mightUnify ks lks
+
+
+The guarantee that RoughMap provides is that
+
+if
+   insert_ty `tcMatchTy` lookup_ty
+then definitely
+   typeToRoughMatchTc insert_ty `mightMatch` typeToRoughMatchLookupTc lookup_ty
+but not vice versa
+
+this statement encodes the intuition that the RoughMap is used as a quick pre-filter
+to remove instances from the matching pool. The contrapositive states that if the
+RoughMap reports that the instance doesn't match then `tcMatchTy` will report that the
+types don't match as well.
+
+-}
+
+-- Key for insertion into a RoughMap
+data RoughMatchTc
+  = RM_KnownTc Name   -- INVARIANT: Name refers to a TyCon tc that responds
+                   -- true to `isGenerativeTyCon tc Nominal`. See
+                   -- Note [Rough matching in class and family instances]
+  | RM_WildCard    -- e.g. type variable at the head
+  deriving( Data )
+
+-- Key for lookup into a RoughMap
+-- See Note [Matching a RoughMap]
+data RoughMatchLookupTc
+  = RML_KnownTc Name -- ^ The position only matches the specified KnownTc
+  | RML_NoKnownTc -- ^ The position definitely doesn't match any KnownTc
+  | RML_WildCard -- ^ The position can match anything
+  deriving ( Data )
+
+instance Outputable RoughMatchLookupTc where
+    ppr (RML_KnownTc nm) = text "RML_KnownTc" <+> ppr nm
+    ppr RML_NoKnownTc = text "RML_NoKnownTC"
+    ppr RML_WildCard = text "_"
+
+roughMatchTcToLookup :: RoughMatchTc -> RoughMatchLookupTc
+roughMatchTcToLookup (RM_KnownTc n) = RML_KnownTc n
+roughMatchTcToLookup RM_WildCard = RML_WildCard
+
+instance Outputable RoughMatchTc where
+    ppr (RM_KnownTc nm) = text "KnownTc" <+> ppr nm
+    ppr RM_WildCard = text "OtherTc"
+
+isRoughWildcard :: RoughMatchTc -> Bool
+isRoughWildcard RM_WildCard  = True
+isRoughWildcard (RM_KnownTc {}) = False
+
+typeToRoughMatchLookupTc :: Type -> RoughMatchLookupTc
+typeToRoughMatchLookupTc ty
+  | Just (ty', _) <- splitCastTy_maybe ty   = typeToRoughMatchLookupTc ty'
+  | otherwise =
+      case splitAppTys ty of
+        -- Case 1: Head of application is a type variable, does not match any KnownTc.
+        (TyVarTy {}, _) -> RML_NoKnownTc
+        (TyConApp tc _, _)
+          -- Case 2: Head of application is a known type constructor, hence KnownTc.
+          | not (isTypeFamilyTyCon tc) -> RML_KnownTc $! tyConName tc
+          -- Case 3: Head is a type family so it's stuck and therefore doesn't match
+          -- any KnownTc
+          | isTypeFamilyTyCon tc -> RML_NoKnownTc
+        -- Fallthrough: Otherwise, anything might match this position
+        _ -> RML_WildCard
+
+typeToRoughMatchTc :: Type -> RoughMatchTc
+typeToRoughMatchTc ty
+  | Just (ty', _) <- splitCastTy_maybe ty   = typeToRoughMatchTc ty'
+  | Just (tc,_)   <- splitTyConApp_maybe ty
+  , not (isTypeFamilyTyCon tc)              = assertPpr (isGenerativeTyCon tc Nominal) (ppr tc)
+                                              RM_KnownTc $! tyConName tc
+    -- See Note [Rough matching in class and family instances]
+  | otherwise                               = RM_WildCard
+
+-- | Trie of @[RoughMatchTc]@
+--
+-- *Examples*
+-- @
+-- insert [OtherTc] 1
+-- insert [OtherTc] 2
+-- lookup [OtherTc] == [1,2]
+-- @
+data RoughMap a = RM { rm_empty   :: Bag a
+                     , rm_known   :: DNameEnv (RoughMap a)
+                        -- See Note [InstEnv determinism] in GHC.Core.InstEnv
+                     , rm_unknown :: RoughMap a }
+                | RMEmpty -- an optimised (finite) form of emptyRM
+                          -- invariant: Empty RoughMaps are always represented with RMEmpty
+
+                deriving (Functor)
+
+instance Outputable a => Outputable (RoughMap a) where
+  ppr (RM empty known unknown) =
+      vcat [text "RM"
+           , nest 2 (vcat [ text "Empty:" <+> ppr empty
+                          , text "Known:" <+> ppr known
+                          , text "Unknown:" <+> ppr unknown])]
+  ppr RMEmpty = text "{}"
+
+emptyRM :: RoughMap a
+emptyRM = RMEmpty
+
+-- | Order of result is deterministic.
+lookupRM :: [RoughMatchLookupTc] -> RoughMap a -> [a]
+lookupRM tcs rm = bagToList (fst $ lookupRM' tcs rm)
+
+
+-- | N.B. Returns a 'Bag' for matches, which allows us to avoid rebuilding all of the lists
+-- we find in 'rm_empty', which would otherwise be necessary due to '++' if we
+-- returned a list. We use a list for unifiers becuase the tail is computed lazily and
+-- we often only care about the first couple of potential unifiers. Constructing a
+-- bag forces the tail which performs much too much work.
+--
+-- See Note [Matching a RoughMap]
+-- See Note [Matches vs Unifiers]
+lookupRM' :: [RoughMatchLookupTc] -> RoughMap a -> (Bag a -- Potential matches
+                                                   , [a]) -- Potential unifiers
+lookupRM' _                  RMEmpty = (emptyBag, [])
+-- See Note [Simple Matching Semantics] about why we return everything when the lookup
+-- key runs out.
+lookupRM' []                 rm      = let m = elemsRM rm
+                                       in (listToBag m, m)
+lookupRM' (RML_KnownTc tc : tcs) rm  =
+  let (common_m, common_u) = lookupRM' tcs (rm_unknown rm)
+      (m, u) = maybe (emptyBag, []) (lookupRM' tcs) (lookupDNameEnv (rm_known rm) tc)
+  in (rm_empty rm `unionBags` common_m `unionBags` m
+     , bagToList (rm_empty rm) ++ common_u ++ u)
+-- A RML_NoKnownTC does **not** match any KnownTC but can unify
+lookupRM' (RML_NoKnownTc : tcs)  rm      =
+
+  let (u_m, _u_u) = lookupRM' tcs (rm_unknown rm)
+  in (rm_empty rm `unionBags` u_m -- Definitely don't match
+     , snd $ lookupRM' (RML_WildCard : tcs) rm) -- But could unify..
+
+lookupRM' (RML_WildCard : tcs)    rm  =
+  let (m, u) = bimap unionManyBags concat (mapAndUnzip (lookupRM' tcs) (eltsDNameEnv $ rm_known rm))
+      (u_m, u_u) = lookupRM' tcs (rm_unknown rm)
+  in (rm_empty rm `unionBags` u_m `unionBags` m
+     , bagToList (rm_empty rm) ++ u_u ++ u)
+
+unionRM :: RoughMap a -> RoughMap a -> RoughMap a
+unionRM RMEmpty a = a
+unionRM a RMEmpty = a
+unionRM a b =
+  RM { rm_empty = rm_empty a `unionBags` rm_empty b
+     , rm_known = plusDNameEnv_C unionRM (rm_known a) (rm_known b)
+     , rm_unknown = rm_unknown a `unionRM` rm_unknown b
+     }
+
+
+insertRM :: [RoughMatchTc] -> a -> RoughMap a -> RoughMap a
+insertRM k v RMEmpty =
+    insertRM k v $ RM { rm_empty = emptyBag
+                      , rm_known = emptyDNameEnv
+                      , rm_unknown = emptyRM }
+insertRM [] v rm@(RM {}) =
+    -- See Note [Simple Matching Semantics]
+    rm { rm_empty = v `consBag` rm_empty rm }
+insertRM (RM_KnownTc k : ks) v rm@(RM {}) =
+    rm { rm_known = alterDNameEnv f (rm_known rm) k }
+  where
+    f Nothing  = Just $ (insertRM ks v emptyRM)
+    f (Just m) = Just $ (insertRM ks v m)
+insertRM (RM_WildCard : ks) v rm@(RM {}) =
+    rm { rm_unknown = insertRM ks v (rm_unknown rm) }
+
+filterRM :: (a -> Bool) -> RoughMap a -> RoughMap a
+filterRM _ RMEmpty = RMEmpty
+filterRM pred rm =
+    normalise $ RM {
+      rm_empty = filterBag pred (rm_empty rm),
+      rm_known = mapDNameEnv (filterRM pred) (rm_known rm),
+      rm_unknown = filterRM pred (rm_unknown rm)
+    }
+
+-- | Place a 'RoughMap' in normal form, turning all empty 'RM's into
+-- 'RMEmpty's. Necessary after removing items.
+normalise :: RoughMap a -> RoughMap a
+normalise RMEmpty = RMEmpty
+normalise (RM empty known RMEmpty)
+  | isEmptyBag empty
+  , isEmptyDNameEnv known = RMEmpty
+normalise rm = rm
+
+-- | Filter all elements that might match a particular key with the given
+-- predicate.
+filterMatchingRM :: (a -> Bool) -> [RoughMatchTc] -> RoughMap a -> RoughMap a
+filterMatchingRM _    _  RMEmpty = RMEmpty
+filterMatchingRM pred [] rm      = filterRM pred rm
+filterMatchingRM pred (RM_KnownTc tc : tcs) rm =
+    normalise $ RM {
+      rm_empty = filterBag pred (rm_empty rm),
+      rm_known = alterDNameEnv (join . fmap (dropEmpty . filterMatchingRM pred tcs)) (rm_known rm) tc,
+      rm_unknown = filterMatchingRM pred tcs (rm_unknown rm)
+    }
+filterMatchingRM pred (RM_WildCard : tcs) rm =
+    normalise $ RM {
+      rm_empty = filterBag pred (rm_empty rm),
+      rm_known = mapDNameEnv (filterMatchingRM pred tcs) (rm_known rm),
+      rm_unknown = filterMatchingRM pred tcs (rm_unknown rm)
+    }
+
+dropEmpty :: RoughMap a -> Maybe (RoughMap a)
+dropEmpty RMEmpty = Nothing
+dropEmpty rm = Just rm
+
+elemsRM :: RoughMap a -> [a]
+elemsRM = foldRM (:) []
+
+foldRM :: (a -> b -> b) -> b -> RoughMap a -> b
+foldRM f = go
+  where
+    -- N.B. local worker ensures that the loop can be specialised to the fold
+    -- function.
+    go z RMEmpty = z
+    go z (RM{ rm_unknown = unk, rm_known = known, rm_empty = empty}) =
+      foldr
+        f
+        (foldDNameEnv
+           (flip go)
+           (go z unk)
+           known
+        )
+        empty
+
+nonDetStrictFoldRM :: (b -> a -> b) -> b -> RoughMap a -> b
+nonDetStrictFoldRM f = go
+  where
+    -- N.B. local worker ensures that the loop can be specialised to the fold
+    -- function.
+    go !z RMEmpty = z
+    go  z rm@(RM{}) =
+      foldl'
+        f
+        (nonDetStrictFoldDNameEnv
+           (flip go)
+           (go z (rm_unknown rm))
+           (rm_known rm)
+        )
+        (rm_empty rm)
+
+sizeRM :: RoughMap a -> Int
+sizeRM = nonDetStrictFoldRM (\acc _ -> acc + 1) 0
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index a4dbdcb75d..a18899ec09 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -11,8 +11,8 @@ module GHC.Core.Unify (
         tcMatchTyX_BM, ruleMatchTyKiX,
 
         -- * Rough matching
-        RoughMatchTc(..), roughMatchTcs, instanceCantMatch,
-        typesCantMatch, isRoughOtherTc,
+        RoughMatchTc(..), roughMatchTcs, roughMatchTcsLookup, instanceCantMatch,
+        typesCantMatch, isRoughWildcard,
 
         -- Side-effect free unification
         tcUnifyTy, tcUnifyTyKi, tcUnifyTys, tcUnifyTyKis,
@@ -39,6 +39,7 @@ import GHC.Core.TyCon
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.FVs   ( tyCoVarsOfCoList, tyCoFVsOfTypes )
 import GHC.Core.TyCo.Subst ( mkTvSubst )
+import GHC.Core.RoughMap
 import GHC.Core.Map.Type
 import GHC.Utils.FV( FV, fvVarSet, fvVarList )
 import GHC.Utils.Misc
@@ -49,11 +50,9 @@ import GHC.Types.Unique.FM
 import GHC.Types.Unique.Set
 import {-# SOURCE #-} GHC.Tc.Utils.TcType ( tcEqType )
 import GHC.Exts( oneShot )
-import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
 import GHC.Data.FastString
 
-import Data.Data ( Data )
 import Data.List ( mapAccumL )
 import Control.Monad
 import qualified Data.Semigroup as S
@@ -291,27 +290,11 @@ But it is never
              albeit perhaps only after 'a' is instantiated.
 -}
 
-data RoughMatchTc
-  = KnownTc Name   -- INVARIANT: Name refers to a TyCon tc that responds
-                   -- true to `isGenerativeTyCon tc Nominal`. See
-                   -- Note [Rough matching in class and family instances]
-  | OtherTc        -- e.g. type variable at the head
-  deriving( Data )
-
-isRoughOtherTc :: RoughMatchTc -> Bool
-isRoughOtherTc OtherTc      = True
-isRoughOtherTc (KnownTc {}) = False
-
 roughMatchTcs :: [Type] -> [RoughMatchTc]
-roughMatchTcs tys = map rough tys
-  where
-    rough ty
-      | Just (ty', _) <- splitCastTy_maybe ty   = rough ty'
-      | Just (tc,_)   <- splitTyConApp_maybe ty
-      , not (isTypeFamilyTyCon tc)              = assertPpr (isGenerativeTyCon tc Nominal) (ppr tc) $
-                                                  KnownTc (tyConName tc)
-        -- See Note [Rough matching in class and family instances]
-      | otherwise                               = OtherTc
+roughMatchTcs tys = map typeToRoughMatchTc tys
+
+roughMatchTcsLookup :: [Type] -> [RoughMatchLookupTc]
+roughMatchTcsLookup tys = map typeToRoughMatchLookupTc tys
 
 instanceCantMatch :: [RoughMatchTc] -> [RoughMatchTc] -> Bool
 -- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot
@@ -321,7 +304,7 @@ instanceCantMatch (mt : ts) (ma : as) = itemCantMatch mt ma || instanceCantMatch
 instanceCantMatch _         _         =  False  -- Safe
 
 itemCantMatch :: RoughMatchTc -> RoughMatchTc -> Bool
-itemCantMatch (KnownTc t) (KnownTc a) = t /= a
+itemCantMatch (RM_KnownTc t) (RM_KnownTc a) = t /= a
 itemCantMatch _           _           = False