[Git][ghc/ghc][master] 2 commits: Desugar bindings in the context of their evidence

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Fri Aug 4 16:24:27 UTC 2023



Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
e2c91bff by Gergő Érdi at 2023-08-03T02:55:46+01:00
Desugar bindings in the context of their evidence

Closes #23172

- - - - -
481f4a46 by Gergő Érdi at 2023-08-03T07:48:43+01:00
Add flag to `-f{no-}specialise-incoherents` to enable/disable specialisation of
incoherent instances

Fixes #23287

- - - - -


25 changed files:

- compiler/GHC/Core/InstEnv.hs
- compiler/GHC/Driver/DynFlags.hs
- compiler/GHC/Driver/Flags.hs
- compiler/GHC/Driver/Session.hs
- compiler/GHC/Hs/Decls.hs
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/HsToCore/Monad.hs
- compiler/GHC/HsToCore/Quote.hs
- compiler/GHC/HsToCore/Types.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Gen/Splice.hs
- compiler/GHC/Tc/Instance/Class.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Irred.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Types/Basic.hs
- docs/users_guide/using-optimisation.rst
- testsuite/tests/simplCore/should_run/T22448.hs
- utils/check-exact/ExactPrint.hs


Changes:

=====================================
compiler/GHC/Core/InstEnv.hs
=====================================
@@ -11,7 +11,7 @@ The bits common to GHC.Tc.TyCl.Instance and GHC.Tc.Deriv.
 
 module GHC.Core.InstEnv (
         DFunId, InstMatch, ClsInstLookupResult,
-        Coherence(..), PotentialUnifiers(..), getPotentialUnifiers, nullUnifiers,
+        Canonical, PotentialUnifiers(..), getPotentialUnifiers, nullUnifiers,
         OverlapFlag(..), OverlapMode(..), setOverlapModeMaybe,
         ClsInst(..), DFunInstType, pprInstance, pprInstanceHdr, pprDFunId, pprInstances,
         instanceWarning, instanceHead, instanceSig, mkLocalClsInst, mkImportedClsInst,
@@ -128,10 +128,11 @@ fuzzyClsInstCmp x y =
     cmp (RM_KnownTc _, RM_WildCard)   = GT
     cmp (RM_KnownTc x, RM_KnownTc y) = stableNameCmp x y
 
-isOverlappable, isOverlapping, isIncoherent :: ClsInst -> Bool
+isOverlappable, isOverlapping, isIncoherent, isNonCanonical :: ClsInst -> Bool
 isOverlappable i = hasOverlappableFlag (overlapMode (is_flag i))
 isOverlapping  i = hasOverlappingFlag  (overlapMode (is_flag i))
 isIncoherent   i = hasIncoherentFlag   (overlapMode (is_flag i))
+isNonCanonical i = hasNonCanonicalFlag (overlapMode (is_flag i))
 
 {-
 Note [ClsInst laziness and the rough-match fields]
@@ -838,14 +839,49 @@ example
 
   Here both (I7) and (I8) match, GHC picks an arbitrary one.
 
-So INCOHERENT may break the Coherence Assumption.  To avoid this
-incoherence breaking the specialiser,
+So INCOHERENT may break the Coherence Assumption. But sometimes that
+is fine, because the programmer promises that it doesn't matter which
+one is chosen.  A good example is in the `optics` library:
 
-* We label as "incoherent" the dictionary constructed by a
-  (potentially) incoherent use of an instance declaration.
+  data IxEq i is js where { IxEq :: IxEq i is is }
 
-* We do not specialise a function if there is an incoherent dictionary
-  in the /transistive dependencies/ of its dictionary arguments.
+  class AppendIndices xs ys ks | xs ys -> ks where
+    appendIndices :: IxEq i (Curry xs (Curry ys i)) (Curry ks i)
+
+  instance {-# INCOHERENT #-} xs ~ zs => AppendIndices xs '[] zs where
+    appendIndices = IxEq
+
+  instance ys ~ zs => AppendIndices '[] ys zs where
+    appendIndices = IxEq
+
+Here `xs` and `ys` are type-level lists, and for type inference purposes we want to
+solve the `AppendIndices` constraint when /either/ of them are the empty list. The
+dictionaries are the same in both cases (indeed the dictionary type is a singleton!),
+so we really don't care which is used.  See #23287 for discussion.
+
+
+In short, sometimes we want to specialise on these incoherently-selected dictionaries,
+and sometimes we don't.  It would be best to have a per-instance pragma, but for now
+we have a global flag:
+
+* If an instance has an `{-# INCOHERENT #-}` pragma, we use its `OverlapFlag` to
+  label it as either
+  * `Incoherent`: meaning incoherent but still specialisable, or
+  * `NonCanonical`: meaning incoherent and not specialisable.
+
+The module-wide `-fspecialise-incoherents` flag determines which
+choice is made.  The rest of this note describes what happens for
+`NonCanonical` instances, i.e. with `-fno-specialise-incoherents`.
+
+To avoid this incoherence breaking the specialiser,
+
+* We label as "non-canonical" the dictionary constructed by a
+  (potentially) incoherent use of an instance declaration whose
+  `OverlapFlag` is `NonCanonical`.
+
+* We do not specialise a function if there is a non-canonical
+  dictionary in the /transistive dependencies/ of its dictionary
+  arguments.
 
 To see the transitive closure issue, consider
   deeplyRisky :: C b => b -> Int
@@ -876,7 +912,7 @@ Here are the moving parts:
 * `GHC.HsToCore.Binds.dsHsWrapper` desugars the evidence application (f d) into
   (nospec f d) if `d` is incoherent. It has to do a dependency analysis to
   determine transitive dependencies, but we need to do that anyway.
-  See Note [Desugaring incoherent evidence] in GHC.HsToCore.Binds.
+  See Note [Desugaring non-canonical evidence] in GHC.HsToCore.Binds.
 
   See also Note [nospecId magic] in GHC.Types.Id.Make.
 -}
@@ -981,10 +1017,13 @@ data LookupInstanceErrReason =
   LookupInstErrNotFound
   deriving (Generic)
 
-data Coherence = IsCoherent | IsIncoherent
+type Canonical = Bool
 
 -- See Note [Recording coherence information in `PotentialUnifiers`]
-data PotentialUnifiers = NoUnifiers Coherence
+data PotentialUnifiers = NoUnifiers Canonical
+                       -- NoUnifiers True: We have a unique solution modulo canonicity
+                       -- NoUnifiers False: The solutions is not canonical, and thus
+                       --   we shouldn't specialise on it.
                        | OneOrMoreUnifiers (NonEmpty ClsInst)
                        -- This list is lazy as we only look at all the unifiers when
                        -- printing an error message. It can be expensive to compute all
@@ -993,33 +1032,28 @@ data PotentialUnifiers = NoUnifiers Coherence
 
 {- Note [Recording coherence information in `PotentialUnifiers`]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we have any potential unifiers, then we go down the `NotSure` route
-in `matchInstEnv`.  According to Note [Rules for instance lookup]
-steps IL4 and IL6, we only care about non-`INCOHERENT` instances for
-this purpose.
-
-It is only when we don't have any potential unifiers (i.e. we know
-that we have a unique solution modulo `INCOHERENT` instances) that we
-care about that unique solution being coherent or not (see
-Note [Coherence and specialisation: overview] for why we care at all).
-So we only need the `Coherent` flag in the case where the set of
-potential unifiers is otherwise empty.
--}
 
-instance Outputable Coherence where
-  ppr IsCoherent = text "coherent"
-  ppr IsIncoherent = text "incoherent"
+When we find a matching instance, there might be other instances that
+could potentially unify with the goal. For `INCOHERENT` instances, we
+don't care (see steps IL4 and IL6 in Note [Rules for instance
+lookup]). But if we have potentially unifying coherent instance, we
+report these `OneOrMoreUnifiers` so that `matchInstEnv` can go down
+the `NotSure` route.
+
+If this hurdle is passed, i.e. we have a unique solution up to
+`INCOHERENT` instances, the specialiser needs to know if that unique
+solution is canonical or not (see Note [Coherence and specialisation:
+overview] for why we care at all). So when the set of potential
+unifiers is empty, we record in `NoUnifiers` if the one solution is
+`Canonical`.
+-}
 
 instance Outputable PotentialUnifiers where
