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

Gergő Érdi (@cactus) gitlab at gitlab.haskell.org
Tue Jul 4 02:54:19 UTC 2023



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


Commits:
880126b3 by Gergő Érdi at 2023-07-04T03:54:08+01:00
Add flag to enable/disable incoherent instances

Fixes #23287

- - - - -


9 changed files:

- compiler/GHC/Core/InstEnv.hs
- compiler/GHC/Driver/DynFlags.hs
- compiler/GHC/Driver/Flags.hs
- compiler/GHC/Driver/Session.hs
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/HsToCore/Monad.hs
- compiler/GHC/HsToCore/Types.hs
- compiler/GHC/Tc/Instance/Class.hs
- testsuite/tests/simplCore/should_run/T22448.hs


Changes:

=====================================
compiler/GHC/Core/InstEnv.hs
=====================================
@@ -812,8 +812,19 @@ 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. However, the
+specialiser crucially depends on evidence dictionaries being
+singletons. Something has to give: either we avoid specialising
+dictionaries that were incoherently constructed, leaving optimisation
+opportunities on the table (see discussions in #23287); or we assume
+that the choice of instance doesn't matter for the behaviour of the
+program, leaving this as a proof obligation to the user. The flags
+`-fspecialise-incoherents` (on by default) selects the second
+behaviour, i.e. enables specialisation on incoherent evidence. 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.
@@ -955,7 +966,18 @@ data LookupInstanceErrReason =
   LookupInstErrNotFound
   deriving (Generic)
 
-data Coherence = IsCoherent | IsIncoherent
+data Coherence =
+    -- | Coherent evidence that is always safe to specialise on
+    IsCoherent
+    |
+    -- | Incoherent evidence. The user might decide that they're OK with
+    -- specialising these. See Note [Coherence and specialisation: overview]
+    -- for the subtleties of this situation.
+    IsIncoherent
+    |
+    -- | Non-canonical evidence, a la `withDict`. Never OK to specialise.
+    -- See Note [withDict] in GHC.Tc.Instance.Class for details.
+    IsNoncanonical
 
 -- See Note [Recording coherence information in `PotentialUnifiers`]
 data PotentialUnifiers = NoUnifiers Coherence
@@ -983,6 +1005,7 @@ potential unifiers is otherwise empty.
 instance Outputable Coherence where
   ppr IsCoherent = text "coherent"
   ppr IsIncoherent = text "incoherent"
+  ppr IsNoncanonical = text "non-canonical"
 
 instance Outputable PotentialUnifiers where
   ppr (NoUnifiers c) = text "NoUnifiers" <+> ppr c
@@ -990,6 +1013,8 @@ instance Outputable PotentialUnifiers where
 
 instance Semigroup Coherence where
   IsCoherent <> IsCoherent = IsCoherent
+  IsNoncanonical <> _ = IsNoncanonical
+  _ <> IsNoncanonical = IsNoncanonical
   _ <> _ = IsIncoherent
 
 instance Semigroup PotentialUnifiers where


=====================================
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/HsToCore/Binds.hs
=====================================
@@ -1201,20 +1201,23 @@ 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 incoherent 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 }
 
 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)
@@ -1236,40 +1239,46 @@ dsTcEvBinds (EvBinds bs)   = dsEvBinds bs
 --     for each binder in ev_binds, before invoking thing_inside
 dsEvBinds :: Bag EvBind -> ([CoreBind] -> DsM a) -> DsM a
 dsEvBinds ev_binds thing_inside
