Implement QuantifiedConstraints

We have wanted quantified constraints for ages and, as I hoped,
they proved remarkably simple to implement.   All the machinery was
already in place.

The main ticket is Trac #2893, but also relevant are
  #5927
  #8516
  #9123 (especially!  higher kinded roles)
  #14070
  #14317

The wiki page is
  https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints
which in turn contains a link to the GHC Proposal where the change
is specified.

Here is the relevant Note:

Note [Quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The -XQuantifiedConstraints extension allows type-class contexts like
this:

  data Rose f x = Rose x (f (Rose f x))

  instance (Eq a, forall b. Eq b => Eq (f b))
        => Eq (Rose f a)  where
    (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 >= rs2

Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
This quantified constraint is needed to solve the
 [W] (Eq (f (Rose f x)))
constraint which arises form the (==) definition.

Here are the moving parts
  * Language extension {-# LANGUAGE QuantifiedConstraints #-}
    and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension

  * A new form of evidence, EvDFun, that is used to discharge
    such wanted constraints

  * checkValidType gets some changes to accept forall-constraints
    only in the right places.

  * Type.PredTree gets a new constructor ForAllPred, and
    and classifyPredType analyses a PredType to decompose
    the new forall-constraints

  * Define a type TcRnTypes.QCInst, which holds a given
    quantified constraint in the inert set

  * TcSMonad.InertCans gets an extra field, inert_insts :: [QCInst],
    which holds all the Given forall-constraints.  In effect,
    such Given constraints are like local instance decls.

  * When trying to solve a class constraint, via
    TcInteract.matchInstEnv, use the InstEnv from inert_insts
    so that we include the local Given forall-constraints
    in the lookup.  (See TcSMonad.getInstEnvs.)

  * topReactionsStage calls doTopReactOther for CIrredCan and
    CTyEqCan, so they can try to react with any given
    quantified constraints (TcInteract.matchLocalInst)

  * TcCanonical.canForAll deals with solving a
    forall-constraint.  See
       Note [Solving a Wanted forall-constraint]
       Note [Solving a Wanted forall-constraint]

  * We augment the kick-out code to kick out an inert
    forall constraint if it can be rewritten by a new
    type equality; see TcSMonad.kick_out_rewritable

Some other related refactoring
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

* Move SCC on evidence bindings to post-desugaring, which fixed
  #14735, and is generally nicer anyway because we can use
  existing CoreSyn free-var functions.  (Quantified constraints
  made the free-vars of an ev-term a bit more complicated.)

* In LookupInstResult, replace GenInst with OneInst and NotSure,
  using the latter for multiple matches and/or one or more
  unifiers

44 files changed, 1779 insertions, 542 deletions

diff --git a/compiler/basicTypes/Id.hs b/compiler/basicTypes/Id.hs
index bf48bad7b9..e38769a14f 100644
--- a/compiler/basicTypes/Id.hs
+++ b/compiler/basicTypes/Id.hs
@@ -221,7 +221,7 @@ setIdInfo :: Id -> IdInfo -> Id
 setIdInfo id info = info `seq` (lazySetIdInfo id info)
         -- Try to avoid spack leaks by seq'ing
 
-modifyIdInfo :: (IdInfo -> IdInfo) -> Id -> Id
+modifyIdInfo :: HasDebugCallStack => (IdInfo -> IdInfo) -> Id -> Id
 modifyIdInfo fn id = setIdInfo id (fn (idInfo id))
 
 -- maybeModifyIdInfo tries to avoid unnecessary thrashing
diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index 4684d436a4..ba904c1122 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -53,7 +53,7 @@ import Name
 import VarSet
 import Rules
 import VarEnv
-import Var( EvVar )
+import Var( EvVar, varType )
 import Outputable
 import Module
 import SrcLoc
@@ -64,6 +64,7 @@ import BasicTypes
 import DynFlags
 import FastString
 import Util
+import UniqSet( nonDetEltsUniqSet )
 import MonadUtils
 import qualified GHC.LanguageExtensions as LangExt
 import Control.Monad
@@ -1144,15 +1145,39 @@ dsTcEvBinds (TcEvBinds {}) = panic "dsEvBinds"    -- Zonker has got rid of this
 dsTcEvBinds (EvBinds bs)   = dsEvBinds bs
 
 dsEvBinds :: Bag EvBind -> DsM [CoreBind]
-dsEvBinds bs = mapM ds_scc (sccEvBinds bs)
+dsEvBinds bs
+  = do { ds_bs <- mapBagM dsEvBind bs
+       ; return (mk_ev_binds ds_bs) }
+
+mk_ev_binds :: Bag (Id,CoreExpr) -> [CoreBind]
+-- We do SCC analysis of the evidence bindings, /after/ desugaring
+-- them. This is convenient: it means we can use the CoreSyn
+-- free-variable functions rather than having to do accurate free vars
+-- for EvTerm.
+mk_ev_binds ds_binds
+  = map ds_scc (stronglyConnCompFromEdgedVerticesUniq edges)
   where
-    ds_scc (AcyclicSCC (EvBind { eb_lhs = v, eb_rhs = r}))
-                          = liftM (NonRec v) (dsEvTerm r)
-    ds_scc (CyclicSCC bs) = liftM Rec (mapM dsEvBind bs)
+    edges :: [ Node EvVar (EvVar,CoreExpr) ]
+    edges = foldrBag ((:) . mk_node) [] ds_binds
+
+    mk_node :: (Id, CoreExpr) -> Node EvVar (EvVar,CoreExpr)
+    mk_node b@(var, rhs)
+      = DigraphNode { node_payload = b
+                    , node_key = var
+                    , node_dependencies = nonDetEltsUniqSet $
+                                          exprFreeVars rhs `unionVarSet`
+                                          coVarsOfType (varType var) }
+      -- It's OK to use nonDetEltsUniqSet here as stronglyConnCompFromEdgedVertices
+      -- is still deterministic even if the edges are in nondeterministic order
+      -- as explained in Note [Deterministic SCC] in Digraph.
+
+    ds_scc (AcyclicSCC (v,r)) = NonRec v r
+    ds_scc (CyclicSCC prs)    = Rec prs
 
 dsEvBind :: EvBind -> DsM (Id, CoreExpr)
 dsEvBind (EvBind { eb_lhs = v, eb_rhs = r}) = liftM ((,) v) (dsEvTerm r)
 
+
 {-**********************************************************************
 *                                                                      *
            Desugaring EvTerms
@@ -1162,6 +1187,13 @@ dsEvBind (EvBind { eb_lhs = v, eb_rhs = r}) = liftM ((,) v) (dsEvTerm r)
 dsEvTerm :: EvTerm -> DsM CoreExpr
 dsEvTerm (EvExpr e)          = return e
 dsEvTerm (EvTypeable ty ev)  = dsEvTypeable ty ev
+dsEvTerm (EvFun { et_tvs = tvs, et_given = given
+                , et_binds = ev_binds, et_body = wanted_id })
+  = do { ds_ev_binds <- dsTcEvBinds ev_binds
+       ; return $ (mkLams (tvs ++ given) $
+                   mkCoreLets ds_ev_binds $
+                   Var wanted_id) }
+
 
 {-**********************************************************************
 *                                                                      *
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index b2c82fa2ee..306a15a15b 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -4186,6 +4186,7 @@ xFlagsDeps = [
   flagSpec "PatternSynonyms"                  LangExt.PatternSynonyms,
   flagSpec "PolyKinds"                        LangExt.PolyKinds,
   flagSpec "PolymorphicComponents"            LangExt.RankNTypes,
+  flagSpec "QuantifiedConstraints"            LangExt.QuantifiedConstraints,
   flagSpec "PostfixOperators"                 LangExt.PostfixOperators,
   flagSpec "QuasiQuotes"                      LangExt.QuasiQuotes,
   flagSpec "Rank2Types"                       LangExt.RankNTypes,
@@ -4309,6 +4310,7 @@ impliedXFlags :: [(LangExt.Extension, TurnOnFlag, LangExt.Extension)]
 impliedXFlags
 -- See Note [Updating flag description in the User's Guide]
   = [ (LangExt.RankNTypes,                turnOn, LangExt.ExplicitForAll)
+    , (LangExt.QuantifiedConstraints,     turnOn, LangExt.ExplicitForAll)
     , (LangExt.ScopedTypeVariables,       turnOn, LangExt.ExplicitForAll)
     , (LangExt.LiberalTypeSynonyms,       turnOn, LangExt.ExplicitForAll)
     , (LangExt.ExistentialQuantification, turnOn, LangExt.ExplicitForAll)
diff --git a/compiler/specialise/Specialise.hs b/compiler/specialise/Specialise.hs
index c4fe042b1f..bc3e27f674 100644
--- a/compiler/specialise/Specialise.hs
+++ b/compiler/specialise/Specialise.hs
@@ -2011,6 +2011,7 @@ mkCallUDs' env f args
             EqPred {}       -> True
             IrredPred {}    -> True   -- Things like (D []) where D is a
                                       -- Constraint-ranged family; Trac #7785
+            ForAllPred {}   -> True
 
 {-
 Note [Type determines value]
diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index 7b27dfa3b4..bcd511b982 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -55,6 +55,7 @@ import TcType
 import HscTypes
 import Class( Class )
 import MkId( mkDictFunId )
+import CoreSyn( Expr(..) )  -- For the Coercion constructor
 import Id
 import Name
 import Var      ( EvVar, mkTyVar, tyVarName, TyVarBndr(..) )
@@ -352,6 +353,7 @@ instCallConstraints orig preds
        ; traceTc "instCallConstraints" (ppr evs)
        ; return (mkWpEvApps evs) }
   where
+    go :: TcPredType -> TcM EvTerm
     go pred
      | Just (Nominal, ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut #1
      = do  { co <- unifyType Nothing ty1 ty2
@@ -361,7 +363,7 @@ instCallConstraints orig preds
      | Just (tc, args@[_, _, ty1, ty2]) <- splitTyConApp_maybe pred
      , tc `hasKey` heqTyConKey
      = do { co <- unifyType Nothing ty1 ty2
-          ; return (evDFunApp (dataConWrapId heqDataCon) args [evCoercion co]) }
+          ; return (evDFunApp (dataConWrapId heqDataCon) args [Coercion co]) }
 
      | otherwise
      = emitWanted orig pred
@@ -371,10 +373,14 @@ instDFunType :: DFunId -> [DFunInstType]
                     , TcThetaType ) -- instantiated constraint
 -- See Note [DFunInstType: instantiating types] in InstEnv
 instDFunType dfun_id dfun_inst_tys
-  = do { (subst, inst_tys) <- go emptyTCvSubst dfun_tvs dfun_inst_tys
+  = do { (subst, inst_tys) <- go empty_subst dfun_tvs dfun_inst_tys
        ; return (inst_tys, substTheta subst dfun_theta) }
   where
-    (dfun_tvs, dfun_theta, _) = tcSplitSigmaTy (idType dfun_id)
+    dfun_ty = idType dfun_id
+    (dfun_tvs, dfun_theta, _) = tcSplitSigmaTy dfun_ty
+    empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType dfun_ty))
+                  -- With quantified constraints, the
+                  -- type of a dfun may not be closed
 
     go :: TCvSubst -> [TyVar] -> [DFunInstType] -> TcM (TCvSubst, [TcType])
     go subst [] [] = return (subst, [])
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index d540272a53..b0ff962e5c 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -24,10 +24,13 @@ import Class
 import TyCon
 import TyCoRep   -- cleverly decomposes types, good for completeness checking
 import Coercion
+import CoreSyn
+import Id( idType, mkTemplateLocals )
 import FamInstEnv ( FamInstEnvs )
 import FamInst ( tcTopNormaliseNewTypeTF_maybe )
 import Var
 import VarEnv( mkInScopeSet )
+import VarSet( delVarSetList )
 import Outputable
 import DynFlags( DynFlags )
 import NameSet
@@ -81,15 +84,31 @@ last time through, so we can skip the classification step.
 canonicalize :: Ct -> TcS (StopOrContinue Ct)
 canonicalize (CNonCanonical { cc_ev = ev })
   = {-# SCC "canNC" #-}
-    case classifyPredType (ctEvPred ev) of
+    case classifyPredType pred of
       ClassPred cls tys     -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
                                   canClassNC ev cls tys
       EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
                                   canEqNC    ev eq_rel ty1 ty2
-      IrredPred {}          -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
+      IrredPred {}          -> do traceTcS "canEvNC:irred" (ppr pred)
                                   canIrred ev
+      ForAllPred _ _ pred   -> do traceTcS "canEvNC:forall" (ppr pred)
+                                  canForAll ev (isClassPred pred)
+  where
+    pred = ctEvPred ev
+
+canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
+  = canForAll ev pend_sc
 
 canonicalize (CIrredCan { cc_ev = ev })
+  | EqPred eq_rel ty1 ty2 <- classifyPredType (ctEvPred ev)
+  = -- For insolubles (all of which are equalities, do /not/ flatten the arguments
+    -- In Trac #14350 doing so led entire-unnecessary and ridiculously large
+    -- type function expansion.  Instead, canEqNC just applies
+    -- the substitution to the predicate, and may do decomposition;
+    --    e.g. a ~ [a], where [G] a ~ [Int], can decompose
+    canEqNC ev eq_rel ty1 ty2
+
+  | otherwise
   = canIrred ev
 
 canonicalize (CDictCan { cc_ev = ev, cc_class  = cls
@@ -130,7 +149,7 @@ canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
 -- Precondition: EvVar is class evidence
 canClassNC ev cls tys
   | isGiven ev  -- See Note [Eagerly expand given superclasses]
-  = do { sc_cts <- mkStrictSuperClasses ev cls tys
+  = do { sc_cts <- mkStrictSuperClasses ev [] [] cls tys
        ; emitWork sc_cts
        ; canClass ev cls tys False }
 
@@ -174,7 +193,7 @@ solveCallStack ev ev_cs = do
   -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
   cs_tm <- evCallStack ev_cs
   let ev_tm = mkEvCast cs_tm (wrapIP (ctEvPred ev))
-  setWantedEvBind (ctEvEvId ev) (EvExpr ev_tm)
+  setEvBindIfWanted ev ev_tm
 
 canClass :: CtEvidence
          -> Class -> [Type]
@@ -424,67 +443,52 @@ makeSuperClasses :: [Ct] -> TcS [Ct]
 makeSuperClasses cts = concatMapM go cts
   where
     go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
-          = mkStrictSuperClasses ev cls tys
+      = mkStrictSuperClasses ev [] [] cls tys
+    go (CQuantCan (QCI { qci_pred = pred, qci_ev = ev }))
+      = ASSERT2( isClassPred pred, ppr pred )  -- The cts should all have
+                                               -- class pred heads
+        mkStrictSuperClasses ev tvs theta cls tys
+      where
+        (tvs, theta, cls, tys) = tcSplitDFunTy (ctEvPred ev)
     go ct = pprPanic "makeSuperClasses" (ppr ct)
 
-mkStrictSuperClasses :: CtEvidence -> Class -> [Type] -> TcS [Ct]
--- Return constraints for the strict superclasses of (c tys)
-mkStrictSuperClasses ev cls tys
-  = mk_strict_superclasses (unitNameSet (className cls)) ev cls tys
-
-mk_superclasses :: NameSet -> CtEvidence -> TcS [Ct]
--- Return this constraint, plus its superclasses, if any
-mk_superclasses rec_clss ev
-  | ClassPred cls tys <- classifyPredType (ctEvPred ev)
-  = mk_superclasses_of rec_clss ev cls tys
-
-  | otherwise   -- Superclass is not a class predicate
-  = return [mkNonCanonical ev]
-
-mk_superclasses_of :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct]
--- Always return this class constraint,
--- and expand its superclasses
-mk_superclasses_of rec_clss ev cls tys
-  | loop_found = do { traceTcS "mk_superclasses_of: loop" (ppr cls <+> ppr tys)
-                    ; return [this_ct] }  -- cc_pend_sc of this_ct = True
-  | otherwise  = do { traceTcS "mk_superclasses_of" (vcat [ ppr cls <+> ppr tys
-                                                          , ppr (isCTupleClass cls)
-                                                          , ppr rec_clss
-                                                          ])
-                    ; sc_cts <- mk_strict_superclasses rec_clss' ev cls tys
-                    ; return (this_ct : sc_cts) }
-                                   -- cc_pend_sc of this_ct = False
-  where
-    cls_nm     = className cls
-    loop_found = not (isCTupleClass cls) && cls_nm `elemNameSet` rec_clss
-                 -- Tuples never contribute to recursion, and can be nested
-    rec_clss'  = rec_clss `extendNameSet` cls_nm
-    this_ct    = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
-                          , cc_pend_sc = loop_found }
-                 -- NB: If there is a loop, we cut off, so we have not
-                 --     added the superclasses, hence cc_pend_sc = True
-
-mk_strict_superclasses :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct]
+mkStrictSuperClasses
+    :: CtEvidence
+    -> [TyVar] -> ThetaType  -- These two args are non-empty only when taking
+                             -- superclasses of a /quantified/ constraint
+    -> Class -> [Type] -> TcS [Ct]
+-- Return constraints for the strict superclasses of
+--   ev :: forall as. theta => cls tys
+mkStrictSuperClasses ev tvs theta cls tys
+  = mk_strict_superclasses (unitNameSet (className cls))
+                           ev tvs theta cls tys
+
+mk_strict_superclasses :: NameSet -> CtEvidence
+                       -> [TyVar] -> ThetaType
+                       -> Class -> [Type] -> TcS [Ct]
 -- Always return the immediate superclasses of (cls tys);
 -- and expand their superclasses, provided none of them are in rec_clss
 -- nor are repeated
-mk_strict_superclasses rec_clss ev cls tys
+mk_strict_superclasses rec_clss ev tvs theta cls tys
   | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
-  = do { sc_evs <- newGivenEvVars (mk_given_loc loc)
-                                  (mkEvScSelectors (evId evar) cls tys)
-       ; concatMapM (mk_superclasses rec_clss) sc_evs }
+  = concatMapM (do_one_given evar (mk_given_loc loc)) $
+    classSCSelIds cls
+  where
+    dict_ids  = mkTemplateLocals theta
+    size      = sizeTypes tys
 
-  | all noFreeVarsOfType tys
-  = return [] -- Wanteds with no variables yield no deriveds.
-              -- See Note [Improvement from Ground Wanteds]
+    do_one_given evar given_loc sel_id
+      = do { let sc_pred = funResultTy (piResultTys (idType sel_id) tys)
+                 given_ty = mkInfSigmaTy tvs theta sc_pred
+           ; given_ev <- newGivenEvVar given_loc $
+                         (given_ty, mk_sc_sel evar sel_id)
+           ; mk_superclasses rec_clss given_ev tvs theta sc_pred }
+
+    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)
 
-  | otherwise -- Wanted/Derived case, just add Derived superclasses
-              -- that can lead to improvement.
-  = do { let loc = ctEvLoc ev
-       ; sc_evs <- mapM (newDerivedNC loc) (immSuperClasses cls tys)
-       ; concatMapM (mk_superclasses rec_clss) sc_evs }
-  where
-    size = sizeTypes tys
     mk_given_loc loc
        | isCTupleClass cls
        = loc   -- For tuple predicates, just take them apart, without
@@ -503,6 +507,63 @@ mk_strict_superclasses rec_clss ev cls tys
        | otherwise  -- Probably doesn't happen, since this function
        = loc        -- is only used for Givens, but does no harm
 
+mk_strict_superclasses rec_clss ev tvs theta cls tys
+  | all noFreeVarsOfType tys
+  = return [] -- Wanteds with no variables yield no deriveds.
+              -- See Note [Improvement from Ground Wanteds]
+
+  | otherwise -- Wanted/Derived case, just add Derived superclasses
+              -- that can lead to improvement.
+  = ASSERT2( null tvs && null theta, ppr tvs $$ ppr theta )
+    concatMapM do_one_derived (immSuperClasses cls tys)
+  where
+    loc = ctEvLoc ev
+
+    do_one_derived sc_pred
+      = do { sc_ev <- newDerivedNC loc sc_pred
+           ; mk_superclasses rec_clss sc_ev [] [] sc_pred }
+
+mk_superclasses :: NameSet -> CtEvidence
+                -> [TyVar] -> ThetaType -> PredType -> TcS [Ct]
+-- Return this constraint, plus its superclasses, if any
+mk_superclasses rec_clss ev tvs theta pred
+  | ClassPred cls tys <- classifyPredType pred
+  = mk_superclasses_of rec_clss ev tvs theta cls tys
+
+  | otherwise   -- Superclass is not a class predicate
+  = return [mkNonCanonical ev]
+
+mk_superclasses_of :: NameSet -> CtEvidence
+                   -> [TyVar] -> ThetaType -> Class -> [Type]
+                   -> TcS [Ct]
+-- Always return this class constraint,
+-- and expand its superclasses
+mk_superclasses_of rec_clss ev tvs theta cls tys
+  | loop_found = do { traceTcS "mk_superclasses_of: loop" (ppr cls <+> ppr tys)
+                    ; return [this_ct] }  -- cc_pend_sc of this_ct = True
+  | otherwise  = do { traceTcS "mk_superclasses_of" (vcat [ ppr cls <+> ppr tys
+                                                          , ppr (isCTupleClass cls)
+                                                          , ppr rec_clss
+                                                          ])
+                    ; sc_cts <- mk_strict_superclasses rec_clss' ev tvs theta cls tys
+                    ; return (this_ct : sc_cts) }
+                                   -- cc_pend_sc of this_ct = False
+  where
+    cls_nm     = className cls
+    loop_found = not (isCTupleClass cls) && cls_nm `elemNameSet` rec_clss
+                 -- Tuples never contribute to recursion, and can be nested
+    rec_clss'  = rec_clss `extendNameSet` cls_nm
+
+    this_ct | null tvs, null theta
+            = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
+                       , cc_pend_sc = loop_found }
+                 -- NB: If there is a loop, we cut off, so we have not
+                 --     added the superclasses, hence cc_pend_sc = True
+            | otherwise
+            = CQuantCan (QCI { qci_tvs = tvs, qci_pred = mkClassPred cls tys
+                             , qci_ev = ev
+                             , qci_pend_sc = loop_found })
+
 
 {-
 ************************************************************************
@@ -515,16 +576,8 @@ mk_strict_superclasses rec_clss ev cls tys
 canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
 -- Precondition: ty not a tuple and no other evidence form
 canIrred ev
-  | EqPred eq_rel ty1 ty2 <- classifyPredType pred
-  = -- For insolubles (all of which are equalities, do /not/ flatten the arguments
-    -- In Trac #14350 doing so led entire-unnecessary and ridiculously large
-    -- type function expansion.  Instead, canEqNC just applies
-    -- the substitution to the predicate, and may do decomposition;
-    --    e.g. a ~ [a], where [G] a ~ [Int], can decompose
-    canEqNC ev eq_rel ty1 ty2
-
-  | otherwise
-  = do { traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
+  = do { let pred = ctEvPred ev
+       ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
        ; (xi,co) <- flatten FM_FlattenAll ev pred -- co :: xi ~ pred
        ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
     do { -- Re-classify, in case flattening has improved its shape
@@ -533,19 +586,172 @@ canIrred ev
            EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
            _                     -> continueWith $
                                     mkIrredCt new_ev } }
-  where
-    pred = ctEvPred ev
 
 canHole :: CtEvidence -> Hole -> TcS (StopOrContinue Ct)
 canHole ev hole
-  = do { let ty = ctEvPred ev
-       ; (xi,co) <- flatten FM_SubstOnly ev ty -- co :: xi ~ ty
+  = do { let pred = ctEvPred ev
+       ; (xi,co) <- flatten FM_SubstOnly ev pred -- co :: xi ~ pred
        ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
     do { updInertIrreds (`snocCts` (CHoleCan { cc_ev = new_ev
                                              , cc_hole = hole }))
        ; stopWith new_ev "Emit insoluble hole" } }
 
-{-
+
+{- *********************************************************************
+*                                                                      *
+*                      Quantified predicates
+*                                                                      *
+********************************************************************* -}
+
+{- Note [Quantified constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The -XQuantifiedConstraints extension allows type-class contexts like this:
+
+  data Rose f x = Rose x (f (Rose f x))
+
+  instance (Eq a, forall b. Eq b => Eq (f b))
+        => Eq (Rose f a)  where
+    (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 == rs2
+
+Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
+This quantified constraint is needed to solve the
+ [W] (Eq (f (Rose f x)))
+constraint which arises form the (==) definition.
+
+The wiki page is
+  https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints
+which in turn contains a link to the GHC Proposal where the change
+is specified, and a Haskell Symposium paper about it.
+
+We implement two main extensions to the design in the paper:
+
+ 1. We allow a variable in the instance head, e.g.
+      f :: forall m a. (forall b. m b) => D (m a)
+    Notice the 'm' in the head of the quantified constraint, not
+    a class.
+
+ 2. We suport superclasses to quantified constraints.
+    For example (contrived):
+      f :: (Ord b, forall b. Ord b => Ord (m b)) => m a -> m a -> Bool
+      f x y = x==y
+    Here we need (Eq (m a)); but the quantifed constraint deals only
+    with Ord.  But we can make it work by using its superclass.
+
+Here are the moving parts
+  * Language extension {-# LANGUAGE QuantifiedConstraints #-}
+    and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension
+
+  * A new form of evidence, EvDFun, that is used to discharge
+    such wanted constraints
+
+  * checkValidType gets some changes to accept forall-constraints
+    only in the right places.
+
+  * Type.PredTree gets a new constructor ForAllPred, and
+    and classifyPredType analyses a PredType to decompose
+    the new forall-constraints
+
+  * TcSMonad.InertCans gets an extra field, inert_insts,
+    which holds all the Given forall-constraints.  In effect,
+    such Given constraints are like local instance decls.
+
+  * When trying to solve a class constraint, via
+    TcInteract.matchInstEnv, use the InstEnv from inert_insts
+    so that we include the local Given forall-constraints
+    in the lookup.  (See TcSMonad.getInstEnvs.)
+
+  * TcCanonical.canForAll deals with solving a
+    forall-constraint.  See
+       Note [Solving a Wanted forall-constraint]
+       Note [Solving a Wanted forall-constraint]
+
+  * We augment the kick-out code to kick out an inert
+    forall constraint if it can be rewritten by a new
+    type equality; see TcSMonad.kick_out_rewritable
+
+Note that a quantified constraint is never /inferred/
+(by TcSimplify.simplifyInfer).  A function can only have a
+quantified constraint in its type if it is given an explicit
+type signature.
+
+Note that we implement
+-}
+
+canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct)
+-- We have a constraint (forall as. blah => C tys)
+canForAll ev pend_sc
+  = do { -- First rewrite it to apply the current substitution
+         -- Do not bother with type-family reductions; we can't
+         -- do them under a forall anyway (c.f. Flatten.flatten_one
+         -- on a forall type)
+         let pred = ctEvPred ev
+       ; (xi,co) <- flatten FM_SubstOnly ev pred -- co :: xi ~ pred
+       ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
+
+    do { -- Now decompose into its pieces and solve it
+         -- (It takes a lot less code to flatten before decomposing.)
+       ; case classifyPredType (ctEvPred new_ev) of
+           ForAllPred tv_bndrs theta pred
+              -> solveForAll new_ev tv_bndrs theta pred pend_sc
+           _  -> pprPanic "canForAll" (ppr new_ev)
+    } }
+
+solveForAll :: CtEvidence -> [TyVarBinder] -> TcThetaType -> PredType -> Bool
+            -> TcS (StopOrContinue Ct)
+solveForAll ev tv_bndrs theta pred pend_sc
+  | CtWanted { ctev_dest = dest } <- ev
+  = -- See Note [Solving a Wanted forall-constraint]
+    do { let skol_info = QuantCtxtSkol
+             empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
+                           tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs
+       ; (subst, skol_tvs) <- tcInstSkolTyVarsX empty_subst tvs
+       ; given_ev_vars <- mapM newEvVar (substTheta subst theta)
+
+       ; (w_id, ev_binds)
+             <- checkConstraintsTcS skol_info skol_tvs given_ev_vars $
+                do { wanted_ev <- newWantedEvVarNC loc $
+                                  substTy subst pred
+                   ; return ( ctEvEvId wanted_ev
+                            , unitBag (mkNonCanonical wanted_ev)) }
+
+      ; setWantedEvTerm dest $
+        EvFun { et_tvs = skol_tvs, et_given = given_ev_vars
+              , et_binds = ev_binds, et_body = w_id }
+
+      ; stopWith ev "Wanted forall-constraint" }
+
+  | isGiven ev   -- See Note [Solving a Given forall-constraint]
+  = do { addInertForAll qci
+       ; stopWith ev "Given forall-constraint" }
+
+  | otherwise
+  = stopWith ev "Derived forall-constraint"
+  where
+    loc = ctEvLoc ev
+    tvs = binderVars tv_bndrs
+    qci = QCI { qci_ev = ev, qci_tvs = tvs
+              , qci_pred = pred, qci_pend_sc = pend_sc }
+
+{- Note [Solving a Wanted forall-constraint]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Solving a wanted forall (quantified) constraint
+  [W] df :: forall ab. (Eq a, Ord b) => C x a b
+is delightfully easy.   Just build an implication constraint
+    forall ab. (g1::Eq a, g2::Ord b) => [W] d :: C x a
+and discharge df thus:
+    df = /\ab. \g1 g2. let <binds> in d
+where <binds> is filled in by solving the implication constraint.
+All the machinery is to hand; there is little to do.
+
+Note [Solving a Given forall-constraint]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For a Given constraint
+  [G] df :: forall ab. (Eq a, Ord b) => C x a b
+we just add it to TcS's local InstEnv of known instances,
+via addInertForall.  Then, if we look up (C x Int Bool), say,
+we'll find a match in the InstEnv.
+
+
 ************************************************************************
 *                                                                      *
 *        Equalities
@@ -630,11 +836,14 @@ can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
   = canEqReflexive ev ReprEq ty1
 
 -- When working with ReprEq, unwrap newtypes.
-can_eq_nc' _flat rdr_env envs ev ReprEq ty1 _ ty2 ps_ty2
-  | Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
+-- See Note [Unwrap newtypes first]
+can_eq_nc' _flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+  | ReprEq <- eq_rel
+  , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
   = can_eq_newtype_nc ev NotSwapped ty1 stuff1 ty2 ps_ty2
-can_eq_nc' _flat rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _
-  | Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
+
+  | ReprEq <- eq_rel
+  , Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
   = can_eq_newtype_nc ev IsSwapped  ty2 stuff2 ty1 ps_ty1
 
 -- Then, get rid of casts
@@ -657,7 +866,7 @@ can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) ps_ty2
 -- Literals
 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
  | l1 == l2
-  = do { setEqIfWanted ev (mkReflCo (eqRelRole eq_rel) ty1)
+  = do { setEvBindIfWanted ev (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1)
        ; stopWith ev "Equal LitTy" }
 
 -- Try to decompose type constructor applications
@@ -727,27 +936,28 @@ can_eq_nc_forall ev eq_rel s1 s2
             phi1' = substTy subst1 phi1
 
             -- Unify the kinds, extend the substitution
+            go :: [TcTyVar] -> TCvSubst -> [TyVarBinder]
+               -> TcS (TcCoercion, Cts)
             go (skol_tv:skol_tvs) subst (bndr2:bndrs2)
               = do { let tv2 = binderVar bndr2
-                   ; kind_co <- unifyWanted loc Nominal
-                                            (tyVarKind skol_tv)
-                                            (substTy subst (tyVarKind tv2))
+                   ; (kind_co, wanteds1) <- unify loc Nominal (tyVarKind skol_tv)
+                                                  (substTy subst (tyVarKind tv2))
                    ; let subst' = extendTvSubst subst tv2
                                        (mkCastTy (mkTyVarTy skol_tv) kind_co)
-                   ; co <- go skol_tvs subst' bndrs2
-                   ; return (mkForAllCo skol_tv kind_co co) }
+                   ; (co, wanteds2) <- go skol_tvs subst' bndrs2
+                   ; return ( mkTcForAllCo skol_tv kind_co co
+                            , wanteds1 `unionBags` wanteds2 ) }
 
             -- Done: unify phi1 ~ phi2
             go [] subst bndrs2
               = ASSERT( null bndrs2 )
-                unifyWanted loc (eqRelRole eq_rel)
-                            phi1' (substTy subst phi2)
+                unify loc (eqRelRole eq_rel) phi1' (substTy subst phi2)
 
             go _ _ _ = panic "cna_eq_nc_forall"  -- case (s:ss) []
 
             empty_subst2 = mkEmptyTCvSubst (getTCvInScope subst1)
 
-      ; all_co <- checkConstraintsTcS skol_info skol_tvs $
+      ; all_co <- checkTvConstraintsTcS skol_info skol_tvs $
                   go skol_tvs empty_subst2 bndrs2
 
       ; setWantedEq orig_dest all_co
@@ -758,6 +968,17 @@ can_eq_nc_forall ev eq_rel s1 s2
         pprEq s1 s2    -- See Note [Do not decompose given polytype equalities]
       ; stopWith ev "Discard given polytype equality" }
 
+ where
+    unify :: CtLoc -> Role -> TcType -> TcType -> TcS (TcCoercion, Cts)
+    -- This version returns the wanted constraint rather
+    -- than putting it in the work list
+    unify loc role ty1 ty2
+      | ty1 `tcEqType` ty2
+      = return (mkTcReflCo role ty1, emptyBag)
+      | otherwise
+      = do { (wanted, co) <- newWantedEq loc role ty1 ty2
+           ; return (co, unitBag (mkNonCanonical wanted)) }
+
 ---------------------------------
 -- | Compare types for equality, while zonking as necessary. Gives up
 -- as soon as it finds that two types are not equal.
@@ -895,7 +1116,26 @@ zonk_eq_types = go
     combine_rev f (Right tys) (Left elt) = Left (f <$> elt     <*> pure tys)
     combine_rev f (Right tys) (Right ty) = Right (f ty tys)
 
-{-
+{- See Note [Unwrap newtypes first]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  newtype N m a = MkN (m a)
+Then N will get a conservative, Nominal role for its second paramter 'a',
+because it appears as an argument to the unknown 'm'. Now consider
+  [W] N Maybe a  ~R#  N Maybe b
+
+If we decompose, we'll get
+  [W] a ~N# b
+
+But if instead we unwrap we'll get
+  [W] Maybe a ~R# Maybe b
+which in turn gives us
+  [W] a ~R# b
+which is easier to satisfy.
+
+Bottom line: unwrap newtypes before decomposing them!
+c.f. Trac #9123 comment:52,53 for a compelling example.
+
 Note [Newtypes can blow the stack]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have
@@ -1962,8 +2202,8 @@ rewriteEvidence ev@(CtWanted { ctev_dest = dest
   = do { mb_new_ev <- newWanted loc new_pred
        ; MASSERT( tcCoercionRole co == ctEvRole ev )
        ; setWantedEvTerm dest
-            (EvExpr $ mkEvCast (getEvExpr mb_new_ev)
-                               (tcDowngradeRole Representational (ctEvRole ev) co))
+            (mkEvCast (getEvExpr mb_new_ev)
+                      (tcDowngradeRole Representational (ctEvRole ev) co))
        ; case mb_new_ev of
             Fresh  new_ev -> continueWith new_ev
             Cached _      -> stopWith ev "Cached wanted" }
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index fb60ba350b..897ed96329 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -864,11 +864,11 @@ addDeferredBinding ctxt err ct
 
        ; case dest of
            EvVarDest evar
-             -> addTcEvBind ev_binds_var $ mkWantedEvBind evar (EvExpr err_tm)
+             -> addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm
            HoleDest hole
              -> do { -- See Note [Deferred errors for coercion holes]
                      let co_var = coHoleCoVar hole
-                   ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var (EvExpr err_tm)
+                   ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var err_tm
                    ; fillCoercionHole hole (mkTcCoVarCo co_var) }}
 
   | otherwise   -- Do not set any evidence for Given/Derived
diff --git a/compiler/typecheck/TcEvTerm.hs b/compiler/typecheck/TcEvTerm.hs
index 4c3961964c..8d8aa9bb10 100644
--- a/compiler/typecheck/TcEvTerm.hs
+++ b/compiler/typecheck/TcEvTerm.hs
@@ -23,9 +23,10 @@ import SrcLoc
 -- Used with Opt_DeferTypeErrors
 -- See Note [Deferring coercion errors to runtime]
 -- in TcSimplify
-evDelayedError :: Type -> FastString -> EvExpr
+evDelayedError :: Type -> FastString -> EvTerm
 evDelayedError ty msg
-  = Var errorId `mkTyApps` [getRuntimeRep ty, ty] `mkApps` [litMsg]
+  = EvExpr $
+    Var errorId `mkTyApps` [getRuntimeRep ty, ty] `mkApps` [litMsg]
   where
     errorId = tYPE_ERROR_ID
     litMsg  = Lit (MachStr (fastStringToByteString msg))
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 8abfc90f04..66fcb7a589 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -16,14 +16,14 @@ module TcEvidence (
   lookupEvBind, evBindMapBinds, foldEvBindMap, filterEvBindMap,
   isEmptyEvBindMap,
   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
-  sccEvBinds, evBindVar, isNoEvBindsVar,
+  evBindVar, isNoEvBindsVar,
 
   -- EvTerm (already a CoreExpr)
   EvTerm(..), EvExpr,
   evId, evCoercion, evCast, evDFunApp,  evSelector,
   mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,
 
-  evTermCoercion,
+  evTermCoercion, evTermCoercion_maybe,
   EvCallStack(..),
   EvTypeable(..),
 
@@ -69,7 +69,6 @@ import CoreFVs ( exprSomeFreeVars )
 
 import Util
 import Bag
-import Digraph
 import qualified Data.Data as Data
 import Outputable
 import SrcLoc
@@ -315,8 +314,8 @@ mkWpCastN co
 mkWpTyApps :: [Type] -> HsWrapper
 mkWpTyApps tys = mk_co_app_fn WpTyApp tys
 
-mkWpEvApps :: [EvExpr] -> HsWrapper
-mkWpEvApps args = mk_co_app_fn WpEvApp (map EvExpr args)
+mkWpEvApps :: [EvTerm] -> HsWrapper
+mkWpEvApps args = mk_co_app_fn WpEvApp args
 
 mkWpEvVarApps :: [EvVar] -> HsWrapper
 mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map (EvExpr . evId) vs)
@@ -416,7 +415,6 @@ instance Data.Data TcEvBinds where
 
 {- Note [No evidence bindings]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 Class constraints etc give rise to /term/ bindings for evidence, and
 we have nowhere to put term bindings in /types/.  So in some places we
 use NoEvBindsVar (see newNoTcEvBinds) to signal that no term-level
@@ -501,8 +499,8 @@ mkWantedEvBind :: EvVar -> EvTerm -> EvBind
 mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm }
 
 -- EvTypeable are never given, so we can work with EvExpr here instead of EvTerm
-mkGivenEvBind :: EvVar -> EvExpr -> EvBind
-mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = EvExpr tm }
+mkGivenEvBind :: EvVar -> EvTerm -> EvBind
+mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm }
 
 
 -- An EvTerm is, conceptually, a CoreExpr that implements the constraint.
@@ -510,8 +508,17 @@ mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = EvExpr
 --   type EvTerm  = CoreExpr
 -- Because of staging problems issues around EvTypeable
 data EvTerm
-    = EvExpr EvExpr
-    | EvTypeable Type EvTypeable   -- Dictionary for (Typeable ty)
+  = EvExpr EvExpr
+
+  | EvTypeable Type EvTypeable   -- Dictionary for (Typeable ty)
+
+  | EvFun     -- /\as \ds. let binds in v
+      { et_tvs   :: [TyVar]
+      , et_given :: [EvVar]
+      , et_binds :: TcEvBinds -- This field is why we need an EvFun
+                              -- constructor, and can't just use EvExpr
+      , et_body  :: EvVar }
+
   deriving Data.Data
 
 type EvExpr = CoreExpr
@@ -525,17 +532,17 @@ evId = Var
 
 -- coercion bindings
 -- See Note [Coercion evidence terms]
-evCoercion :: TcCoercion -> EvExpr
-evCoercion = Coercion
+evCoercion :: TcCoercion -> EvTerm
+evCoercion co = EvExpr (Coercion co)
 
 -- | d |> co
-evCast :: EvExpr -> TcCoercion -> EvExpr
-evCast et tc | isReflCo tc = et
-             | otherwise   = Cast et tc
+evCast :: EvExpr -> TcCoercion -> EvTerm
+evCast et tc | isReflCo tc = EvExpr et
+             | otherwise   = EvExpr (Cast et tc)
 
 -- Dictionary instance application
-evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvExpr
-evDFunApp df tys ets = Var df `mkTyApps` tys `mkApps` ets
+evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm
+evDFunApp df tys ets = EvExpr $ Var df `mkTyApps` tys `mkApps` ets
 
 -- Selector id plus the types at which it
 -- should be instantiated, used for HasField
@@ -544,7 +551,6 @@ evDFunApp df tys ets = Var df `mkTyApps` tys `mkApps` ets
 evSelector :: Id -> [Type] -> [EvExpr] -> EvExpr
 evSelector sel_id tys tms = Var sel_id `mkTyApps` tys `mkApps` tms
 
-
 -- Dictionary for (Typeable ty)
 evTypeable :: Type -> EvTypeable -> EvTerm
 evTypeable = EvTypeable
@@ -762,17 +768,23 @@ Important Details:
 
 -}
 
-mkEvCast :: EvExpr -> TcCoercion -> EvExpr
+mkEvCast :: EvExpr -> TcCoercion -> EvTerm
 mkEvCast ev lco
-  | ASSERT2(tcCoercionRole lco == Representational, (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]))
-    isTcReflCo lco = ev
+  | ASSERT2( tcCoercionRole lco == Representational
+           , (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]))
+    isTcReflCo lco = EvExpr ev
   | otherwise      = evCast ev lco
 
-mkEvScSelectors :: EvExpr -> Class -> [TcType] -> [(TcPredType, EvExpr)]
-mkEvScSelectors ev cls tys
+
+mkEvScSelectors         -- Assume   class (..., D ty, ...) => C a b
+  :: Class -> [TcType]  -- C ty1 ty2
+  -> [(TcPredType,      -- D ty[ty1/a,ty2/b]
+       EvExpr)          -- :: C ty1 ty2 -> D ty[ty1/a,ty2/b]
+     ]
+mkEvScSelectors cls tys
    = zipWith mk_pr (immSuperClasses cls tys) [0..]
   where
-    mk_pr pred i = (pred, Var sc_sel_id `mkTyApps` tys `App` ev)
+    mk_pr pred i = (pred, Var sc_sel_id `mkTyApps` tys)
       where
         sc_sel_id  = classSCSelId cls i -- Zero-indexed
 
@@ -783,17 +795,31 @@ isEmptyTcEvBinds :: TcEvBinds -> Bool
 isEmptyTcEvBinds (EvBinds b)    = isEmptyBag b
 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
 
-evTermCoercion :: EvTerm -> TcCoercion
+evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion
 -- Applied only to EvTerms of type (s~t)
 -- See Note [Coercion evidence terms]
+evTermCoercion_maybe ev_term
+  | EvExpr e <- ev_term = go e
+  | otherwise           = Nothing
+  where
+    go :: EvExpr -> Maybe TcCoercion
+    go (Var v)       = return (mkCoVarCo v)
+    go (Coercion co) = return co
+    go (Cast tm co)  = do { co' <- go tm
+                          ; return (mkCoCast co' co) }
+    go _             = Nothing
 
-{-
-************************************************************************
+evTermCoercion :: EvTerm -> TcCoercion
+evTermCoercion tm = case evTermCoercion_maybe tm of
+                      Just co -> co
+                      Nothing -> pprPanic "evTermCoercion" (ppr tm)
+
+
+{- *********************************************************************
 *                                                                      *
                   Free variables
 *                                                                      *
-************************************************************************
--}
+********************************************************************* -}
 
 findNeededEvVars :: EvBindMap -> VarSet -> VarSet
 findNeededEvVars ev_binds seeds
@@ -813,14 +839,10 @@ findNeededEvVars ev_binds seeds
      | otherwise
      = needs
 
-evTermCoercion (EvExpr (Var v))       = mkCoVarCo v
-evTermCoercion (EvExpr (Coercion co)) = co
-evTermCoercion (EvExpr (Cast tm co))  = mkCoCast (evTermCoercion (EvExpr tm)) co
-evTermCoercion tm                     = pprPanic "evTermCoercion" (ppr tm)
-
 evVarsOfTerm :: EvTerm -> VarSet
 evVarsOfTerm (EvExpr e)         = exprSomeFreeVars isEvVar e
 evVarsOfTerm (EvTypeable _ ev)  = evVarsOfTypeable ev
+evVarsOfTerm (EvFun {})         = emptyVarSet -- See Note [Free vars of EvFun]
 
 evVarsOfTerms :: [EvTerm] -> VarSet
 evVarsOfTerms = mapUnionVarSet evVarsOfTerm
@@ -833,22 +855,20 @@ evVarsOfTypeable ev =
     EvTypeableTrFun e1 e2 -> evVarsOfTerms [e1,e2]
     EvTypeableTyLit e     -> evVarsOfTerm e
 
--- | Do SCC analysis on a bag of 'EvBind's.
-sccEvBinds :: Bag EvBind -> [SCC EvBind]
-sccEvBinds bs = stronglyConnCompFromEdgedVerticesUniq edges
-  where
-    edges :: [ Node EvVar EvBind ]
-    edges = foldrBag ((:) . mk_node) [] bs
 
-    mk_node :: EvBind -> Node EvVar EvBind
-    mk_node b@(EvBind { eb_lhs = var, eb_rhs = term })
-      = DigraphNode b var (nonDetEltsUniqSet (evVarsOfTerm term `unionVarSet`
-                                coVarsOfType (varType var)))
-      -- It's OK to use nonDetEltsUniqSet here as stronglyConnCompFromEdgedVertices
-      -- is still deterministic even if the edges are in nondeterministic order
-      -- as explained in Note [Deterministic SCC] in Digraph.
+{- Note [Free vars of EvFun]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Finding the free vars of an EvFun is made tricky by the fact the
+bindings et_binds may be a mutable variable.  Fortunately, we
+can just squeeze by.  Here's how.
+
+* evVarsOfTerm is used only by TcSimplify.neededEvVars.
+* Each EvBindsVar in an et_binds field of an EvFun is /also/ in the
+  ic_binds field of an Implication
+* So we can track usage via the processing for that implication,
+  (see Note [Tracking redundant constraints] in TcSimplify).
+  We can ignore usage from the EvFun altogether.
 
-{-
 ************************************************************************
 *                                                                      *
                   Pretty printing
@@ -881,11 +901,12 @@ pprHsWrapper wrap pp_thing_inside
                                               <+> pprParendCo co)]
     help it (WpEvApp id)  = no_parens  $ sep [it True, nest 2 (ppr id)]
     help it (WpTyApp ty)  = no_parens  $ sep [it True, text "@" <+> pprParendType ty]
-    help it (WpEvLam id)  = add_parens $ sep [ text "\\" <> pp_bndr id, it False]
-    help it (WpTyLam tv)  = add_parens $ sep [text "/\\" <> pp_bndr tv, it False]
+    help it (WpEvLam id)  = add_parens $ sep [ text "\\" <> pprLamBndr id <> dot, it False]
+    help it (WpTyLam tv)  = add_parens $ sep [text "/\\" <> pprLamBndr tv <> dot, it False]
     help it (WpLet binds) = add_parens $ sep [text "let" <+> braces (ppr binds), it False]
 
-    pp_bndr v = pprBndr LambdaBind v <> dot
+pprLamBndr :: Id -> SDoc
+pprLamBndr v = pprBndr LambdaBind v
 
 add_parens, no_parens :: SDoc -> Bool -> SDoc
 add_parens d True  = parens d
@@ -916,6 +937,9 @@ instance Outputable EvBind where
 instance Outputable EvTerm where
   ppr (EvExpr e)         = ppr e
   ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
+  ppr (EvFun { et_tvs = tvs, et_given = gs, et_binds = bs, et_body = w })
+      = hang (text "\\" <+> sep (map pprLamBndr (tvs ++ gs)) <+> arrow)
+           2 (ppr bs $$ ppr w)   -- Not very pretty
 
 instance Outputable EvCallStack where
   ppr EvCsEmpty
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 0bc5c9c81e..8cabd0ca09 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -346,6 +346,15 @@ zonkEvVarOcc env v
   = return (EvId $ zonkIdOcc env v)
 -}
 
+zonkCoreBndrX :: ZonkEnv -> Var -> TcM (ZonkEnv, Var)
+zonkCoreBndrX env v
+  | isId v = do { v' <- zonkIdBndr env v
+                ; return (extendIdZonkEnv1 env v', v') }
+  | otherwise = zonkTyBndrX env v
+
+zonkCoreBndrsX :: ZonkEnv -> [Var] -> TcM (ZonkEnv, [Var])
+zonkCoreBndrsX = mapAccumLM zonkCoreBndrX
+
 zonkTyBndrsX :: ZonkEnv -> [TcTyVar] -> TcM (ZonkEnv, [TyVar])
 zonkTyBndrsX = mapAccumLM zonkTyBndrX
 
@@ -1437,10 +1446,18 @@ zonkRule _ (XRuleDecl _) = panic "zonkRule"
 -}
 
 zonkEvTerm :: ZonkEnv -> EvTerm -> TcM EvTerm
-zonkEvTerm env (EvExpr e) =
-  EvExpr <$> zonkCoreExpr env e
-zonkEvTerm env (EvTypeable ty ev) =
-  EvTypeable <$> zonkTcTypeToType env ty <*> zonkEvTypeable env ev
+zonkEvTerm env (EvExpr e)
+  = EvExpr <$> zonkCoreExpr env e
+zonkEvTerm env (EvTypeable ty ev)
+  = EvTypeable <$> zonkTcTypeToType env ty <*> zonkEvTypeable env ev
+zonkEvTerm env (EvFun { et_tvs = tvs, et_given = evs
+                      , et_binds = ev_binds, et_body = body_id })
+  = do { (env0, new_tvs) <- zonkTyBndrsX env tvs
+       ; (env1, new_evs) <- zonkEvBndrsX env0 evs
+       ; (env2, new_ev_binds) <- zonkTcEvBinds env1 ev_binds
+       ; let new_body_id = zonkIdOcc env2 body_id
+       ; return (EvFun { et_tvs = new_tvs, et_given = new_evs
+                       , et_binds = new_ev_binds, et_body = new_body_id }) }
 
 zonkCoreExpr :: ZonkEnv -> CoreExpr -> TcM CoreExpr
 zonkCoreExpr env (Var v)
@@ -1463,9 +1480,8 @@ zonkCoreExpr env (Tick t e)
 zonkCoreExpr env (App e1 e2)
     = App <$> zonkCoreExpr env e1 <*> zonkCoreExpr env e2
 zonkCoreExpr env (Lam v e)
-    = do v' <- zonkIdBndr env v
-         let env1 = extendIdZonkEnv1 env v'
-         Lam v' <$> zonkCoreExpr env1 e
+    = do { (env1, v') <- zonkCoreBndrX env v
+         ; Lam v' <$> zonkCoreExpr env1 e }
 zonkCoreExpr env (Let bind e)
     = do (env1, bind') <- zonkCoreBind env bind
          Let bind'<$> zonkCoreExpr env1 e
@@ -1478,11 +1494,10 @@ zonkCoreExpr env (Case scrut b ty alts)
          return $ Case scrut' b' ty' alts'
 
 zonkCoreAlt :: ZonkEnv -> CoreAlt -> TcM CoreAlt
-zonkCoreAlt env (dc, pats, rhs)
-    = do pats' <- mapM (zonkIdBndr env) pats
-         let env1 = extendZonkEnv env pats'
+zonkCoreAlt env (dc, bndrs, rhs)
+    = do (env1, bndrs') <- zonkCoreBndrsX env bndrs
          rhs' <- zonkCoreExpr env1 rhs
-         return $ (dc, pats', rhs')
+         return $ (dc, bndrs', rhs')
 
 zonkCoreBind :: ZonkEnv -> CoreBind -> TcM (ZonkEnv, CoreBind)
 zonkCoreBind env (NonRec v e)
@@ -1558,7 +1573,7 @@ zonkEvBind env bind@(EvBind { eb_lhs = var, eb_rhs = term })
 
        ; term' <- case getEqPredTys_maybe (idType var') of
            Just (r, ty1, ty2) | ty1 `eqType` ty2
-                  -> return (EvExpr (evCoercion (mkTcReflCo r ty1)))
+                  -> return (evCoercion (mkTcReflCo r ty1))
            _other -> zonkEvTerm env term
 
        ; return (bind { eb_lhs = var', eb_rhs = term' }) }
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 21a8209b5e..d09675778d 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -1052,7 +1052,7 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds sc_theta
 
            ; sc_top_name  <- newName (mkSuperDictAuxOcc n (getOccName cls))
            ; sc_ev_id     <- newEvVar sc_pred
-           ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id (EvExpr sc_ev_tm)
+           ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id sc_ev_tm
            ; let sc_top_ty = mkInvForAllTys tyvars (mkLamTypes dfun_evs sc_pred)
                  sc_top_id = mkLocalId sc_top_name sc_top_ty
                  export = ABE { abe_ext  = noExt
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index b2be509b69..3e41c61264 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -44,7 +44,7 @@ import FieldLabel
 import FunDeps
 import FamInst
 import FamInstEnv
-import Unify ( tcUnifyTyWithTFs )
+import Unify ( tcUnifyTyWithTFs, ruleMatchTyKiX )
 
 import TcEvidence
 import MkCore ( mkStringExprFS, mkNaturalExpr )
@@ -720,11 +720,11 @@ interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble })
   = continueWith workItem
 
   where
-    swap_me :: SwapFlag -> CtEvidence -> EvExpr
+    swap_me :: SwapFlag -> CtEvidence -> EvTerm
     swap_me swap ev
       = case swap of
-           NotSwapped -> ctEvExpr ev
-           IsSwapped  -> evCoercion (mkTcSymCo (evTermCoercion (EvExpr (ctEvExpr ev))))
+           NotSwapped -> ctEvTerm ev
+           IsSwapped  -> evCoercion (mkTcSymCo (evTermCoercion (ctEvTerm ev)))
 
 interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
 
@@ -1055,14 +1055,14 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
          then stopWith ev_w "interactDict/solved from instance"
          else
 
-    do { -- We were unable to solve the [W] constraint from in-scope
-         -- instances so we solve it from the matching inert we found
+    do { -- Ths short-cut solver didn't fire, so we
+         -- solve ev_w from the matching inert ev_i we found
          what_next <- solveOneFromTheOther ev_i ev_w
        ; traceTcS "lookupInertDict" (ppr what_next)
        ; case what_next of
-           KeepInert -> do { setEvBindIfWanted ev_w (ctEvExpr ev_i)
+           KeepInert -> do { setEvBindIfWanted ev_w (ctEvTerm ev_i)
                            ; return $ Stop ev_w (text "Dict equal" <+> parens (ppr what_next)) }
-           KeepWork  -> do { setEvBindIfWanted ev_i (ctEvExpr ev_w)
+           KeepWork  -> do { setEvBindIfWanted ev_i (ctEvTerm ev_w)
                            ; updInertDicts $ \ ds -> delDict ds cls tys
                            ; continueWith workItem } } }
 
@@ -1127,9 +1127,9 @@ shortCutSolver dflags ev_w ev_i
     try_solve_from_instance loc (ev_binds, solved_dicts) ev
       | let pred = ctEvPred ev
       , ClassPred cls tys <- classifyPredType pred
-      = do { inst_res <- lift $ match_class_inst dflags True cls tys loc_w
+      = do { inst_res <- lift $ matchGlobalInst dflags True cls tys loc_w
            ; case inst_res of
-               GenInst { lir_new_theta = preds
+               OneInst { lir_new_theta = preds
                        , lir_mk_ev = mk_ev
                        , lir_safe_over = safeOverlap }
                  | safeOverlap
@@ -1625,10 +1625,10 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
        ; stopWith ev "Solved from inert" }
 
   | ReprEq <- eq_rel   -- See Note [Do not unify representational equalities]
-  = unsolved_inert
+  = continueWith workItem
 
   | isGiven ev         -- See Note [Touchables and givens]
-  = unsolved_inert
+  = continueWith workItem
 
   | otherwise
   = do { tclvl <- getTcLevel
@@ -1637,18 +1637,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
                  ; n_kicked <- kickOutAfterUnification tv
                  ; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) }
 
-         else unsolved_inert }
-
-  where
-    unsolved_inert
-      = do { traceTcS "Can't solve tyvar equality"
-                (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
-                      , ppWhen (isMetaTyVar tv) $
-                        nest 4 (text "TcLevel of" <+> ppr tv
-                                <+> text "is" <+> ppr (metaTyVarTcLevel tv))
-                      , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs) ])
-           ; addInertEq workItem
-           ; stopWith ev "Kept as inert" }
+         else continueWith workItem }
 
 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
 
@@ -1814,7 +1803,7 @@ emitFunDepDeriveds fd_eqns
      = do { traceTcS "emitFunDepDeriveds 1" (ppr (ctl_depth loc) $$ ppr eqs $$ ppr (isGivenLoc loc))
           ; mapM_ (unifyDerived loc Nominal) eqs }
      | otherwise
-     = do { traceTcS "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ ppr eqs)
+     = do { traceTcS "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs)
           ; subst <- instFlexi tvs  -- Takes account of kind substitution
           ; mapM_ (do_one_eq loc subst) eqs }
 
@@ -1831,31 +1820,33 @@ emitFunDepDeriveds fd_eqns
 -}
 
 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
-topReactionsStage wi
- = do { tir <- doTopReact wi
-      ; case tir of
-          ContinueWith wi -> continueWith wi
-          Stop ev s       -> return (Stop ev (text "Top react:" <+> s)) }
-
-doTopReact :: WorkItem -> TcS (StopOrContinue Ct)
--- The work item does not react with the inert set, so try interaction with top-level
--- instances. Note:
---
---   (a) The place to add superclasses in not here in doTopReact stage.
---       Instead superclasses are added in the worklist as part of the
---       canonicalization process. See Note [Adding superclasses].
-
-doTopReact work_item
+-- The work item does not react with the inert set,
+-- so try interaction with top-level instances. Note:
+topReactionsStage work_item
   = do { traceTcS "doTopReact" (ppr work_item)
        ; case work_item of
            CDictCan {}  -> do { inerts <- getTcSInerts
                               ; doTopReactDict inerts work_item }
            CFunEqCan {} -> doTopReactFunEq work_item
+           CIrredCan {} -> doTopReactOther work_item
+           CTyEqCan {}  -> doTopReactOther work_item
            _  -> -- Any other work item does not react with any top-level equations
                  continueWith work_item  }
 
 
 --------------------
+doTopReactOther :: Ct -> TcS (StopOrContinue Ct)
+doTopReactOther work_item
+  = do { -- Try local quantified constraints
+         res <- matchLocalInst pred (ctEvLoc ev)
+       ; case res of
+           OneInst {} -> chooseInstance ev pred res
+           _          -> continueWith work_item }
+  where
+    ev = ctEvidence work_item
+    pred = ctEvPred ev
+
+--------------------
 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
                                      , cc_tyargs = args, cc_fsk = fsk })
@@ -2227,41 +2218,69 @@ Another example is indexed-types/should_compile/T10634
 
 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
 -- Try to use type-class instance declarations to simplify the constraint
-doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
+doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
                                           , cc_tyargs = xis })
-  | isGiven fl   -- Never use instances for Given constraints
+  | isGiven ev   -- Never use instances for Given constraints
   = do { try_fundep_improvement
        ; continueWith work_item }
 
-  | Just ev <- lookupSolvedDict inerts dict_loc cls xis   -- Cached
-  = do { setEvBindIfWanted fl (ctEvExpr ev)
-       ; stopWith fl "Dict/Top (cached)" }
+  | Just solved_ev <- lookupSolvedDict inerts dict_loc cls xis   -- Cached
+  = do { setEvBindIfWanted ev (ctEvTerm solved_ev)
+       ; stopWith ev "Dict/Top (cached)" }
 
   | otherwise  -- Wanted or Derived, but not cached
    = do { dflags <- getDynFlags
-        ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
-        ; case lkup_inst_res of
-               GenInst { lir_new_theta = theta
-                       , lir_mk_ev     = mk_ev
-                       , lir_safe_over = s } ->
-                 do { traceTcS "doTopReact/found instance for" $ ppr fl
-                    ; checkReductionDepth deeper_loc dict_pred
-                    ; unless s $ insertSafeOverlapFailureTcS work_item
-                    ; if isDerived fl then finish_derived theta
-                                      else finish_wanted  theta mk_ev }
-               NoInstance ->
-                 do { when (isImprovable fl) $
-                      try_fundep_improvement
-                    ; continueWith work_item } }
+        ; lkup_res <- matchClassInst dflags inerts cls xis dict_loc
+        ; case lkup_res of
+               OneInst { lir_safe_over = s }
+                  -> do { unless s $ insertSafeOverlapFailureTcS work_item
+                        ; when (isWanted ev) $ addSolvedDict ev cls xis
+                        ; chooseInstance ev dict_pred lkup_res }
+               _  ->  -- NoInstance or NotSure
+                     do { when (isImprovable ev) $
+                          try_fundep_improvement
+                        ; continueWith work_item } }
    where
      dict_pred   = mkClassPred cls xis
-     dict_loc    = ctEvLoc fl
+     dict_loc    = ctEvLoc ev
      dict_origin = ctLocOrigin dict_loc
-     deeper_loc  = zap_origin (bumpCtLocDepth dict_loc)
+
+     -- We didn't solve it; so try functional dependencies with
+     -- the instance environment, and return
+     -- See also Note [Weird fundeps]
+     try_fundep_improvement
+        = do { traceTcS "try_fundeps" (ppr work_item)
+             ; instEnvs <- getInstEnvs
+             ; emitFunDepDeriveds $
+               improveFromInstEnv instEnvs mk_ct_loc dict_pred }
+
+     mk_ct_loc :: PredType   -- From instance decl
+               -> SrcSpan    -- also from instance deol
+               -> CtLoc
+     mk_ct_loc inst_pred inst_loc
+       = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
+                                               inst_pred inst_loc }
+
+doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
+
+
+chooseInstance :: CtEvidence -> TcPredType -> LookupInstResult
+               -> TcS (StopOrContinue Ct)
+chooseInstance ev pred
+               (OneInst { lir_new_theta = theta
+                        , lir_mk_ev     = mk_ev })
+  = do { traceTcS "doTopReact/found instance for" $ ppr ev
+       ; checkReductionDepth deeper_loc pred
+       ; if isDerived ev then finish_derived theta
+                         else finish_wanted  theta mk_ev }
+  where
+     loc        = ctEvLoc ev
+     deeper_loc = zap_origin (bumpCtLocDepth loc)
+     origin     = ctLocOrigin loc
 
      zap_origin loc  -- After applying an instance we can set ScOrigin to
                      -- infinity, so that prohibitedSuperClassSolve never fires
-       | ScOrigin {} <- dict_origin
+       | ScOrigin {} <- origin
        = setCtLocOrigin loc (ScOrigin infinity)
        | otherwise
        = loc
@@ -2270,11 +2289,10 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
                    -> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct)
       -- Precondition: evidence term matches the predicate workItem
      finish_wanted theta mk_ev
-        = do { addSolvedDict fl cls xis
-             ; evc_vars <- mapM (newWanted deeper_loc) theta
-             ; setWantedEvBind (ctEvEvId fl) (mk_ev (map getEvExpr evc_vars))
+        = do { evc_vars <- mapM (newWanted deeper_loc) theta
+             ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars))
              ; emitWorkNC (freshGoals evc_vars)
-             ; stopWith fl "Dict/Top (solved wanted)" }
+             ; stopWith ev "Dict/Top (solved wanted)" }
 
      finish_derived theta  -- Use type-class instances for Deriveds, in the hope
        =                   -- of generating some improvements
@@ -2282,26 +2300,10 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
                            -- It's easy because no evidence is involved
          do { emitNewDeriveds deeper_loc theta
             ; traceTcS "finish_derived" (ppr (ctl_depth deeper_loc))
-            ; stopWith fl "Dict/Top (solved derived)" }
-
-     -- We didn't solve it; so try functional dependencies with
-     -- the instance environment, and return
-     -- See also Note [Weird fundeps]
-     try_fundep_improvement
-        = do { traceTcS "try_fundeps" (ppr work_item)
-             ; instEnvs <- getInstEnvs
-             ; emitFunDepDeriveds $
-               improveFromInstEnv instEnvs mk_ct_loc dict_pred }
-
-     mk_ct_loc :: PredType   -- From instance decl
-               -> SrcSpan    -- also from instance deol
-               -> CtLoc
-     mk_ct_loc inst_pred inst_loc
-       = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
-                                               inst_pred inst_loc }
-
-doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
+            ; stopWith ev "Dict/Top (solved derived)" }
 