-  ppr (NoUnifiers c) = text "NoUnifiers" <+> ppr c
+  ppr (NoUnifiers c) = text "NoUnifiers" <+> if c then text "canonical" else text "non-canonical"
   ppr xs = ppr (getPotentialUnifiers xs)
 
-instance Semigroup Coherence where
-  IsCoherent <> IsCoherent = IsCoherent
-  _ <> _ = IsIncoherent
-
 instance Semigroup PotentialUnifiers where
-  NoUnifiers c1 <> NoUnifiers c2 = NoUnifiers (c1 <> c2)
+  NoUnifiers c1 <> NoUnifiers c2 = NoUnifiers (c1 && c2)
   NoUnifiers _ <> u = u
   OneOrMoreUnifiers (unifier :| unifiers) <> u = OneOrMoreUnifiers (unifier :| (unifiers <> getPotentialUnifiers u))
 
@@ -1065,22 +1099,24 @@ lookupInstEnv' (InstEnv rm) vis_mods cls tys
       = acc
 
 
-    incoherently_matched :: PotentialUnifiers -> PotentialUnifiers
-    incoherently_matched (NoUnifiers _) = NoUnifiers IsIncoherent
-    incoherently_matched u = u
+    noncanonically_matched :: PotentialUnifiers -> PotentialUnifiers
+    noncanonically_matched (NoUnifiers _) = NoUnifiers False
+    noncanonically_matched u = u
 
     check_unifier :: [ClsInst] -> PotentialUnifiers
-    check_unifier [] = NoUnifiers IsCoherent
+    check_unifier [] = NoUnifiers True
     check_unifier (item at ClsInst { is_tvs = tpl_tvs, is_tys = tpl_tys }:items)
       | not (instIsVisible vis_mods item)
       = check_unifier items  -- See Note [Instance lookup and orphan instances]
       | Just {} <- tcMatchTys tpl_tys tys = check_unifier items
         -- Does not match, so next check whether the things unify
         -- See Note [Overlapping instances]
+        -- Record that we encountered non-canonical instances: Note [Coherence and specialisation: overview]
+      | isNonCanonical item
+      = noncanonically_matched $ check_unifier items
         -- Ignore ones that are incoherent: Note [Incoherent instances]
-        -- Record that we encountered incoherent instances: Note [Coherence and specialisation: overview]
       | isIncoherent item
-      = incoherently_matched $ check_unifier items
+      = check_unifier items
 
       | otherwise
       = assertPpr (tys_tv_set `disjointVarSet` tpl_tv_set)
@@ -1137,7 +1173,7 @@ lookupInstEnv check_overlap_safe
 
     -- If the selected match is incoherent, discard all unifiers
     final_unifs = case final_matches of
-                    (m:_) | isIncoherent (fst m) -> NoUnifiers IsCoherent
+                    (m:_) | isIncoherent (fst m) -> NoUnifiers True
                     _                            -> all_unifs
 
     -- Note [Safe Haskell isSafeOverlap]
@@ -1315,7 +1351,7 @@ noMatches = InstMatches { instMatches = [], instGuards = [] }
 pruneOverlappedMatches :: [InstMatch] -> [InstMatch]
 -- ^ Remove from the argument list any InstMatches for which another
 -- element of the list is more specific, and overlaps it, using the
--- rules of Nove [Rules for instance lookup]
+-- rules of Note [Rules for instance lookup]
 pruneOverlappedMatches all_matches =
   instMatches $ foldr insert_overlapping noMatches all_matches
 
@@ -1472,33 +1508,8 @@ If the choice of instance *does* matter, all bets are still not off:
 users can consult the detailed specification of the instance selection
 algorithm in the GHC Users' Manual. However, this means we can end up
 with different instances at the same types at different parts of the
-program, and this difference has to be preserved. For example, if we
-have
-
-    class C a where
-      op :: a -> String
-
-    instance {-# OVERLAPPABLE #-} C a where ...
-    instance {-# INCOHERENT #-} C () where ...
-
-then depending on the circumstances (see #22448 for a full setup) some
-occurrences of `op :: () -> String` may be resolved to the generic
-instance, and other to the specific one; so we end up in the desugared
-code with occurrences of both
-
-    op @() ($dC_a @())
-
-and
-
-    op @() $dC_()
-
-In particular, the specialiser needs to ignore the incoherently
-selected instance in `op @() ($dC_a @())`. So during instance lookup,
-we record in `PotentialUnifiers` if a given solution was arrived at
-incoherently; we then use this information to inhibit specialisation
-a la Note [nospecId magic] in GHC.Types.Id.Make.
-
-
+program, and this difference has to be preserved. Note [Coherence and
+specialisation: overview] details how we achieve that.
 
 ************************************************************************
 *                                                                      *


=====================================
compiler/GHC/Driver/DynFlags.hs
=====================================
@@ -1169,7 +1169,8 @@ defaultFlags settings
       Opt_CompactUnwind,
       Opt_ShowErrorContext,
       Opt_SuppressStgReps,
-      Opt_UnoptimizedCoreForInterpreter
+      Opt_UnoptimizedCoreForInterpreter,
+      Opt_SpecialiseIncoherents
     ]
 
     ++ [f | (ns,f) <- optLevelFlags, 0 `elem` ns]


=====================================
compiler/GHC/Driver/Flags.hs
=====================================
@@ -268,6 +268,7 @@ data GeneralFlag
    | Opt_LiberateCase
    | Opt_SpecConstr
    | Opt_SpecConstrKeen
+   | Opt_SpecialiseIncoherents
    | Opt_DoLambdaEtaExpansion
    | Opt_IgnoreAsserts
    | Opt_DoEtaReduction


=====================================
compiler/GHC/Driver/Session.hs
=====================================
@@ -2423,6 +2423,7 @@ fFlagsDeps = [
   flagSpec "cross-module-specialise"          Opt_CrossModuleSpecialise,
   flagSpec "cross-module-specialize"          Opt_CrossModuleSpecialise,
   flagSpec "polymorphic-specialisation"       Opt_PolymorphicSpecialisation,
+  flagSpec "specialise-incoherents"           Opt_SpecialiseIncoherents,
   flagSpec "inline-generics"                  Opt_InlineGenerics,
   flagSpec "inline-generics-aggressively"     Opt_InlineGenericsAggressively,
   flagSpec "static-argument-transformation"   Opt_StaticArgumentTransformation,


=====================================
compiler/GHC/Hs/Decls.hs
=====================================
@@ -935,6 +935,7 @@ ppOverlapPragma mb =
     Just (L _ (Overlapping s))  -> maybe_stext s "{-# OVERLAPPING #-}"
     Just (L _ (Overlaps s))     -> maybe_stext s "{-# OVERLAPS #-}"
     Just (L _ (Incoherent s))   -> maybe_stext s "{-# INCOHERENT #-}"
+    Just (L _ (NonCanonical s)) -> maybe_stext s "{-# INCOHERENT #-}" -- No surface syntax for NONCANONICAL yet
   where
     maybe_stext NoSourceText     alt = text alt
     maybe_stext (SourceText src) _   = ftext src <+> text "#-}"


=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -41,7 +41,7 @@ import GHC.Hs             -- lots of things
 import GHC.Core           -- lots of things
 import GHC.Core.SimpleOpt    ( simpleOptExpr )
 import GHC.Core.Opt.OccurAnal ( occurAnalyseExpr )
-import GHC.Core.InstEnv ( Coherence(..) )
+import GHC.Core.InstEnv ( Canonical )
 import GHC.Core.Make
 import GHC.Core.Utils
 import GHC.Core.Opt.Arity     ( etaExpand )
@@ -252,16 +252,15 @@ dsHsBind
                         , abs_exports = exports
                         , abs_ev_binds = ev_binds
                         , abs_binds = binds, abs_sig = has_sig }))
