[Git][ghc/ghc][wip/incoherent-spec-flag] Add flag to enable/disable incoherent instances

Gergő Érdi (@cactus) gitlab at gitlab.haskell.org
Fri Jul 7 03:28:40 UTC 2023



Gergő Érdi pushed to branch wip/incoherent-spec-flag at Glasgow Haskell Compiler / GHC


Commits:
0a7fcb54 by Gergő Érdi at 2023-07-07T04:26:18+01:00
Add flag to enable/disable incoherent instances

Fixes #23287

- - - - -


24 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
- 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, pprInstances,
         instanceHead, instanceSig, mkLocalClsInst, mkImportedClsInst,
@@ -122,10 +122,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]
@@ -812,8 +813,33 @@ 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:
+
+  data IxEq i is js where { IxEq :: IxEq i is is }
+
+  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.  The flag `-fspecialise-incoherents` (on by default) enables
+specialisation on incoherent evidence (as has been the case previously).
+The rest of this note describes what happens with `-fno-specialise-incoherents`.
+
+To avoid this incoherence breaking the specialiser,
 
 * We label as "incoherent" the dictionary constructed by a
   (potentially) incoherent use of an instance declaration.
@@ -850,7 +876,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.
 -}
@@ -955,10 +981,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
@@ -972,28 +1001,19 @@ 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.
+If we don't have any potential unifiers (i.e. we know that we have a
+unique solution modulo `INCOHERENT` instances), we need 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 if it's `Canonical`.
 -}
 
-instance Outputable Coherence where
-  ppr IsCoherent = text "coherent"
-  ppr IsIncoherent = text "incoherent"
-
 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))
 
@@ -1039,22 +1059,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)
@@ -1111,7 +1133,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]
@@ -1289,7 +1311,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
 


=====================================
compiler/GHC/Driver/DynFlags.hs
=====================================
@@ -1168,7 +1168,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
=====================================
@@ -267,6 +267,7 @@ data GeneralFlag
    | Opt_LiberateCase
    | Opt_SpecConstr
    | Opt_SpecConstrKeen
+   | Opt_SpecialiseIncoherents
    | Opt_DoLambdaEtaExpansion
    | Opt_IgnoreAsserts
    | Opt_DoEtaReduction


=====================================
compiler/GHC/Driver/Session.hs
=====================================
@@ -2433,6 +2433,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
=====================================
@@ -911,6 +911,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 )
@@ -1152,14 +1152,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
 
@@ -1170,14 +1170,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.
 
 -}
 
@@ -1201,20 +1201,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)
@@ -1232,7 +1239,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
@@ -1240,53 +1247,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`
@@ -1295,13 +1299,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,
@@ -357,7 +357,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)
 
@@ -413,11 +413,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
=====================================
@@ -2628,6 +2628,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
=====================================
@@ -1212,11 +1212,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
=====================================
@@ -92,7 +92,7 @@ data ClsInstResult
 
   | OneInst { cir_new_theta   :: [TcPredType]
             , cir_mk_ev       :: [EvExpr] -> EvTerm
-            , cir_coherence   :: Coherence -- See Note [Coherence and specialisation: overview]
+            , cir_canonical   :: Canonical -- See Note [Coherence and specialisation: overview]
             , cir_what        :: InstanceWhat }
 
   | NotSure      -- Multiple matches and/or one or more unifiers
@@ -162,7 +162,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
@@ -175,12 +175,11 @@ matchInstEnv dflags short_cut_solver clas tys
                 | otherwise
                 -> do { let dfun_id = instanceDFunId 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 }
+                      ; match_one (null unsafeOverlaps) canonical dfun_id inst_tys }
 
             -- More than one matches (or Safe Haskell fail!). Defer any
             -- reactions of a multitude until we learn more about the reagent
@@ -191,15 +190,15 @@ matchInstEnv dflags short_cut_solver clas tys
    where
      pred = mkClassPred clas tys
 
-match_one :: SafeOverlapping -> Coherence -> DFunId -> [DFunInstType] -> TcM ClsInstResult
+match_one :: SafeOverlapping -> Canonical -> DFunId -> [DFunInstType] -> TcM ClsInstResult
              -- See Note [DFunInstType: instantiating types] in GHC.Core.InstEnv
-match_one so coherence dfun_id mb_inst_tys
+match_one so canonical dfun_id mb_inst_tys
   = 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 } } }
 
@@ -235,7 +234,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
@@ -399,7 +398,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
@@ -448,7 +447,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 }
        }
 
@@ -555,7 +554,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
@@ -641,7 +640,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]
@@ -658,7 +657,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
@@ -690,7 +689,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)
@@ -711,7 +710,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)]
@@ -946,7 +945,7 @@ matchHasField dflags short_cut clas tys
                              ; keepAlive (greName gre)
                              ; 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 )
@@ -184,7 +184,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]
@@ -394,7 +394,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" }
 
@@ -715,10 +715,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 () } } }
 
@@ -784,7 +784,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]
@@ -804,7 +804,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 }
@@ -847,7 +847,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
@@ -869,14 +869,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
@@ -1070,7 +1070,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
@@ -1317,7 +1317,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") }
@@ -2158,4 +2158,3 @@ constraints.
 
 See also Note [Evidence for quantified constraints] in GHC.Core.Predicate.
 -}
-


=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -32,7 +32,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
@@ -357,7 +356,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)
@@ -1847,7 +1846,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
@@ -1958,7 +1957,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" }
 
@@ -2541,7 +2540,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)
@@ -3188,4 +3187,4 @@ To avoid this situation we do not cache as solved any workitems (or inert)
 which did not really made a 'step' towards proving some goal. Solved's are
 just an optimization so we don't lose anything in terms of completeness of
 solving.
--}
\ No newline at end of file
+-}


=====================================
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
=====================================
@@ -1688,19 +1688,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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1726,10 +1726,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
=====================================
@@ -1482,7 +1482,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
@@ -451,7 +451,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]
     }
 
 -----------------
@@ -465,7 +465,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   #-}
 
@@ -820,16 +821,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
=====================================
@@ -43,7 +43,7 @@ module GHC.Types.Basic (
         TopLevelFlag(..), isTopLevel, isNotTopLevel,
 
         OverlapFlag(..), OverlapMode(..), setOverlapModeMaybe,
-        hasOverlappingFlag, hasOverlappableFlag, hasIncoherentFlag,
+        hasOverlappingFlag, hasOverlappableFlag, hasIncoherentFlag, hasNonCanonicalFlag,
 
         Boxity(..), isBoxed,
 
@@ -628,6 +628,7 @@ hasIncoherentFlag :: OverlapMode -> Bool
 hasIncoherentFlag mode =
   case mode of
     Incoherent   _ -> True
+    NonCanonical _ -> True
     _              -> False
 
 hasOverlappableFlag :: OverlapMode -> Bool
@@ -636,6 +637,7 @@ hasOverlappableFlag mode =
     Overlappable _ -> True
     Overlaps     _ -> True
     Incoherent   _ -> True
+    NonCanonical _ -> True
     _              -> False
 
 hasOverlappingFlag :: OverlapMode -> Bool
@@ -644,8 +646,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]
@@ -700,6 +708,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)
 
 
@@ -712,6 +730,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
@@ -719,6 +738,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
@@ -727,6 +747,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)
 
 


=====================================
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
=====================================
@@ -2081,6 +2081,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/-/commit/0a7fcb545dc7923964d7527480565d8fbc04010a

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0a7fcb545dc7923964d7527480565d8fbc04010a
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/20230706/49ce7340/attachment-0001.html>


More information about the ghc-commits mailing list