+  = do { spec_incoherents <- getSpecIncoherents
+       ; ds_ev_binds spec_incoherents ev_binds thing_inside }
+
+ds_ev_binds :: Bool -> Bag EvBind -> ([CoreBind] -> DsM a) -> DsM a
+ds_ev_binds spec_incoherents ev_binds thing_inside
   = do { ds_binds <- mapBagM dsEvBind ev_binds
        ; let comps = sort_ev_binds ds_binds
        ; go comps thing_inside }
   where
     go ::[SCC (Node EvVar (Coherence, 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
+    is_specable IsCoherent = True
+    is_specable IsIncoherent = spec_incoherents
+    is_specable IsNoncanonical = 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
+        transitively_unspecable = not (is_specable this_coherence) || 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
 
-        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 (is_specable this_coherence) || any is_unspecable_remote deps | (this_coherence, deps) <- direct_coherence ]
+            -- Bindings from a given SCC are transitively specialisable if
+            -- all are specialisable and all their remote dependencies are
+            -- also specialisable; see Note [Desugaring incoherent 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))


=====================================
compiler/GHC/HsToCore/Monad.hs
=====================================
@@ -37,7 +37,7 @@ module GHC.HsToCore.Monad (
         getPmNablas, updPmNablas,
 
         -- Tracking evidence variable coherence
-        addIncoherents, getIncoherents,
+        getSpecIncoherents, addUnspecables, getUnspecables,
 
         -- Get COMPLETE sets of a TyCon
         dsGetCompleteMatches,
@@ -248,8 +248,10 @@ mkDsEnvsFromTcGbl hsc_env msg_var tcg_env
                                 ++ eps_complete_matches eps     -- from imports
              -- re-use existing next_wrapper_num to ensure uniqueness
              next_wrapper_num_var = tcg_next_wrapper_num tcg_env
+             spec_incoherents = gopt Opt_SpecialiseIncoherents (hsc_dflags hsc_env)
        ; return $ mkDsEnvs unit_env this_mod rdr_env type_env fam_inst_env ptc
                            msg_var cc_st_var next_wrapper_num_var complete_matches
+                           spec_incoherents
        }
 
 runDs :: HscEnv -> (DsGblEnv, DsLclEnv) -> DsM a -> IO (Messages DsMessage, Maybe a)
@@ -282,6 +284,7 @@ initDsWithModGuts hsc_env (ModGuts { mg_module = this_mod, mg_binds = binds
              complete_matches = hptCompleteSigs hsc_env     -- from the home package
                                 ++ local_complete_matches  -- from the current module
                                 ++ eps_complete_matches eps -- from imports
+             spec_incoherents = gopt Opt_SpecialiseIncoherents (hsc_dflags hsc_env)
 
              bindsToIds (NonRec v _)   = [v]
              bindsToIds (Rec    binds) = map fst binds
@@ -290,6 +293,7 @@ initDsWithModGuts hsc_env (ModGuts { mg_module = this_mod, mg_binds = binds
              envs  = mkDsEnvs unit_env this_mod rdr_env type_env
                               fam_inst_env ptc msg_var cc_st_var
                               next_wrapper_num complete_matches
+                              spec_incoherents
        ; runDs hsc_env envs thing_inside
        }
 
@@ -330,9 +334,10 @@ mkDsEnvs :: UnitEnv -> Module -> GlobalRdrEnv -> TypeEnv -> FamInstEnv
          -> PromotionTickContext
          -> IORef (Messages DsMessage) -> IORef CostCentreState
          -> IORef (ModuleEnv Int) -> CompleteMatches
+         -> Bool
          -> (DsGblEnv, DsLclEnv)
 mkDsEnvs unit_env mod rdr_env type_env fam_inst_env ptc msg_var cc_st_var
-         next_wrapper_num complete_matches
+         next_wrapper_num complete_matches spec_incoherents
   = let if_genv = IfGblEnv { if_doc       = text "mkDsEnvs"
   -- Failing tests here are `ghci` and `T11985` if you get this wrong.
   -- this is very very "at a distance" because the reason for this check is that the type_env in interactive
@@ -353,11 +358,12 @@ mkDsEnvs unit_env mod rdr_env type_env fam_inst_env ptc msg_var cc_st_var
                            , ds_complete_matches = complete_matches
                            , ds_cc_st   = cc_st_var
                            , ds_next_wrapper_num = next_wrapper_num
+                           , ds_spec_incoherents = spec_incoherents
                            }
         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 +419,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
@@ -523,6 +529,9 @@ discardWarningsDs thing_inside
 
         ; return result }
 
+getSpecIncoherents :: DsM Bool
+getSpecIncoherents = ds_spec_incoherents <$> getGblEnv
+
 -- | Inject a trace message into the compiled program. Whereas
 -- pprTrace prints out information *while compiling*, pprRuntimeTrace
 -- captures that information and causes it to be printed *at runtime*


=====================================
compiler/GHC/HsToCore/Types.hs
=====================================
@@ -11,7 +11,7 @@ module GHC.HsToCore.Types (
         DsMetaEnv, DsMetaVal(..), CompleteMatches
     ) where
 
-import GHC.Prelude (Int)
+import GHC.Prelude (Int, Bool)
 
 import Data.IORef
 import qualified Data.Set as S
@@ -65,6 +65,8 @@ data DsGblEnv
      -- Tracking indices for cost centre annotations
   , ds_next_wrapper_num :: IORef (ModuleEnv Int)
     -- ^ See Note [Generating fresh names for FFI wrappers]
+
+  , ds_spec_incoherents :: Bool
   }
 
 instance ContainsModule DsGblEnv where
@@ -79,9 +81,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
+  , dsl_unspecables :: S.Set EvVar
   -- ^ See Note [Desugaring incoherent evidence]: this field collects
-  -- all incoherent evidence variables in scope.
+  -- all un-specialisable evidence variables in scope.
   }
 
 -- Inside [| |] brackets, the desugarer looks


=====================================
compiler/GHC/Tc/Instance/Class.hs
=====================================
@@ -448,7 +448,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_coherence   = IsNoncanonical -- See (WD6) in Note [withDict]
                           , cir_what        = BuiltinInstance }
        }
 


=====================================
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
 



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/880126b39b65269d5e34239208fcad8505acadfa

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/880126b39b65269d5e34239208fcad8505acadfa
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/20230703/e7259929/attachment-0001.html>


More information about the ghc-commits mailing list