After talking to Richard

* Use SimplifierStage Void when no ContinueWith
* Fast path for equality classes

8 files changed, 139 insertions, 70 deletions

diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs
index f4c25d6369..c84e93e64c 100644
--- a/compiler/GHC/Tc/Instance/Class.hs
+++ b/compiler/GHC/Tc/Instance/Class.hs
@@ -2,7 +2,7 @@
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 
 module GHC.Tc.Instance.Class (
-     matchGlobalInst,
+     matchGlobalInst, matchEqualityInst,
      ClsInstResult(..),
      safeOverlap, instanceReturnsDictCon,
      AssocInstInfo(..), isNotAssociated,
@@ -127,9 +127,6 @@ matchGlobalInst dflags short_cut clas tys
   | isCTupleClass clas                 = matchCTuple                       clas tys
   | cls_name == typeableClassName      = matchTypeable                     clas tys
   | cls_name == withDictClassName      = matchWithDict                          tys
-  | clas `hasKey` heqTyConKey          = matchHeteroEquality                    tys
-  | clas `hasKey` eqTyConKey           = matchHomoEquality                      tys
-  | clas `hasKey` coercibleTyConKey    = matchCoercible                         tys
   | cls_name == hasFieldClassName      = matchHasField    dflags short_cut clas tys
   | cls_name == unsatisfiableClassName = return NoInstance -- See (B) in Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors
   | otherwise                          = matchInstEnv     dflags short_cut clas tys
@@ -798,33 +795,24 @@ if you'd written
 ***********************************************************************-}
 
 -- See also Note [The equality types story] in GHC.Builtin.Types.Prim
-matchHeteroEquality :: [Type] -> TcM ClsInstResult
--- Solves (t1 ~~ t2)
-matchHeteroEquality args
-  = return (OneInst { cir_new_theta   = [ mkTyConApp eqPrimTyCon args ]
-                    , cir_mk_ev       = evDataConApp heqDataCon args
-                    , cir_coherence   = IsCoherent
-                    , cir_what        = BuiltinEqInstance })
+matchEqualityInst :: Class -> [Type] -> (DataCon, Role, Type, Type)
 
-matchHomoEquality :: [Type] -> TcM ClsInstResult
--- Solves (t1 ~ t2)
-matchHomoEquality args@[k,t1,t2]
-  = return (OneInst { cir_new_theta   = [ mkTyConApp eqPrimTyCon [k,k,t1,t2] ]
-                    , cir_mk_ev       = evDataConApp eqDataCon args
-                    , cir_coherence   = IsCoherent
-                    , cir_what        = BuiltinEqInstance })
-matchHomoEquality args = pprPanic "matchHomoEquality" (ppr args)
+matchEqualityInst cls args
+  | cls `hasKey` eqTyConKey  -- Solves (t1 ~ t2)
+  , [_,t1,t2] <- args
+  = (eqDataCon, Nominal, t1, t2)
+
+  | cls `hasKey` heqTyConKey -- Solves (t1 ~~ t2)
+  , [_,_,t1,t2] <- args
+  = (heqDataCon,  Nominal, t1, t2)
+
+  | cls `hasKey` coercibleTyConKey  -- Solves (Coercible t1 t2)
+  , [_, t1, t2] <- args
+  = (coercibleDataCon, Representational, t1, t2)
+
+  | otherwise
+  = pprPanic "matchEqualityInst" (ppr (mkClassPred cls args))
 
