Two fast paths

* Naturally coherent constraints
* Hole-fits

2 files changed, 138 insertions, 60 deletions

diff --git a/compiler/GHC/Tc/Errors/Hole.hs b/compiler/GHC/Tc/Errors/Hole.hs
index 76929e8c11..5d3f046a15 100644
--- a/compiler/GHC/Tc/Errors/Hole.hs
+++ b/compiler/GHC/Tc/Errors/Hole.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE ExistentialQuantification #-}
 
 module GHC.Tc.Errors.Hole
@@ -40,7 +41,10 @@ import GHC.Tc.Utils.TcMType
 import GHC.Tc.Types.Evidence
 import GHC.Tc.Utils.TcType
 import GHC.Core.Type
+import GHC.Core.TyCon( TyCon, isGenerativeTyCon )
+import GHC.Core.TyCo.Rep( Type(..) )
 import GHC.Core.DataCon
+import GHC.Core.Predicate( Pred(..), classifyPredType, eqRelRole )
 import GHC.Types.Name
 import GHC.Types.Name.Reader
 import GHC.Builtin.Names ( gHC_ERR )
@@ -981,28 +985,33 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
                          tcSubTypeSigma orig (ExprSigCtxt NoRRC) ty hole_ty
      ; traceTc "Checking hole fit {" empty
      ; traceTc "wanteds are: " $ ppr wanted
-     ; if isEmptyWC wanted && isEmptyBag th_relevant_cts
-       then do { traceTc "}" empty
-               ; return (True, wrap) }
-       else do { fresh_binds <- newTcEvBinds
-                -- The relevant constraints may contain HoleDests, so we must
-                -- take care to clone them as well (to avoid #15370).
-               ; cloned_relevants <- mapBagM cloneWantedCtEv th_relevant_cts
-                 -- We wrap the WC in the nested implications, for details, see
-                 -- Note [Checking hole fits]
-               ; let wrapInImpls cts = foldl (flip (setWCAndBinds fresh_binds)) cts th_implics
-                     final_wc  = wrapInImpls $ addSimples wanted $
-                                                          mapBag mkNonCanonical cloned_relevants
-                 -- We add the cloned relevants to the wanteds generated
-                 -- by the call to tcSubType_NC, for details, see
-                 -- Note [Relevant constraints]. There's no need to clone
-                 -- the wanteds, because they are freshly generated by the
-                 -- call to`tcSubtype_NC`.
-               ; traceTc "final_wc is: " $ ppr final_wc
-                 -- See Note [Speeding up valid hole-fits]
-               ; (rem, _) <- tryTc $ runTcSEarlyAbort $ simplifyTopWanteds final_wc
-               ; traceTc "}" empty
-               ; return (any isSolvedWC rem, wrap) } }
+     ; if | isEmptyWC wanted, isEmptyBag th_relevant_cts
+          -> do { traceTc "}" empty
+                ; return (True, wrap) }
+
+          | checkInsoluble wanted
+          -> return (False, wrap)
+
+          | otherwise
+          -> do { fresh_binds <- newTcEvBinds
+                 -- The relevant constraints may contain HoleDests, so we must
+                 -- take care to clone them as well (to avoid #15370).
+                ; cloned_relevants <- mapBagM cloneWantedCtEv th_relevant_cts
+                  -- We wrap the WC in the nested implications, for details, see
+                  -- Note [Checking hole fits]
+                ; let wrapInImpls cts = foldl (flip (setWCAndBinds fresh_binds)) cts th_implics
+                      final_wc  = wrapInImpls $ addSimples wanted $
+                                                           mapBag mkNonCanonical cloned_relevants
+                  -- We add the cloned relevants to the wanteds generated
+                  -- by the call to tcSubType_NC, for details, see
+                  -- Note [Relevant constraints]. There's no need to clone
+                  -- the wanteds, because they are freshly generated by the
+                  -- call to`tcSubtype_NC`.
+                ; traceTc "final_wc is: " $ ppr final_wc
+                  -- See Note [Speeding up valid hole-fits]
+                ; (rem, _) <- tryTc $ runTcSEarlyAbort $ simplifyTopWanteds final_wc
+                ; traceTc "}" empty
+                ; return (any isSolvedWC rem, wrap) } }
   where
     orig = ExprHoleOrigin (hole_occ <$> th_hole)
 
@@ -1012,3 +1021,31 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
                   -> WantedConstraints  -- The new constraints.
     setWCAndBinds binds imp wc
       = mkImplicWC $ unitBag $ imp { ic_wanted = wc , ic_binds = binds }
