diff --git a/compiler/GHC/Core/InstEnv.hs b/compiler/GHC/Core/InstEnv.hs
index 70681c84a4ee3d171547f293096eb2b6613ac2a6..53d1652df4d78a3524220299c232260cad50b9cb 100644
--- a/compiler/GHC/Core/InstEnv.hs
+++ b/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,14 +813,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
@@ -850,7 +886,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 +991,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
@@ -967,33 +1006,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))
 
@@ -1039,22 +1073,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@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 +1147,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 +1325,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
 
@@ -1446,33 +1482,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.
 
 ************************************************************************
 *                                                                      *
diff --git a/compiler/GHC/Driver/DynFlags.hs b/compiler/GHC/Driver/DynFlags.hs
index 00cbaf6fea25391c03ffa02ac08a041f063dc72a..fa48094b4bfe75a328838cd504777336525b583c 100644
--- a/compiler/GHC/Driver/DynFlags.hs
+++ b/compiler/GHC/Driver/DynFlags.hs
@@ -1187,7 +1187,8 @@ defaultFlags settings
       Opt_CompactUnwind,
       Opt_ShowErrorContext,
       Opt_SuppressStgReps,
-      Opt_UnoptimizedCoreForInterpreter
+      Opt_UnoptimizedCoreForInterpreter,
+      Opt_SpecialiseIncoherents
     ]
 
     ++ [f | (ns,f) <- optLevelFlags, 0 `elem` ns]
diff --git a/compiler/GHC/Driver/Flags.hs b/compiler/GHC/Driver/Flags.hs
index 868c8783f65b31eba1001bc3ea10722ba2ee64ba..8a00f0b0cc5bf99a9ff89aefbd3303e54fb470e8 100644
--- a/compiler/GHC/Driver/Flags.hs
+++ b/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
diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs
index 4922dfb851cf59b1759a1447cd867c0d6ec1161b..e00b5971e75994800c5bf1c98b1454cce47b2c29 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -2445,6 +2445,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,
diff --git a/compiler/GHC/Hs/Decls.hs b/compiler/GHC/Hs/Decls.hs
index 605fb40f6a06d19b993ca35c808ecb010e7c67fe..282d80136b1609aef77d1be6ac31d63edca8705e 100644
--- a/compiler/GHC/Hs/Decls.hs
+++ b/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 "#-}"
diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs
index 02d4bd8b12ab31ac7556d9a27cddb730304b56e1..c98e97b38f5df6c5311357f8f801b63e01ee38fc 100644
--- a/compiler/GHC/HsToCore/Binds.hs
+++ b/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 )
@@ -1153,14 +1153,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
 
@@ -1171,14 +1171,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.
 
 -}
 