-  = do { ds_binds <- addTyCs FromSource (listToBag dicts) $
+  = dsTcEvBinds_s ev_binds $ \ds_ev_binds -> do
+    { ds_binds <- addTyCs FromSource (listToBag dicts) $
                      dsLHsBinds binds
              -- addTyCs: push type constraints deeper
              --            for inner pattern match check
              -- See Check, Note [Long-distance information]
 
-       ; dsTcEvBinds_s ev_binds $ \ds_ev_binds -> do
-
-       -- dsAbsBinds does the hard work
-       { dsAbsBinds dflags tyvars dicts exports ds_ev_binds ds_binds (isSingletonBag binds) has_sig } }
+    -- dsAbsBinds does the hard work
+    ; dsAbsBinds dflags tyvars dicts exports ds_ev_binds ds_binds (isSingletonBag binds) has_sig }
 
 dsHsBind _ (PatSynBind{}) = panic "dsHsBind: PatSynBind"
 
@@ -1234,14 +1233,14 @@ evidence that is used in `e`.
 This question arose when thinking about deep subsumption; see
 https://github.com/ghc-proposals/ghc-proposals/pull/287#issuecomment-1125419649).
 
-Note [Desugaring incoherent evidence]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If the evidence is coherent, we desugar WpEvApp by simply passing
+Note [Desugaring non-canonical evidence]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If the evidence is canonical, we desugar WpEvApp by simply passing
 core_tm directly to k:
 
   k core_tm
 
-If the evidence is not coherent, we mark the application with nospec:
+If the evidence is not canonical, we mark the application with nospec:
 
   nospec @(cls => a) k core_tm
 
@@ -1252,14 +1251,14 @@ of the same type (see Note [nospecId magic] in GHC.Types.Id.Make).
 See Note [Coherence and specialisation: overview] for why we shouldn't
 specialise incoherent evidence.
 
-We can find out if a given evidence is coherent or not during the
-desugaring of its WpLet wrapper: an evidence is incoherent if its
+We can find out if a given evidence is canonical or not during the
+desugaring of its WpLet wrapper: an evidence is non-canonical if its
 own resolution was incoherent (see Note [Incoherent instances]), or
-if its definition refers to other incoherent evidence. dsEvBinds is
+if its definition refers to other non-canonical evidence. dsEvBinds is
 the convenient place to compute this, since it already needs to do
 inter-evidence dependency analysis to generate well-scoped
-bindings. We then record this coherence information in the
-dsl_coherence field of DsM's local environment.
+bindings. We then record this specialisability information in the
+dsl_unspecables field of DsM's local environment.
 
 -}
 
@@ -1283,20 +1282,27 @@ dsHsWrapper (WpFun c1 c2 (Scaled w t1)) k -- See Note [Desugaring WpFun]
 dsHsWrapper (WpCast co)       k = assert (coercionRole co == Representational) $
                                   k $ \e -> mkCastDs e co
 dsHsWrapper (WpEvApp tm)      k = do { core_tm <- dsEvTerm tm
-                                     ; incoherents <- getIncoherents
+                                     ; unspecables <- getUnspecables
                                      ; let vs = exprFreeVarsList core_tm
-                                           is_incoherent_var v = v `S.member` incoherents
-                                           is_coherent = all (not . is_incoherent_var) vs -- See Note [Desugaring incoherent evidence]
-                                     ; k (\e -> app_ev is_coherent e core_tm) }
+                                           is_unspecable_var v = v `S.member` unspecables
+                                           is_specable = not $ any (is_unspecable_var) vs -- See Note [Desugaring non-canonical evidence]
+                                     ; k (\e -> app_ev is_specable e core_tm) }
   -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
 dsHsWrapper (WpMultCoercion co) k = do { unless (isReflexiveCo co) $
                                            diagnosticDs DsMultiplicityCoercionsNotSupported
                                        ; k $ \e -> e }
 
+-- We are about to construct an evidence application `f dict`.  If the dictionary is
+-- non-specialisable, instead construct
+--     nospec f dict
+-- See Note [nospecId magic] in GHC.Types.Id.Make for what `nospec` does.
 app_ev :: Bool -> CoreExpr -> CoreExpr -> CoreExpr
-app_ev is_coherent k core_tm
-    | is_coherent = k `App` core_tm
-    | otherwise   = Var nospecId `App` Type (exprType k) `App` k `App` core_tm
+app_ev is_specable k core_tm
+    | not is_specable
+    = Var nospecId `App` Type (exprType k) `App` k `App` core_tm
+
+    | otherwise
+    = k `App` core_tm
 
 dsHsWrappers :: [HsWrapper] -> ([CoreExpr -> CoreExpr] -> DsM a) -> DsM a
 dsHsWrappers (wp:wps) k = dsHsWrapper wp $ \wrap -> dsHsWrappers wps $ \wraps -> k (wrap:wraps)
@@ -1314,7 +1320,7 @@ dsTcEvBinds (EvBinds bs)   = dsEvBinds bs
 
 --   * Desugars the ev_binds, sorts them into dependency order, and
 --     passes the resulting [CoreBind] to thing_inside
---   * Extends the DsM (dsl_coherence field) with coherence information
+--   * Extends the DsM (dsl_unspecable field) with specialisability information
 --     for each binder in ev_binds, before invoking thing_inside
 dsEvBinds :: Bag EvBind -> ([CoreBind] -> DsM a) -> DsM a
 dsEvBinds ev_binds thing_inside
@@ -1322,53 +1328,50 @@ dsEvBinds ev_binds thing_inside
        ; let comps = sort_ev_binds ds_binds
        ; go comps thing_inside }
   where
-    go ::[SCC (Node EvVar (Coherence, CoreExpr))] -> ([CoreBind] -> DsM a) -> DsM a
+    go ::[SCC (Node EvVar (Canonical, CoreExpr))] -> ([CoreBind] -> DsM a) -> DsM a
     go (comp:comps) thing_inside
-      = do { incoherents <- getIncoherents
-           ; let (core_bind, new_incoherents) = ds_component incoherents comp
-           ; addIncoherents new_incoherents $ go comps $ \ core_binds -> thing_inside (core_bind:core_binds) }
+      = do { unspecables <- getUnspecables
+           ; let (core_bind, new_unspecables) = ds_component unspecables comp
+           ; addUnspecables new_unspecables $ go comps $ \ core_binds -> thing_inside (core_bind:core_binds) }
     go [] thing_inside = thing_inside []
 
-    is_coherent IsCoherent = True
-    is_coherent IsIncoherent = False
-
-    ds_component incoherents (AcyclicSCC node) = (NonRec v rhs, new_incoherents)
+    ds_component unspecables (AcyclicSCC node) = (NonRec v rhs, new_unspecables)
       where
-        ((v, rhs), (this_coherence, deps)) = unpack_node node
-        transitively_incoherent = not (is_coherent this_coherence) || any is_incoherent deps
-        is_incoherent dep = dep `S.member` incoherents
-        new_incoherents
-            | transitively_incoherent = S.singleton v
+        ((v, rhs), (this_canonical, deps)) = unpack_node node
+        transitively_unspecable = not this_canonical || any is_unspecable deps
+        is_unspecable dep = dep `S.member` unspecables
+        new_unspecables
+            | transitively_unspecable = S.singleton v
             | otherwise = mempty
-    ds_component incoherents (CyclicSCC nodes) = (Rec pairs, new_incoherents)
+    ds_component unspecables (CyclicSCC nodes) = (Rec pairs, new_unspecables)
       where
-        (pairs, direct_coherence) = unzip $ map unpack_node nodes
+        (pairs, direct_canonicity) = unzip $ map unpack_node nodes
 
