Refactor the treatment of predicate types

Trac #15648 showed that GHC was a bit confused about the
difference between the types for

* Predicates
* Coercions
* Evidence (in the typechecker constraint solver)

This patch cleans it up. See especially Type.hs
Note [Types for coercions, predicates, and evidence]

Particular changes

* Coercion types (a ~# b) and (a ~#R b) are not predicate types
  (so isPredTy reports False for them) and are not implicitly
  instantiated by the type checker.  This is a real change, but
  it consistently reflects that fact that (~#) and (~R#) really
  are different from predicates.

* isCoercionType is renamed to isCoVarType

* During type inference, simplifyInfer, we do /not/ want to infer
  a constraint (a ~# b), because that is no longer a predicate type.
  So we 'lift' it to (a ~ b). See TcType
  Note [Lift equality constaints when quantifying]

* During type inference for pattern synonyms, we need to 'lift'
  provided constraints of type (a ~# b) to (a ~ b).  See
  Note [Equality evidence in pattern synonyms] in PatSyn

* But what about (forall a. Eq a => a ~# b)? Is that a
  predicate type?  No -- it does not have kind Constraint.
  Is it an evidence type?  Perhaps, but awkwardly so.

  In the end I decided NOT to make it an evidence type,
  and to ensure the the type inference engine never
  meets it.  This made me /simplify/ the code in
  TcCanonical.makeSuperClasses; see TcCanonical
  Note [Equality superclasses in quantified constraints]

  Instead I moved the special treatment for primitive
  equality to TcInteract.doTopReactOther.  See TcInteract
  Note [Looking up primitive equalities in quantified constraints]

  Also see Note [Evidence for quantified constraints] in Type.

  All this means I can have
     isEvVarType ty = isCoVarType ty || isPredTy ty
  which is nice.

All in all, rather a lot of work for a small refactoring,
but I think it's a real improvement.

14 files changed, 276 insertions, 114 deletions

diff --git a/compiler/basicTypes/Id.hs b/compiler/basicTypes/Id.hs
index c1d281edd6..78518ee094 100644
--- a/compiler/basicTypes/Id.hs
+++ b/compiler/basicTypes/Id.hs
@@ -267,20 +267,20 @@ mkVanillaGlobalWithInfo = mkGlobalId VanillaId
 -- | For an explanation of global vs. local 'Id's, see "Var#globalvslocal"
 mkLocalId :: Name -> Type -> Id
 mkLocalId name ty = mkLocalIdWithInfo name ty vanillaIdInfo
- -- It's tempting to ASSERT( not (isCoercionType ty) ), but don't. Sometimes,
+ -- It's tempting to ASSERT( not (isCoVarType ty) ), but don't. Sometimes,
  -- the type is a panic. (Search invented_id)
 
 -- | Make a local CoVar
 mkLocalCoVar :: Name -> Type -> CoVar
 mkLocalCoVar name ty
-  = ASSERT( isCoercionType ty )
+  = ASSERT( isCoVarType ty )
     Var.mkLocalVar CoVarId name ty vanillaIdInfo
 
 -- | Like 'mkLocalId', but checks the type to see if it should make a covar
 mkLocalIdOrCoVar :: Name -> Type -> Id
 mkLocalIdOrCoVar name ty
-  | isCoercionType ty = mkLocalCoVar name ty
-  | otherwise         = mkLocalId    name ty
+  | isCoVarType ty = mkLocalCoVar name ty
+  | otherwise      = mkLocalId    name ty
 
 -- | Make a local id, with the IdDetails set to CoVarId if the type indicates
 -- so.
@@ -288,8 +288,8 @@ mkLocalIdOrCoVarWithInfo :: Name -> Type -> IdInfo -> Id
 mkLocalIdOrCoVarWithInfo name ty info
   = Var.mkLocalVar details name ty info
   where
-    details | isCoercionType ty = CoVarId
-            | otherwise         = VanillaId
+    details | isCoVarType ty = CoVarId
+            | otherwise      = VanillaId
 
     -- proper ids only; no covars!
 mkLocalIdWithInfo :: Name -> Type -> IdInfo -> Id
@@ -311,7 +311,7 @@ mkExportedVanillaId name ty = Var.mkExportedLocalVar VanillaId name ty vanillaId
 -- | Create a system local 'Id'. These are local 'Id's (see "Var#globalvslocal")
 -- that are created by the compiler out of thin air
 mkSysLocal :: FastString -> Unique -> Type -> Id
-mkSysLocal fs uniq ty = ASSERT( not (isCoercionType ty) )
+mkSysLocal fs uniq ty = ASSERT( not (isCoVarType ty) )
                         mkLocalId (mkSystemVarName uniq fs) ty
 
 -- | Like 'mkSysLocal', but checks to see if we have a covar type
@@ -328,7 +328,7 @@ mkSysLocalOrCoVarM fs ty
 
 -- | Create a user local 'Id'. These are local 'Id's (see "Var#globalvslocal") with a name and location that the user might recognize
 mkUserLocal :: OccName -> Unique -> Type -> SrcSpan -> Id
-mkUserLocal occ uniq ty loc = ASSERT( not (isCoercionType ty) )
+mkUserLocal occ uniq ty loc = ASSERT( not (isCoVarType ty) )
                               mkLocalId (mkInternalName uniq occ loc) ty
 
 -- | Like 'mkUserLocal', but checks if we have a coercion type
@@ -585,7 +585,7 @@ isDeadBinder bndr | isId bndr = isDeadOcc (idOccInfo bndr)
 -}
 
 isEvVar :: Var -> Bool
-isEvVar var = isPredTy (varType var)
+isEvVar var = isEvVarType (varType var)
 
 isDictId :: Id -> Bool
 isDictId id = isDictTy (idType id)
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 3aa668e952..d5f5f39682 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -1214,7 +1214,7 @@ lintCoBndr cv thing_inside
   = do { subst <- getTCvSubst
        ; let (subst', cv') = substCoVarBndr subst cv
        ; lintKind (varType cv')
-       ; lintL (isCoercionType (varType cv'))
+       ; lintL (isCoVarType (varType cv'))
                (text "CoVar with non-coercion type:" <+> pprTyVar cv)
        ; updateTCvSubst subst' (thing_inside cv') }
 
@@ -1260,7 +1260,7 @@ lintIdBndr top_lvl bind_site id linterF
 
        -- Check that the Id does not have type (t1 ~# t2) or (t1 ~R# t2);
        -- if so, it should be a CoVar, and checked by lintCoVarBndr
-       ; lintL (not (isCoercionType ty))
+       ; lintL (not (isCoVarType ty))
                (text "Non-CoVar has coercion type" <+> ppr id <+> dcolon <+> ppr ty)
 
        ; let id' = setIdType id ty
diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
index 2367c4548d..cc0ae6fe28 100644
--- a/compiler/coreSyn/CoreOpt.hs
+++ b/compiler/coreSyn/CoreOpt.hs
@@ -243,7 +243,7 @@ simple_opt_expr env expr
          -- Note [Getting the map/coerce RULE to work]
       | isDeadBinder b
       , [(DEFAULT, _, rhs)] <- as
-      , isCoercionType (varType b)
+      , isCoVarType (varType b)
       , (Var fun, _args) <- collectArgs e
       , fun `hasKey` coercibleSCSelIdKey
          -- without this last check, we get #11230
diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs
index c498258775..c39e681ccb 100644
--- a/compiler/coreSyn/CoreUtils.hs
+++ b/compiler/coreSyn/CoreUtils.hs
@@ -266,7 +266,7 @@ mkCast e co
   = e
 
 mkCast (Coercion e_co) co
-  | isCoercionType (pSnd (coercionKind co))
+  | isCoVarType (pSnd (coercionKind co))
        -- The guard here checks that g has a (~#) on both sides,
        -- otherwise decomposeCo fails.  Can in principle happen
        -- with unsafeCoerce
diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index 421adcaccd..f2ff5dd623 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -888,9 +888,9 @@ decomposeRuleLhs dflags orig_bndrs orig_lhs
                               , text "Orig lhs:" <+> ppr orig_lhs
                               , text "optimised lhs:" <+> ppr lhs2 ])
    pp_bndr bndr
-    | isTyVar bndr                      = text "type variable" <+> quotes (ppr bndr)
-    | Just pred <- evVarPred_maybe bndr = text "constraint" <+> quotes (ppr pred)
-    | otherwise                         = text "variable" <+> quotes (ppr bndr)
+    | isTyVar bndr = text "type variable" <+> quotes (ppr bndr)
+    | isEvVar bndr = text "constraint"    <+> quotes (ppr (varType bndr))
+    | otherwise    = text "variable"      <+> quotes (ppr bndr)
 
    constructor_msg con = vcat
      [ text "A constructor," <+> ppr con <>
diff --git a/compiler/typecheck/ClsInst.hs b/compiler/typecheck/ClsInst.hs
index b8ff6ddf6a..cacceef3d2 100644
--- a/compiler/typecheck/ClsInst.hs
+++ b/compiler/typecheck/ClsInst.hs
@@ -512,14 +512,14 @@ matchHeteroEquality :: [Type] -> TcM ClsInstResult
 -- Solves (t1 ~~ t2)
 matchHeteroEquality args
   = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon args ]
-                    , cir_mk_ev     = evDFunApp (dataConWrapId heqDataCon) args
+                    , cir_mk_ev     = evDataConApp heqDataCon args
                     , cir_what      = BuiltinInstance })
 
 matchHomoEquality :: [Type] -> TcM ClsInstResult
 -- Solves (t1 ~ t2)
 matchHomoEquality args@[k,t1,t2]
   = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon [k,k,t1,t2] ]
-                    , cir_mk_ev     = evDFunApp (dataConWrapId eqDataCon) args
+                    , cir_mk_ev     = evDataConApp eqDataCon args
                     , cir_what      = BuiltinInstance })
 matchHomoEquality args = pprPanic "matchHomoEquality" (ppr args)
 
@@ -527,8 +527,7 @@ matchHomoEquality args = pprPanic "matchHomoEquality" (ppr args)
 matchCoercible :: [Type] -> TcM ClsInstResult
 matchCoercible args@[k, t1, t2]
   = return (OneInst { cir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
-                    , cir_mk_ev     = evDFunApp (dataConWrapId coercibleDataCon)
-                                                args
+                    , cir_mk_ev     = evDataConApp coercibleDataCon args
                     , cir_what      = BuiltinInstance })
   where
     args' = [k, k, t1, t2]
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 6579556843..a0932ace40 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -23,7 +23,6 @@ import TcEvTerm
 import Class
 import TyCon
 import TyCoRep   -- cleverly decomposes types, good for completeness checking
-import TysWiredIn( cTupleTyConName )
 import Coercion
 import CoreSyn
 import Id( idType, mkTemplateLocals )
@@ -488,31 +487,22 @@ mk_strict_superclasses rec_clss ev tvs theta cls tys
     size      = sizeTypes tys
 
     do_one_given evar given_loc sel_id
-      | not (null tvs)
-      , null theta
-      , isUnliftedType sc_pred
-      -- Very special case for equality
-      -- See Note [Equality superclasses in quantified constraints]
-      = do { empty_ctuple_cls <- tcLookupClass (cTupleTyConName 0)
-           ; let theta1    = [mkClassPred empty_ctuple_cls []]
-                 dict_ids1 = mkTemplateLocals theta1
-           ; given_ev <- new_given theta1 dict_ids1 []
-           ; return [mkNonCanonical given_ev] }
-
-      | otherwise  -- Normal case
-      = do { given_ev <- new_given theta dict_ids dict_ids
+      | isUnliftedType sc_pred
+      , not (null tvs && null theta)
+      = -- See Note [Equality superclasses in quantified constraints]
+        return []
+      | otherwise
+      = do { given_ev <- newGivenEvVar given_loc $
+                         (given_ty, mk_sc_sel evar sel_id)
            ; mk_superclasses rec_clss given_ev tvs theta sc_pred }
-
       where
-        sc_pred = funResultTy (piResultTys (idType sel_id) tys)
+        sc_pred  = funResultTy (piResultTys (idType sel_id) tys)
+        given_ty = mkInfSigmaTy tvs theta sc_pred
 
-        new_given theta_abs dict_ids_abs dict_ids_app
-          = newGivenEvVar given_loc (given_ty, given_ev)
-          where
-            given_ty = mkInfSigmaTy tvs theta_abs sc_pred
-            given_ev = EvExpr $ mkLams tvs $ mkLams dict_ids_abs $
-                       Var sel_id `mkTyApps` tys `App`
-                       (evId evar `mkTyApps` mkTyVarTys tvs `mkVarApps` dict_ids_app)
+    mk_sc_sel evar sel_id
+      = EvExpr $ mkLams tvs $ mkLams dict_ids $
+        Var sel_id `mkTyApps` tys `App`
+        (evId evar `mkTyApps` mkTyVarTys tvs `mkVarApps` dict_ids)
 
     mk_given_loc loc
        | isCTupleClass cls
@@ -609,24 +599,22 @@ There is a wrinkle though, in the case where 'theta' is empty, so
 we have
   f :: (forall a. a~b) => stuff
 
-Now the superclass machinery kicks in, in makeSuperClasses,
-giving us a a second quantified constrait
+Now, potentially, the superclass machinery kicks in, in
+makeSuperClasses, giving us a a second quantified constrait
        (forall a. a ~# b)
 BUT this is an unboxed value!  And nothing has prepared us for
 dictionary "functions" that are unboxed.  Actually it does just
 about work, but the simplier ends up with stuff like
    case (/\a. eq_sel d) of df -> ...(df @Int)...
-and fails to simplify that any further.
+and fails to simplify that any further.  And it doesn't satisfy
+isPredTy any more.
 
-It seems eaiser to give such unboxed quantifed constraints a
-dummmy () argument, thus
-      (forall a. (% %) => a ~# b)
-where (% %) is the empty constraint tuple.  That makes everything
-be nicely boxed.
+So for now we simply decline to take superclasses in the quantified
+case.  Instead we have a special case in TcInteract.doTopReactOther,
+which looks for primitive equalities specially in the quantified
+constraints.
 
-(One might wonder about using void# instead, but this seems more
-uniform -- it's a constraint argument -- and I'm not worried about
-the last drop of efficiency for this very rare case.)
+See also Note [Evidence for quantified constraints] in Type.
 
 
 ************************************************************************
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 6827a58f55..35f31d1b9e 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -1186,8 +1186,8 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole })
 
     pp_hole_type_with_kind
       | isLiftedTypeKind hole_kind
-        || isCoercionType hole_ty -- Don't print the kind of unlifted
-                                  -- equalities (#15039)
+        || isCoVarType hole_ty -- Don't print the kind of unlifted
+                               -- equalities (#15039)
       = pprType hole_ty
       | otherwise
       = pprType hole_ty <+> dcolon <+> pprKind hole_kind
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index dffbd2bea3..fa1908983a 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -20,7 +20,7 @@ module TcEvidence (
 
   -- EvTerm (already a CoreExpr)
   EvTerm(..), EvExpr,
-  evId, evCoercion, evCast, evDFunApp,  evSelector,
+  evId, evCoercion, evCast, evDFunApp,  evDataConApp, evSelector,
   mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,
 
   evTermCoercion, evTermCoercion_maybe,
@@ -56,6 +56,7 @@ import PprCore ()   -- Instance OutputableBndr TyVar
 import TcType
 import Type
 import TyCon
+import DataCon( DataCon, dataConWrapId )
 import Class( Class )
 import PrelNames
 import DynFlags   ( gopt, GeneralFlag(Opt_PrintTypecheckerElaboration) )
@@ -552,6 +553,9 @@ evCast et tc | isReflCo tc = EvExpr et
 evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm
 evDFunApp df tys ets = EvExpr $ Var df `mkTyApps` tys `mkApps` ets
 
+evDataConApp :: DataCon -> [Type] -> [EvExpr] -> EvTerm
+evDataConApp dc tys ets = evDFunApp (dataConWrapId dc) tys ets
+
 -- Selector id plus the types at which it
 -- should be instantiated, used for HasField
 -- dictionaries; see Note [HasField instances]
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 1771e19849..3914db6c13 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -39,6 +39,7 @@ import TcSMonad
 import Bag
 import MonadUtils ( concatMapM, foldlM )
 
+import CoreSyn
 import Data.List( partition, foldl', deleteFirstsBy )
 import SrcLoc
 import VarEnv
@@ -1827,14 +1828,51 @@ doTopReactOther :: Ct -> TcS (StopOrContinue Ct)
 -- Why equalities? See TcCanonical
 -- Note [Equality superclasses in quantified constraints]
 doTopReactOther work_item
-  = do { res <- matchLocalInst pred (ctEvLoc ev)
+  | isGiven ev
+  = continueWith work_item
+
+  | EqPred eq_rel t1 t2 <- classifyPredType pred
+  = -- See Note [Looking up primitive equalities in quantified constraints]
+    case boxEqPred eq_rel t1 t2 of
+      Nothing -> continueWith work_item
+      Just (cls, tys)
+        -> do { res <- matchLocalInst (mkClassPred cls tys) loc
+              ; case res of
+                  OneInst { cir_mk_ev = mk_ev }
+                    -> chooseInstance work_item
+                           (res { cir_mk_ev = mk_eq_ev cls tys mk_ev })
+                    where
+                  _ -> continueWith work_item }
+
+  | otherwise
+  = do { res <- matchLocalInst pred loc
        ; case res of
            OneInst {} -> chooseInstance work_item res
            _          -> continueWith work_item }
   where
     ev = ctEvidence work_item
+    loc  = ctEvLoc ev
     pred = ctEvPred ev
 
+    mk_eq_ev cls tys mk_ev evs
+      = case (mk_ev evs) of
+          EvExpr e -> EvExpr (Var sc_id `mkTyApps` tys `App` e)
+          ev       -> pprPanic "mk_eq_ev" (ppr ev)
+      where
+        [sc_id] = classSCSelIds cls
+
+{- Note [Looking up primitive equalities in quantified constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For equalities (a ~# b) look up (a ~ b), and then do a superclass
+selection. This avoids having to support quantified constraints whose
+kind is not Constraint, such as (forall a. F a ~# b)
+
+See
+ * Note [Evidence for quantified constraints] in Type
+ * Note [Equality superclasses in quantified constraints]
+   in TcCanonical
+-}
+
 --------------------
 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
@@ -2539,8 +2577,8 @@ nullary case of what's happening here.
 -}
 
 matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
--- Try any Given quantified constraints, which are
--- effectively just local instance declarations.
+-- Look up the predicate in Given quantified constraints,
+-- which are effectively just local instance declarations.
 matchLocalInst pred loc
   = do { ics <- getInertCans
        ; case match_local_inst (inert_insts ics) of
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index a2406df319..8f59e39a4f 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -41,6 +41,8 @@ import TcBinds
 import BasicTypes
 import TcSimplify
 import TcUnify
+import Type( PredTree(..), EqRel(..), classifyPredType )
+import TysWiredIn
 import TcType
 import TcEvidence
 import BuildTyCl
@@ -52,6 +54,7 @@ import FieldLabel
 import Bag
 import Util
 import ErrUtils
+import Data.Maybe( mapMaybe )
 import Control.Monad ( zipWithM )
 import Data.List( partition )
 
@@ -157,8 +160,9 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
 
        ; prov_dicts <- mapM zonkId prov_dicts
        ; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts
-             prov_theta = map evVarPred filtered_prov_dicts
              -- Filtering: see Note [Remove redundant provided dicts]
+             (prov_theta, prov_evs)
+                 = unzip (mapMaybe mkProvEvidence filtered_prov_dicts)
 
        -- Report bad universal type variables
        -- See Note [Type variables whose kind is captured]
@@ -181,12 +185,38 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
                           (mkTyVarBinders Inferred univ_tvs
                             , req_theta,  ev_binds, req_dicts)
                           (mkTyVarBinders Inferred ex_tvs
-                            , mkTyVarTys ex_tvs, prov_theta
-                            , map (EvExpr . evId) filtered_prov_dicts)
+                            , mkTyVarTys ex_tvs, prov_theta, prov_evs)
                           (map nlHsVar args, map idType args)
                           pat_ty rec_fields } }
 tcInferPatSynDecl (XPatSynBind _) = panic "tcInferPatSynDecl"
 
+mkProvEvidence :: EvId -> Maybe (PredType, EvTerm)
+-- See Note [Equality evidence in pattern synonyms]
+mkProvEvidence ev_id
+  | EqPred r ty1 ty2 <- classifyPredType pred
+  , let k1 = typeKind ty1
+        k2 = typeKind ty2
+        is_homo = k1 `tcEqType` k2
+        homo_tys   = [k1, ty1, ty2]
+        hetero_tys = [k1, k2, ty1, ty2]
+  = case r of
+      ReprEq | is_homo
+             -> Just ( mkClassPred coercibleClass    homo_tys
+                     , evDataConApp coercibleDataCon homo_tys eq_con_args )
+             | otherwise -> Nothing
+      NomEq  | is_homo
+             -> Just ( mkClassPred eqClass    homo_tys
+                     , evDataConApp eqDataCon homo_tys eq_con_args )
+             | otherwise
+             -> Just ( mkClassPred heqClass    hetero_tys
+                     , evDataConApp heqDataCon hetero_tys eq_con_args )
+
+  | otherwise
+  = Just (pred, EvExpr (evId ev_id))
+  where
+    pred = evVarPred ev_id
+    eq_con_args = [evId ev_id]
+
 badUnivTvErr :: [TyVar] -> TyVar -> TcM ()
 -- See Note [Type variables whose kind is captured]
 badUnivTvErr ex_tvs bad_tv
@@ -239,6 +269,30 @@ Similarly consider
 The pattern (Bam x y) binds two (Ord a) dictionaries, but we only
 need one.  Agian mkMimimalWithSCs removes the redundant one.
 
+Note [Equality evidence in pattern synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  data X a where
+     MkX :: Eq a => [a] -> X (Maybe a)
+  pattern P x = MkG x
+
+Then there is a danger that GHC will infer
+  P :: forall a.  () =>
+       forall b. (a ~# Maybe b, Eq b) => [b] -> X a
+
+The 'builder' for P, which is called in user-code, will then
+have type
+  $bP :: forall a b. (a ~# Maybe b, Eq b) => [b] -> X a
+
+and that is bad because (a ~# Maybe b) is not a predicate type
+(see Note [Types for coercions, predicates, and evidence] in Type)
+and is not implicitly instantiated.
+
+So in mkProvEvidence we lift (a ~# b) to (a ~ b).  Tiresome, and
+marginally less efficient, if the builder/martcher are not inlined.
+
+See also Note [Lift equality constaints when quantifying] in TcType
+
 Note [Type variables whose kind is captured]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index e6cd0731e5..32026365b1 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -90,14 +90,13 @@ module TcType (
   deNoteType,
   orphNamesOfType, orphNamesOfCo,
   orphNamesOfTypes, orphNamesOfCoCon,
-  getDFunTyKey,
-  evVarPred_maybe, evVarPred,
+  getDFunTyKey, evVarPred,
 
   ---------------------------------
   -- Predicate types
   mkMinimalBySCs, transSuperClasses,
   pickQuantifiablePreds, pickCapturedPreds,
-  immSuperClasses,
+  immSuperClasses, boxEqPred,
   isImprovementPred,
 
   -- * Finding type instances
@@ -215,7 +214,7 @@ import Name -- hiding (varName)
 import NameSet
 import VarEnv
 import PrelNames
-import TysWiredIn( coercibleClass, unitTyCon, unitTyConKey
+import TysWiredIn( coercibleClass, eqClass, heqClass, unitTyCon, unitTyConKey
                  , listTyCon, constraintKind )
 import BasicTypes
 import Util
@@ -1986,18 +1985,12 @@ hasTyVarHead ty                 -- Haskell 98 allows predicates of form
        Just (ty, _) -> hasTyVarHead ty
        Nothing      -> False
 
-evVarPred_maybe :: EvVar -> Maybe PredType
-evVarPred_maybe v = if isPredTy ty then Just ty else Nothing
-  where ty = varType v
-
 evVarPred :: EvVar -> PredType
 evVarPred var
- | debugIsOn
-  = case evVarPred_maybe var of
-      Just pred -> pred
-      Nothing   -> pprPanic "tcEvVarPred" (ppr var <+> ppr (varType var))
- | otherwise
-  = varType var
+  = ASSERT2( isEvVarType var_ty, ppr var <+> dcolon <+> ppr var_ty )
+    var_ty
+ where
+    var_ty = varType var
 
 ------------------
 -- | When inferring types, should we quantify over a given predicate?
@@ -2015,31 +2008,38 @@ pickQuantifiablePreds qtvs theta
   = let flex_ctxt = True in  -- Quantify over non-tyvar constraints, even without
                              -- -XFlexibleContexts: see Trac #10608, #10351
          -- flex_ctxt <- xoptM Opt_FlexibleContexts
-    filter (pick_me flex_ctxt) theta
+    mapMaybe (pick_me flex_ctxt) theta
   where
     pick_me flex_ctxt pred
       = case classifyPredType pred of
 
           ClassPred cls tys
             | Just {} <- isCallStackPred cls tys
-              -- NEVER infer a CallStack constraint
-              -- Otherwise, we let the constraints bubble up to be
-              -- solved from the outer context, or be defaulted when we
-              -- reach the top-level.
-              -- see Note [Overview of implicit CallStacks]
-              -> False
+              -- NEVER infer a CallStack constraint.  Otherwise we let
+              -- the constraints bubble up to be solved from the outer
+              -- context, or be defaulted when we reach the top-level.
+              -- See Note [Overview of implicit CallStacks]
+            -> Nothing
 
-            | isIPClass cls    -> True -- See note [Inheriting implicit parameters]
+            | isIPClass cls
+            -> Just pred -- See note [Inheriting implicit parameters]
 
-            | otherwise
-              -> pick_cls_pred flex_ctxt cls tys
+            | pick_cls_pred flex_ctxt cls tys
+            -> Just pred
 
-          EqPred ReprEq ty1 ty2 -> pick_cls_pred flex_ctxt coercibleClass [ty1, ty2]
-            -- representational equality is like a class constraint
+          EqPred eq_rel ty1 ty2
+            | quantify_equality eq_rel ty1 ty2
+            , Just (cls, tys) <- boxEqPred eq_rel ty1 ty2
+              -- boxEqPred: See Note [Lift equality constaints when quantifying]
+            , pick_cls_pred flex_ctxt cls tys
+            -> Just (mkClassPred cls tys)
+
+          IrredPred ty
+            | tyCoVarsOfType ty `intersectsVarSet` qtvs
+            -> Just pred
+
+          _ -> Nothing
 
-          EqPred NomEq ty1 ty2  -> quant_fun ty1 || quant_fun ty2
-          IrredPred ty          -> tyCoVarsOfType ty `intersectsVarSet` qtvs
-          ForAllPred {}         -> False
 
     pick_cls_pred flex_ctxt cls tys
       = tyCoVarsOfTypes tys `intersectsVarSet` qtvs
@@ -2048,12 +2048,31 @@ pickQuantifiablePreds qtvs theta
            -- will pass!  See Trac #10351.
 
     -- See Note [Quantifying over equality constraints]
+    quantify_equality NomEq  ty1 ty2 = quant_fun ty1 || quant_fun ty2
+    quantify_equality ReprEq _   _   = True
+
     quant_fun ty
       = case tcSplitTyConApp_maybe ty of
           Just (tc, tys) | isTypeFamilyTyCon tc
                          -> tyCoVarsOfTypes tys `intersectsVarSet` qtvs
           _ -> False
 
+boxEqPred :: EqRel -> Type -> Type -> Maybe (Class, [Type])
+-- Given (t1 ~# t2) or (t1 ~R# t2) return the boxed version
+--       (t1 ~ t2)  or (t1 `Coercible` t2)
+boxEqPred eq_rel ty1 ty2
+  = case eq_rel of
+      NomEq  | homo_kind -> Just (eqClass,        [k1,     ty1, ty2])
+             | otherwise -> Just (heqClass,       [k1, k2, ty1, ty2])
+      ReprEq | homo_kind -> Just (coercibleClass, [k1,     ty1, ty2])
+             | otherwise -> Nothing -- Sigh: we do not have hererogeneous Coercible
+                                    --       so we can't abstract over it
+                                    -- Nothing fundamental: we could add it
+ where
+   k1 = typeKind ty1
+   k2 = typeKind ty2
+   homo_kind = k1 `tcEqType` k2
+
 pickCapturedPreds
   :: TyVarSet           -- Quantifying over these
   -> TcThetaType        -- Proposed constraints to quantify
@@ -2210,6 +2229,18 @@ Notice that
 
 See also TcTyDecls.checkClassCycles.
 
+Note [Lift equality constaints when quantifying]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We can't quantify over a constraint (t1 ~# t2) because that isn't a
+predicate type; see Note [Types for coercions, predicates, and evidence]
+in Type.hs.
+
+So we have to 'lift' it to (t1 ~ t2).  Similarly (~R#) must be lifted
+to Coercible.
+
+This tiresome lifting is the reason that pick_me (in
+pickQuantifiablePreds) returns a Maybe rather than a Bool.
+
 Note [Quantifying over equality constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Should we quantify over an equality constraint (s ~ t)?  In general, we don't.
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 6a05978512..d1c4626238 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -46,7 +46,7 @@ module TyCoRep (
         mkPiTys,
         isTYPE,
         isLiftedTypeKind, isUnliftedTypeKind,
-        isCoercionType, isRuntimeRepTy, isRuntimeRepVar,
+        isRuntimeRepTy, isRuntimeRepVar,
         sameVis,
 
         -- * Functions over binders
@@ -841,17 +841,6 @@ mkTyCoPiTys tbs ty = foldr mkTyCoPiTy ty tbs
 mkPiTys :: [TyCoBinder] -> Type -> Type
 mkPiTys tbs ty = foldr mkPiTy ty tbs
 
--- | Does this type classify a core (unlifted) Coercion?
--- At either role nominal or representational
---    (t1 ~# t2) or (t1 ~R# t2)
-isCoercionType :: Type -> Bool
-isCoercionType (TyConApp tc tys)
-  | (tc `hasKey` eqPrimTyConKey) || (tc `hasKey` eqReprPrimTyConKey)
-  , tys `lengthIs` 4
-  = True
-isCoercionType _ = False
-
-
 -- | Create the plain type constructor type which has been applied to no type arguments at all.
 mkTyConTy :: TyCon -> Type
 mkTyConTy tycon = TyConApp tycon []
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 1846525d77..34639202db 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -110,9 +110,10 @@ module Type (
 
         -- ** Predicates on types
         isTyVarTy, isFunTy, isDictTy, isPredTy, isCoercionTy,
-        isCoercionTy_maybe, isCoercionType, isForAllTy,
+        isCoercionTy_maybe, isForAllTy,
         isForAllTy_ty, isForAllTy_co,
         isPiTy, isTauTy, isFamFreeTy,
+        isCoVarType, isEvVarType,
 
         isValidJoinPointType,
 
@@ -1694,6 +1695,36 @@ caseBinder (Anon t)  _ d = d t
 
 Predicates on PredType
 
+Note [Types for coercions, predicates, and evidence]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We treat differently:
+
+  (a) Predicate types
+        Test: isPredTy
+        Binders: DictIds
+        Kind: Constraint
+        Examples: (Eq a), and (a ~ b)
+
+  (b) Coercion types are primitive, unboxed equalities
+        Test: isCoVarTy
+        Binders: CoVars (can appear in coercions)
+        Kind: TYPE (TupleRep [])
+        Examples: (t1 ~# t2) or (t1 ~R# t2)
+
+  (c) Evidence types is the type of evidence manipulated by
+      the type constraint solver.
+        Test: isEvVarType
+        Binders: EvVars
+        Kind: Constraint or TYPE (TupleRep [])
+        Examples: all coercion types and predicate types
+
+Coercion types and predicate types are mutually exclusive,
+but evidence types are a superset of both.
+
+When treated as a user type, predicates are invisible and are
+implicitly instantiated; but coercion types, and non-pred evidence
+types, are just regular old types.
+
 Note [isPredTy complications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 You would think that we could define
@@ -1714,6 +1745,19 @@ But there are a number of complications:
   print it as such. But that means that isPredTy must return True for
   (C a => C [a]).  Admittedly that type is illegal in Haskell, but we
   want to print it nicely in error messages.
+
+Note [Evidence for quantified constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The superclass mechanism in TcCanonical.makeSuperClasses risks
+taking a quantified constraint like
+   (forall a. C a => a ~ b)
+and generate superclass evidence
+   (forall a. C a => a ~# b)
+
+This is a funny thing: neither isPredTy nor isCoVarType are true
+of it.  So we are careful not to generate it in the first place:
+see Note [Equality superclasses in quantified constraints]
+in TcCanonical.
 -}
 
 -- | Split a type constructor application into its type constructor and
@@ -1766,16 +1810,39 @@ tcReturnsConstraintKind (FunTy    _ ty) = tcReturnsConstraintKind ty
 tcReturnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
 tcReturnsConstraintKind _               = False
 
+isEvVarType :: Type -> Bool
+-- True of (a) predicates, of kind Constraint, such as (Eq a), and (a ~ b)
+--         (b) coercion types, such as (t1 ~# t2) or (t1 ~R# t2)
+-- See Note [Types for coercions, predicates, and evidence]
+-- See Note [Evidence for quantified constraints]
+isEvVarType ty = isCoVarType ty || isPredTy ty
+
+-- | Does this type classify a core (unlifted) Coercion?
+-- At either role nominal or representational
+--    (t1 ~# t2) or (t1 ~R# t2)
+-- See Note [Types for coercions, predicates, and evidence]
+isCoVarType :: Type -> Bool
+isCoVarType ty
+  | Just (tc,tys) <- splitTyConApp_maybe ty
+  , (tc `hasKey` eqPrimTyConKey) || (tc `hasKey` eqReprPrimTyConKey)
+  , tys `lengthIs` 4
+  = True
+isCoVarType _ = False
+
 -- | Is the type suitable to classify a given/wanted in the typechecker?
 isPredTy :: Type -> Bool
 -- See Note [isPredTy complications]
+-- NB: /not/ true of (t1 ~# t2) or (t1 ~R# t2)
+--     See Note [Types for coercions, predicates, and evidence]
 isPredTy ty = go ty []
   where
     go :: Type -> [KindOrType] -> Bool
+    -- Since we are looking at the kind,
+    -- no need to look through type synonyms
     go (AppTy ty1 ty2)   args       = go ty1 (ty2 : args)
     go (TyVarTy tv)      args       = go_k (tyVarKind tv) args
     go (TyConApp tc tys) args       = ASSERT( null args )  -- TyConApp invariant
-                                      go_tc tc tys
+                                      go_k (tyConKind tc) tys
     go (FunTy arg res) []
       | isPredTy arg                = isPredTy res   -- (Eq a => C a)
       | otherwise                   = False          -- (Int -> Bool)
@@ -1783,14 +1850,6 @@ isPredTy ty = go ty []
     go (CastTy _ co) args           = go_k (pSnd (coercionKind co)) args
     go _ _ = False
 
-    go_tc :: TyCon -> [KindOrType] -> Bool
-    go_tc tc args
-      | tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
-                  = args `lengthIs` 4  -- ~# and ~R# sadly have result kind #
-                                       -- not Constraint; but we still want
-                                       -- isPredTy to reply True.
-      | otherwise = go_k (tyConKind tc) args
-
     go_k :: Kind -> [KindOrType] -> Bool
     -- True <=> ('k' applied to 'kts') = Constraint
     go_k k [] = tcIsConstraintKind k