@@ -1202,20 +1202,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)
@@ -1233,7 +1240,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
@@ -1241,53 +1248,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`
@@ -1296,13 +1300,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)
 
 
 {-**********************************************************************
diff --git a/compiler/GHC/HsToCore/Monad.hs b/compiler/GHC/HsToCore/Monad.hs
index 6ba19bb95892004e6cd7a2363cc44f3f9019ea46..575efd3f98d40ce9657a0858612e1163df32cad7 100644
--- a/compiler/GHC/HsToCore/Monad.hs
+++ b/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
diff --git a/compiler/GHC/HsToCore/Quote.hs b/compiler/GHC/HsToCore/Quote.hs
index dc3dc2c96e79a23e4fa23698f804f2ce2215ef45..a71a791a5b4331121a59fbf27bbe99ad9bce7bb2 100644
--- a/compiler/GHC/HsToCore/Quote.hs
+++ b/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
diff --git a/compiler/GHC/HsToCore/Types.hs b/compiler/GHC/HsToCore/Types.hs
index 93a065a7da7b43c5549d524abff51923f1f5fd57..d6e4ae1aa89549aae8b5daf266f2287ba6d22897 100644
--- a/compiler/GHC/HsToCore/Types.hs
+++ b/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
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index e1cdea6cf826974073a17c59f4e0f1c008b55092..43d6f172357d88661c4796438ea83977a434adaf 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -1216,11 +1216,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
 
diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs
index 52540fa3f02f1999c6df61d4389d5eb0e1d5f79d..fa5c7a4b3aa8f467c79228dbec829b2f41fb2412 100644
--- a/compiler/GHC/Tc/Gen/Splice.hs
+++ b/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]
diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs
index a22ff699d16ca245e9127488aa929f0eda2f2a16..1bb0366bdfa60d9c1bffa83ef0de854ccc172824 100644
--- a/compiler/GHC/Tc/Instance/Class.hs
+++ b/compiler/GHC/Tc/Instance/Class.hs
@@ -92,7 +92,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
@@ -162,7 +165,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 +178,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 +193,15 @@ matchInstEnv dflags short_cut_solver clas tys
    where
      pred = mkClassPred clas tys
 
-match_one :: SafeOverlapping -> Coherence -> DFunId -> [DFunInstType] -> TcM ClsInstResult
-             -- See Note [DFunInstType: instantiating types] in GHC.Core.InstEnv
-match_one so coherence dfun_id mb_inst_tys
+match_one :: SafeOverlapping -> Canonical -> DFunId -> [DFunInstType]
+          -> TcM ClsInstResult
+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 +237,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 +401,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 +450,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 +557,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 +643,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 +660,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 +692,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 +713,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 +948,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 }
 
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index fb2926a74233a27be63e8ed148939f2169333f44..094ee9d3d05342f51f52ef4f4d64449fc8b1518d 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/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
diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs
index c7298ddf0d1b8dbc6a10d88ff8c8388de1ada17b..936b86b371853bbd14e518a3c670217e3effcf2b 100644
--- a/compiler/GHC/Tc/Solver/Dict.hs
+++ b/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]
@@ -409,7 +409,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" }
 
@@ -730,10 +730,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 () } } }
 
@@ -799,7 +799,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]
@@ -821,7 +821,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 }
@@ -864,7 +864,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
@@ -886,14 +886,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
@@ -1087,7 +1087,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
@@ -1334,7 +1334,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") }
@@ -2175,4 +2175,3 @@ constraints.
 
 See also Note [Evidence for quantified constraints] in GHC.Core.Predicate.
 -}
-
diff --git a/compiler/GHC/Tc/Solver/Equality.hs b/compiler/GHC/Tc/Solver/Equality.hs
index 0dc574723279862183cb237343f853b1d437df16..a54a8f8ccedf92b65c8b2db39a4f3ad630fe1ad8 100644
--- a/compiler/GHC/Tc/Solver/Equality.hs
+++ b/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)
diff --git a/compiler/GHC/Tc/Solver/Irred.hs b/compiler/GHC/Tc/Solver/Irred.hs
index 18b07c9d6420cf5c615c9a6206bd120bcb464f52..5bf36ac2668458739ab1c65d3b436c1d80f95361 100644
--- a/compiler/GHC/Tc/Solver/Irred.hs
+++ b/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 () } }
 
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index bf21783397f154daadbc238d84d0aee29dcee01d..a95da0a1acdadcb73948dcffbf4e83afab98d914 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/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
diff --git a/compiler/GHC/Tc/Solver/Solve.hs b/compiler/GHC/Tc/Solver/Solve.hs
index 7d0c9bfabf428d00038a8fe9c7982a8f21f9ecf7..95af74d4df5db7ae7c319ba12af00eeec5cec5df 100644
--- a/compiler/GHC/Tc/Solver/Solve.hs
+++ b/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
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 56ff78423ef2e9057145839110f6d7f9cbb7ecda..2951154802ed8dd378cab8e20964717798b28c0f 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -1491,7 +1491,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
diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs
index 81266433f117900063e2bcc63d904a6c048b0f56..298749e7be237cb4f4f7fa1a7ccf99704436f1da 100644
--- a/compiler/GHC/Tc/Types/Evidence.hs
+++ b/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
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index e2b25da1e9a1ddf4eabb807e95628344108ab293..bcc4fadfe04df16338564229a15ca6d79a1a8abe 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/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@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.
diff --git a/compiler/GHC/Types/Basic.hs b/compiler/GHC/Types/Basic.hs
index e743276e0ee83c84d9bbc3d17ba176dee306cffe..493f810ccd90273cde4bad44c00cf008ffa3c3da 100644
--- a/compiler/GHC/Types/Basic.hs
+++ b/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,
 
@@ -673,6 +673,7 @@ hasIncoherentFlag :: OverlapMode -> Bool
 hasIncoherentFlag mode =
   case mode of
     Incoherent   _ -> True
+    NonCanonical _ -> True
     _              -> False
 
 hasOverlappableFlag :: OverlapMode -> Bool
@@ -681,6 +682,7 @@ hasOverlappableFlag mode =
     Overlappable _ -> True
     Overlaps     _ -> True
     Incoherent   _ -> True
+    NonCanonical _ -> True
     _              -> False
 
 hasOverlappingFlag :: OverlapMode -> Bool
@@ -689,8 +691,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]
@@ -745,6 +753,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)
 
 
@@ -757,6 +775,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
@@ -764,6 +783,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
@@ -772,6 +792,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)
 
 
diff --git a/docs/users_guide/using-optimisation.rst b/docs/users_guide/using-optimisation.rst
index 3b766ea57fe65a6db008a420af80f830fdb371fd..930d1a8d7eb191ea51cd89771855af443ee6f7dd 100644
--- a/docs/users_guide/using-optimisation.rst
+++ b/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`.
diff --git a/testsuite/tests/simplCore/should_run/T22448.hs b/testsuite/tests/simplCore/should_run/T22448.hs
index 97eb3064ba30716ea9aaa073c1ed5ebf6d9bdc20..fce0a45101e6037f978b9e45e4677f8674086803 100644
--- a/testsuite/tests/simplCore/should_run/T22448.hs
+++ b/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
 
diff --git a/utils/check-exact/ExactPrint.hs b/utils/check-exact/ExactPrint.hs
index 73d268412c7c42ed3095f723cffd363f2c04573c..4d52754d09658a803abee99afe1ee9d15bd25abe 100644
--- a/utils/check-exact/ExactPrint.hs
+++ b/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