-        is_incoherent_remote dep = dep `S.member` incoherents
-        transitively_incoherent = or [ not (is_coherent this_coherence) || any is_incoherent_remote deps | (this_coherence, deps) <- direct_coherence ]
-            -- Bindings from a given SCC are transitively coherent if
-            -- all are coherent and all their remote dependencies are
-            -- also coherent; see Note [Desugaring incoherent evidence]
+        is_unspecable_remote dep = dep `S.member` unspecables
+        transitively_unspecable = or [ not this_canonical || any is_unspecable_remote deps | (this_canonical, deps) <- direct_canonicity ]
+            -- Bindings from a given SCC are transitively specialisable if
+            -- all are specialisable and all their remote dependencies are
+            -- also specialisable; see Note [Desugaring non-canonical evidence]
 
-        new_incoherents
-            | transitively_incoherent = S.fromList [ v | (v, _) <- pairs]
+        new_unspecables
+            | transitively_unspecable = S.fromList [ v | (v, _) <- pairs]
             | otherwise = mempty
 
-    unpack_node DigraphNode { node_key = v, node_payload = (coherence, rhs), node_dependencies = deps } = ((v, rhs), (coherence, deps))
+    unpack_node DigraphNode { node_key = v, node_payload = (canonical, rhs), node_dependencies = deps } = ((v, rhs), (canonical, deps))
 
-sort_ev_binds :: Bag (Id, Coherence, CoreExpr) -> [SCC (Node EvVar (Coherence, CoreExpr))]
+sort_ev_binds :: Bag (Id, Canonical, CoreExpr) -> [SCC (Node EvVar (Canonical, CoreExpr))]
 -- We do SCC analysis of the evidence bindings, /after/ desugaring
 -- them. This is convenient: it means we can use the GHC.Core
 -- free-variable functions rather than having to do accurate free vars
 -- for EvTerm.
 sort_ev_binds ds_binds = stronglyConnCompFromEdgedVerticesUniqR edges
   where
-    edges :: [ Node EvVar (Coherence, CoreExpr) ]
+    edges :: [ Node EvVar (Canonical, CoreExpr) ]
     edges = foldr ((:) . mk_node) [] ds_binds
 