--- See also Note [The equality types story] in GHC.Builtin.Types.Prim
-matchCoercible :: [Type] -> TcM ClsInstResult
-matchCoercible args@[k, t1, t2]
-  = return (OneInst { cir_new_theta   = [ mkTyConApp eqReprPrimTyCon args' ]
-                    , cir_mk_ev       = evDataConApp coercibleDataCon args
-                    , cir_coherence   = IsCoherent
-                    , cir_what        = BuiltinEqInstance })
-  where
-    args' = [k, k, t1, t2]
-matchCoercible args = pprPanic "matchLiftedCoercible" (ppr args)
 
 {- ********************************************************************
 *                                                                     *
diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs
index a329711cad..558ff24002 100644
--- a/compiler/GHC/Tc/Solver/Dict.hs
+++ b/compiler/GHC/Tc/Solver/Dict.hs
@@ -10,9 +10,8 @@ module GHC.Tc.Solver.Dict (
 import GHC.Prelude
 
 import GHC.Tc.Errors.Types
-import GHC.Tc.Utils.TcType
 import GHC.Tc.Instance.FunDeps
-import GHC.Tc.Instance.Class( safeOverlap )
+import GHC.Tc.Instance.Class( safeOverlap, matchEqualityInst )
 import GHC.Tc.Types.Evidence
 import GHC.Tc.Types.Constraint
 import GHC.Tc.Types.Origin
@@ -20,6 +19,8 @@ import GHC.Tc.Types.EvTerm( evCallStack )
 import GHC.Tc.Solver.InertSet
 import GHC.Tc.Solver.Monad
 import GHC.Tc.Solver.Types
+import GHC.Tc.Utils.TcType
+import GHC.Tc.Utils.Unify( uType )
 
 import GHC.Hs.Type( HsIPName(..) )
 
@@ -53,6 +54,7 @@ import GHC.Driver.Session
 import qualified GHC.LanguageExtensions as LangExt
 
 import Data.Maybe ( listToMaybe, mapMaybe, isJust )
+import Data.Void( Void )
 
 import Control.Monad.Trans.Maybe( MaybeT, runMaybeT )
 import Control.Monad.Trans.Class( lift )
@@ -65,15 +67,27 @@ import Control.Monad( mzero, when )
 *                                                                      *
 ********************************************************************* -}
 
-solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage ()
+{- Note [Solving equality classes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We have a special solver for the "equality classes"
+   (t1 ~ t2), (t1 ~~ t2), and (Coercible t1 t2)
+
+      TODO: expand this Note
+-}
+
+solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage Void
 -- NC: this comes from CNonCanonical or CIrredCan
 -- Precondition: already rewritten by inert set
 solveDictNC ev cls tys
+  | isEqualityClass cls
+  = solveEqualityDict ev cls tys
+
+  | otherwise
   = do { simpleStage $ traceTcS "solveDictNC" (ppr (mkClassPred cls tys) $$ ppr ev)
        ; dict_ct <- canDictCt ev cls tys
        ; solveDict dict_ct }
 
-solveDict :: DictCt -> SolverStage ()
+solveDict :: DictCt -> SolverStage Void
 -- Preconditions: `tys` are already rewritten by the inert set
 solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
   = assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
@@ -96,7 +110,7 @@ solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
 
 updInertDicts :: DictCt -> TcS ()
 updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev })
-  = do { -- See [Kick out existing binding for implicit parameter]
+  = do { -- See Note [Shadowing of Implicit Parameters]
        ; when (isGiven ev && isIPClass cls) $
          updInertCans (updDicts (delIPDict dict_ct))
 
@@ -113,19 +127,10 @@ canDictCt ev cls tys
     do { dflags <- getDynFlags
        ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys
          -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
+       ; emitWork (listToBag sc_cts)
 
-       -- For equality classes, /replace/ the current constraint with its
-       -- superclasses, rather than /adding/ them.
-       -- See (NC1) in Note [Naturally coherent classes]
-       ; if isEqualityClass cls
-         then case sc_cts of
-                [ct] -> startAgainWith ct
-                _    -> pprPanic "canDictCt" (ppr cls)
-         else
-
-    do { emitWork (listToBag sc_cts)
        ; continueWith (DictCt { di_ev = ev, di_cls = cls
-                              , di_tys = tys, di_pend_sc = doNotExpand }) } }
+                              , di_tys = tys, di_pend_sc = doNotExpand }) }
          -- doNotExpand: We have already expanded superclasses for /this/ dict
          -- so set the fuel to doNotExpand to avoid repeating expansion
 