+chooseInstance ev _ lookup_res
+  = pprPanic "chooseInstance" (ppr ev $$ ppr lookup_res)
 
 {- *******************************************************************
 *                                                                    *
@@ -2317,20 +2319,26 @@ doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
 type SafeOverlapping = Bool
 
 data LookupInstResult
-  = NoInstance
-  | GenInst { lir_new_theta :: [TcPredType]
+  = NoInstance   -- Definitely no instance
+
+  | OneInst { lir_new_theta :: [TcPredType]
             , lir_mk_ev     :: [EvExpr] -> EvTerm
             , lir_safe_over :: SafeOverlapping }
 
+  | NotSure      -- Multiple matches and/or one or more unifiers
+
 instance Outputable LookupInstResult where
   ppr NoInstance = text "NoInstance"
-  ppr (GenInst { lir_new_theta = ev
+  ppr NotSure    = text "NotSure"
+  ppr (OneInst { lir_new_theta = ev
                , lir_safe_over = s })
-    = text "GenInst" <+> vcat [ppr ev, ss]
+    = text "OneInst" <+> vcat [ppr ev, ss]
     where ss = text $ if s then "[safe]" else "[unsafe]"
 
 
-matchClassInst :: DynFlags -> InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
+matchClassInst :: DynFlags -> InertSet
+               -> Class -> [Type]
+               -> CtLoc -> TcS LookupInstResult
 matchClassInst dflags inerts clas tys loc
 -- First check whether there is an in-scope Given that could
 -- match this constraint.  In that case, do not use top-level
@@ -2342,21 +2350,33 @@ matchClassInst dflags inerts clas tys loc
   = do { traceTcS "Delaying instance application" $
            vcat [ text "Work item=" <+> pprClassPred clas tys
                 , text "Potential matching givens:" <+> ppr matchable_givens ]
-       ; return NoInstance }
+       ; return NotSure }
+
+  | otherwise
+  = do { traceTcS "matchClassInst" $ text "pred =" <+> ppr pred <+> char '{'
+       ; local_res <- matchLocalInst pred loc
+       ; case local_res of
+           OneInst {} ->
+                do { traceTcS "} matchClassInst local match" $ ppr local_res
+                   ; return local_res }
+
+           NotSure -> -- In the NotSure case for local instances
+                      -- we don't want to try global instances
+                do { traceTcS "} matchClassInst local not sure" empty
+                   ; return local_res }
+
+           NoInstance  -- No local instances, so try global ones
+              -> do { global_res <- matchGlobalInst dflags False clas tys loc
+                    ; traceTcS "} matchClassInst global result" $ ppr global_res
+                    ; return global_res } }
   where
-     pred = mkClassPred clas tys
+    pred = mkClassPred clas tys
 
-matchClassInst dflags _ clas tys loc
- = do { traceTcS "matchClassInst" $ text "pred =" <+> ppr (mkClassPred clas tys) <+> char '{'
-      ; res <- match_class_inst dflags False clas tys loc
-      ; traceTcS "} matchClassInst result" $ ppr res
-      ; return res }
-
-match_class_inst :: DynFlags
-                 -> Bool      -- True <=> caller is the short-cut solver
-                              -- See Note [Shortcut solving: overlap]
-                 -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
-match_class_inst dflags short_cut clas tys loc
+matchGlobalInst :: DynFlags
+                -> Bool      -- True <=> caller is the short-cut solver
+                             -- See Note [Shortcut solving: overlap]
+                -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
+matchGlobalInst dflags short_cut clas tys loc
   | cls_name == knownNatClassName     = matchKnownNat        clas tys
   | cls_name == knownSymbolClassName  = matchKnownSymbol     clas tys
   | isCTupleClass clas                = matchCTuple          clas tys
@@ -2507,12 +2527,42 @@ PS: the term "naturally coherent" doesn't really seem helpful.
 Perhaps "invertible" or something?  I left it for now though.
 -}
 
+matchLocalInst :: TcPredType -> CtLoc -> TcS LookupInstResult
+matchLocalInst pred loc
+  = do { ics <- getInertCans
+       ; case match_local_inst (inert_insts ics) of
+           ([], False) -> return NoInstance
+           ([(dfun_ev, inst_tys)], unifs)
+             | not unifs
+             -> match_one pred loc True (ctEvEvId dfun_ev) inst_tys
+           _ -> return NotSure }
+  where
+    pred_tv_set = tyCoVarsOfType pred
+
+    match_local_inst :: [QCInst]
+                     -> ( [(CtEvidence, [DFunInstType])]
+                        , Bool )      -- True <=> Some unify but do not match
+    match_local_inst []
+      = ([], False)
+    match_local_inst (qci@(QCI { qci_tvs = qtvs, qci_pred = qpred
+                               , qci_ev = ev })
+                     : qcis)
+      | let in_scope = mkInScopeSet (qtv_set `unionVarSet` pred_tv_set)
+      , Just tv_subst <- ruleMatchTyKiX qtv_set (mkRnEnv2 in_scope)
+                                        emptyTvSubstEnv qpred pred
+      , let match = (ev, map (lookupVarEnv tv_subst) qtvs)
+      = (match:matches, unif)
 
-{- *******************************************************************
-*                                                                    *
-                Class lookup in the instance environment
-*                                                                    *
-**********************************************************************-}
+      | otherwise
+      = ASSERT2( disjointVarSet qtv_set (tyCoVarsOfType pred)
+               , ppr qci $$ ppr pred )
+            -- ASSERT: unification relies on the
+            -- quantified variables being fresh
+        (matches, unif || this_unif)
+      where
+        qtv_set = mkVarSet qtvs
+        this_unif = mightMatchLater qpred (ctEvLoc ev) pred loc
+        (matches, unif) = match_local_inst qcis
 
 matchInstEnv :: DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
 matchInstEnv dflags short_cut_solver clas tys loc
@@ -2520,51 +2570,57 @@ matchInstEnv dflags short_cut_solver clas tys loc
         ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
               (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
               safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
+        ; traceTcS "matchInstEnv" $
+            vcat [ text "goal:" <+> ppr clas <+> ppr tys
+                 , text "matches:" <+> ppr matches
+                 , text "unify:" <+> ppr unify ]
         ; case (matches, unify, safeHaskFail) of
 
             -- Nothing matches
-            ([], _, _)
+            ([], [], _)
                 -> do { traceTcS "matchClass not matching" (ppr pred)
                       ; return NoInstance }
 
             -- A single match (& no safe haskell failure)
             ([(ispec, inst_tys)], [], False)
-                | short_cut_solver
+                | short_cut_solver      -- Called from the short-cut solver
                 , isOverlappable ispec
                 -- If the instance has OVERLAPPABLE or OVERLAPS or INCOHERENT
                 -- then don't let the short-cut solver choose it, because a
                 -- later instance might overlap it.  Trac #14434 is an example
                 -- See Note [Shortcut solving: overlap]
-                -> do { traceTcS "matchClass: ingnoring overlappable" (ppr pred)
-                      ; return NoInstance }
+                -> do { traceTcS "matchClass: ignoring overlappable" (ppr pred)
+                      ; return NotSure }
 
                 | otherwise
-                -> do   { let dfun_id = instanceDFunId ispec
-                        ; traceTcS "matchClass success" $
-                          vcat [text "dict" <+> ppr pred,
-                                text "witness" <+> ppr dfun_id
-                                               <+> ppr (idType dfun_id) ]
-                                  -- Record that this dfun is needed
-                        ; match_one (null unsafeOverlaps) dfun_id inst_tys }
+                -> do { let dfun_id = instanceDFunId ispec
+                      ; traceTcS "matchClass success" $
+                        vcat [text "dict" <+> ppr pred,
+                              text "witness" <+> ppr dfun_id
+                                             <+> ppr (idType dfun_id) ]
+                                -- Record that this dfun is needed
+                      ; match_one pred loc (null unsafeOverlaps) dfun_id inst_tys }
 
             -- More than one matches (or Safe Haskell fail!). Defer any
             -- reactions of a multitude until we learn more about the reagent
-            (matches, _, _)
-                -> do   { traceTcS "matchClass multiple matches, deferring choice" $
-                          vcat [text "dict" <+> ppr pred,
-                                text "matches" <+> ppr matches]
-                        ; return NoInstance } }
+            _   -> do { traceTcS "matchClass multiple matches, deferring choice" $
+                        vcat [text "dict" <+> ppr pred,
+                              text "matches" <+> ppr matches]
+                      ; return NotSure } }
    where
      pred = mkClassPred clas tys
 
-     match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcS LookupInstResult
-                  -- See Note [DFunInstType: instantiating types] in InstEnv
-     match_one so dfun_id mb_inst_tys
-       = do { checkWellStagedDFun pred dfun_id loc
-            ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
-            ; return $ GenInst { lir_new_theta = theta
-                               , lir_mk_ev     = EvExpr . evDFunApp dfun_id tys
-                               , lir_safe_over = so } }
+match_one :: TcPredType -> CtLoc -> SafeOverlapping
+          -> DFunId -> [DFunInstType] -> TcS LookupInstResult
+             -- See Note [DFunInstType: instantiating types] in InstEnv
+match_one pred loc so dfun_id mb_inst_tys
+  = do { traceTcS "match_one" (ppr dfun_id $$ ppr mb_inst_tys)
+       ; checkWellStagedDFun pred dfun_id loc
+       ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
+       ; traceTcS "match_one 2" (ppr dfun_id $$ ppr tys $$ ppr theta)
+       ; return $ OneInst { lir_new_theta = theta
+                          , lir_mk_ev     = evDFunApp dfun_id tys
+                          , lir_safe_over = so } }
 
 
 {- ********************************************************************
@@ -2575,13 +2631,13 @@ matchInstEnv dflags short_cut_solver clas tys loc
 
 matchCTuple :: Class -> [Type] -> TcS LookupInstResult
 matchCTuple clas tys   -- (isCTupleClass clas) holds
-  = return (GenInst { lir_new_theta = tys
+  = return (OneInst { lir_new_theta = tys
                     , lir_mk_ev     = tuple_ev
                     , lir_safe_over = True })
             -- The dfun *is* the data constructor!
   where
      data_con = tyConSingleDataCon (classTyCon clas)
-     tuple_ev = EvExpr . evDFunApp (dataConWrapId data_con) tys
+     tuple_ev = evDFunApp (dataConWrapId data_con) tys
 
 {- ********************************************************************
 *                                                                     *
@@ -2673,8 +2729,8 @@ makeLitDict clas ty et
                       $ idType meth         -- forall n. KnownNat n => SNat n
     , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
           -- SNat n ~ Integer
-    , let ev_tm = EvExpr $ mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))
-    = return $ GenInst { lir_new_theta = []
+    , let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))
+    = return $ OneInst { lir_new_theta = []
                        , lir_mk_ev     = \_ -> ev_tm
                        , lir_safe_over = True }
 
@@ -2710,12 +2766,15 @@ matchTypeable _ _ = return NoInstance
 -- | Representation for a type @ty@ of the form @arg -> ret@.
 doFunTy :: Class -> Type -> Type -> Type -> TcS LookupInstResult
 doFunTy clas ty arg_ty ret_ty
-  = do { let preds = map (mk_typeable_pred clas) [arg_ty, ret_ty]
-             build_ev [arg_ev, ret_ev] =
-                 evTypeable ty $ EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev)
-             build_ev _ = panic "TcInteract.doFunTy"
-       ; return $ GenInst preds build_ev True
-       }
+  = return $ OneInst { lir_new_theta = preds
+                     , lir_mk_ev     = mk_ev
+                     , lir_safe_over = True }
+  where
+    preds = map (mk_typeable_pred clas) [arg_ty, ret_ty]
+    mk_ev [arg_ev, ret_ev] = evTypeable ty $
+                             EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev)
+    mk_ev _ = panic "TcInteract.doFunTy"
+
 
 -- | Representation for type constructor applied to some kinds.
 -- 'onlyNamedBndrsApplied' has ensured that this application results in a type