-    mk_node :: (Id, Coherence, CoreExpr) -> Node EvVar (Coherence, CoreExpr)
-    mk_node (var, coherence, rhs)
-      = DigraphNode { node_payload = (coherence, rhs)
+    mk_node :: (Id, Canonical, CoreExpr) -> Node EvVar (Canonical, CoreExpr)
+    mk_node (var, canonical, rhs)
+      = DigraphNode { node_payload = (canonical, rhs)
                     , node_key = var
                     , node_dependencies = nonDetEltsUniqSet $
                                           exprFreeVars rhs `unionVarSet`
@@ -1377,13 +1380,13 @@ sort_ev_binds ds_binds = stronglyConnCompFromEdgedVerticesUniqR edges
       -- is still deterministic even if the edges are in nondeterministic order
       -- as explained in Note [Deterministic SCC] in GHC.Data.Graph.Directed.
 
-dsEvBind :: EvBind -> DsM (Id, Coherence, CoreExpr)
+dsEvBind :: EvBind -> DsM (Id, Canonical, CoreExpr)
 dsEvBind (EvBind { eb_lhs = v, eb_rhs = r, eb_info = info }) = do
     e <- dsEvTerm r
-    let coherence = case info of
-            EvBindGiven{} -> IsCoherent
-            EvBindWanted{ ebi_coherence = coherence } -> coherence
-    return (v, coherence, e)
+    let canonical = case info of
+            EvBindGiven{} -> True
+            EvBindWanted{ ebi_canonical = canonical } -> canonical
+    return (v, canonical, e)
 
 
 {-**********************************************************************


=====================================
compiler/GHC/HsToCore/Monad.hs
=====================================
@@ -37,7 +37,7 @@ module GHC.HsToCore.Monad (
         getPmNablas, updPmNablas,
 
         -- Tracking evidence variable coherence
-        addIncoherents, getIncoherents,
+        addUnspecables, getUnspecables,
 
         -- Get COMPLETE sets of a TyCon
         dsGetCompleteMatches,
@@ -373,7 +373,7 @@ mkDsEnvs unit_env mod rdr_env type_env fam_inst_env ptc msg_var cc_st_var
         lcl_env = DsLclEnv { dsl_meta        = emptyNameEnv
                            , dsl_loc         = real_span
                            , dsl_nablas      = initNablas
-                           , dsl_incoherents = mempty
+                           , dsl_unspecables = mempty
                            }
     in (gbl_env, lcl_env)
 
@@ -429,11 +429,11 @@ getPmNablas = do { env <- getLclEnv; return (dsl_nablas env) }
 updPmNablas :: Nablas -> DsM a -> DsM a
 updPmNablas nablas = updLclEnv (\env -> env { dsl_nablas = nablas })
 
-addIncoherents :: S.Set EvId -> DsM a -> DsM a
-addIncoherents incoherents = updLclEnv (\env -> env{ dsl_incoherents = incoherents `mappend` dsl_incoherents env })
+addUnspecables :: S.Set EvId -> DsM a -> DsM a
+addUnspecables unspecables = updLclEnv (\env -> env{ dsl_unspecables = unspecables `mappend` dsl_unspecables env })
 
-getIncoherents :: DsM (S.Set EvId)
-getIncoherents = dsl_incoherents <$> getLclEnv
+getUnspecables :: DsM (S.Set EvId)
+getUnspecables = dsl_unspecables <$> getLclEnv
 
 getSrcSpanDs :: DsM SrcSpan
 getSrcSpanDs = do { env <- getLclEnv


=====================================
compiler/GHC/HsToCore/Quote.hs
=====================================
@@ -2636,6 +2636,7 @@ repOverlap mb =
         Overlapping _  -> just =<< dataCon overlappingDataConName
         Overlaps _     -> just =<< dataCon overlapsDataConName
         Incoherent _   -> just =<< dataCon incoherentDataConName
+        NonCanonical _ -> just =<< dataCon incoherentDataConName
   where
   nothing = coreNothing overlapTyConName
   just    = coreJust overlapTyConName


=====================================
compiler/GHC/HsToCore/Types.hs
=====================================
@@ -79,9 +79,9 @@ data DsLclEnv
   -- ^ See Note [Long-distance information] in "GHC.HsToCore.Pmc".
   -- The set of reaching values Nablas is augmented as we walk inwards, refined
   -- through each pattern match in turn
-  , dsl_incoherents :: S.Set EvVar
-  -- ^ See Note [Desugaring incoherent evidence]: this field collects
-  -- all incoherent evidence variables in scope.
+  , dsl_unspecables :: S.Set EvVar
+  -- ^ See Note [Desugaring non-canonical evidence]: this field collects
+  -- all un-specialisable evidence variables in scope.
   }
 
 -- Inside [| |] brackets, the desugarer looks


=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -1213,11 +1213,11 @@ addDeferredBinding ctxt err (EI { ei_evdest = Just dest, ei_pred = item_ty
 
        ; case dest of
            EvVarDest evar
-             -> addTcEvBind ev_binds_var $ mkWantedEvBind evar IsCoherent err_tm
+             -> addTcEvBind ev_binds_var $ mkWantedEvBind evar True err_tm
            HoleDest hole
              -> do { -- See Note [Deferred errors for coercion holes]
                      let co_var = coHoleCoVar hole
-                   ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var IsCoherent err_tm
+                   ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var True err_tm
                    ; fillCoercionHole hole (mkCoVarCo co_var) } }
 addDeferredBinding _ _ _ = return ()    -- Do not set any evidence for Given
 


=====================================
compiler/GHC/Tc/Gen/Splice.hs
=====================================
@@ -2514,6 +2514,7 @@ reifyClassInstance is_poly_tvs i
                   Overlapping _   -> Just TH.Overlapping
                   Overlaps _      -> Just TH.Overlaps
                   Incoherent _    -> Just TH.Incoherent
+                  NonCanonical _  -> Just TH.Incoherent
 
 ------------------------------
 reifyFamilyInstances :: TyCon -> [FamInst] -> TcM [TH.Dec]


=====================================
compiler/GHC/Tc/Instance/Class.hs
=====================================
@@ -99,7 +99,10 @@ data ClsInstResult
 
   | OneInst { cir_new_theta   :: [TcPredType]
             , cir_mk_ev       :: [EvExpr] -> EvTerm
-            , cir_coherence   :: Coherence -- See Note [Coherence and specialisation: overview]
+            , cir_canonical   :: Canonical --   cir_canonical=True => you can specialise on this instance
+                                           --   cir_canonical= False => you cannot specialise on this instance
+                                           --                           (its OverlapFlag is NonCanonical)
+                                           -- See Note [Coherence and specialisation: overview]
             , cir_what        :: InstanceWhat }
 
   | NotSure      -- Multiple matches and/or one or more unifiers
@@ -169,7 +172,7 @@ matchInstEnv dflags short_cut_solver clas tys
                       ; return NoInstance }
 
             -- A single match (& no safe haskell failure)
-            ([(ispec, inst_tys)], NoUnifiers coherence, False)
+            ([(ispec, inst_tys)], NoUnifiers canonical, False)
                 | short_cut_solver      -- Called from the short-cut solver
                 , isOverlappable ispec
                 -- If the instance has OVERLAPPABLE or OVERLAPS or INCOHERENT
@@ -183,12 +186,11 @@ matchInstEnv dflags short_cut_solver clas tys
                 -> do { let dfun_id = instanceDFunId ispec
                             warn    = instanceWarning ispec
                       ; traceTc "matchClass success" $
-                        vcat [text "dict" <+> ppr pred,
-                              ppr coherence,
+                        vcat [text "dict" <+> ppr pred <+> parens (if canonical then text "canonical" else text "non-canonical"),
                               text "witness" <+> ppr dfun_id
                                              <+> ppr (idType dfun_id) ]
                                 -- Record that this dfun is needed
-                      ; match_one (null unsafeOverlaps) coherence dfun_id inst_tys warn }
+                      ; match_one (null unsafeOverlaps) canonical dfun_id inst_tys warn }
 
             -- More than one matches (or Safe Haskell fail!). Defer any
             -- reactions of a multitude until we learn more about the reagent
@@ -199,16 +201,15 @@ matchInstEnv dflags short_cut_solver clas tys
    where
      pred = mkClassPred clas tys
 
-match_one :: SafeOverlapping -> Coherence -> DFunId -> [DFunInstType]
+match_one :: SafeOverlapping -> Canonical -> DFunId -> [DFunInstType]
           -> Maybe (WarningTxt GhcRn) -> TcM ClsInstResult
-             -- See Note [DFunInstType: instantiating types] in GHC.Core.InstEnv
-match_one so coherence dfun_id mb_inst_tys warn
+match_one so canonical dfun_id mb_inst_tys warn
   = do { traceTc "match_one" (ppr dfun_id $$ ppr mb_inst_tys)
        ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
        ; traceTc "match_one 2" (ppr dfun_id $$ ppr tys $$ ppr theta)
        ; return $ OneInst { cir_new_theta   = theta
                           , cir_mk_ev       = evDFunApp dfun_id tys
-                          , cir_coherence   = coherence
+                          , cir_canonical   = canonical
                           , cir_what        = TopLevInstance { iw_dfun_id = dfun_id
                                                              , iw_safe_over = so
                                                              , iw_warn = warn } } }
@@ -245,7 +246,7 @@ matchCTuple :: Class -> [Type] -> TcM ClsInstResult
 matchCTuple clas tys   -- (isCTupleClass clas) holds
   = return (OneInst { cir_new_theta   = tys
                     , cir_mk_ev       = tuple_ev
-                    , cir_coherence   = IsCoherent
+                    , cir_canonical   = True
                     , cir_what        = BuiltinInstance })
             -- The dfun *is* the data constructor!
   where
@@ -409,7 +410,7 @@ makeLitDict clas ty et
     , let ev_tm = mkEvCast et (mkSymCo (mkTransCo co_dict co_rep))
     = return $ OneInst { cir_new_theta   = []
                        , cir_mk_ev       = \_ -> ev_tm
-                       , cir_coherence   = IsCoherent
+                       , cir_canonical   = True
                        , cir_what        = BuiltinInstance }
 
     | otherwise
@@ -458,7 +459,7 @@ matchWithDict [cls, mty]
 
        ; return $ OneInst { cir_new_theta   = [mkPrimEqPred mty inst_meth_ty]
                           , cir_mk_ev       = mk_ev
-                          , cir_coherence   = IsIncoherent -- See (WD6) in Note [withDict]
+                          , cir_canonical   = False -- See (WD6) in Note [withDict]
                           , cir_what        = BuiltinInstance }
        }
 
@@ -565,7 +566,7 @@ Some further observations about `withDict`:
            k (sv |> (sub co2 ; sym co)))
 
       That is, we cast the method using a coercion, and apply k to
-      it. Moreover, we mark the evidence as incoherent, resulting in
+      it. Moreover, we mark the evidence as non-canonical, resulting in
       the use of the 'nospec' magicId (see Note [nospecId magic] in
       GHC.Types.Id.Make) to ensure that the typeclass specialiser
       doesn't incorrectly common-up distinct evidence terms. This is
@@ -651,7 +652,7 @@ doFunTy :: Class -> Type -> Mult -> Type -> Type -> TcM ClsInstResult
 doFunTy clas ty mult arg_ty ret_ty
   = return $ OneInst { cir_new_theta   = preds
                      , cir_mk_ev       = mk_ev
-                     , cir_coherence   = IsCoherent
+                     , cir_canonical   = True
                      , cir_what        = BuiltinInstance }
   where
     preds = map (mk_typeable_pred clas) [mult, arg_ty, ret_ty]
@@ -668,7 +669,7 @@ doTyConApp clas ty tc kind_args
   | tyConIsTypeable tc
   = return $ OneInst { cir_new_theta   = map (mk_typeable_pred clas) kind_args
                      , cir_mk_ev       = mk_ev
-                     , cir_coherence   = IsCoherent
+                     , cir_canonical   = True
                      , cir_what        = BuiltinTypeableInstance tc }
   | otherwise
   = return NoInstance
@@ -700,7 +701,7 @@ doTyApp clas ty f tk
   | otherwise
   = return $ OneInst { cir_new_theta   = map (mk_typeable_pred clas) [f, tk]
                      , cir_mk_ev       = mk_ev
-                     , cir_coherence   = IsCoherent
+                     , cir_canonical   = True
                      , cir_what        = BuiltinInstance }
   where
     mk_ev [t1,t2] = evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2)
@@ -721,7 +722,7 @@ doTyLit kc t = do { kc_clas <- tcLookupClass kc
                         mk_ev _    = panic "doTyLit"
                   ; return (OneInst { cir_new_theta   = [kc_pred]
                                     , cir_mk_ev       = mk_ev
-                                    , cir_coherence   = IsCoherent
+                                    , cir_canonical   = True
                                     , cir_what        = BuiltinInstance }) }
 
 {- Note [Typeable (T a b c)]
@@ -961,7 +962,7 @@ matchHasField dflags short_cut clas tys
                                  -- See Note [Detecting incomplete record selectors] in GHC.HsToCore.Pmc
                              ; return OneInst { cir_new_theta   = theta
                                               , cir_mk_ev       = mk_ev
-                                              , cir_coherence   = IsCoherent
+                                              , cir_canonical   = True
                                               , cir_what        = BuiltinInstance } }
                      else matchInstEnv dflags short_cut clas tys }
 


=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -33,7 +33,6 @@ import GHC.Data.Bag
 import GHC.Core.Class
 import GHC.Core
 import GHC.Core.DataCon
-import GHC.Core.InstEnv ( Coherence(IsCoherent) )
 import GHC.Core.Make
 import GHC.Driver.DynFlags
 import GHC.Data.FastString
@@ -612,7 +611,7 @@ solveImplicationUsingUnsatGiven
     go_simple ct = case ctEvidence ct of
       CtWanted { ctev_pred = pty, ctev_dest = dst }
         -> do { ev_expr <- unsatisfiableEvExpr unsat_given pty
-              ; setWantedEvTerm dst IsCoherent $ EvExpr ev_expr }
+              ; setWantedEvTerm dst True $ EvExpr ev_expr }
       _ -> return ()
 
 -- | Create an evidence expression for an arbitrary constraint using