@@ -183,10 +188,17 @@ solveCallStack ev ev_cs
        ; setEvBindIfWanted ev IsCoherent ev_tm }
 
 
-{- Note [Kick out existing binding for implicit parameter]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Shadowing of Implicit Parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When we add a new /given/ implicit parameter to the inert set, it /replaces/
-any existing givens for the same implicit parameter.
+any existing givens for the same implicit parameter.  This makes a difference
+in two places:
+
+* In `GHC.Tc.Solver.InertSet.solveOneFromTheOther`, be careful when we have
+   (?x :: ty) in the inert set and an identical (?x :: ty) as the work item.
+
+* In `updInertDicts` in this module, when adding [G] (?x :: ty), remove  any
+  existing [G] (?x :: ty'), regardless of ty'
 
 Example 1:
 
@@ -265,6 +277,37 @@ I can think of two ways to fix this:
 
 {- ******************************************************************************
 *                                                                               *
+                   solveEqualityDict
+*                                                                               *
+****************************************************************************** -}
+
+solveEqualityDict :: CtEvidence -> Class -> [Type] -> SolverStage Void
+-- Precondition: (isEqualityClass cls) True, so cls is (~), (~~), or Coercible
+solveEqualityDict ev cls tys
+  | CtWanted { ctev_dest = dest } <- ev
+  = Stage $
+    do { let (data_con, role, t1, t2) = matchEqualityInst cls tys
+         -- Unify t1~t2, putting anything that can't be solved
+         -- immediately into the work list
+       ; (co, _, _) <- wrapUnifierTcS ev role $ \uenv ->
+                       uType uenv t1 t2
+         -- Set  d :: (t1~t2) = Eq# co
+       ; setWantedEvTerm dest IsCoherent $
+         evDataConApp data_con tys [Coercion co]
+       ; stopWith ev "Solved wanted lifted equality" }
+
+  | CtGiven { ctev_evar = ev_id, ctev_loc = loc } <- ev
+  , [sel_id] <- classSCSelIds cls  -- Equality classes have just one superclass
+  = Stage $
+    do { let sc_pred = classMethodInstTy sel_id tys
+             ev_expr = EvExpr $ Var sel_id `mkTyApps` tys `App` evId ev_id
+       ; given_ev <- newGivenEvVar loc (sc_pred, ev_expr)
+       ; startAgainWith (mkNonCanonical given_ev) }
+  | otherwise
+  = pprPanic "solveEqualityDict" (ppr cls)
+
+{- ******************************************************************************
+*                                                                               *
                    interactDict
 *                                                                               *
 *********************************************************************************
@@ -770,7 +813,6 @@ matchClassInst dflags inerts clas tys loc
 -- whether top level, or local quantified constraints.
 -- See Note [Instance and Given overlap]
   | not (xopt LangExt.IncoherentInstances dflags)
-  , not (naturallyCoherentClass clas)  -- See (NC3) in Note [Naturally coherent classes]
   , not (noMatchableGivenDicts inerts loc clas tys)
   = do { traceTcS "Delaying instance application" $
            vcat [ text "Work item=" <+> pprClassPred clas tys ]
@@ -796,6 +838,7 @@ matchClassInst dflags inerts clas tys loc
   where
     pred = mkClassPred clas tys
 
+{-
 -- | If a class is "naturally coherent", then we needn't worry at all, in any
 -- way, about overlapping/incoherent instances. Just solve the thing!
 -- See Note [Naturally coherent classes]
@@ -803,6 +846,7 @@ matchClassInst dflags inerts clas tys loc
 naturallyCoherentClass :: Class -> Bool
 naturallyCoherentClass cls
   = isCTupleClass cls || isEqualityClass cls
+-}
 
 isEqualityClass :: Class -> Bool
 -- True of (~), (~~), and Coercible
@@ -903,14 +947,15 @@ this:
 (See Note [The equality types story] in GHC.Builtin.Types.Prim.)
 
 PS: the term "naturally coherent" doesn't really seem helpful.
-Perhaps "invertible" or something?  I left it for now though.
+Perhaps "invertible" or "bidirectional" or something?  I left it for
+now though.
 
 For naturally coherent classes:
 
-(NC1) For Givens, when expanding superclasses, we /replace/ the constraint
-  with its superclasses (which, remember, are equally powerful) rather than
-  /adding/ them. This can make a huge difference.  Consider T17836, which
-  has a constraint like
+(NC1) For Givens, when expanding the superclasses of a naturally coherent class,
+  we can /replace/ the constraint with its superclasses (which, remember, are
+  equally powerful) rather than /adding/ them. This can make a huge difference.
+  Consider T17836, which has a constraint like
       forall b,c. a ~ (b,c) =>
         forall d,e. c ~ (d,e) =>
           ...etc...
@@ -923,7 +968,7 @@ For naturally coherent classes:
   Originally I tried this for all naturally-coherent classes, including
   tuples.  But discarding the tuple Given (which "replacing" does) means that
   we may have to reconstruct it for a recursive call, and the optimiser isn't
-  quite clever enought to figure that out: see #10359 and its test case.
+  quite clever enough to figure that out: see #10359 and its test case.
   This is less pressing for equality classes because they have to be unpacked
   strictly, so CSE-ing away the reconstuction works fine.  Hence the use
   of isEqualityClass rather than naturallyCoherentClass in canDictCt.
@@ -944,7 +989,7 @@ For naturally coherent classes:
   so the reduction of the [W] constraint does not risk losing any solutions.
 
   On the other hand, it can be fatal to /fail/ to reduce such equalities
-  on the grounds of Note [Instance and Given overlap], fbecause many good
+  on the grounds of Note [Instance and Given overlap], because many good
   things flow from [W] t1 ~# t2.
 
 The same reasoning applies to
@@ -1923,8 +1968,8 @@ mk_strict_superclasses fuel rec_clss ev@(CtGiven { ctev_evar = evar, ctev_loc =
       | otherwise
       = do { given_ev <- newGivenEvVar sc_loc $
                          mk_given_desc sel_id sc_pred
-           ; assertFuelPrecondition fuel
-             $ mk_superclasses fuel rec_clss given_ev tvs theta sc_pred }
+           ; assertFuelPrecondition fuel $
+             mk_superclasses fuel rec_clss given_ev tvs theta sc_pred }
       where
         sc_pred = classMethodInstTy sel_id tys
 
@@ -1952,7 +1997,7 @@ mk_strict_superclasses fuel rec_clss ev@(CtGiven { ctev_evar = evar, ctev_loc =
             `App` (evId evar `mkVarApps` (tvs ++ dict_ids))
             `mkVarApps` sc_tvs
 
-    sc_loc | naturallyCoherentClass cls
+    sc_loc | isCTupleClass cls
            = loc  -- See (NC2) in Note [Naturally coherent classes]
            | otherwise
            = loc { ctl_origin = mk_sc_origin (ctLocOrigin loc) }
diff --git a/compiler/GHC/Tc/Solver/Equality.hs b/compiler/GHC/Tc/Solver/Equality.hs
index a3cfc18df1..7c9ce3fe42 100644
--- a/compiler/GHC/Tc/Solver/Equality.hs
+++ b/compiler/GHC/Tc/Solver/Equality.hs
@@ -60,7 +60,7 @@ import Data.List  ( zip4 )
 
 import qualified Data.Semigroup as S
 import Data.Bifunctor ( bimap )
-
+import Data.Void( Void )
 
 {- *********************************************************************
 *                                                                      *
@@ -102,7 +102,7 @@ indeed they are!
 -}
 
 solveEquality :: CtEvidence -> EqRel -> Type -> Type
-              -> SolverStage ()
+              -> SolverStage Void
 solveEquality ev eq_rel ty1 ty2
   = do { Pair ty1' ty2' <- zonkEqTypes ev eq_rel ty1 ty2
        ; let ev' | debugIsOn = setCtEvPredType ev $
diff --git a/compiler/GHC/Tc/Solver/Irred.hs b/compiler/GHC/Tc/Solver/Irred.hs
index 8db8241c45..4863bc1ff1 100644
--- a/compiler/GHC/Tc/Solver/Irred.hs
+++ b/compiler/GHC/Tc/Solver/Irred.hs
@@ -21,9 +21,10 @@ import GHC.Types.Basic( SwapFlag(..) )
 
 import GHC.Utils.Outputable
 
-
 import GHC.Data.Bag
 
+import Data.Void( Void )
+
 
 {- *********************************************************************
 *                                                                      *
@@ -31,7 +32,7 @@ import GHC.Data.Bag
 *                                                                      *
 ********************************************************************* -}
 
-solveIrred :: IrredCt -> SolverStage ()
+solveIrred :: IrredCt -> SolverStage Void
 solveIrred irred
   = do { simpleStage $ traceTcS "solveIrred:" (ppr irred)
        ; tryInertIrreds irred
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 2ea316b893..508b7ca17c 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -211,8 +211,9 @@ data StopOrContinue a
   = StartAgain Ct     -- Constraint is not solved, but some unifications
                       --   happened, so go back to the beginning of the pipeline
 
-  | ContinueWith a    -- The constraint was not solved, although it may have
-                      --   been rewritten
+  | ContinueWith !a   -- The constraint was not solved, although it may have
+                      --   been rewritten.  It is strict so that
+                      --   ContinueWith Void can't happen
 
   | Stop CtEvidence   -- The (rewritten) constraint was solved
          SDoc         -- Tells how it was solved
diff --git a/compiler/GHC/Tc/Solver/Solve.hs b/compiler/GHC/Tc/Solver/Solve.hs
index 55f5e0b311..771095583f 100644
--- a/compiler/GHC/Tc/Solver/Solve.hs
+++ b/compiler/GHC/Tc/Solver/Solve.hs
@@ -43,6 +43,7 @@ import Data.List( deleteFirstsBy )
 
 import Control.Monad
 import Data.Semigroup as S
+import Data.Void( Void )
 
 {-
 **********************************************************************
@@ -196,7 +197,10 @@ solveOne workItem
                                ; traceTcS "End solver pipeline }" empty
                                ; return () }
 
-               ContinueWith {} -> pprPanic "Pipeline finished without solving" (ppr ct) }
+               -- ContinueWith can't happen: res :: SolverStage Void
+               -- solveCt either solves the constraint, or puts
+               -- the unsolved constraint in the inert set.
+            }
 
 {- *********************************************************************
 *                                                                      *
@@ -224,7 +228,9 @@ it must be recanonicalized. But we know a bit about its shape from the
 last time through, so we can skip the classification step.
 -}
 
-solveCt :: Ct -> SolverStage ()
+solveCt :: Ct -> SolverStage Void
+-- The Void result tells us that solveCt cannot return
+-- a ContinueWith; it must return Stop or StartAgain.
 solveCt (CNonCanonical ev)                   = solveNC ev
 solveCt (CIrredCan (IrredCt { ir_ev = ev })) = solveNC ev
 
@@ -234,12 +240,18 @@ solveCt (CEqCan (EqCt { eq_ev = ev, eq_eq_rel = eq_rel
 
 solveCt (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
   = do { ev <- rewriteEvidence ev
+         -- It is (much) easier to rewrite and re-classify than to
+         -- rewrite the pieces and build a Reduction that will rewrite
+         -- the whole constraint
        ; case classifyPredType (ctEvPred ev) of
            ForAllPred tvs th p -> Stage $ solveForAll ev tvs th p pend_sc
            _ -> pprPanic "SolveCt" (ppr ev) }
 
 solveCt (CDictCan (DictCt { di_ev = ev, di_pend_sc = pend_sc }))
   = do { ev <- rewriteEvidence ev
+         -- It is easier to rewrite and re-classify than to rewrite
+         -- the pieces and build a Reduction that will rewrite the
+         -- whole constraint
        ; case classifyPredType (ctEvPred ev) of
            ClassPred cls tys
              -> solveDict (DictCt { di_ev = ev, di_cls = cls
@@ -247,7 +259,7 @@ solveCt (CDictCan (DictCt { di_ev = ev, di_pend_sc = pend_sc }))
            _ -> pprPanic "solveCt" (ppr ev) }
 
 ------------------
-solveNC :: CtEvidence -> SolverStage ()
+solveNC :: CtEvidence -> SolverStage Void
 solveNC ev
   = -- Instead of rewriting the evidence before classifying, it's possible we
     -- can make progress without the rewrite. Try this first.
@@ -354,7 +366,7 @@ type signature.
 -}
 
 solveForAllNC :: CtEvidence -> [TcTyVar] -> TcThetaType -> TcPredType
-              -> TcS (StopOrContinue ())
+              -> TcS (StopOrContinue Void)
 -- NC: this came from CNonCanonical, so we have not yet expanded superclasses
 -- Precondition: already rewritten by inert set
 solveForAllNC ev tvs theta pred
@@ -380,7 +392,7 @@ solveForAllNC ev tvs theta pred
     cls_pred_tys_maybe = getClassPredTys_maybe pred
 
 solveForAll :: CtEvidence -> [TcTyVar] -> TcThetaType -> PredType -> ExpansionFuel
-            -> TcS (StopOrContinue ())
+            -> TcS (StopOrContinue Void)
 -- Precondition: already rewritten by inert set
 solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_loc = loc })
             tvs theta pred _fuel
diff --git a/compiler/GHC/Utils/Outputable.hs b/compiler/GHC/Utils/Outputable.hs
index 49c0b10251..8fc1467527 100644
--- a/compiler/GHC/Utils/Outputable.hs
+++ b/compiler/GHC/Utils/Outputable.hs
@@ -906,6 +906,9 @@ class Outputable a where
 -- There's no Outputable for Char; it's too easy to use Outputable
 -- on String and have ppr "hello" rendered as "h,e,l,l,o".
 
+instance Outputable Void where
+    ppr _ = text "<<Void>>"
+
 instance Outputable Bool where
     ppr True  = text "True"
     ppr False = text "False"
diff --git a/testsuite/tests/quantified-constraints/T17267b.hs b/testsuite/tests/quantified-constraints/T17267b.hs
index 82285d0265..5f0ffdf6e1 100644
--- a/testsuite/tests/quantified-constraints/T17267b.hs
+++ b/testsuite/tests/quantified-constraints/T17267b.hs
@@ -14,3 +14,22 @@ uc = oops where
   oops :: (a ~ b => a ~ b) => a -> b
   oops x = x
 
+{-
+Consider the ambiguity check for oops.
+
+[G] (a ~ b => a ~ b)
+[W] (a ~ b => a ~ b)
+==>
+
+[G] (a ~ b => a ~ b)
+[G] (a ~# b)     was [G] (a ~ b) [G] a ~# b
+
+kick out the QC and (old) (a~b)
+[G] (b ~ b => b ~ b)    Quantified constraint
+[G] (a ~# b)     was [G] (b ~ b) [G] a ~# b
+
+[W] (a~b)   DictCt
+
+Wanted is rewritten
+   (b~b)    DictCt
+-}