+
+checkInsoluble :: WantedConstraints -> Bool
+checkInsoluble (WC { wc_simple = simples })
+  = any is_insol simples
+  where
+    is_insol ct = case classifyPredType (ctPred ct) of
+                    EqPred r t1 t2 -> definitelyNotEqual (eqRelRole r) t1 t2
+                    _              -> False
+
+definitelyNotEqual :: Role -> TcType -> TcType -> Bool
+definitelyNotEqual r t1 t2
+  = go t1 t2
+  where
+    go t1 t2
+      | Just t1' <- coreView t1 = go t1' t2
+      | Just t2' <- coreView t2 = go t1 t2'
+
+    go (TyConApp tc _) t2 | isGenerativeTyCon tc r = go_tc tc t2
+    go t1 (TyConApp tc _) | isGenerativeTyCon tc r = go_tc tc t1
+    go (FunTy {ft_af = af1}) (FunTy {ft_af = af2}) = af1 /= af2
+    go _ _ = False
+
+    go_tc :: TyCon -> TcType -> Bool
+    -- The TyCon is generative, and is not a saturated FunTy
+    go_tc tc1 (TyConApp tc2 _) | isGenerativeTyCon tc2 r = tc1 /= tc2
+    go_tc _ (FunTy {})    = True
+    go_tc _ (ForAllTy {}) = True
+    go_tc _ _ = False
\ No newline at end of file
diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs
index 8beff8279c..ae4835c683 100644
--- a/compiler/GHC/Tc/Solver/Dict.hs
+++ b/compiler/GHC/Tc/Solver/Dict.hs
@@ -69,7 +69,7 @@ solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage ()
 -- NC: this comes from CNonCanonical or CIrredCan
 -- Precondition: already rewritten by inert set
 solveDictNC ev cls tys
-  = do { dict_ct <- simpleStage (canDictCt ev cls tys)
+  = do { dict_ct <- canDictCt ev cls tys
        ; solveDict dict_ct }
 
 solveDict :: DictCt -> SolverStage ()
@@ -100,18 +100,29 @@ updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev })
        -- Add the new constraint to the inert set
        ; updInertCans (updDicts (addDict dict_ct)) }
 
-canDictCt :: CtEvidence -> Class -> [Type] -> TcS DictCt
+canDictCt :: CtEvidence -> Class -> [Type] -> SolverStage DictCt
 -- Once-only processing of Dict constraints:
 --   * expand superclasses
 --   * deal with CallStack
 canDictCt ev cls tys
   | isGiven ev  -- See Note [Eagerly expand given superclasses]
-  = do { dflags <- getDynFlags
+  = Stage $
+    do { dflags <- getDynFlags
        ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys
-                   -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
-       ; emitWork (listToBag sc_cts)
-       ; return (DictCt { di_ev = ev, di_cls = cls
-                        , di_tys = tys, di_pend_sc = doNotExpand }) }
+         -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
+
+       -- 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 }) } }
          -- doNotExpand: We have already expanded superclasses for /this/ dict
          -- so set the fuel to doNotExpand to avoid repeating expansion
 
@@ -123,7 +134,8 @@ canDictCt ev cls tys
   -- of solving it directly from a given.
   -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
   -- and Note [Solving CallStack constraints] in GHC.Tc.Solver.Types
-  = do { -- First we emit a new constraint that will capture the
+  = Stage $
+    do { -- First we emit a new constraint that will capture the
          -- given CallStack.
          let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
                             -- We change the origin to IPOccOrigin so
@@ -139,18 +151,19 @@ canDictCt ev cls tys
                                   (ctLocSpan loc) (ctEvExpr new_ev)
        ; solveCallStack ev ev_cs
 
-       ; return (DictCt { di_ev = new_ev, di_cls = cls
-                        , di_tys = tys, di_pend_sc = doNotExpand }) }
+       ; continueWith (DictCt { di_ev = new_ev, di_cls = cls
+                              , di_tys = tys, di_pend_sc = doNotExpand }) }
          -- doNotExpand: No superclasses for class CallStack
          -- See invariants in CDictCan.cc_pend_sc
 
   | otherwise
-  = do { dflags <- getDynFlags
+  = Stage $
+    do { dflags <- getDynFlags
        ; let fuel | classHasSCs cls = wantedsFuel dflags
                   | otherwise       = doNotExpand
                   -- See Invariants in `CCDictCan.cc_pend_sc`
-       ; return (DictCt { di_ev = ev, di_cls = cls
-                        , di_tys = tys, di_pend_sc = fuel }) }
+       ; continueWith (DictCt { di_ev = ev, di_cls = cls
+                              , di_tys = tys, di_pend_sc = fuel }) }
   where
     loc  = ctEvLoc ev
     orig = ctLocOrigin loc