=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -28,7 +28,7 @@ import GHC.Hs.Type( HsIPName(..) )
 
 import GHC.Core
 import GHC.Core.Type
-import GHC.Core.InstEnv     ( DFunInstType, Coherence(..) )
+import GHC.Core.InstEnv     ( DFunInstType )
 import GHC.Core.Class
 import GHC.Core.Predicate
 import GHC.Core.Multiplicity ( scaledThing )
@@ -187,7 +187,7 @@ solveCallStack ev ev_cs
   -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
   = do { cs_tm <- evCallStack ev_cs
        ; let ev_tm = mkEvCast cs_tm (wrapIP (ctEvPred ev))
-       ; setEvBindIfWanted ev IsCoherent ev_tm }
+       ; setEvBindIfWanted ev True ev_tm }
 
 
 {- Note [Shadowing of implicit parameters]
@@ -397,7 +397,7 @@ solveEqualityDict ev cls tys
        ; (co, _, _) <- wrapUnifierTcS ev role $ \uenv ->
                        uType uenv t1 t2
          -- Set  d :: (t1~t2) = Eq# co
-       ; setWantedEvTerm dest IsCoherent $
+       ; setWantedEvTerm dest True $
          evDataConApp data_con tys [Coercion co]
        ; stopWith ev "Solved wanted lifted equality" }
 
@@ -718,10 +718,10 @@ try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys
          -- the inert from the work-item or vice-versa.
        ; case solveOneFromTheOther (CDictCan dict_i) (CDictCan dict_w) of
            KeepInert -> do { traceTcS "lookupInertDict:KeepInert" (ppr dict_w)
-                           ; setEvBindIfWanted ev_w IsCoherent (ctEvTerm ev_i)
+                           ; setEvBindIfWanted ev_w True (ctEvTerm ev_i)
                            ; return $ Stop ev_w (text "Dict equal" <+> ppr dict_w) }
            KeepWork  -> do { traceTcS "lookupInertDict:KeepWork" (ppr dict_w)
-                           ; setEvBindIfWanted ev_i IsCoherent (ctEvTerm ev_w)
+                           ; setEvBindIfWanted ev_i True (ctEvTerm ev_w)
                            ; updInertCans (updDicts $ delDict dict_w)
                            ; continueWith () } } }
 
@@ -789,7 +789,7 @@ shortCutSolver dflags ev_w ev_i
            ; case inst_res of
                OneInst { cir_new_theta   = preds
                        , cir_mk_ev       = mk_ev
-                       , cir_coherence   = coherence
+                       , cir_canonical   = canonical
                        , cir_what        = what }
                  | safeOverlap what
                  , all isTyFamFree preds  -- Note [Shortcut solving: type families]
@@ -809,7 +809,7 @@ shortCutSolver dflags ev_w ev_i
 
                        ; let ev_tm     = mk_ev (map getEvExpr evc_vs)
                              ev_binds' = extendEvBinds ev_binds $
-                                         mkWantedEvBind (ctEvEvId ev) coherence ev_tm
+                                         mkWantedEvBind (ctEvEvId ev) canonical ev_tm
 
                        ; foldlM try_solve_from_instance (ev_binds', solved_dicts') $
                          freshGoals evc_vs }