@@ -2723,11 +2782,13 @@ doFunTy clas ty arg_ty ret_ty
 doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcS LookupInstResult
 doTyConApp clas ty tc kind_args
   | Just _ <- tyConRepName_maybe tc
-  = return $ GenInst (map (mk_typeable_pred clas) kind_args)
-                     (\kinds -> evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds))
-                     True
+  = return $ OneInst { lir_new_theta = (map (mk_typeable_pred clas) kind_args)
+                     , lir_mk_ev = mk_ev
+                     , lir_safe_over = True }
   | otherwise
   = return NoInstance
+  where
+    mk_ev kinds = evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds)
 
 -- | Representation for TyCon applications of a concrete kind. We just use the
 -- kind itself, but first we must make sure that we've instantiated all kind-
@@ -2752,9 +2813,13 @@ doTyApp clas ty f tk
   | isForAllTy (typeKind f)
   = return NoInstance -- We can't solve until we know the ctr.
   | otherwise
-  = return $ GenInst (map (mk_typeable_pred clas) [f, tk])
-                     (\[t1,t2] -> evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2))
-                     True
+  = return $ OneInst { lir_new_theta = map (mk_typeable_pred clas) [f, tk]
+                     , lir_mk_ev     = mk_ev
+                     , lir_safe_over = True }
+  where
+    mk_ev [t1,t2] = evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2)
+    mk_ev _ = panic "doTyApp"
+
 
 -- Emit a `Typeable` constraint for the given type.
 mk_typeable_pred :: Class -> Type -> PredType