@@ -790,7 +803,7 @@ 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)
+  , 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 ]
@@ -822,8 +835,13 @@ matchClassInst dflags inerts clas tys loc
 -- See also Note [The equality types story] in GHC.Builtin.Types.Prim.
 naturallyCoherentClass :: Class -> Bool
 naturallyCoherentClass cls
-  = isCTupleClass cls
-    || cls `hasKey` heqTyConKey
+  = isCTupleClass cls || isEqualityClass cls
+
+isEqualityClass :: Class -> Bool
+-- True of (~), (~~), and Coercible
+-- These all have a single primitive-equality superclass, either (~N# or ~R#)
+isEqualityClass cls
+  = cls `hasKey` heqTyConKey
     || cls `hasKey` eqTyConKey
     || cls `hasKey` coercibleTyConKey
 
@@ -917,14 +935,50 @@ this:
   instance a ~# b => a ~~ b
 (See Note [The equality types story] in GHC.Builtin.Types.Prim.)
 
-Faced with [W] t1 ~~ t2, it's always OK to reduce it to [W] t1 ~# t2,
-without worrying about Note [Instance and Given overlap].  Why?  Because
-if we had [G] s1 ~~ s2, then we'd get the superclass [G] s1 ~# s2, and
-so the reduction of the [W] constraint does not risk losing any solutions.
+PS: the term "naturally coherent" doesn't really seem helpful.
+Perhaps "invertible" or something?  I left it for now though.
 
-On the other hand, it can be fatal to /fail/ to reduce such
-equalities, on the grounds of Note [Instance and Given overlap],
-because many good things flow from [W] t1 ~# t2.
+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
+      forall b,c. a ~ (b,c) =>
+        forall d,e. c ~ (d,e) =>
+          ...etc...
+  If we just /add/ the superclasses of [G] g1:a ~ (b,c), we'll put
+  [G] g1:(a~(b,c)) in the inert set and emit [G] g2:a ~# (b,c).  That will
+  kick out g1, and it'll be re-inserted as [G] g1':(b,c)~(b,c) which does
+  no good to anyone.  When the implication is deeply nested, this has
+  quadratic cost, and no benefit.  Just replace!
+
+  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.
+  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.
+  A bit ad-hoc.
+
+(NC2) Because of this replacement, we don't need do the fancy footwork
+  of Note [Solving superclass constraints], so the computation of `sc_loc`
+  in `mk_strict_superclasses` can be simpler.
+
+  For tuple predicates, this matters, because their size can be large,
+  and we don't want to add a big class to the size of the dictionaries
+  in the chain. When we get down to a base predicate, we'll include
+  its size. See #10335
+
+(NC3) Faced with [W] t1 ~ t2, it's always OK to reduce it to [W] t1 ~# t2,
+  without worrying about Note [Instance and Given overlap].  Why?  Because
+  if we had [G] s1 ~ s2, then we'd get the superclass [G] s1 ~# s2, and
+  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
+  things flow from [W] t1 ~# t2.
 
 The same reasoning applies to
 
@@ -947,9 +1001,6 @@ And less obviously to:
 
 Examples: T5853, T10432, T5315, T9222, T2627b, T3028b
 
-PS: the term "naturally coherent" doesn't really seem helpful.
-Perhaps "invertible" or something?  I left it for now though.
-
 Note [Local instances and incoherence]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
@@ -1934,18 +1985,8 @@ 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 | isCTupleClass cls
-           = loc   -- For tuple predicates, just take them apart, without
-                   -- adding their (large) size into the chain.  When we
-                   -- get down to a base predicate, we'll include its size.
-                   -- #10335
-
-           |  isEqPredClass cls || cls `hasKey` coercibleTyConKey
-           = loc   -- The only superclasses of ~, ~~, and Coercible are primitive
-                   -- equalities, and they don't use the GivenSCOrigin mechanism
-                   -- detailed in Note [Solving superclass constraints] in
-                   -- GHC.Tc.TyCl.Instance. Skip for a tiny performance win.
-
+    sc_loc | naturallyCoherentClass cls
+           = loc  -- See (NC2) in Note [Naturally coherent classes]
            | otherwise
            = loc { ctl_origin = mk_sc_origin (ctLocOrigin loc) }