@@ -852,7 +852,7 @@ try_instances inerts work_item@(DictCt { di_ev = ev, di_cls = cls
      -- See Note [No Given/Given fundeps]
 
   | Just solved_ev <- lookupSolvedDict inerts dict_loc cls xis   -- Cached
-  = do { setEvBindIfWanted ev IsCoherent (ctEvTerm solved_ev)
+  = do { setEvBindIfWanted ev True (ctEvTerm solved_ev)
        ; stopWith ev "Dict/Top (cached)" }
 
   | otherwise  -- Wanted, but not cached
@@ -874,14 +874,14 @@ chooseInstance work_item
                (OneInst { cir_new_theta   = theta
                         , cir_what        = what
                         , cir_mk_ev       = mk_ev
-                        , cir_coherence   = coherence })
+                        , cir_canonical   = canonical })
   = do { traceTcS "doTopReact/found instance for" $ ppr work_item
        ; deeper_loc <- checkInstanceOK loc what pred
        ; checkReductionDepth deeper_loc pred
        ; assertPprM (getTcEvBindsVar >>= return . not . isCoEvBindsVar)
                     (ppr work_item)
        ; evc_vars <- mapM (newWanted deeper_loc (ctEvRewriters work_item)) theta
-       ; setEvBindIfWanted work_item coherence (mk_ev (map getEvExpr evc_vars))
+       ; setEvBindIfWanted work_item canonical (mk_ev (map getEvExpr evc_vars))
        ; emitWorkNC (freshGoals evc_vars)
        ; stopWith work_item "Dict/Top (solved wanted)" }
   where
@@ -1127,7 +1127,7 @@ matchLocalInst pred loc
             ->
             do { let result = OneInst { cir_new_theta   = theta
                                       , cir_mk_ev       = evDFunApp dfun_id tys
-                                      , cir_coherence   = IsCoherent
+                                      , cir_canonical   = True
                                       , cir_what        = LocalInstance }
                ; traceTcS "Best local instance found:" $
                   vcat [ text "pred:" <+> ppr pred
@@ -1374,7 +1374,7 @@ last_resort inerts (DictCt { di_ev = ev_w, di_cls = cls, di_tys = xis })
   , Just ct_i <- lookupInertDict inerts loc_w cls xis
   , let ev_i = dictCtEvidence ct_i
   , isGiven ev_i
-  = do { setEvBindIfWanted ev_w IsCoherent (ctEvTerm ev_i)
+  = do { setEvBindIfWanted ev_w True (ctEvTerm ev_i)
        ; ctLocWarnTcS loc_w $
          TcRnLoopySuperclassSolve loc_w (ctEvPred ev_w)
        ; return $ Stop ev_w (text "Loopy superclass") }
@@ -2215,4 +2215,3 @@ constraints.
 
 See also Note [Evidence for quantified constraints] in GHC.Core.Predicate.
 -}
-


=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -33,7 +33,6 @@ import GHC.Core.Coercion
 import GHC.Core.Coercion.Axiom
 import GHC.Core.Reduction
 import GHC.Core.Unify( tcUnifyTyWithTFs )
-import GHC.Core.InstEnv ( Coherence(..) )
 import GHC.Core.FamInstEnv ( FamInstEnvs, FamInst(..), apartnessCheck
                            , lookupFamInstEnvByTyCon )
 import GHC.Core
@@ -358,7 +357,7 @@ can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
 -- Literals
 can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
  | l1 == l2
-  = do { setEvBindIfWanted ev IsCoherent (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1)
+  = do { setEvBindIfWanted ev True (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1)
        ; stopWith ev "Equal LitTy" }
 
 -- Decompose FunTy: (s -> t) and (c => t)
@@ -1909,7 +1908,7 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
 
        -- Provide Refl evidence for the constraint
        -- Ignore 'swapped' because it's Refl!
-       ; setEvBindIfWanted new_ev IsCoherent $
+       ; setEvBindIfWanted new_ev True $
          evCoercion (mkNomReflCo final_rhs)
 
        -- Kick out any constraints that can now be rewritten
@@ -2020,7 +2019,7 @@ canEqReflexive :: CtEvidence    -- ty ~ ty
                -> TcType        -- ty
                -> TcS (StopOrContinue a)   -- always Stop
 canEqReflexive ev eq_rel ty
-  = do { setEvBindIfWanted ev IsCoherent $
+  = do { setEvBindIfWanted ev True $
          evCoercion (mkReflCo (eqRelRole eq_rel) ty)
        ; stopWith ev "Solved by reflexivity" }
 
@@ -2603,7 +2602,7 @@ tryInertEqs work_item@(EqCt { eq_ev = ev, eq_eq_rel = eq_rel })
   = Stage $
     do { inerts <- getInertCans
        ; if | Just (ev_i, swapped) <- inertsCanDischarge inerts work_item
-            -> do { setEvBindIfWanted ev IsCoherent $
+            -> do { setEvBindIfWanted ev True $
                     evCoercion (maybeSymCo swapped $
                                 downgradeRole (eqRelRole eq_rel)
                                               (ctEvRole ev_i)


=====================================
compiler/GHC/Tc/Solver/Irred.hs
=====================================
@@ -15,7 +15,6 @@ import GHC.Tc.Solver.Monad
 import GHC.Tc.Types.Evidence
 
 import GHC.Core.Coercion
-import GHC.Core.InstEnv ( Coherence(..) )
 
 import GHC.Types.Basic( SwapFlag(..) )
 
@@ -74,9 +73,9 @@ try_inert_irreds inerts irred_w@(IrredCt { ir_ev = ev_w, ir_reason = reason })
          vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))
               , text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i)) ]
        ; case solveOneFromTheOther ct_i ct_w of
-            KeepInert -> do { setEvBindIfWanted ev_w IsCoherent (swap_me swap ev_i)
+            KeepInert -> do { setEvBindIfWanted ev_w True (swap_me swap ev_i)
                             ; return (Stop ev_w (text "Irred equal:KeepInert" <+> ppr ct_w)) }
-            KeepWork ->  do { setEvBindIfWanted ev_i IsCoherent (swap_me swap ev_w)
+            KeepWork ->  do { setEvBindIfWanted ev_i True (swap_me swap ev_w)
                             ; updInertCans (updIrreds (\_ -> others))
                             ; continueWith () } }
 


=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -1687,19 +1687,19 @@ setWantedEq (HoleDest hole) co
 setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq: EvVarDest" (ppr ev)
 
 -- | Good for both equalities and non-equalities
-setWantedEvTerm :: TcEvDest -> Coherence -> EvTerm -> TcS ()
-setWantedEvTerm (HoleDest hole) _coherence tm
+setWantedEvTerm :: TcEvDest -> Canonical -> EvTerm -> TcS ()
+setWantedEvTerm (HoleDest hole) _canonical tm
   | Just co <- evTermCoercion_maybe tm
   = do { useVars (coVarsOfCo co)
        ; fillCoercionHole hole co }
   | otherwise
   = -- See Note [Yukky eq_sel for a HoleDest]
     do { let co_var = coHoleCoVar hole
-       ; setEvBind (mkWantedEvBind co_var IsCoherent tm)
+       ; setEvBind (mkWantedEvBind co_var True tm)
        ; fillCoercionHole hole (mkCoVarCo co_var) }
 
-setWantedEvTerm (EvVarDest ev_id) coherence tm
-  = setEvBind (mkWantedEvBind ev_id coherence tm)
+setWantedEvTerm (EvVarDest ev_id) canonical tm
+  = setEvBind (mkWantedEvBind ev_id canonical tm)
 
 {- Note [Yukky eq_sel for a HoleDest]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1725,10 +1725,10 @@ fillCoercionHole hole co
   = do { wrapTcS $ TcM.fillCoercionHole hole co
        ; kickOutAfterFillingCoercionHole hole }
 
-setEvBindIfWanted :: CtEvidence -> Coherence -> EvTerm -> TcS ()
-setEvBindIfWanted ev coherence tm
+setEvBindIfWanted :: CtEvidence -> Canonical -> EvTerm -> TcS ()
+setEvBindIfWanted ev canonical tm
   = case ev of
-      CtWanted { ctev_dest = dest } -> setWantedEvTerm dest coherence tm
+      CtWanted { ctev_dest = dest } -> setWantedEvTerm dest canonical tm
       _                             -> return ()
 
 newTcEvBinds :: TcS EvBindsVar


=====================================
compiler/GHC/Tc/Solver/Solve.hs
=====================================
@@ -20,7 +20,6 @@ import GHC.Tc.Types.Constraint
 import GHC.Tc.Solver.InertSet
 import GHC.Tc.Solver.Monad
 
-import GHC.Core.InstEnv     ( Coherence(..) )
 import GHC.Core.Predicate
 import GHC.Core.Reduction
 import GHC.Core.Coercion
@@ -427,7 +426,7 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
 
       ; ev_binds <- emitImplicationTcS lvl skol_info_anon skol_tvs given_ev_vars wanteds
 
-      ; setWantedEvTerm dest IsCoherent $
+      ; setWantedEvTerm dest True $
         EvFun { et_tvs = skol_tvs, et_given = given_ev_vars
               , et_binds = ev_binds, et_body = w_id }
 
@@ -556,7 +555,7 @@ finish_rewrite ev@(CtWanted { ctev_dest = dest
                 (Reduction co new_pred) new_rewriters
   = do { mb_new_ev <- newWanted loc rewriters' new_pred
        ; massert (coercionRole co == ctEvRole ev)
-       ; setWantedEvTerm dest IsCoherent $
+       ; setWantedEvTerm dest True $
             mkEvCast (getEvExpr mb_new_ev)
                      (downgradeRole Representational (ctEvRole ev) (mkSymCo co))
        ; case mb_new_ev of
@@ -631,7 +630,7 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1 })
   where
     setEv :: (EvTerm,Ct) -> TcS ()
     setEv (ev,ct) = case ctEvidence ct of
-      CtWanted { ctev_dest = dest } -> setWantedEvTerm dest IsCoherent ev -- TODO: plugins should be able to signal non-coherence
+      CtWanted { ctev_dest = dest } -> setWantedEvTerm dest True ev -- TODO: plugins should be able to signal non-canonicity
       _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"
 
 -- | A pair of (given, wanted) constraints to pass to plugins


=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -1494,7 +1494,7 @@ tcSuperClasses skol_info dfun_id cls tyvars dfun_evs 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 IsCoherent sc_ev_tm
+           ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id True sc_ev_tm
            ; let sc_top_ty = tcMkDFunSigmaTy tyvars (map idType dfun_evs) sc_pred
                  sc_top_id = mkLocalId sc_top_name ManyTy sc_top_ty
                  export = ABE { abe_wrap = idHsWrapper


=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -70,7 +70,7 @@ import GHC.Types.Basic
 import GHC.Core
 import GHC.Core.Class (Class, classSCSelId )
 import GHC.Core.FVs   ( exprSomeFreeVars )
-import GHC.Core.InstEnv ( Coherence(..) )
+import GHC.Core.InstEnv ( Canonical )
 
 import GHC.Utils.Misc
 import GHC.Utils.Panic
@@ -466,7 +466,7 @@ instance Outputable EvBindMap where
 data EvBindInfo
   = EvBindGiven { -- See Note [Tracking redundant constraints] in GHC.Tc.Solver
     }
-  | EvBindWanted { ebi_coherence :: Coherence -- See Note [Desugaring incoherent evidence]
+  | EvBindWanted { ebi_canonical :: Canonical -- See Note [Desugaring non-canonical evidence]
     }
 
 -----------------
@@ -480,7 +480,7 @@ data EvBind
 evBindVar :: EvBind -> EvVar
 evBindVar = eb_lhs
 
-mkWantedEvBind :: EvVar -> Coherence -> EvTerm -> EvBind
+mkWantedEvBind :: EvVar -> Canonical -> EvTerm -> EvBind
 mkWantedEvBind ev c tm = EvBind { eb_info = EvBindWanted c, eb_lhs = ev, eb_rhs = tm }
 
 -- EvTypeable are never given, so we can work with EvExpr here instead of EvTerm


=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -1,5 +1,6 @@
 {-# LANGUAGE FlexibleContexts, RecursiveDo #-}
 {-# LANGUAGE DisambiguateRecordFields #-}
+{-# LANGUAGE LambdaCase #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
 
@@ -840,16 +841,31 @@ getOverlapFlag :: Maybe OverlapMode -> TcM OverlapFlag
 --     set the OverlapMode to 'm'
 getOverlapFlag overlap_mode
   = do  { dflags <- getDynFlags
-        ; let overlap_ok    = xopt LangExt.OverlappingInstances dflags
-              incoherent_ok = xopt LangExt.IncoherentInstances  dflags
+        ; let overlap_ok               = xopt LangExt.OverlappingInstances dflags
+              incoherent_ok            = xopt LangExt.IncoherentInstances  dflags
+              noncanonical_incoherence = not $ gopt Opt_SpecialiseIncoherents dflags
+
               use x = OverlapFlag { isSafeOverlap = safeLanguageOn dflags
                                   , overlapMode   = x }
               default_oflag | incoherent_ok = use (Incoherent NoSourceText)
                             | overlap_ok    = use (Overlaps NoSourceText)
                             | otherwise     = use (NoOverlap NoSourceText)
 
-              final_oflag = setOverlapModeMaybe default_oflag overlap_mode
+              oflag = setOverlapModeMaybe default_oflag overlap_mode
+              final_oflag = effective_oflag noncanonical_incoherence oflag
         ; return final_oflag }
+  where
+    effective_oflag noncanonical_incoherence oflag at OverlapFlag{ overlapMode = overlap_mode }
+      = oflag { overlapMode = effective_overlap_mode noncanonical_incoherence overlap_mode }
+
+    -- The `-fspecialise-incoherents` flag controls the meaning of the
+    -- `Incoherent` overlap mode: as either an Incoherent overlap
+    -- flag, or a NonCanonical overlap flag. See Note [Coherence and specialisation: overview]
+    -- in GHC.Core.InstEnv for why we care about this distinction.
+    effective_overlap_mode noncanonical_incoherence = \case
+        Incoherent s | noncanonical_incoherence -> NonCanonical s
+        overlap_mode -> overlap_mode
+
 
 tcGetInsts :: TcM [ClsInst]
 -- Gets the local class instances.


=====================================
compiler/GHC/Types/Basic.hs
=====================================
@@ -44,7 +44,7 @@ module GHC.Types.Basic (
         TopLevelFlag(..), isTopLevel, isNotTopLevel,
 
         OverlapFlag(..), OverlapMode(..), setOverlapModeMaybe,
-        hasOverlappingFlag, hasOverlappableFlag, hasIncoherentFlag,
+        hasOverlappingFlag, hasOverlappableFlag, hasIncoherentFlag, hasNonCanonicalFlag,
 
         Boxity(..), isBoxed,
 
@@ -674,6 +674,7 @@ hasIncoherentFlag :: OverlapMode -> Bool
 hasIncoherentFlag mode =
   case mode of
     Incoherent   _ -> True
+    NonCanonical _ -> True
     _              -> False
 
 hasOverlappableFlag :: OverlapMode -> Bool
@@ -682,6 +683,7 @@ hasOverlappableFlag mode =
     Overlappable _ -> True
     Overlaps     _ -> True
     Incoherent   _ -> True
+    NonCanonical _ -> True
     _              -> False
 
 hasOverlappingFlag :: OverlapMode -> Bool
@@ -690,8 +692,14 @@ hasOverlappingFlag mode =
     Overlapping  _ -> True
     Overlaps     _ -> True
     Incoherent   _ -> True
+    NonCanonical _ -> True
     _              -> False
 
+hasNonCanonicalFlag :: OverlapMode -> Bool
+hasNonCanonicalFlag = \case
+  NonCanonical{} -> True
+  _              -> False
+
 data OverlapMode  -- See Note [Rules for instance lookup] in GHC.Core.InstEnv
   = NoOverlap SourceText
                   -- See Note [Pragma source text]
@@ -746,6 +754,16 @@ data OverlapMode  -- See Note [Rules for instance lookup] in GHC.Core.InstEnv
     -- instantiating 'b' would change which instance
     -- was chosen. See also Note [Incoherent instances] in "GHC.Core.InstEnv"
 
+  | NonCanonical SourceText
+    -- ^ Behave like Incoherent, but the instance choice is observable
+    -- by the program behaviour. See Note [Coherence and specialisation: overview].
+    --
+    -- We don't have surface syntax for the distinction between
+    -- Incoherent and NonCanonical instances; instead, the flag
+    -- `-f{no-}specialise-incoherents` (on by default) controls
+    -- whether `INCOHERENT` instances are regarded as Incoherent or
+    -- NonCanonical.
+
   deriving (Eq, Data)
 
 
@@ -758,6 +776,7 @@ instance Outputable OverlapMode where
    ppr (Overlapping  _) = text "[overlapping]"
    ppr (Overlaps     _) = text "[overlap ok]"
    ppr (Incoherent   _) = text "[incoherent]"
+   ppr (NonCanonical _) = text "[noncanonical]"
 
 instance Binary OverlapMode where
     put_ bh (NoOverlap    s) = putByte bh 0 >> put_ bh s
@@ -765,6 +784,7 @@ instance Binary OverlapMode where
     put_ bh (Incoherent   s) = putByte bh 2 >> put_ bh s
     put_ bh (Overlapping  s) = putByte bh 3 >> put_ bh s
     put_ bh (Overlappable s) = putByte bh 4 >> put_ bh s
+    put_ bh (NonCanonical s) = putByte bh 5 >> put_ bh s
     get bh = do
         h <- getByte bh
         case h of
@@ -773,6 +793,7 @@ instance Binary OverlapMode where
             2 -> (get bh) >>= \s -> return $ Incoherent s
             3 -> (get bh) >>= \s -> return $ Overlapping s
             4 -> (get bh) >>= \s -> return $ Overlappable s
+            5 -> (get bh) >>= \s -> return $ NonCanonical s
             _ -> panic ("get OverlapMode" ++ show h)
 
 


=====================================
docs/users_guide/using-optimisation.rst
=====================================
@@ -1144,6 +1144,25 @@ as such you shouldn't need to set any of them explicitly. A flag
     which returns a constrained type. For example, a type class where one
     of the methods implements a traversal.
 
+
+.. ghc-flag:: -fspecialise-incoherents
+    :shortdesc: Enable specialisation on incoherent instances
+    :type: dynamic
+    :reverse: -fno-specialise-incoherents
+    :category:
+
+    :default: on
+
+    Enable specialisation of overloaded functions in cases when the
+    selected instance is incoherent. This makes the choice of instance
+    non-deterministic, so it is only safe to do if there is no
+    observable runtime behaviour difference between potentially
+    unifying instances. Turning this flag off ensures the incoherent
+    instance selection adheres to the algorithm described in
+    :extension:`IncoherentInstances` at the cost of optimisation
+    opportunities arising from specialisation.
+
+
 .. ghc-flag:: -finline-generics
     :shortdesc: Annotate methods of derived Generic and Generic1 instances with
         INLINE[1] pragmas based on heuristics. Implied by :ghc-flag:`-O`.


=====================================
testsuite/tests/simplCore/should_run/T22448.hs
=====================================
@@ -1,4 +1,5 @@
 {-# LANGUAGE MonoLocalBinds #-}
+{-# OPTIONS_GHC -fno-specialise-incoherents #-}
 class C a where
   op :: a -> String
 


=====================================
utils/check-exact/ExactPrint.hs
=====================================
@@ -2079,6 +2079,11 @@ instance ExactPrint (LocatedP OverlapMode) where
     an1 <- markAnnCloseP an0
     return (L (SrcSpanAnn an1 l) (Incoherent src))
 
+  exact (L (SrcSpanAnn an l) (NonCanonical src)) = do
+    an0 <- markAnnOpenP an src "{-# INCOHERENT"
+    an1 <- markAnnCloseP an0
+    return (L (SrcSpanAnn an1 l) (Incoherent src))
+
 -- ---------------------------------------------------------------------
 
 instance ExactPrint (HsBind GhcPs) where



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/fa4e5913251786f2b535b31abd3fad39da8b3602...481f4a46a4efccff7242afcdda42c8df6325117f

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/fa4e5913251786f2b535b31abd3fad39da8b3602...481f4a46a4efccff7242afcdda42c8df6325117f
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230804/40a9db6d/attachment-0001.html>


More information about the ghc-commits mailing list