@@ -2768,7 +2833,9 @@ doTyLit kc t = do { kc_clas <- tcLookupClass kc
                   ; let kc_pred    = mkClassPred kc_clas [ t ]
                         mk_ev [ev] = evTypeable t $ EvTypeableTyLit (EvExpr ev)
                         mk_ev _    = panic "doTyLit"
-                  ; return (GenInst [kc_pred] mk_ev True) }
+                  ; return (OneInst { lir_new_theta = [kc_pred]
+                                    , lir_mk_ev     = mk_ev
+                                    , lir_safe_over   = True }) }
 
 {- Note [Typeable (T a b c)]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2818,15 +2885,15 @@ a TypeRep for them.  For qualified but not polymorphic types, like
 -- See also Note [The equality types story] in TysPrim
 matchLiftedEquality :: [Type] -> TcS LookupInstResult
 matchLiftedEquality args
-  = return (GenInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ]
-                    , lir_mk_ev     = EvExpr . evDFunApp (dataConWrapId heqDataCon) args
+  = return (OneInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ]
+                    , lir_mk_ev     = evDFunApp (dataConWrapId heqDataCon) args
                     , lir_safe_over = True })
 
 -- See also Note [The equality types story] in TysPrim
 matchLiftedCoercible :: [Type] -> TcS LookupInstResult
 matchLiftedCoercible args@[k, t1, t2]
-  = return (GenInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
-                    , lir_mk_ev     = EvExpr . evDFunApp (dataConWrapId coercibleDataCon)
+  = return (OneInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
+                    , lir_mk_ev     = evDFunApp (dataConWrapId coercibleDataCon)
                                                 args
                     , lir_safe_over = True })
   where
@@ -2928,7 +2995,7 @@ matchHasField dflags short_cut clas tys loc
                          -- Use the equality proof to cast the selector Id to
                          -- type (r -> a), then use the newtype coercion to cast
                          -- it to a HasField dictionary.
-                         mk_ev (ev1:evs) = EvExpr $ evSelector sel_id tvs evs `evCast` co
+                         mk_ev (ev1:evs) = evSelector sel_id tvs evs `evCast` co
                            where
                              co = mkTcSubCo (evTermCoercion (EvExpr ev1))
                                       `mkTcTransCo` mkTcSymCo co2
@@ -2944,7 +3011,7 @@ matchHasField dflags short_cut clas tys loc
                      -- it must not be higher-rank.
                    ; if not (isNaughtyRecordSelector sel_id) && isTauTy sel_ty
                      then do { addUsedGRE True gre
-                             ; return GenInst { lir_new_theta = theta
+                             ; return OneInst { lir_new_theta = theta
                                               , lir_mk_ev     = mk_ev
                                               , lir_safe_over = True
                                               } }
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 89741d2c4b..87a9fa395d 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -205,11 +205,11 @@ cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
            ; return (implic { ic_wanted = inner_wanted' }) }
 
 -- | Emits a new Wanted. Deals with both equalities and non-equalities.
-emitWanted :: CtOrigin -> TcPredType -> TcM EvExpr
+emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
 emitWanted origin pty
   = do { ev <- newWanted origin Nothing pty
        ; emitSimple $ mkNonCanonical ev
-       ; return $ ctEvExpr ev }
+       ; return $ ctEvTerm ev }
 
 -- | Emits a new equality constraint
 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
@@ -247,8 +247,9 @@ newDict cls tys
 predTypeOccName :: PredType -> OccName
 predTypeOccName ty = case classifyPredType ty of
     ClassPred cls _ -> mkDictOcc (getOccName cls)
-    EqPred _ _ _    -> mkVarOccFS (fsLit "co")
-    IrredPred _     -> mkVarOccFS (fsLit "irred")
+    EqPred {}       -> mkVarOccFS (fsLit "co")
+    IrredPred {}    -> mkVarOccFS (fsLit "irred")
+    ForAllPred {}   -> mkVarOccFS (fsLit "df")
 
 {-
 ************************************************************************
@@ -1477,7 +1478,7 @@ zonkCt ct
   = ASSERT( not (isCFunEqCan ct) )
   -- We do not expect to see any CFunEqCans, because zonkCt is only called on
   -- unflattened constraints.
-    do { fl' <- zonkCtEvidence (cc_ev ct)
+    do { fl' <- zonkCtEvidence (ctEvidence ct)
        ; return (mkNonCanonical fl') }
 
 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index fcea649d01..f43072f59b 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -116,7 +116,8 @@ 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 evId filtered_prov_dicts)
+                            , mkTyVarTys ex_tvs, prov_theta
+                            , map (EvExpr . evId) filtered_prov_dicts)
                           (map nlHsVar args, map idType args)
                           pat_ty rec_fields }
 tcInferPatSynDecl (XPatSynBind _) = panic "tcInferPatSynDecl"
@@ -539,7 +540,7 @@ tc_patsyn_finish :: Located Name      -- ^ PatSyn Name
                  -> Bool              -- ^ Whether infix
                  -> LPat GhcTc        -- ^ Pattern of the PatSyn
                  -> ([TcTyVarBinder], [PredType], TcEvBinds, [EvVar])
-                 -> ([TcTyVarBinder], [TcType], [PredType], [EvExpr])
+                 -> ([TcTyVarBinder], [TcType], [PredType], [EvTerm])
                  -> ([LHsExpr GhcTcId], [TcType])   -- ^ Pattern arguments and
                                                     -- types
                  -> TcType            -- ^ Pattern type
@@ -625,7 +626,7 @@ tc_patsyn_finish lname dir is_infix lpat'
 tcPatSynMatcher :: Located Name
                 -> LPat GhcTc
                 -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
-                -> ([TcTyVar], [TcType], ThetaType, [EvExpr])
+                -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
                 -> ([LHsExpr GhcTcId], [TcType])
                 -> TcType
                 -> TcM ((Id, Bool), LHsBinds GhcTc)
diff --git a/compiler/typecheck/TcPluginM.hs b/compiler/typecheck/TcPluginM.hs
index b84e5ad832..a112003ef9 100644
--- a/compiler/typecheck/TcPluginM.hs
+++ b/compiler/typecheck/TcPluginM.hs
@@ -69,7 +69,7 @@ import TcRnMonad  ( TcGblEnv, TcLclEnv, Ct, CtLoc, TcPluginM
                   , liftIO, traceTc )
 import TcMType    ( TcTyVar, TcType )
 import TcEnv      ( TcTyThing )
-import TcEvidence ( TcCoercion, CoercionHole
+import TcEvidence ( TcCoercion, CoercionHole, EvTerm(..)
                   , EvExpr, EvBind, mkGivenEvBind )
 import TcRnTypes  ( CtEvidence(..) )
 import Var        ( EvVar )
@@ -173,7 +173,7 @@ newDerived loc pty = return CtDerived { ctev_pred = pty, ctev_loc = loc }
 newGiven :: CtLoc -> PredType -> EvExpr -> TcPluginM CtEvidence
 newGiven loc pty evtm = do
    new_ev <- newEvVar pty
-   setEvBind $ mkGivenEvBind new_ev evtm
+   setEvBind $ mkGivenEvBind new_ev (EvExpr evtm)
    return CtGiven { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc }
 
 -- | Create a fresh evidence variable.
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index fb09fdd923..73b15a5252 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -64,6 +64,9 @@ module TcRnTypes(
         TcIdSigInst(..), TcPatSynInfo(..),
         isPartialSig, hasCompleteSig,
 
+        -- QCInst
+        QCInst(..), isPendingScInst,
+
         -- Canonical constraints
         Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts,
         singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
@@ -78,7 +81,7 @@ module TcRnTypes(
         mkNonCanonical, mkNonCanonicalCt, mkGivens,
         mkIrredCt, mkInsolubleCt,
         ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
-        ctEvExpr, ctEvCoercion, ctEvEvId,
+        ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId,
         tyCoVarsOfCt, tyCoVarsOfCts,
         tyCoVarsOfCtList, tyCoVarsOfCtsList,
 
@@ -1699,6 +1702,26 @@ data Ct
       cc_hole :: Hole
     }
 
+  | CQuantCan QCInst       -- A quantified constraint
+      -- NB: I expect to make more of the cases in Ct
+      --     look like this, with the payload in an
+      --     auxiliary type
+
+------------
+data QCInst  -- A much simplified version of ClsInst
+             -- See Note [Quantified constraints] in TcCanonical
+  = QCI { qci_ev   :: CtEvidence -- Always of type forall tvs. context => ty
+                                 -- Always Given
+        , qci_tvs  :: [TcTyVar]  -- The tvs
+        , qci_pred :: TcPredType -- The ty
+        , qci_pend_sc :: Bool    -- Same as cc_pend_sc flag in CDictCan
+                                 -- Invariant: True => qci_pred is a ClassPred
+    }
+
+instance Outputable QCInst where
+  ppr (QCI { qci_ev = ev }) = ppr ev
+
+------------
 -- | An expression or type hole
 data Hole = ExprHole UnboundVar
             -- ^ Either an out-of-scope variable or a "true" hole in an
@@ -1785,7 +1808,8 @@ mkGivens loc ev_ids
                                        , ctev_loc = loc })
 
 ctEvidence :: Ct -> CtEvidence
-ctEvidence = cc_ev
+ctEvidence (CQuantCan (QCI { qci_ev = ev })) = ev
+ctEvidence ct = cc_ev ct
 
 ctLoc :: Ct -> CtLoc
 ctLoc = ctEvLoc . ctEvidence
@@ -1798,7 +1822,7 @@ ctOrigin = ctLocOrigin . ctLoc
 
 ctPred :: Ct -> PredType
 -- See Note [Ct/evidence invariant]
-ctPred ct = ctEvPred (cc_ev ct)
+ctPred ct = ctEvPred (ctEvidence ct)
 
 ctEvId :: Ct -> EvVar
 -- The evidence Id for this Ct
@@ -1823,7 +1847,7 @@ ctEqRel :: Ct -> EqRel
 ctEqRel = ctEvEqRel . ctEvidence
 
 instance Outputable Ct where
-  ppr ct = ppr (cc_ev ct) <+> parens pp_sort
+  ppr ct = ppr (ctEvidence ct) <+> parens pp_sort
     where
       pp_sort = case ct of
          CTyEqCan {}      -> text "CTyEqCan"
@@ -1836,6 +1860,9 @@ instance Outputable Ct where
             | insol     -> text "CIrredCan(insol)"
             | otherwise -> text "CIrredCan(sol)"
          CHoleCan { cc_hole = hole } -> text "CHoleCan:" <+> ppr hole
+         CQuantCan (QCI { qci_pend_sc = pend_sc })
+            | pend_sc   -> text "CQuantCan(psc)"
+            | otherwise -> text "CQuantCan"
 
 {-
 ************************************************************************
@@ -1866,9 +1893,7 @@ tyCoFVsOfCt (CFunEqCan { cc_tyargs = tys, cc_fsk = fsk })
   = tyCoFVsOfTypes tys `unionFV` FV.unitFV fsk
                        `unionFV` tyCoFVsOfType (tyVarKind fsk)
 tyCoFVsOfCt (CDictCan { cc_tyargs = tys }) = tyCoFVsOfTypes tys
-tyCoFVsOfCt (CIrredCan { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
-tyCoFVsOfCt (CHoleCan { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
-tyCoFVsOfCt (CNonCanonical { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
+tyCoFVsOfCt ct = tyCoFVsOfType (ctPred ct)
 
 -- | Returns free variables of a bag of constraints as a non-deterministic
 -- set. See Note [Deterministic FV] in FV.
@@ -2069,13 +2094,13 @@ NB: we keep *all* derived insolubles under some circumstances:
 -}
 
 isWantedCt :: Ct -> Bool
-isWantedCt = isWanted . cc_ev
+isWantedCt = isWanted . ctEvidence
 
 isGivenCt :: Ct -> Bool
-isGivenCt = isGiven . cc_ev
+isGivenCt = isGiven . ctEvidence
 
 isDerivedCt :: Ct -> Bool
-isDerivedCt = isDerived . cc_ev
+isDerivedCt = isDerived . ctEvidence
 
 isCTyEqCan :: Ct -> Bool
 isCTyEqCan (CTyEqCan {})  = True
@@ -2170,11 +2195,18 @@ isUserTypeErrorCt ct = case getUserTypeErrorMsg ct of
                          _      -> False
 
 isPendingScDict :: Ct -> Maybe Ct
--- Says whether cc_pend_sc is True, AND if so flips the flag
+-- Says whether this is a CDictCan with cc_pend_sc is True,
+-- AND if so flips the flag
 isPendingScDict ct@(CDictCan { cc_pend_sc = True })
                   = Just (ct { cc_pend_sc = False })
 isPendingScDict _ = Nothing
 
+isPendingScInst :: QCInst -> Maybe QCInst
+-- Same as isPrendinScDict, but for QCInsts
+isPendingScInst qci@(QCI { qci_pend_sc = True })
+                  = Just (qci { qci_pend_sc = False })
+isPendingScInst _ = Nothing
+
 setPendingScDict :: Ct -> Ct
 -- Set the cc_pend_sc flag to True
 setPendingScDict ct@(CDictCan { cc_pend_sc = False })
@@ -2722,8 +2754,12 @@ ctEvEqRel = predTypeEqRel . ctEvPred
 ctEvRole :: CtEvidence -> Role
 ctEvRole = eqRelRole . ctEvEqRel
 
+ctEvTerm :: CtEvidence -> EvTerm
+ctEvTerm ev = EvExpr (ctEvExpr ev)
+
 ctEvExpr :: CtEvidence -> EvExpr
-ctEvExpr ev@(CtWanted { ctev_dest = HoleDest _ }) = evCoercion $ ctEvCoercion ev
+ctEvExpr ev@(CtWanted { ctev_dest = HoleDest _ })
+            = Coercion $ ctEvCoercion ev
 ctEvExpr ev = evId (ctEvEvId ev)
 
 ctEvCoercion :: CtEvidence -> Coercion
@@ -2856,7 +2892,7 @@ ctFlavourRole (CFunEqCan { cc_ev = ev })
 ctFlavourRole (CHoleCan { cc_ev = ev })
   = (ctEvFlavour ev, NomEq)
 ctFlavourRole ct
-  = ctEvFlavourRole (cc_ev ct)
+  = ctEvFlavourRole (ctEvidence ct)
 
 {- Note [eqCanRewrite]
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -3224,6 +3260,9 @@ data SkolemInfo
 
   | ReifySkol           -- Bound during Template Haskell reification
 
+  | QuantCtxtSkol       -- Quantified context, e.g.
+                        --   f :: forall c. (forall a. c a => c [a]) => blah
+
   | UnkSkol             -- Unhelpful info (until I improve it)
 
 instance Outputable SkolemInfo where
@@ -3253,6 +3292,8 @@ pprSkolInfo (TyConSkol flav name) = text "the" <+> ppr flav <+> text "declaratio
 pprSkolInfo (DataConSkol name)= text "the data constructor" <+> quotes (ppr name)
 pprSkolInfo ReifySkol         = text "the type being reified"
 
+pprSkolInfo (QuantCtxtSkol {}) = text "a quantified context"
+
 -- UnkSkol
 -- For type variables the others are dealt with by pprSkolTvBinding.
 -- For Insts, these cases should not happen
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index d26275b839..9814358c74 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -16,10 +16,13 @@ module TcSMonad (
     TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
     failTcS, warnTcS, addErrTcS,
     runTcSEqualities,
-    nestTcS, nestImplicTcS, setEvBindsTcS, checkConstraintsTcS,
+    nestTcS, nestImplicTcS, setEvBindsTcS,
+    checkConstraintsTcS, checkTvConstraintsTcS,
 
     runTcPluginTcS, addUsedGRE, addUsedGREs,
 
+    QCInst(..),
+
     -- Tracing etc
     panicTcS, traceTcS,
     traceFireTcS, bumpStepCountTcS, csTraceTcS,
@@ -33,8 +36,8 @@ module TcSMonad (
     newWanted, newWantedEvVar, newWantedNC, newWantedEvVarNC, newDerivedNC,
     newBoundEvVarId,
     unifyTyVar, unflattenFmv, reportUnifications,
-    setEvBind, setWantedEq, setEqIfWanted,
-    setWantedEvTerm, setWantedEvBind, setEvBindIfWanted,
+    setEvBind, setWantedEq,
+    setWantedEvTerm, setEvBindIfWanted,
     newEvVar, newGivenEvVar, newGivenEvVars,
     emitNewDeriveds, emitNewDerivedEq,
     checkReductionDepth,
@@ -53,10 +56,10 @@ module TcSMonad (
     getInertEqs, getInertCans, getInertGivens,
     getInertInsols,
     getTcSInerts, setTcSInerts,
-    matchableGivens, prohibitedSuperClassSolve,
+    matchableGivens, prohibitedSuperClassSolve, mightMatchLater,
     getUnsolvedInerts,
     removeInertCts, getPendingScDicts,
-    addInertCan, addInertEq, insertFunEq,
+    addInertCan, insertFunEq, addInertForAll,
     emitWorkNC, emitWork,
     isImprovable,
 
@@ -137,6 +140,7 @@ import Kind
 import TcType
 import DynFlags
 import Type
+import TyCoRep( coHoleCoVar )
 import Coercion
 import Unify
 
@@ -168,7 +172,7 @@ import Control.Monad
 import qualified Control.Monad.Fail as MonadFail
 import MonadUtils
 import Data.IORef
-import Data.List ( foldl', partition )
+import Data.List ( foldl', partition, mapAccumL )
 
 #if defined(DEBUG)
 import Digraph
@@ -438,17 +442,22 @@ instance Outputable InertSet where
          where
            dicts = bagToList (dictsToBag solved_dicts)
 
+emptyInertCans :: InertCans
+emptyInertCans
+  = IC { inert_count    = 0
+       , inert_eqs      = emptyDVarEnv
+       , inert_dicts    = emptyDicts
+       , inert_safehask = emptyDicts
+       , inert_funeqs   = emptyFunEqs
+       , inert_insts    = []
+       , inert_irreds   = emptyCts }
+
 emptyInert :: InertSet
 emptyInert
-  = IS { inert_cans = IC { inert_count    = 0
-                         , inert_eqs      = emptyDVarEnv
-                         , inert_dicts    = emptyDicts
-                         , inert_safehask = emptyDicts
-                         , inert_funeqs   = emptyFunEqs
-                         , inert_irreds   = emptyCts }
-       , inert_flat_cache    = emptyExactFunEqs
-       , inert_fsks          = []
-       , inert_solved_dicts  = emptyDictMap }
+  = IS { inert_cans         = emptyInertCans
+       , inert_fsks         = []
+       , inert_flat_cache   = emptyExactFunEqs
+       , inert_solved_dicts = emptyDictMap }
 
 
 {- Note [Solved dictionaries]
@@ -480,6 +489,12 @@ Other notes about solved dictionaries
 
 * THe inert_solved_dicts are all Wanteds, never givens
 
+* We only cache dictionaries from top-level instances, not from
+  local quantified constraints.  Reason: if we cached the latter
+  we'd need to purge the cache when bringing new quantified
+  constraints into scope, because quantified constraints "shadow"
+  top-level instances.
+
 Note [Do not add superclasses of solved dictionaries]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Every member of inert_solved_dicts is the result of applying a dictionary
@@ -639,6 +654,8 @@ data InertCans   -- See Note [Detailed InertCans Invariants] for more
               -- All fully rewritten (modulo flavour constraints)
               --     wrt inert_eqs
 
+       , inert_insts :: [QCInst]
+
        , inert_safehask :: DictMap Ct
               -- Failed dictionary resolution due to Safe Haskell overlapping
               -- instances restriction. We keep this separate from inert_dicts
@@ -995,6 +1012,7 @@ instance Outputable InertCans where
   ppr (IC { inert_eqs = eqs
           , inert_funeqs = funeqs, inert_dicts = dicts
           , inert_safehask = safehask, inert_irreds = irreds
+          , inert_insts = insts
           , inert_count = count })
     = braces $ vcat
       [ ppUnless (isEmptyDVarEnv eqs) $
@@ -1008,6 +1026,8 @@ instance Outputable InertCans where
         text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
       , ppUnless (isEmptyCts irreds) $
         text "Irreds =" <+> pprCts irreds
+      , ppUnless (null insts) $
+        text "Given instances =" <+> vcat (map ppr insts)
       , text "Unsolved goals =" <+> int count
       ]
 
@@ -1457,6 +1477,45 @@ equalities arising from injectivity.
 
 {- *********************************************************************
 *                                                                      *
+                   Inert instances: inert_insts
+*                                                                      *
+********************************************************************* -}
+
+addInertForAll :: QCInst -> TcS ()
+-- Add a local Given instance, typically arising from a type signature
+addInertForAll qci
+  = updInertCans $ \ics ->
+    ics { inert_insts = qci : inert_insts ics }
+
+{- Note [Local instances and incoherence]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   f :: forall b c. (Eq b, forall a. Eq a => Eq (c a))
+                 => c b -> Bool
+   f x = x==x
+
+We get [W] Eq (c b), and we must use the local instance to solve it.
+
+BUT that wanted also unifies with the top-level Eq [a] instance,
+and Eq (Maybe a) etc.  We want the local instance to "win", otherwise
+we can't solve the wanted at all.  So we mark it as Incohherent.
+According to Note [Rules for instance lookup] in InstEnv, that'll
+make it win even if there are other instances that unify.
+
+Moreover this is not a hack!  The evidence for this local instance
+will be constructed by GHC at a call site... from the very instances
+that unify with it here.  It is not like an incoherent user-written
+instance which might have utterly different behaviour.
+
+Consdider  f :: Eq a => blah.  If we have [W] Eq a, we certainly
+get it from the Eq a context, without worrying that there are
+lots of top-level instances that unify with [W] Eq a!  We'll use
+those instances to build evidence to pass to f. That's just the
+nullary case of what's happening here.
+-}
+
+{- *********************************************************************
+*                                                                      *
                   Adding an inert
 *                                                                      *
 ************************************************************************
@@ -1495,43 +1554,37 @@ So in kickOutRewritable we look at all the tyvars of the
 CFunEqCan, including the fsk.
 -}
 
-addInertEq :: Ct -> TcS ()
--- This is a key function, because of the kick-out stuff
+addInertCan :: Ct -> TcS ()  -- Constraints *other than* equalities
 -- Precondition: item /is/ canonical
 -- See Note [Adding an equality to the InertCans]
-addInertEq ct
-  = do { traceTcS "addInertEq {" $
-         text "Adding new inert equality:" <+> ppr ct
-
-       ; ics <- getInertCans
-
-       ; ct@(CTyEqCan { cc_tyvar = tv, cc_ev = ev, cc_eq_rel = eq_rel })
-             <- maybeEmitShadow ics ct
-
-       ; (_, ics1) <- kickOutRewritable (ctEvFlavour ev, eq_rel) tv ics
-
-       ; let ics2 = ics1 { inert_eqs   = addTyEq (inert_eqs ics1) tv ct
-                         , inert_count = bumpUnsolvedCount ev (inert_count ics1) }
-       ; setInertCans ics2
-
-       ; traceTcS "addInertEq }" $ empty }
-
---------------
-addInertCan :: Ct -> TcS ()  -- Constraints *other than* equalities
 addInertCan ct
   = do { traceTcS "insertInertCan {" $
-         text "Trying to insert new non-eq inert item:" <+> ppr ct
+         text "Trying to insert new inert item:" <+> ppr ct
 
        ; ics <- getInertCans
-       ; ct <- maybeEmitShadow ics ct
+       ; ct  <- maybeEmitShadow ics ct
+       ; ics <- maybeKickOut ics ct
        ; setInertCans (add_item ics ct)
 
        ; traceTcS "addInertCan }" $ empty }
 
+maybeKickOut :: InertCans -> Ct -> TcS InertCans
+-- For a CTyEqCan, kick out any inert that can be rewritten by the CTyEqCan
+maybeKickOut ics ct
+  | CTyEqCan { cc_tyvar = tv, cc_ev = ev, cc_eq_rel = eq_rel } <- ct
+  = do { (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) tv ics
+       ; return ics' }
+  | otherwise
+  = return ics
+
 add_item :: InertCans -> Ct -> InertCans
 add_item ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
   = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
 
+add_item ics item@(CTyEqCan { cc_tyvar = tv, cc_ev = ev })
+  = ics { inert_eqs   = addTyEq (inert_eqs ics) tv item
+        , inert_count = bumpUnsolvedCount ev (inert_count ics) }
+
 add_item ics@(IC { inert_irreds = irreds, inert_count = count })
          item@(CIrredCan { cc_ev = ev, cc_insol = insoluble })
   = ics { inert_irreds = irreds `Bag.snocBag` item
@@ -1545,8 +1598,7 @@ add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
 
 add_item _ item
   = pprPanic "upd_inert set: can't happen! Inserting " $
-    ppr item   -- CTyEqCan is dealt with by addInertEq
-               -- Can't be CNonCanonical, CHoleCan,
+    ppr item   -- Can't be CNonCanonical, CHoleCan,
                -- because they only land in inert_irreds
 
 bumpUnsolvedCount :: CtEvidence -> Int -> Int
@@ -1580,12 +1632,14 @@ kick_out_rewritable :: CtFlavourRole  -- Flavour/role of the equality that
                     -> InertCans
                     -> (WorkList, InertCans)
 -- See Note [kickOutRewritable]
-kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
-                                        , inert_dicts    = dictmap
-                                        , inert_safehask = safehask
-                                        , inert_funeqs   = funeqmap
-                                        , inert_irreds   = irreds
-                                        , inert_count    = n })
+kick_out_rewritable new_fr new_tv
+                    ics@(IC { inert_eqs      = tv_eqs
+                            , inert_dicts    = dictmap
+                            , inert_safehask = safehask
+                            , inert_funeqs   = funeqmap
+                            , inert_irreds   = irreds
+                            , inert_insts    = old_insts
+                            , inert_count    = n })
   | not (new_fr `eqMayRewriteFR` new_fr)
   = (emptyWorkList, ics)
         -- If new_fr can't rewrite itself, it can't rewrite
@@ -1601,6 +1655,7 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
                        , inert_safehask = safehask   -- ??
                        , inert_funeqs   = feqs_in
                        , inert_irreds   = irs_in
+                       , inert_insts    = insts_in
                        , inert_count    = n - workListWantedCount kicked_out }
 
     kicked_out :: WorkList
@@ -1613,7 +1668,8 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
     kicked_out = foldrBag extendWorkListCt
                           (emptyWorkList { wl_eqs    = tv_eqs_out
                                          , wl_funeqs = feqs_out })
-                          (dicts_out `andCts` irs_out)
+                          ((dicts_out `andCts` irs_out)
+                            `extendCtsList` insts_out)
 
     (tv_eqs_out, tv_eqs_in) = foldDVarEnv kick_out_eqs ([], emptyDVarEnv) tv_eqs
     (feqs_out,   feqs_in)   = partitionFunEqs  kick_out_ct funeqmap
@@ -1624,6 +1680,22 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
       -- Of course we must kick out irreducibles like (c a), in case
       -- we can rewrite 'c' to something more useful
 
+    -- Kick-out for inert instances
+    -- See Note [Quantified constraints] in TcCanonical
+    insts_out :: [Ct]
+    insts_in  :: [QCInst]
+    (insts_out, insts_in)
+       | fr_may_rewrite (Given, NomEq)  -- All the insts are Givens
+       = partitionWith kick_out_qci old_insts
+       | otherwise
+       = ([], old_insts)
+    kick_out_qci qci
+      | let ev = qci_ev qci
+      , fr_can_rewrite_ty NomEq (ctEvPred (qci_ev qci))
+      = Left (mkNonCanonical ev)
+      | otherwise
+      = Right qci
+
     (_, new_role) = new_fr
 
     fr_can_rewrite_ty :: EqRel -> Type -> Bool
@@ -1868,14 +1940,17 @@ getPendingScDicts :: TcS [Ct]
 -- Set the flag to False in the inert set, and return that Ct
 getPendingScDicts = updRetInertCans get_sc_dicts
   where
-    get_sc_dicts ic@(IC { inert_dicts = dicts })
-      = (sc_pend_dicts, ic')
+    get_sc_dicts ic@(IC { inert_dicts = dicts, inert_insts = insts })
+      = (sc_pend_insts ++ sc_pend_dicts, ic')
       where
-        ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts }
+        ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts
+                 , inert_insts = insts' }
 
         sc_pend_dicts :: [Ct]
         sc_pend_dicts = foldDicts get_pending dicts []
 
+        (sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts
+
     get_pending :: Ct -> [Ct] -> [Ct]  -- Get dicts with cc_pend_sc = True
                                        -- but flipping the flag
     get_pending dict dicts
@@ -1887,6 +1962,13 @@ getPendingScDicts = updRetInertCans get_sc_dicts
         = addDict dicts cls tys ct
     add ct _ = pprPanic "getPendingScDicts" (ppr ct)
 
+    get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
+    get_pending_inst cts qci
+       | Just qci' <- isPendingScInst qci
+       = (CQuantCan qci' : cts, qci')
+       | otherwise
+       = (cts, qci)
+
 getUnsolvedInerts :: TcS ( Bag Implication
                          , Cts     -- Tyvar eqs: a ~ ty
                          , Cts     -- Fun eqs:   F a ~ ty
@@ -1995,7 +2077,7 @@ getNoGivenEqs tclvl skol_tvs
 -- Given might overlap with an instance. See Note [Instance and Given overlap]
 -- in TcInteract.
 matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
-matchableGivens loc_w pred (IS { inert_cans = inert_cans })
+matchableGivens loc_w pred_w (IS { inert_cans = inert_cans })
   = filterBag matchable_given all_relevant_givens
   where
     -- just look in class constraints and irreds. matchableGivens does get called
@@ -2004,7 +2086,7 @@ matchableGivens loc_w pred (IS { inert_cans = inert_cans })
     -- non-canonical -- that is, irreducible -- equalities.
     all_relevant_givens :: Cts
     all_relevant_givens
-      | Just (clas, _) <- getClassPredTys_maybe pred
+      | Just (clas, _) <- getClassPredTys_maybe pred_w
       = findDictsByClass (inert_dicts inert_cans) clas
         `unionBags` inert_irreds inert_cans
       | otherwise
@@ -2012,16 +2094,17 @@ matchableGivens loc_w pred (IS { inert_cans = inert_cans })
 
     matchable_given :: Ct -> Bool
     matchable_given ct
-      | CtGiven { ctev_loc = loc_g } <- ctev
-      , Just _ <- tcUnifyTys bind_meta_tv [ctEvPred ctev] [pred]
-      , not (prohibitedSuperClassSolve loc_g loc_w)
-      = True
+      | CtGiven { ctev_loc = loc_g, ctev_pred = pred_g } <- ctEvidence ct
+      = mightMatchLater pred_g loc_g pred_w loc_w
 
       | otherwise
       = False
-      where
-        ctev = cc_ev ct
 
+mightMatchLater :: TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
+mightMatchLater given_pred given_loc wanted_pred wanted_loc
+  =  not (prohibitedSuperClassSolve given_loc wanted_loc)
+  && isJust (tcUnifyTys bind_meta_tv [given_pred] [wanted_pred])
+  where
     bind_meta_tv :: TcTyVar -> BindFlag
     -- Any meta tyvar may be unified later, so we treat it as
     -- bindable when unifying with givens. That ensures that we
@@ -2134,6 +2217,7 @@ removeInertCt is ct =
     CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty } ->
       is { inert_eqs    = delTyEq (inert_eqs is) x ty }
 
+    CQuantCan {}     -> panic "removeInertCt: CQuantCan"
     CIrredCan {}     -> panic "removeInertCt: CIrredEvCan"
     CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
     CHoleCan {}      -> panic "removeInertCt: CHoleCan"
@@ -2662,9 +2746,10 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
                    , tcs_count         = count
                    } ->
     do { inerts <- TcM.readTcRef old_inert_var
-       ; let nest_inert = emptyInert { inert_cans         = inert_cans inerts
-                                     , inert_solved_dicts = inert_solved_dicts inerts }
-                          -- See Note [Do not inherit the flat cache]
+       ; let nest_inert = emptyInert
+                            { inert_cans = inert_cans inerts
+                            , inert_solved_dicts = inert_solved_dicts inerts }
+                              -- See Note [Do not inherit the flat cache]
        ; new_inert_var <- TcM.newTcRef nest_inert
        ; new_wl_var    <- TcM.newTcRef emptyWorkList
        ; let nest_env = TcSEnv { tcs_ev_binds      = ref
@@ -2724,28 +2809,30 @@ nestTcS (TcS thing_inside)
 
        ; return res }
 
-checkConstraintsTcS :: SkolemInfo
-                    -> [TcTyVar]        -- Skolems
-                    -> TcS result
-                    -> TcS result
--- Just like TcUnify.checkTvConstraints, but in the TcS monnad,
--- using the work-list to gather the constraints
-checkConstraintsTcS skol_info skol_tvs (TcS thing_inside)
+checkTvConstraintsTcS :: SkolemInfo
+                      -> [TcTyVar]        -- Skolems
+                      -> TcS (result, Cts)
+                      -> TcS result
+-- Just like TcUnify.checkTvConstraints, but
+--   - In the TcS monnad
+--   - The thing-inside should not put things in the work-list
+--     Instead, it returns the Wanted constraints it needs
+--   - No 'givens', and no TcEvBinds; this is type-level constraints only
+checkTvConstraintsTcS skol_info skol_tvs (TcS thing_inside)
   = TcS $ \ tcs_env ->
-    do { new_wl_var <- TcM.newTcRef emptyWorkList
-       ; let new_tcs_env = tcs_env { tcs_worklist = new_wl_var }
+    do { let wl_panic  = pprPanic "TcSMonad.buildImplication" $
+                         ppr skol_info $$ ppr skol_tvs
+                         -- This panic checks that the thing-inside
+                         -- does not emit any work-list constraints
+             new_tcs_env = tcs_env { tcs_worklist = wl_panic }
 
-       ; (res, new_tclvl) <- TcM.pushTcLevelM $
-                             thing_inside new_tcs_env
+       ; ((res, wanteds), new_tclvl) <- TcM.pushTcLevelM $
+                                        thing_inside new_tcs_env
 
-       ; wl@WL { wl_eqs = eqs } <- TcM.readTcRef new_wl_var
-       ; ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) &&
-                  null (wl_implics wl), ppr wl )
-         unless (null eqs) $
+       ; unless (null wanteds) $
          do { tcl_env <- TcM.getLclEnv
             ; ev_binds_var <- TcM.newNoTcEvBinds
-            ; let wc  = WC { wc_simple = listToCts eqs
-                           , wc_impl   = emptyBag }
+            ; let wc = emptyWC { wc_simple = wanteds }
                   imp = newImplication { ic_tclvl  = new_tclvl
                                        , ic_skols  = skol_tvs
                                        , ic_wanted = wc
@@ -2759,6 +2846,47 @@ checkConstraintsTcS skol_info skol_tvs (TcS thing_inside)
 
       ; return res }
 
+checkConstraintsTcS :: SkolemInfo
+                    -> [TcTyVar]        -- Skolems
+                    -> [EvVar]          -- Givens
+                    -> TcS (result, Cts)
+                    -> TcS (result, TcEvBinds)
+-- Just like checkConstraintsTcS, but
+--   - In the TcS monnad
+--   - The thing-inside should not put things in the work-list
+--     Instead, it returns the Wanted constraints it needs
+--   - I did not bother to put in the fast-path for
+--     empty-skols/empty-givens, or for empty-wanteds, because
+--     this function is used only for "quantified constraints" in
+--     with both tests are pretty much guaranteed to fail
+checkConstraintsTcS skol_info skol_tvs given (TcS thing_inside)
+  = TcS $ \ tcs_env ->
+    do { let wl_panic  = pprPanic "TcSMonad.buildImplication" $
+                         ppr skol_info $$ ppr skol_tvs
+                         -- This panic checks that the thing-inside
+                         -- does not emit any work-list constraints
+             new_tcs_env = tcs_env { tcs_worklist = wl_panic }
+
+       ; ((res, wanteds), new_tclvl) <- TcM.pushTcLevelM $
+                                        thing_inside new_tcs_env
+
+       ; tcl_env <- TcM.getLclEnv
+       ; ev_binds_var <- TcM.newTcEvBinds
+       ; let wc = emptyWC { wc_simple = wanteds }
+             imp = newImplication { ic_tclvl  = new_tclvl
+                                  , ic_skols  = skol_tvs
+                                  , ic_given  = given
+                                  , ic_wanted = wc
+                                  , ic_binds  = ev_binds_var
+                                  , ic_env    = tcl_env
+                                  , ic_info   = skol_info }
+
+           -- Add the implication to the work-list
+       ; TcM.updTcRef (tcs_worklist tcs_env)
+                      (extendWorkListImplic (unitBag imp))
+
+       ; return (res, TcEvBinds ev_binds_var) }
+
 {-
 Note [Propagate the solved dictionaries]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -3076,7 +3204,7 @@ dischargeFunEq (CtGiven { ctev_evar = old_evar, ctev_loc = loc }) fsk co xi
 
 dischargeFunEq ev@(CtWanted { ctev_dest = dest }) fmv co xi
   = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
-    do { setWantedEvTerm dest (EvExpr (evCoercion co))
+    do { setWantedEvTerm dest (evCoercion co)
        ; unflattenFmv fmv xi
        ; n_kicked <- kickOutAfterUnification fmv
        ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ pprKicked n_kicked) }
@@ -3173,28 +3301,25 @@ setWantedEq (HoleDest hole) co
        ; wrapTcS $ TcM.fillCoercionHole hole co }
 setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq" (ppr ev)
 
--- | Equalities only
-setEqIfWanted :: CtEvidence -> Coercion -> TcS ()
-setEqIfWanted (CtWanted { ctev_dest = dest }) co = setWantedEq dest co
-setEqIfWanted _ _ = return ()
-
--- | Good for equalities and non-equalities
+-- | Good for both equalities and non-equalities
 setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
 setWantedEvTerm (HoleDest hole) tm
-  = do { let co = evTermCoercion tm
-       ; useVars (coVarsOfCo co)
+  | Just co <- evTermCoercion_maybe tm
+  = do { useVars (coVarsOfCo co)
        ; wrapTcS $ TcM.fillCoercionHole hole co }
-setWantedEvTerm (EvVarDest ev) tm = setWantedEvBind ev tm
+  | otherwise
+  = do { let co_var = coHoleCoVar hole
+       ; setEvBind (mkWantedEvBind co_var tm)
+       ; wrapTcS $ TcM.fillCoercionHole hole (mkTcCoVarCo co_var) }
 
-setWantedEvBind :: EvVar -> EvTerm -> TcS ()
-setWantedEvBind ev_id tm = setEvBind (mkWantedEvBind ev_id tm)
+setWantedEvTerm (EvVarDest ev_id) tm
+  = setEvBind (mkWantedEvBind ev_id tm)
 
-setEvBindIfWanted :: CtEvidence -> EvExpr -> TcS ()
+setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
 setEvBindIfWanted ev tm
   = case ev of
-      CtWanted { ctev_dest = dest }
-        -> setWantedEvTerm dest (EvExpr tm)
-      _ -> return ()
+      CtWanted { ctev_dest = dest } -> setWantedEvTerm dest tm
+      _                             -> return ()
 
 newTcEvBinds :: TcS EvBindsVar
 newTcEvBinds = wrapTcS TcM.newTcEvBinds
@@ -3205,7 +3330,7 @@ newNoTcEvBinds = wrapTcS TcM.newNoTcEvBinds
 newEvVar :: TcPredType -> TcS EvVar
 newEvVar pred = wrapTcS (TcM.newEvVar pred)
 
-newGivenEvVar :: CtLoc -> (TcPredType, EvExpr) -> TcS CtEvidence
+newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
 -- Make a new variable of the given PredType,
 -- immediately bind it to the given term
 -- and return its CtEvidence
@@ -3216,13 +3341,13 @@ newGivenEvVar loc (pred, rhs)
 
 -- | Make a new 'Id' of the given type, bound (in the monad's EvBinds) to the
 -- given term
-newBoundEvVarId :: TcPredType -> EvExpr -> TcS EvVar
+newBoundEvVarId :: TcPredType -> EvTerm -> TcS EvVar
 newBoundEvVarId pred rhs
   = do { new_ev <- newEvVar pred
        ; setEvBind (mkGivenEvBind new_ev rhs)
        ; return new_ev }
 
-newGivenEvVars :: CtLoc -> [(TcPredType, EvExpr)] -> TcS [CtEvidence]
+newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
 newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts
 
 emitNewWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS Coercion
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index e6c00aea4a..bd04fd5b9c 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -254,7 +254,7 @@ defaultCallStacks wanteds
   defaultCallStack ct
     | ClassPred cls tys <- classifyPredType (ctPred ct)
     , Just {} <- isCallStackPred cls tys
-    = do { solveCallStack (cc_ev ct) EvCsEmpty
+    = do { solveCallStack (ctEvidence ct) EvCsEmpty
          ; return Nothing }
 
   defaultCallStack ct
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index f5f7532075..21d030c060 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -1718,7 +1718,7 @@ tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
 --     df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
 --
 -- Also NB splitFunTys, not tcSplitFunTys;
--- the latter  specifically stops at PredTy arguments,
+-- the latter specifically stops at PredTy arguments,
 -- and we don't want to do that here
 tcSplitDFunTy ty
   = case tcSplitForAllTys ty   of { (tvs, rho)    ->
@@ -1990,6 +1990,7 @@ pickQuantifiablePreds qtvs theta
 
           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
@@ -2094,6 +2095,7 @@ isImprovementPred ty
       EqPred ReprEq _ _  -> False
       ClassPred cls _    -> classHasFds cls
       IrredPred {}       -> True -- Might have equalities after reduction?
+      ForAllPred {}      -> False
 
 {- Note [Expanding superclasses]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index ab31e2ef7f..1e15f658bd 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -10,7 +10,7 @@ module TcValidity (
   ContextKind(..), expectedKindInCtxt,
   checkValidTheta, checkValidFamPats,
   checkValidInstance, checkValidInstHead, validDerivPred,
-  checkInstTermination, checkTySynRhs,
+  checkTySynRhs,
   ClsInstInfo, checkValidCoAxiom, checkValidCoAxBranch,
   checkValidTyFamEqn,
   arityErr, badATErr,
@@ -441,7 +441,8 @@ rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank
 rankZeroMonoType   = MonoType (text "Perhaps you intended to use RankNTypes or Rank2Types")
 tyConArgMonoType   = MonoType (text "GHC doesn't yet support impredicative polymorphism")
 synArgMonoType     = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms")
-constraintMonoType = MonoType (text "A constraint must be a monotype")
+constraintMonoType = MonoType (vcat [ text "A constraint must be a monotype"
+                                    , text "Perhaps you intended to use QuantifiedConstraints" ])
 
 funArgResRank :: Rank -> (Rank, Rank)             -- Function argument and result
 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
@@ -727,8 +728,13 @@ check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
 -- Check the validity of a predicate in a signature
 -- See Note [Validity checking for constraints]
 check_pred_ty env dflags ctxt pred
-  = do { check_type env SigmaCtxt constraintMonoType pred
+  = do { check_type env SigmaCtxt rank pred
        ; check_pred_help False env dflags ctxt pred }
+  where
+    rank | xopt LangExt.QuantifiedConstraints dflags
+         = ArbitraryRank
+         | otherwise
+         = constraintMonoType
 
 check_pred_help :: Bool    -- True <=> under a type synonym
                 -> TidyEnv
@@ -1334,7 +1340,7 @@ checkValidInstance ctxt hs_type ty
         ; undecidable_ok <- xoptM LangExt.UndecidableInstances
         ; if undecidable_ok
           then checkAmbiguity ctxt ty
-          else checkInstTermination inst_tys theta
+          else checkInstTermination theta tau
 
         ; traceTc "cvi 2" (ppr ty)
 
@@ -1376,42 +1382,50 @@ The underlying idea is that
     context has fewer type constructors than the head.
 -}
 
-checkInstTermination :: [TcType] -> ThetaType -> TcM ()
+checkInstTermination :: ThetaType -> TcPredType -> TcM ()
 -- See Note [Paterson conditions]
-checkInstTermination tys theta
-  = check_preds theta
+checkInstTermination theta head_pred
+  = check_preds emptyVarSet theta
   where
-   head_fvs  = fvTypes tys
-   head_size = sizeTypes tys
+   head_fvs  = fvType head_pred
+   head_size = sizeType head_pred
 
-   check_preds :: [PredType] -> TcM ()
-   check_preds preds = mapM_ check preds
+   check_preds :: VarSet -> [PredType] -> TcM ()
+   check_preds foralld_tvs preds = mapM_ (check foralld_tvs) preds
 
-   check :: PredType -> TcM ()
-   check pred
+   check :: VarSet -> PredType -> TcM ()
+   check foralld_tvs pred
      = case classifyPredType pred of
          EqPred {}    -> return ()  -- See Trac #4200.
-         IrredPred {} -> check2 pred (sizeType pred)
+         IrredPred {} -> check2 foralld_tvs pred (sizeType pred)
          ClassPred cls tys
            | isTerminatingClass cls
            -> return ()
 
            | isCTupleClass cls  -- Look inside tuple predicates; Trac #8359
-           -> check_preds tys
+           -> check_preds foralld_tvs tys
+
+           | otherwise          -- Other ClassPreds
+           -> check2 foralld_tvs pred bogus_size
+           where
+              bogus_size = 1 + sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys)
+                               -- See Note [Invisible arguments and termination]
 
-           | otherwise
-           -> check2 pred (sizeTypes $ filterOutInvisibleTypes (classTyCon cls) tys)
-                       -- Other ClassPreds
+         ForAllPred tvs theta pred
+           -> do { check (foralld_tvs `extendVarSetList` binderVars tvs) pred
+                 ; checkInstTermination theta pred }
 
-   check2 pred pred_size
+   check2 foralld_tvs pred pred_size
      | not (null bad_tvs)     = addErrTc (noMoreMsg bad_tvs what)
      | not (isTyFamFree pred) = addErrTc (nestedMsg what)
-     | pred_size >= head_size = addErrTc (smallerMsg what)
+     | pred_size >= head_size = traceTc "check2" (ppr pred $$ ppr pred_size $$ ppr head_pred $$ ppr head_size)
+     >> addErrTc (smallerMsg what)
      | otherwise              = return ()
      -- isTyFamFree: see Note [Type families in instance contexts]
      where
         what    = text "constraint" <+> quotes (ppr pred)
-        bad_tvs = fvType pred \\ head_fvs
+        bad_tvs = filterOut (`elemVarSet` foralld_tvs) (fvType pred)
+                  \\ head_fvs
 
 smallerMsg :: SDoc -> SDoc
 smallerMsg what
@@ -1557,6 +1571,20 @@ Here the instance is kind-indexed and really looks like
       type F (k->k) (b::k->k) = Int
 But if the 'b' didn't scope, we would make F's instance too
 poly-kinded.
+
+Note [Invisible arguments and termination]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When checking the ​Paterson conditions for termination an instance
+declaration, we check for the number of "constructors and variables"
+in the instance head and constraints. Question: Do we look at
+
+ * All the arguments, visible or invisible?
+ * Just the visible arguments?
+
+I think both will ensure termination, provided we are consistent.
+Currently we are /not/ consistent, which is really a bug.  It's
+described in Trac #15177, which contains a number of examples.
+The suspicious bits are the calls to filterOutInvisibleTypes.
 -}
 
 -- | Extra information about the parent instance declaration, needed
@@ -1753,30 +1781,33 @@ checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs pp_lhs loc
 
          -- We have a decidable instance unless otherwise permitted
        ; undecidable_ok <- xoptM LangExt.UndecidableInstances
+       ; traceTc "checkVTFE" (pp_lhs $$ ppr rhs $$ ppr (tcTyFamInsts rhs))
        ; unless undecidable_ok $
-           mapM_ addErrTc (checkFamInstRhs typats (tcTyFamInsts rhs)) }
+           mapM_ addErrTc (checkFamInstRhs fam_tc typats (tcTyFamInsts rhs)) }
 
 -- Make sure that each type family application is
 --   (1) strictly smaller than the lhs,
 --   (2) mentions no type variable more often than the lhs, and
 --   (3) does not contain any further type family instances.
 --
-checkFamInstRhs :: [Type]                  -- lhs
-                -> [(TyCon, [Type])]       -- type family instances
+checkFamInstRhs :: TyCon -> [Type]         -- LHS
+                -> [(TyCon, [Type])]       -- type family calls in RHS
                 -> [MsgDoc]
-checkFamInstRhs lhsTys famInsts
+checkFamInstRhs tc lhsTys famInsts
   = mapMaybe check famInsts
   where
-   size = sizeTypes lhsTys
-   fvs  = fvTypes lhsTys
+   lhs_size = sizeTyConAppArgs tc lhsTys
+   fvs      = fvTypes lhsTys
    check (tc, tys)
       | not (all isTyFamFree tys) = Just (nestedMsg what)
       | not (null bad_tvs)        = Just (noMoreMsg bad_tvs what)
-      | size <= sizeTypes tys     = Just (smallerMsg what)
+      | lhs_size <= fam_app_size  = Just (smallerMsg what)
       | otherwise                 = Nothing
       where
-        what    = text "type family application" <+> quotes (pprType (TyConApp tc tys))
-        bad_tvs = fvTypes tys \\ fvs
+        what         = text "type family application"
+                       <+> quotes (pprType (TyConApp tc tys))
+        bad_tvs      = fvTypes tys \\ fvs
+        fam_app_size = sizeTyConAppArgs tc tys
 
 checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar]
                   -> [Type]   -- ^ patterns the user wrote
@@ -1974,7 +2005,7 @@ sizeType :: Type -> Int
 -- Size of a type: the number of variables and constructors
 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
 sizeType (TyVarTy {})      = 1
-sizeType (TyConApp _ tys)  = sizeTypes tys + 1
+sizeType (TyConApp tc tys) = 1 + sizeTyConAppArgs tc tys
 sizeType (LitTy {})        = 1
 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
@@ -1983,16 +2014,17 @@ sizeType (CastTy ty _)     = sizeType ty
 sizeType (CoercionTy _)    = 1
 
 sizeTypes :: [Type] -> Int
-sizeTypes = sum . map sizeType
+sizeTypes = foldr ((+) . sizeType) 0
+
+sizeTyConAppArgs :: TyCon -> [Type] -> Int
+sizeTyConAppArgs _tc tys = sizeTypes tys -- (filterOutInvisibleTypes tc tys)
+                           -- See Note [Invisible arguments and termination]
 
 -- Size of a predicate
 --
 -- We are considering whether class constraints terminate.
 -- Equality constraints and constraints for the implicit
 -- parameter class always terminate so it is safe to say "size 0".
--- (Implicit parameter constraints always terminate because
--- there are no instances for them---they are only solved by
--- "local instances" in expressions).
 -- See Trac #4200.
 sizePred :: PredType -> Int
 sizePred ty = goClass ty
@@ -2002,14 +2034,19 @@ sizePred ty = goClass ty
     go (ClassPred cls tys')
       | isTerminatingClass cls = 0
       | otherwise = sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys')
-    go (EqPred {})        = 0
-    go (IrredPred ty)     = sizeType ty
+                    -- The filtering looks bogus
+                    -- See Note [Invisible arguments and termination]
+    go (EqPred {})           = 0
+    go (IrredPred ty)        = sizeType ty
+    go (ForAllPred _ _ pred) = goClass pred
 
 -- | When this says "True", ignore this class constraint during
 -- a termination check
 isTerminatingClass :: Class -> Bool
 isTerminatingClass cls
-  = isIPClass cls
+  = isIPClass cls    -- Implicit parameter constraints always terminate because
+                     -- there are no instances for them --- they are only solved
+                     -- by "local instances" in expressions
     || cls `hasKey` typeableClassKey
     || cls `hasKey` coercibleTyConKey
     || cls `hasKey` eqTyConKey
diff --git a/compiler/types/Class.hs b/compiler/types/Class.hs
index aa95f13ac3..a50135bd7b 100644
--- a/compiler/types/Class.hs
+++ b/compiler/types/Class.hs
@@ -17,7 +17,7 @@ module Class (
         mkClass, mkAbstractClass, classTyVars, classArity,
         classKey, className, classATs, classATItems, classTyCon, classMethods,
         classOpItems, classBigSig, classExtraBigSig, classTvsFds, classSCTheta,
-        classAllSelIds, classSCSelId, classMinimalDef, classHasFds,
+        classAllSelIds, classSCSelId, classSCSelIds, classMinimalDef, classHasFds,
         isAbstractClass,
     ) where
 
@@ -107,23 +107,23 @@ data ClassBody
         -- Superclasses: eg: (F a ~ b, F b ~ G a, Eq a, Show b)
         -- We need value-level selectors for both the dictionary
         -- superclasses and the equality superclasses
-        classSCThetaStuff :: [PredType],     -- Immediate superclasses,
-        classSCSels  :: [Id],           -- Selector functions to extract the
+        cls_sc_theta :: [PredType],     -- Immediate superclasses,
+        cls_sc_sel_ids :: [Id],          -- Selector functions to extract the
                                         --   superclasses from a
                                         --   dictionary of this class
         -- Associated types
-        classATStuff :: [ClassATItem],  -- Associated type families
+        cls_ats :: [ClassATItem],  -- Associated type families
 
         -- Class operations (methods, not superclasses)
-        classOpStuff :: [ClassOpItem],  -- Ordered by tag
+        cls_ops :: [ClassOpItem],  -- Ordered by tag
 
         -- Minimal complete definition
-        classMinimalDefStuff :: ClassMinimalDef
+        cls_min_def :: ClassMinimalDef
     }
     -- TODO: maybe super classes should be allowed in abstract class definitions
 
 classMinimalDef :: Class -> ClassMinimalDef
-classMinimalDef Class{ classBody = ConcreteClass{ classMinimalDefStuff = d } } = d
+classMinimalDef Class{ classBody = ConcreteClass{ cls_min_def = d } } = d
 classMinimalDef _ = mkTrue -- TODO: make sure this is the right direction
 
 {-
@@ -181,11 +181,11 @@ mkClass cls_name tyvars fds super_classes superdict_sels at_stuff
             classTyVars  = tyvars,
             classFunDeps = fds,
             classBody = ConcreteClass {
-                    classSCThetaStuff = super_classes,
-                    classSCSels  = superdict_sels,
-                    classATStuff = at_stuff,
-                    classOpStuff = op_stuff,
-                    classMinimalDefStuff = mindef
+                    cls_sc_theta = super_classes,
+                    cls_sc_sel_ids = superdict_sels,
+                    cls_ats  = at_stuff,
+                    cls_ops  = op_stuff,
+                    cls_min_def = mindef
                 },
             classTyCon   = tycon }
 
@@ -239,41 +239,47 @@ classArity clas = length (classTyVars clas)
 
 classAllSelIds :: Class -> [Id]
 -- Both superclass-dictionary and method selectors
-classAllSelIds c@(Class { classBody = ConcreteClass { classSCSels = sc_sels }})
+classAllSelIds c@(Class { classBody = ConcreteClass { cls_sc_sel_ids = sc_sels }})
   = sc_sels ++ classMethods c
 classAllSelIds c = ASSERT( null (classMethods c) ) []
 
+classSCSelIds :: Class -> [Id]
+-- Both superclass-dictionary and method selectors
+classSCSelIds (Class { classBody = ConcreteClass { cls_sc_sel_ids = sc_sels }})
+  = sc_sels
+classSCSelIds c = ASSERT( null (classMethods c) ) []
+
 classSCSelId :: Class -> Int -> Id
 -- Get the n'th superclass selector Id
 -- where n is 0-indexed, and counts
 --    *all* superclasses including equalities
-classSCSelId (Class { classBody = ConcreteClass { classSCSels = sc_sels } }) n
+classSCSelId (Class { classBody = ConcreteClass { cls_sc_sel_ids = sc_sels } }) n
   = ASSERT( n >= 0 && lengthExceeds sc_sels n )
     sc_sels !! n
 classSCSelId c n = pprPanic "classSCSelId" (ppr c <+> ppr n)
 
 classMethods :: Class -> [Id]
-classMethods (Class { classBody = ConcreteClass { classOpStuff = op_stuff } })
+classMethods (Class { classBody = ConcreteClass { cls_ops = op_stuff } })
   = [op_sel | (op_sel, _) <- op_stuff]
 classMethods _ = []
 
 classOpItems :: Class -> [ClassOpItem]
-classOpItems (Class { classBody = ConcreteClass { classOpStuff = op_stuff }})
+classOpItems (Class { classBody = ConcreteClass { cls_ops = op_stuff }})
   = op_stuff
 classOpItems _ = []
 
 classATs :: Class -> [TyCon]
-classATs (Class { classBody = ConcreteClass { classATStuff = at_stuff } })
+classATs (Class { classBody = ConcreteClass { cls_ats = at_stuff } })
   = [tc | ATI tc _ <- at_stuff]
 classATs _ = []
 
 classATItems :: Class -> [ClassATItem]
-classATItems (Class { classBody = ConcreteClass { classATStuff = at_stuff }})
+classATItems (Class { classBody = ConcreteClass { cls_ats = at_stuff }})
   = at_stuff
 classATItems _ = []
 
 classSCTheta :: Class -> [PredType]
-classSCTheta (Class { classBody = ConcreteClass { classSCThetaStuff = theta_stuff }})
+classSCTheta (Class { classBody = ConcreteClass { cls_sc_theta = theta_stuff }})
   = theta_stuff
 classSCTheta _ = []
 
@@ -289,9 +295,9 @@ classBigSig (Class {classTyVars = tyvars,
   = (tyvars, [], [], [])
 classBigSig (Class {classTyVars = tyvars,
                     classBody = ConcreteClass {
-                        classSCThetaStuff = sc_theta,
-                        classSCSels = sc_sels,
-                        classOpStuff = op_stuff
+                        cls_sc_theta = sc_theta,
+                        cls_sc_sel_ids = sc_sels,
+                        cls_ops  = op_stuff
                     }})
   = (tyvars, sc_theta, sc_sels, op_stuff)
 
@@ -301,8 +307,8 @@ classExtraBigSig (Class {classTyVars = tyvars, classFunDeps = fundeps,
   = (tyvars, fundeps, [], [], [], [])
 classExtraBigSig (Class {classTyVars = tyvars, classFunDeps = fundeps,
                          classBody = ConcreteClass {
-                             classSCThetaStuff = sc_theta, classSCSels = sc_sels,
-                             classATStuff = ats, classOpStuff = op_stuff
+                             cls_sc_theta = sc_theta, cls_sc_sel_ids = sc_sels,
+                             cls_ats = ats, cls_ops = op_stuff
                          }})
   = (tyvars, fundeps, sc_theta, sc_sels, ats, op_stuff)
 
diff --git a/compiler/types/InstEnv.hs b/compiler/types/InstEnv.hs
index 6f065e9ec5..d05294b197 100644
--- a/compiler/types/InstEnv.hs
+++ b/compiler/types/InstEnv.hs
@@ -18,9 +18,12 @@ module InstEnv (
         fuzzyClsInstCmp, orphNamesOfClsInst,
 
         InstEnvs(..), VisibleOrphanModules, InstEnv,
-        emptyInstEnv, extendInstEnv, deleteFromInstEnv, identicalClsInstHead,
+        emptyInstEnv, extendInstEnv,
+        deleteFromInstEnv, deleteDFunFromInstEnv,
+        identicalClsInstHead,
         extendInstEnvList, lookupUniqueInstEnv, lookupInstEnv, instEnvElts,
-        memberInstEnv, instIsVisible,
+        memberInstEnv,
+        instIsVisible,
         classInstances, instanceBindFun,
         instanceCantMatch, roughMatchTcs,
         isOverlappable, isOverlapping, isIncoherent
@@ -432,11 +435,11 @@ instIsVisible vis_mods ispec
   -- NB: Instances from the interactive package always are visible. We can't
   -- add interactive modules to the set since we keep creating new ones
   -- as a GHCi session progresses.
-  | isInteractiveModule mod     = True
-  | IsOrphan <- is_orphan ispec = mod `elemModuleSet` vis_mods
-  | otherwise                   = True
-  where
-    mod = nameModule $ is_dfun_name ispec
+  = case nameModule_maybe (is_dfun_name ispec) of
+      Nothing -> True
+      Just mod | isInteractiveModule mod     -> True
+               | IsOrphan <- is_orphan ispec -> mod `elemModuleSet` vis_mods
+               | otherwise                   -> True
 
 classInstances :: InstEnvs -> Class -> [ClsInst]
 classInstances (InstEnvs { ie_global = pkg_ie, ie_local = home_ie, ie_visible = vis_mods }) cls
@@ -471,6 +474,15 @@ deleteFromInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm })
   where
     adjust (ClsIE items) = ClsIE (filterOut (identicalClsInstHead ins_item) items)
 
+deleteDFunFromInstEnv :: InstEnv -> DFunId -> InstEnv
+-- Delete a specific instance fron an InstEnv
+deleteDFunFromInstEnv inst_env dfun
+  = adjustUDFM adjust inst_env cls
+  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
 -- ^ True when when the instance heads are the same
 -- e.g.  both are   Eq [(a,b)]
@@ -549,23 +561,38 @@ instance declaration itself, controlled as follows:
 Now suppose that, in some client module, we are searching for an instance
 of the target constraint (C ty1 .. tyn). The search works like this.
 
- * Find all instances I that match the target constraint; that is, the
-   target constraint is a substitution instance of I. These instance
-   declarations are the candidates.
+*  Find all instances `I` that *match* the target constraint; that is, the
+   target constraint is a substitution instance of `I`. These instance
+   declarations are the *candidates*.
+
+*  Eliminate any candidate `IX` for which both of the following hold:
 
- * Find all non-candidate instances that unify with the target
-   constraint. Such non-candidates instances might match when the
-   target constraint is further instantiated. If all of them are
-   incoherent, proceed; if not, the search fails.
+   -  There is another candidate `IY` that is strictly more specific; that
+      is, `IY` is a substitution instance of `IX` but not vice versa.
 
- * Eliminate any candidate IX for which both of the following hold:
-   * There is another candidate IY that is strictly more specific;
-     that is, IY is a substitution instance of IX but not vice versa.
+   -  Either `IX` is *overlappable*, or `IY` is *overlapping*. (This
+      "either/or" design, rather than a "both/and" design, allow a
+      client to deliberately override an instance from a library,
+      without requiring a change to the library.)
 
-   * Either IX is overlappable or IY is overlapping.
+-  If exactly one non-incoherent candidate remains, select it. If all
+   remaining candidates are incoherent, select an arbitrary one.
+   Otherwise the search fails (i.e. when more than one surviving
+   candidate is not incoherent).
 
- * If only one candidate remains, pick it. Otherwise if all remaining
-   candidates are incoherent, pick an arbitrary candidate. Otherwise fail.
+-  If the selected candidate (from the previous step) is incoherent, the
+   search succeeds, returning that candidate.
+
+-  If not, find all instances that *unify* with the target constraint,
+   but do not *match* it. Such non-candidate instances might match when
+   the target constraint is further instantiated. If all of them are
+   incoherent, the search succeeds, returning the selected candidate; if
+   not, the search fails.
+
+Notice that these rules are not influenced by flag settings in the
+client module, where the instances are *used*. These rules make it
+possible for a library author to design a library that relies on
+overlapping instances without the client having to know.
 
 Note [Overlapping instances]   (NB: these notes are quite old)
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -676,7 +703,7 @@ prematurely chosing a generic instance when a more specific one
 exists.
 
 --Jeff
-v
+
 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
 this test.  Suppose the instance envt had
     ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
@@ -741,7 +768,8 @@ 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
+                   [ClsInst])      -- 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]
 -- in an InstEnv that has entries for
@@ -778,7 +806,8 @@ lookupInstEnv' ie vis_mods cls tys
       = find ((item, map (lookupTyVar subst) tpl_tvs) : ms) us rest
 
         -- Does not match, so next check whether the things unify
-        -- See Note [Overlapping instances] and Note [Incoherent instances]
+        -- See Note [Overlapping instances]
+        -- Ignore ones that are incoherent: Note [Incoherent instances]
       | isIncoherent item
       = find ms us rest
 
diff --git a/compiler/types/Kind.hs b/compiler/types/Kind.hs
index 88ed114fe6..58e38f267e 100644
--- a/compiler/types/Kind.hs
+++ b/compiler/types/Kind.hs
@@ -95,6 +95,8 @@ returnsConstraintKind = returnsTyCon constraintKindTyConKey
 
 -- | Tests whether the given kind (which should look like @TYPE x@)
 -- is something other than a constructor tree (that is, constructors at every node).
+-- E.g.  True of   TYPE k, TYPE (F Int)
+--       False of  TYPE 'LiftedRep
 isKindLevPoly :: Kind -> Bool
 isKindLevPoly k = ASSERT2( isStarKind k || _is_type, ppr k )
                       -- the isStarKind check is necessary b/c of Constraint
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 9963208809..8450cd2f84 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1726,9 +1726,12 @@ eqRelRole :: EqRel -> Role
 eqRelRole NomEq  = Nominal
 eqRelRole ReprEq = Representational
 
-data PredTree = ClassPred Class [Type]
-              | EqPred EqRel Type Type
-              | IrredPred PredType
+data PredTree
+  = ClassPred Class [Type]
+  | EqPred EqRel Type Type
+  | IrredPred PredType
+  | ForAllPred [TyVarBinder] [PredType] PredType
+     -- ForAllPred: see Note [Quantified constraints] in TcCanonical
   -- NB: There is no TuplePred case
   --     Tuple predicates like (Eq a, Ord b) are just treated
   --     as ClassPred, as if we had a tuple class with two superclasses
@@ -1737,11 +1740,20 @@ data PredTree = ClassPred Class [Type]
 classifyPredType :: PredType -> PredTree
 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
     Just (tc, [_, _, ty1, ty2])
-      | tc `hasKey` eqReprPrimTyConKey    -> EqPred ReprEq ty1 ty2
-      | tc `hasKey` eqPrimTyConKey        -> EqPred NomEq ty1 ty2
+      | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
+      | tc `hasKey` eqPrimTyConKey     -> EqPred NomEq ty1 ty2
+
     Just (tc, tys)
-      | Just clas <- tyConClass_maybe tc  -> ClassPred clas tys
-    _                                     -> IrredPred ev_ty
+      | Just clas <- tyConClass_maybe tc
+      -> ClassPred clas tys
+
+    _ | (tvs, rho) <- splitForAllTyVarBndrs ev_ty
+      , (theta, pred) <- splitFunTys rho
+      , not (null tvs && null theta)
+      -> ForAllPred tvs theta pred
+
+      | otherwise
+      -> IrredPred ev_ty
 
 getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type])
 getClassPredTys ty = case getClassPredTys_maybe ty of
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 8b99d624e1..9395cbbe55 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -9407,8 +9407,8 @@ the type level:
     GHC.TypeLits> natVal (lg (Proxy :: Proxy 2) (Proxy :: Proxy 8))
     3
 
-Constraints in types
-====================
+Equality constraints, Coercible, and the kind Constraint
+========================================================
 
 .. _equality-constraints:
 
@@ -9567,6 +9567,262 @@ contexts and superclasses, but to do so you must use
 :extension:`UndecidableInstances` to signal that you don't mind if the type
 checker fails to terminate.
 
+Quantified constraints
+======================
+
+The extension :extension:`QuantifiedConstraints` introduces **quantified constraints**,
+which give a new level of expressiveness in constraints. For example, consider ::
+
+ data Rose f a = Branch a (f (Rose f a))
+
+ instance (Eq a, ???) => Eq (Rose f a)
+   where
+     (Branch x1 c1) == (Branch x2 c2)
+        = x1==x1 && c1==c2
+
+From the ``x1==x2`` we need ``Eq a``, which is fine.  From ``c1==c2`` we need ``Eq (f (Rose f a))`` which
+is *not* fine in Haskell today; we have no way to solve such a constraint.
+
+:extension:`QuantifiedConstraints` lets us write this ::
+
+ instance (Eq a, forall b. (Eq b) => Eq (f b))
+        => Eq (Rose f a)
+   where
+     (Branch x1 c1) == (Branch x2 c2)
+        = x1==x1 && c1==c2
+
+Here, the quantified constraint ``forall b. (Eq b) => Eq (f b)`` behaves
+a bit like a local instance declaration, and makes the instance typeable.
+
+The paper `Quantified class constraints <http://i.cs.hku.hk/~bruno//papers/hs2017.pdf>`_ (by Bottu, Karachalias, Schrijvers, Oliveira, Wadler, Haskell Symposium 2017) describes this feature in technical detail, with examples, and so is a primary reference source for this proposal.
+
+Motivation
+----------------
+Introducing quantified constraints offers two main benefits:
+
+- Firstly, they enable terminating resolution where this was not possible before.  Consider for instance the following instance declaration for the general rose datatype ::
+
+   data Rose f x = Rose x (f (Rose f x))
+
+   instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where
+     (Rose x1 rs1) == (Rose x2 rs2) = x1 == x2 && rs1 == rs2
+
+  This extension allows to write constraints of the form ``forall b. Eq b => Eq (f b)``,
+  which is needed to solve the ``Eq (f (Rose f x))`` constraint arising from the
+  second usage of the ``(==)`` method.
+
+- Secondly, quantified constraints allow for more concise and precise specifications. As an example, consider the MTL type class for monad transformers::
+
+   class Trans t where
+     lift :: Monad m => m a -> (t m) a
+
+  The developer knows that a monad transformer takes a monad ``m`` into a new monad ``t m``.
+  But this is property is not formally specified in the above declaration.
+  This omission becomes an issue when defining monad transformer composition::
+
+    newtype (t1 * t2) m a = C { runC :: t1 (t2 m) a }
+
+    instance (Trans t1, Trans t2) => Trans (t1 * t2) where
+      lift = C . lift . lift
+
+  The goal here is to ``lift`` from monad ``m`` to ``t2 m`` and
+  then ``lift`` this again into ``t1 (t2 m)``.
+  However, this second ``lift`` can only be accepted when ``(t2 m)`` is a monad
+  and there is no way of establishing that this fact universally holds.
+
+  Quantified constraints enable this property to be made explicit in the ``Trans``
+  class declaration::
+
+    class (forall m. Monad m => Monad (t m)) => Trans t where
+      lift :: Monad m => m a -> (t m) a
+
+THe idea is very old; see Seciton 7 of `Derivable type classes <https://www.microsoft.com/en-us/research/publication/derivable-type-classes/>`_.
+
+Syntax changes
+----------------
+
+`Haskell 2010 <https://www.haskell.org/onlinereport/haskell2010/haskellch10.html#x17-18000010.5>`_ defines a ``context`` (the bit to the left of ``=>`` in a type) like this ::
+
+ context ::= class
+         |   ( class1, ..., classn )
+
+ class ::= qtycls tyvar
+        |  qtycls (tyvar atype1 ... atypen)
+
+We to extend ``class`` (warning: this is a rather confusingly named non-terminal symbol) with two extra forms, namely precisely what can appear in an instance declaration ::
+
+ class ::= ...
+       | context => qtycls inst
+       | context => tyvar inst
+
+The definition of ``inst`` is unchanged from the Haskell Report (roughly, just a type).
+That is the only syntactic change to the language.
+
+Notes:
+
+- Where GHC allows extensions instance declarations we allow exactly the same extensions to this new form of ``class``.  Specifically, with ``ExplicitForAll`` and ``MultiParameterTypeClasses`` the syntax becomes ::
+
+    class ::= ...
+           | [forall tyavrs .] context => qtycls inst1 ... instn
+           | [forall tyavrs .] context => tyvar inst1 ... instn
+
+  Note that an explicit ``forall`` is often absolutely essential. Consider the rose-tree example ::
+
+    instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where ...
+
+  Without the ``forall b``, the type variable ``b`` would be quantified over the whole instance declaration, which is not what is intended.
+
+- One of these new quantified constraints can appear anywhere that any other constraint can, not just in instance declarations.  Notably, it can appear in a type signature for a value binding, data constructor, or expression.  For example ::
+
+   f :: (Eq a, forall b. Eq b => Eq (f b)) => Rose f a -> Rose f a -> Bool
+   f t1 t2 = not (t1 == t2)
+
+- The form with a type variable at the head allows this::
+
+   instance (forall xx. c (Free c xx)) => Monad (Free c) where
+       Free f >>= g = f g
+
+  See `Iceland Jack's summary <https://ghc.haskell.org/trac/ghc/ticket/14733#comment:6>`_.  The key point is that the bit to the right of the `=>` may be headed by a type *variable* (`c` in this case), rather than a class.  It should not be one of the forall'd variables, though.
+
+  (NB: this goes beyond what is described in `the paper <http://i.cs.hku.hk/~bruno//papers/hs2017.pdf>`_, but does not seem to introduce any new technical difficulties.)
+
+
+Typing changes
+----------------
+
+See `the paper <http://i.cs.hku.hk/~bruno//papers/hs2017.pdf>`_.
+
+Superclasses
+----------------
+
+Suppose we have::
+
+     f :: forall m. (forall a. Ord a => Ord (m a)) => m Int -> Bool
+     f x = x == x
+
+From the ``x==x`` we need an ``Eq (m Int)`` constraint, but the context only gives us a way to figure out ``Ord (m a)`` constraints.  But from the given constraint ``forall a. Ord a => Ord (m a)`` we derive a second given constraint ``forall a. Ord a => Eq (m a)``, and from that we can readily solve ``Eq (m Int)``.  This process is very similar to the way that superclasses already work: given an ``Ord a`` constraint we derive a second given ``Eq a`` constraint.
+
+NB: This treatment of superclasses goes beyond `the paper <http://i.cs.hku.hk/~bruno//papers/hs2017.pdf>`_, but is specifically desired by users.
+
+Overlap
+-------------
+
+Quantified constraints can potentially lead to overlapping local axioms.
+Consider for instance the following example::
+
+ class A a where {}
+ class B a where {}
+ class C a where {}
+ class (A a => C a) => D a where {}
+ class (B a => C a) => E a where {}
+
+ class C a => F a where {}
+ instance (B a, D a, E a) => F a where {}
+
+When type checking the instance declaration for ``F a``,
+we need to check that the superclass ``C`` of ``F`` holds.
+We thus try to entail the constraint ``C a`` under the theory containing:
+
+- The instance axioms : ``(B a, D a, E a) => F a``
+- The local axioms from the instance context : ``B a``, ``D a`` and ``E a``
+- The closure of the superclass relation over these local axioms : ``A a => C a`` and ``B a => C a``
+
+However, the ``A a => C a`` and ``B a => C a`` axioms both match the wanted constraint ``C a``.
+There are several possible approaches for handling these overlapping local axioms:
+
+- **Pick first**.  We can simply select the **first matching axiom** we encounter.
+  In the above example, this would be ``A a => C a``.
+  We'd then need to entail ``A a``, for which we have no matching axioms available, causing the above program to be rejected.
+
+  But suppose we made a slight adjustment to the order of the instance context, putting ``E a`` before ``D a``::
+
+   instance (B a, E a, D a) => F a where {}
+
+  The first matching axiom we encounter while entailing ``C a``, is ``B a => C a``.
+  We have a local axiom ``B a`` available, so now the program is suddenly accepted.
+  This behaviour, where the ordering of an instance context determines
+  whether or not the program is accepted, seems rather confusing for the developer.
+
+- **Reject if in doubt**.  An alternative approach would be to check for overlapping axioms,
+  when solving a constraint.
+  When multiple matching axioms are discovered, we **reject the program**.
+  This approach is a bit conservative, in that it may reject working programs.
+  But it seem much more transparent towards the developer, who
+  can be presented with a clear message, explaining why the program is rejected.
+
+- **Backtracking**.  Lastly, a simple form of **backtracking** could be introduced.
+  We simply select the first matching axiom we encounter and when the entailment fails,
+  we backtrack and look for other axioms that might match the wanted constraint.
+
+  This seems the most intuitive and transparent approach towards the developer,
+  who no longer needs to concern himself with the fact that his code might contain
+  overlapping axioms or with the ordering of his instance contexts.  But backtracking
+  would apply equally to ordinary instance selection (in the presence of overlapping
+  instances), so it is a much more pervasive change, with substantial consequences
+  for the type inference engine.
+
+GHC adoptst **Reject if in doubt** for now.  We can see how painful it
+is in practice, and try something more ambitious if necessary.
+
+Instance lookup
+-------------------
+
+In the light of the overlap decision, instance lookup works like this, when
+trying to solve a class constraint ``C t``
+
+1. First see if there is a given un-quantified constraint ``C t``.  If so, use it to solve the constraint.
+
+2. If not, look at all the available given quantified constraints; if exactly one one matches ``C t``, choose it; if more than one matches, report an error.
+
+3. If no quantified constraints match, look up in the global instances, as described in :ref:`instance-resolution` and :ref:`instance-overlap`.
+
+Termination
+---------------
+
+GHC uses the `Paterson Conditions <http://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html#instance-termination-rules>`_ to ensure that instance resolution terminates:
+
+The Paterson Conditions are these: for each class constraint ``(C t1 ... tn)``
+in the context
+
+1. No type variable has more occurrences in the constraint than in
+   the head
+
+2. The constraint has fewer constructors and variables (taken
+   together and counting repetitions) than the head
+
+3. The constraint mentions no type functions. A type function
+   application can in principle expand to a type of arbitrary size,
+   and so are rejected out of hand
+
+How are those rules modified for quantified constraints? In two ways.
+
+- Each quantified constraint, taken by itself, must satisfy the termination rules for an instance declaration.
+
+- After "for each class constraint ``(C t1 ... tn)``", add "or each quantified constraint ``(forall as. context => C t1 .. tn)``"
+
+Note that the second item only at the *head* of the quantified constraint, not its context.  Reason: the head is the new goal that has to be solved if we use the instance declaration.
+
+Of course, ``UndecidableInstances`` lifts the Paterson Conditions, as now.
+
+Coherence
+-----------
+
+Although quantified constraints are a little like local instance declarations, they differ
+in one big way: the local instances are written by the compiler, not the user, and hence
+cannot introduce incoherence.  Consider ::
+
+  f :: (forall a. Eq a => Eq (f a)) => f b -> f Bool
+  f x = ...rhs...
+
+In ``...rhs...`` there is, in effect a local instance for ``Eq (f a)`` for any ``a``.  But
+at a call site for ``f`` the compiler itself produces evidence to pass to ``f``. For example,
+if we called ``f Nothing``, then ``f`` is ``Maybe`` and the compiler must prove (at the
+call site) that ``forall a. Eq a => Eq (Maybe a)`` holds.  It can do this easily, by
+appealing to the existing instance declaration for ``Eq (Maybe a)``.
+
+In short, quantifed constraints do not introduce incoherence.
+
+
 .. _extensions-to-type-signatures:
 
 Extensions to type signatures
diff --git a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
index b3016e167d..e98c871ce4 100644
--- a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
+++ b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
@@ -135,4 +135,5 @@ data Extension
    | MonadFailDesugaring
    | EmptyDataDeriving
    | NumericUnderscores
+   | QuantifiedConstraints
    deriving (Eq, Enum, Show, Generic)
diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index 5ae423086a..5ea91b47d6 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -40,7 +40,8 @@ expectedGhcOnlyExtensions = ["RelaxedLayout",
                              "AlternativeLayoutRule",
                              "AlternativeLayoutRuleTransitional",
                              "EmptyDataDeriving",
-                             "GeneralisedNewtypeDeriving"]
+                             "GeneralisedNewtypeDeriving",
+                             "QuantifiedConstraints"]
 
 expectedCabalOnlyExtensions :: [String]
 expectedCabalOnlyExtensions = ["Generics",
diff --git a/testsuite/tests/quantified-constraints/Makefile b/testsuite/tests/quantified-constraints/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/quantified-constraints/T14833.hs b/testsuite/tests/quantified-constraints/T14833.hs
new file mode 100644
index 0000000000..43b6491def
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T14833.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T14833 where
+
+data Dict c where
+  Dict :: c => Dict c
+
+class    (a => b) => Implies a b
+instance (a => b) => Implies a b
+
+-- Works ok
+iota1 :: (() => a) => Dict a
+iota1 = Dict
+
+iota2 :: Implies () a => Dict a
+iota2 = Dict
+
+{-
+[G] Implies () a
+[G] (() => a)      -- By superclass
+
+[W] a
+-}
diff --git a/testsuite/tests/quantified-constraints/T14835.hs b/testsuite/tests/quantified-constraints/T14835.hs
new file mode 100644
index 0000000000..de9b450b7c
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T14835.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Bug where
+
+data Dict c where
+  Dict :: c => Dict c
+
+class    (a => b) => Implies a b
+instance (a => b) => Implies a b
+
+curryC1 :: ((a, b) => c) => Dict (Implies a (Implies b c))
+curryC1 = Dict
+
+curryC2 :: Implies (a, b) c => Dict (Implies a (Implies b c))
+curryC2 = Dict
diff --git a/testsuite/tests/quantified-constraints/T14863.hs b/testsuite/tests/quantified-constraints/T14863.hs
new file mode 100644
index 0000000000..35e1a14b42
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T14863.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T14863 where
+
+data Dict c where
+  Dict :: c => Dict c
+
+class    (a => b) => Implies a b
+instance (a => b) => Implies a b
+
+uncurryCImpredic1 :: forall a b c. Implies a (b => c) => Dict (Implies (a, b) c)
+uncurryCImpredic1 = Dict
+
+uncurryCImpredic2 :: forall a b c. a => Implies b c => Dict (Implies (a, b) c)
+uncurryCImpredic2 = Dict
+
+uncurryC1 :: forall a b c. (a => b => c) => Dict (Implies (a, b) c)
+uncurryC1 = Dict
+
+uncurryC2 :: forall a b c. Implies a (Implies b c) => Dict (Implies (a, b) c)
+uncurryC2 = Dict
diff --git a/testsuite/tests/quantified-constraints/T14961.hs b/testsuite/tests/quantified-constraints/T14961.hs
new file mode 100644
index 0000000000..6f15ceb572
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T14961.hs
@@ -0,0 +1,98 @@
+{-# LANGUAGE ConstraintKinds           #-}
+{-# LANGUAGE InstanceSigs              #-}
+{-# LANGUAGE FlexibleContexts          #-}
+{-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE MultiParamTypeClasses     #-}
+{-# LANGUAGE RankNTypes                #-}
+{-# LANGUAGE TypeFamilies              #-}
+{-# LANGUAGE TypeFamilyDependencies    #-}
+{-# LANGUAGE TypeInType                #-}
+{-# LANGUAGE TypeOperators             #-}
+{-# LANGUAGE UndecidableInstances      #-}
+{-# LANGUAGE QuantifiedConstraints     #-}
+
+module T14961 where
+
+import           Data.Kind
+
+import           Control.Arrow              (left, right, (&&&), (|||))
+import           Control.Category
+import           Prelude                    hiding (id, (.))
+
+import           Data.Coerce
+
+class    (forall x. f x => g x) => f ~=> g
+instance (forall x. f x => g x) => f ~=> g
+
+type family (#) (p :: Type -> Type -> Type) (ab :: (Type, Type))
+  = (r :: Type) | r -> p ab where
+  p # '(a, b) = p a b
+
+newtype Glass
+  :: ((Type -> Type -> Type) -> Constraint)
+  -> (Type, Type) -> (Type, Type) -> Type where
+  Glass :: (forall p. z p => p # ab -> p # st) -> Glass z st ab
+
+data A_Prism
+
+type family ConstraintOf (tag :: Type)
+  = (r :: (Type -> Type -> Type) -> Constraint) where
+  ConstraintOf A_Prism = Choice
+
+_Left0
+  :: Glass Choice
+       '(Either a x, Either b x)
+       '(a, b)
+_Left0 = Glass left'
+
+_Left1
+  :: c ~=> Choice
+  => Glass c '(Either a x, Either b x) '(a, b)
+_Left1 = Glass left'
+
+-- fails with
+-- • Could not deduce (Choice p)
+-- _Left2
+--   :: (forall p. c p => ConstraintOf A_Prism p)
+--   => Glass c '(Either a x, Either b x) '(a, b)
+-- _Left2 = Glass left'
+
+_Left3
+  :: d ~ ConstraintOf A_Prism
+  => (forall p . c p => d p)
+  => Glass c
+       '(Either a x, Either b x)
+       '(a, b)
+_Left3 = Glass left'
+
+-- fails to typecheck unless at least a partial type signature is provided
+-- l :: c ~=> Choice => Glass c _ _
+-- l = _Left1 . _Left1
+
+newtype Optic o st ab where
+  Optic
+    :: (forall c d. (d ~ ConstraintOf o, c ~=> d) => Glass c st ab)
+    -> Optic o st ab
+
+_Left
+  :: Optic A_Prism
+       '(Either a x, Either b x)
+       '(a, b)
+_Left = Optic _Left1
+
+instance Category (Glass z) where
+  id :: Glass z a a
+  id = Glass id
+
+  (.) :: Glass z uv ab -> Glass z st uv -> Glass z st ab
+  Glass abuv . Glass uvst = Glass (uvst . abuv)
+
+class Profunctor (p :: Type -> Type -> Type) where
+  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
+  lmap :: (a -> b) -> p b c -> p a c
+  rmap :: (b -> c) -> p a b -> p a c
+
+class Profunctor p => Choice (p :: Type -> Type -> Type) where
+  left' :: p a b -> p (Either a c) (Either b c)
+  right' :: p a b -> p (Either c a) (Either c b)
diff --git a/testsuite/tests/quantified-constraints/T2893.hs b/testsuite/tests/quantified-constraints/T2893.hs
new file mode 100644
index 0000000000..ffec2cf72d
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T2893.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE QuantifiedConstraints  #-}
+
+-- Two simple examples that should work
+
+module T2893 where
+
+f :: forall b c. (Eq b, forall a. Eq a => Eq (c a)) => c b -> Bool
+{-# NOINLINE f #-}
+f x = x==x
+
+g x = f [x]
+
+data Rose f x = Rose x (f (Rose f x))
+
+instance (Eq a, forall b. Eq b => Eq (f b))
+      => Eq (Rose f a)  where
+  (Rose x1 rs1) == (Rose x2 rs2)
+     = x1==x2 && rs1 == rs2
diff --git a/testsuite/tests/quantified-constraints/T2893a.hs b/testsuite/tests/quantified-constraints/T2893a.hs
new file mode 100644
index 0000000000..187029fdd5
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T2893a.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE
+    GADTs
+  , FlexibleContexts
+  , RankNTypes
+  , ScopedTypeVariables
+  , QuantifiedConstraints #-}
+
+module T2893a where
+
+import Control.Monad.ST
+import Data.Array.ST
+
+sortM
+  :: forall a s.
+     (Ord a, MArray (STUArray s) a (ST s))
+  => [a]
+  -> ST s [a]
+sortM xs = do
+  arr <- newListArray (1, length xs) xs
+           :: ST s (STUArray s Int a)
+  -- do some in-place sorting here
+  getElems arr
+
+sortP_3
+  :: (Ord a, forall s. MArray (STUArray s) a (ST s))
+  => [a] -> [a]
+sortP_3 xs = runST (sortM xs)
diff --git a/testsuite/tests/quantified-constraints/T2893c.hs b/testsuite/tests/quantified-constraints/T2893c.hs
new file mode 100644
index 0000000000..832d0f8428
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T2893c.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE QuantifiedConstraints  #-}
+
+module T2893c where
+
+data Rose f x = Rose x (f (Rose f x))
+
+instance Eq a => Eq (Rose f a)  where
+  (Rose x1 _) == (Rose x2 _) = x1==x2
+
+-- Needs superclasses
+instance (Ord a, forall b. Ord b => Ord (f b))
+      => Ord (Rose f a)  where
+  (Rose x1 rs1) >= (Rose x2 rs2)
+     = x1 >= x2 && rs1 == rs2
+  a <= b = False  -- Just to suppress the warning
diff --git a/testsuite/tests/quantified-constraints/T9123.hs b/testsuite/tests/quantified-constraints/T9123.hs
new file mode 100644
index 0000000000..130312b150
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T9123.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE InstanceSigs, RoleAnnotations  #-}
+
+module T9123 where
+
+import Data.Coerce
+
+type role Wrap representational nominal
+newtype Wrap m a = Wrap (m a)
+
+class Monad' m where
+  join' :: forall a. m (m a) -> m a
+
+-- Tests the superclass stuff
+instance (forall p q. Coercible p q => Coercible (m p) (m q), Monad' m) => Monad' (Wrap m) where
+  join' :: forall a. Wrap m (Wrap m a) -> Wrap m a
+  join' = coerce @(m (m a) -> m a)
+                 @(Wrap m (Wrap m a) -> Wrap m a)
+                 join'
+
diff --git a/testsuite/tests/quantified-constraints/T9123a.hs b/testsuite/tests/quantified-constraints/T9123a.hs
new file mode 100644
index 0000000000..76379b6c00
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T9123a.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE QuantifiedConstraints, PolyKinds, ScopedTypeVariables
+           , StandaloneDeriving, RoleAnnotations, TypeApplications
+           , UndecidableInstances, InstanceSigs
+           , GeneralizedNewtypeDeriving #-}
+
+module T9123a where
+
+import Data.Coerce
+
+class MyMonad m where
+  join :: m (m a) -> m a
+
+newtype StateT s m a = StateT (s -> m (a, s))
+
+type role StateT nominal representational nominal   -- as inferred
+
+instance MyMonad m => MyMonad (StateT s m) where
+  join = error "urk"  -- A good impl exists, but is not
+                      -- of interest for this test case
+
+newtype IntStateT m a = IntStateT (StateT Int m a)
+
+type role IntStateT representational nominal   -- as inferred
+
+instance (MyMonad m, forall p q. Coercible p q => Coercible (m p) (m q))
+               => MyMonad (IntStateT m) where
+  join :: forall a. IntStateT m (IntStateT m a) -> IntStateT m a
+  join = coerce @(StateT Int m (StateT Int m a) -> StateT Int m a)
+                @(IntStateT  m (IntStateT  m a) -> IntStateT  m a)
+                join
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
new file mode 100644
index 0000000000..71f5b9159a
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -0,0 +1,10 @@
+
+test('T14833', normal, compile, [''])
+test('T14835', normal, compile, [''])
+test('T2893', normal, compile, [''])
+test('T2893a', normal, compile, [''])
+test('T2893c', normal, compile, [''])
+test('T9123', normal, compile, [''])
+test('T14863', normal, compile, [''])
+test('T14961', normal, compile, [''])
+test('T9123a', normal, compile, [''])
diff --git a/testsuite/tests/rebindable/T5908.hs b/testsuite/tests/rebindable/T5908.hs
index 32a4d4e5e7..2666c3371a 100644
--- a/testsuite/tests/rebindable/T5908.hs
+++ b/testsuite/tests/rebindable/T5908.hs
@@ -26,7 +26,7 @@ class Monad m where
   (>>) :: forall e ex x a b . m e ex a -> m ex x b -> m e x b
   return :: a -> m ex ex a
   fail :: String -> m e x a
-  
+
   {-# INLINE (>>) #-}
   m >> k = m >>= \ _ -> k
   fail = error
diff --git a/testsuite/tests/typecheck/should_compile/T14735.hs b/testsuite/tests/typecheck/should_compile/T14735.hs
new file mode 100644
index 0000000000..c48231b7c2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14735.hs
@@ -0,0 +1,30 @@
+{-# Language QuantifiedConstraints #-}
+{-# Language StandaloneDeriving #-}
+{-# Language DataKinds #-}
+{-# Language TypeOperators #-}
+{-# Language GADTs #-}
+{-# Language KindSignatures #-}
+{-# Language FlexibleInstances #-}
+{-# Language UndecidableInstances #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language RankNTypes #-}
+{-# Language ConstraintKinds #-}
+
+module T14735 where
+
+import Data.Kind
+
+data D c where
+  D :: c => D c
+
+newtype a :- b = S (a => D b)
+
+class C1 a b
+class C2 a b
+instance C1 a b => C2 a b
+
+class    (forall xx. f xx) => Limit f
+instance (forall xx. f xx) => Limit f
+
+impl :: Limit (C1 a) :- Limit (C2 a)
+impl = S D
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index d130a69950..43282341cc 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -620,3 +620,5 @@ test('SplitWD', normal, compile, [''])
 #           with -prof using -osuf to set a different object file suffix.
 test('T14441', omit_ways(['profasm']), compile, [''])
 test('T15050', [expect_broken(15050)], compile, [''])
+test('T14735', normal, compile, [''])
+
diff --git a/testsuite/tests/typecheck/should_fail/T7019.stderr b/testsuite/tests/typecheck/should_fail/T7019.stderr
index 2db5bbb90b..09827e458b 100644
--- a/testsuite/tests/typecheck/should_fail/T7019.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7019.stderr
@@ -2,4 +2,5 @@
 T7019.hs:11:1: error:
     • Illegal polymorphic type: forall a. c (Free c a)
       A constraint must be a monotype
+      Perhaps you intended to use QuantifiedConstraints
     • In the type synonym declaration for ‘C’
diff --git a/testsuite/tests/typecheck/should_fail/T7019a.stderr b/testsuite/tests/typecheck/should_fail/T7019a.stderr
index a50fbcf240..e0e0342b61 100644
--- a/testsuite/tests/typecheck/should_fail/T7019a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7019a.stderr
@@ -2,6 +2,7 @@
 T7019a.hs:11:1: error:
     • Illegal polymorphic type: forall b. Context (Associated a b)
       A constraint must be a monotype
+      Perhaps you intended to use QuantifiedConstraints
     • In the context: forall b. Context (Associated a b)
       While checking the super-classes of class ‘Class’
       In the class declaration for ‘Class’
diff --git a/testsuite/tests/typecheck/should_fail/T9196.stderr b/testsuite/tests/typecheck/should_fail/T9196.stderr
index f843c70929..d6ca149f23 100644
--- a/testsuite/tests/typecheck/should_fail/T9196.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9196.stderr
@@ -2,11 +2,11 @@
 T9196.hs:4:6: error:
     • Illegal polymorphic type: forall a1. Eq a1
       A constraint must be a monotype
-    • In the type signature:
-        f :: (forall a. Eq a) => a -> a
+      Perhaps you intended to use QuantifiedConstraints
+    • In the type signature: f :: (forall a. Eq a) => a -> a
 
 T9196.hs:7:6: error:
     • Illegal qualified type: Eq a => Ord a
       A constraint must be a monotype
-    • In the type signature:
-        g :: (Eq a => Ord a) => a -> a
+      Perhaps you intended to use QuantifiedConstraints
+    • In the type signature: g :: (Eq a => Ord a) => a -> a