[Git][ghc/ghc][wip/T23923-mikolaj-take-2] Deleted 2 commits: Add DCoVarSet to PluginProv

Mikolaj Konarski (@Mikolaj) gitlab at gitlab.haskell.org
Thu Mar 7 22:46:59 UTC 2024



Mikolaj Konarski pushed to branch wip/T23923-mikolaj-take-2 at Glasgow Haskell Compiler / GHC


WARNING: The push did not contain any new commits, but force pushed to delete the commits and changes below.


Deleted commits:
70f2d3ee by Mikolaj Konarski at 2024-03-07T00:34:41+01:00
Add DCoVarSet to PluginProv

Add the only remaining piece of feedback from git add src/Flavour.hs

Help CI check some more of the patch

Fix the 3 plugin tests that fail

Explain better how shallowCoVarsOfCosDSet is entangled with a hundreds of lines bit-rotten refactoring

Fix according to the first round of Simon's instruction

Fix according to the second round of Simon's instruction

Remove a question-comment that's probably absurd

Fix according to the third round of Simon's instruction

- - - - -
053fdb81 by Mikolaj Konarski at 2024-03-07T00:34:41+01:00
Make sure the foldl' accumulators are strict

- - - - -


23 changed files:

- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/FVs.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Core/TyCo/Tidy.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/Iface/Rename.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/Iface/Type.hs
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Tc/TyCl/Utils.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Types/Unique/DSet.hs
- compiler/GHC/Types/Var/Set.hs
- compiler/GHC/Utils/FV.hs
- docs/users_guide/extending_ghc.rst
- testsuite/tests/tcplugins/CtIdPlugin.hs
- testsuite/tests/tcplugins/RewritePlugin.hs
- testsuite/tests/tcplugins/TyFamPlugin.hs


Changes:

=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -97,7 +97,7 @@ module GHC.Core.Coercion (
         emptyLiftingContext, extendLiftingContext, extendLiftingContextAndInScope,
         liftCoSubstVarBndrUsing, isMappedByLC, extendLiftingContextCvSubst,
 
-        mkSubstLiftingContext, zapLiftingContext,
+        mkSubstLiftingContext, liftingContextSubst, zapLiftingContext,
         substForAllCoBndrUsingLC, lcLookupCoVar, lcInScopeSet,
 
         LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight,
@@ -1397,7 +1397,7 @@ setNominalRole_maybe r co
     setNominalRole_maybe_helper (UnivCo prov _ co1 co2)
       | case prov of PhantomProv _    -> False  -- should always be phantom
                      ProofIrrelProv _ -> True   -- it's always safe
-                     PluginProv _     -> False  -- who knows? This choice is conservative.
+                     PluginProv _ _   -> False  -- who knows? This choice is conservative.
       = Just $ UnivCo prov Nominal co1 co2
     setNominalRole_maybe_helper _ = Nothing
 
@@ -1522,7 +1522,7 @@ promoteCoercion co = case co of
 
     UnivCo (PhantomProv kco)    _ _ _ -> kco
     UnivCo (ProofIrrelProv kco) _ _ _ -> kco
-    UnivCo (PluginProv _)       _ _ _ -> mkKindCo co
+    UnivCo (PluginProv _ _)     _ _ _ -> mkKindCo co
 
     SymCo g
       -> mkSymCo (promoteCoercion g)
@@ -1979,6 +1979,9 @@ mkLiftingContext pairs
 mkSubstLiftingContext :: Subst -> LiftingContext
 mkSubstLiftingContext subst = LC subst emptyVarEnv
 
+liftingContextSubst :: LiftingContext -> Subst
+liftingContextSubst (LC subst _) = subst
+
 -- | Extend a lifting context with a new mapping.
 extendLiftingContext :: LiftingContext  -- ^ original LC
                      -> TyCoVar         -- ^ new variable to map...
@@ -2354,7 +2357,7 @@ seqCo (AxiomRuleCo _ cs)        = seqCos cs
 seqProv :: UnivCoProvenance -> ()
 seqProv (PhantomProv co)    = seqCo co
 seqProv (ProofIrrelProv co) = seqCo co
-seqProv (PluginProv _)      = ()
+seqProv (PluginProv _ cvs)  = seqDVarSet cvs
 
 seqCos :: [Coercion] -> ()
 seqCos []       = ()


=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -641,7 +641,7 @@ opt_univ env sym prov role oty1 oty2
   where
     prov' = case prov of
       ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
-      PluginProv _       -> prov
+      PluginProv s cvs   -> PluginProv s $ substDCoVarSet (liftingContextSubst env) cvs
 
 -------------
 opt_transList :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
@@ -722,7 +722,8 @@ opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
       = Just $ PhantomProv $ opt_trans is kco1 kco2
     opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
       = Just $ ProofIrrelProv $ opt_trans is kco1 kco2
-    opt_trans_prov (PluginProv str1)     (PluginProv str2)     | str1 == str2 = Just p1
+    opt_trans_prov (PluginProv str1 cvs1) (PluginProv str2 cvs2)
+      | str1 == str2 = Just (PluginProv str1 (cvs1 `unionDVarSet` cvs2))
     opt_trans_prov _ _ = Nothing
 
 -- Push transitivity down through matching top-level constructors.


=====================================
compiler/GHC/Core/FVs.hs
=====================================
@@ -410,7 +410,7 @@ orphNamesOfCo (HoleCo _)            = emptyNameSet
 orphNamesOfProv :: UnivCoProvenance -> NameSet
 orphNamesOfProv (PhantomProv co)    = orphNamesOfCo co
 orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co
-orphNamesOfProv (PluginProv _)      = emptyNameSet
+orphNamesOfProv (PluginProv _ _)    = emptyNameSet
 
 orphNamesOfCos :: [Coercion] -> NameSet
 orphNamesOfCos = orphNamesOfThings orphNamesOfCo


=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -1931,6 +1931,13 @@ checkTyCon :: TyCon -> LintM ()
 checkTyCon tc
   = checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)
 
+-------------------
+checkTyCoVarInScope :: Subst -> TyCoVar -> LintM ()
+checkTyCoVarInScope subst tcv
+  = checkL (tcv `isInScope` subst) $
+    hang (text "The type or coercion variable" <+> pprBndr LetBind tcv)
+       2 (text "is out of scope")
+
 -------------------
 lintType :: Type -> LintM LintedType
 
@@ -1948,12 +1955,8 @@ lintType (TyVarTy tv)
            -- In GHCi we may lint an expression with a free
            -- type variable.  Then it won't be in the
            -- substitution, but it should be in scope
-           Nothing | tv `isInScope` subst
-                   -> return (TyVarTy tv)
-                   | otherwise
-                   -> failWithL $
-                      hang (text "The type variable" <+> pprBndr LetBind tv)
-                         2 (text "is out of scope")
+           Nothing -> do { checkTyCoVarInScope subst tv
+                         ; return (TyVarTy tv) }
      }
 
 lintType ty@(AppTy t1 t2)
@@ -2325,15 +2328,8 @@ lintCoercion (CoVarCo cv)
   = do { subst <- getSubst
        ; case lookupCoVar subst cv of
            Just linted_co -> return linted_co ;
-           Nothing
-              | cv `isInScope` subst
-                   -> return (CoVarCo cv)
-              | otherwise
-                   ->
-                      -- lintCoBndr always extends the substitution
-                      failWithL $
-                      hang (text "The coercion variable" <+> pprBndr LetBind cv)
-                         2 (text "is out of scope")
+           Nothing        -> do { checkTyCoVarInScope subst cv
+                                ; return (CoVarCo cv) }
      }
 
 
@@ -2532,7 +2528,12 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
             ; check_kinds kco k1 k2
             ; return (ProofIrrelProv kco') }
 
-     lint_prov _ _ prov@(PluginProv _) = return prov
+     lint_prov _ _ (PluginProv s cvs)
+        = do { subst <- getSubst
+             ; mapM_ (checkTyCoVarInScope subst) (dVarSetElems cvs)
+               -- Don't bother to return substituted fvs;
+               -- they don't matter to Lint
+             ; return (PluginProv s cvs) }
 
      check_kinds kco k1 k2
        = do { let Pair k1' k2' = coercionKind kco


=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -19,6 +19,7 @@ module GHC.Core.TyCo.FVs
         tyCoVarsOfCoDSet,
         tyCoFVsOfCo, tyCoFVsOfCos,
         tyCoVarsOfCoList,
+        coVarsOfCosDSet,
 
         almostDevoidCoVarOfCo,
 
@@ -446,6 +447,13 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView
                        -- See Note [CoercionHoles and coercion free variables]
                        -- in GHC.Core.TyCo.Rep
 
+------- Same again, but for DCoVarSet ----------
+--    But this time the free vars are shallow
+
+coVarsOfCosDSet :: [Coercion] -> DCoVarSet
+coVarsOfCosDSet cos = fvDVarSetSome isCoVar (tyCoFVsOfCos cos)
+
+
 {- *********************************************************************
 *                                                                      *
           Closing over kinds
@@ -660,7 +668,7 @@ tyCoFVsOfCoVar v fv_cand in_scope acc
 tyCoFVsOfProv :: UnivCoProvenance -> FV
 tyCoFVsOfProv (PhantomProv co)    fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
-tyCoFVsOfProv (PluginProv _)      fv_cand in_scope acc = emptyFV fv_cand in_scope acc
+tyCoFVsOfProv (PluginProv _ cvs)  fv_cand in_scope acc = mkFVs (dVarSetElems cvs) fv_cand in_scope acc
 
 tyCoFVsOfCos :: [Coercion] -> FV
 tyCoFVsOfCos []       fv_cand in_scope acc = emptyFV fv_cand in_scope acc
@@ -730,7 +738,7 @@ almost_devoid_co_var_of_prov (PhantomProv co) cv
   = almost_devoid_co_var_of_co co cv
 almost_devoid_co_var_of_prov (ProofIrrelProv co) cv
   = almost_devoid_co_var_of_co co cv
-almost_devoid_co_var_of_prov (PluginProv _) _ = True
+almost_devoid_co_var_of_prov (PluginProv _ cvs) cv = not (cv `elemDVarSet` cvs)
 
 almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
 almost_devoid_co_var_of_type (TyVarTy _) _ = True
@@ -1129,7 +1137,7 @@ tyConsOfType ty
 
      go_prov (PhantomProv co)    = go_co co
      go_prov (ProofIrrelProv co) = go_co co
-     go_prov (PluginProv _)      = emptyUniqSet
+     go_prov (PluginProv _ _)    = emptyUniqSet
 
      go_cos cos   = foldr (unionUniqSets . go_co)  emptyUniqSet cos
 
@@ -1340,4 +1348,4 @@ occCheckExpand vs_to_avoid ty
     ------------------
     go_prov cxt (PhantomProv co)    = PhantomProv <$> go_co cxt co
     go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
-    go_prov _   p@(PluginProv _)    = return p
+    go_prov _   p@(PluginProv _ _)  = return p


=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1,4 +1,3 @@
-
 {-# LANGUAGE DeriveDataTypeable #-}
 
 {-# OPTIONS_HADDOCK not-home #-}
@@ -78,7 +77,7 @@ import {-# SOURCE #-} GHC.Core.Type( chooseFunTyFlag, typeKind, typeTypeOrConstr
 
 -- friends:
 import GHC.Types.Var
-import GHC.Types.Var.Set( elemVarSet )
+import GHC.Types.Var.Set( DCoVarSet, dVarSetElems, elemVarSet )
 import GHC.Core.TyCon
 import GHC.Core.Coercion.Axiom
 
@@ -886,7 +885,7 @@ data Coercion
 
   | FunCo  -- FunCo :: "e" -> N/P -> e -> e -> e
            -- See Note [FunCo] for fco_afl, fco_afr
-       { fco_role         :: Role
+        { fco_role         :: Role
         , fco_afl          :: FunTyFlag   -- Arrow for coercionLKind
         , fco_afr          :: FunTyFlag   -- Arrow for coercionRKind
         , fco_mult         :: CoercionN
@@ -1527,15 +1526,19 @@ data UnivCoProvenance
                                  --   considered equivalent. See Note [ProofIrrelProv].
                                  -- Can be used in Nominal or Representational coercions
 
-  | PluginProv String  -- ^ From a plugin, which asserts that this coercion
-                       --   is sound. The string is for the use of the plugin.
+  | PluginProv String !DCoVarSet
+      -- ^ From a plugin, which asserts that this coercion is sound.
+      --   The string and the variable set are for the use by the plugin.
+      --   E.g., the set may contain the in-scope coercion variables
+      --   that the the proof represented by the coercion makes use of.
+      --   See Note [The importance of tracking free coercion variables].
 
   deriving Data.Data
 
 instance Outputable UnivCoProvenance where
-  ppr (PhantomProv _)    = text "(phantom)"
-  ppr (ProofIrrelProv _) = text "(proof irrel.)"
-  ppr (PluginProv str)   = parens (text "plugin" <+> brackets (text str))
+  ppr (PhantomProv _)      = text "(phantom)"
+  ppr (ProofIrrelProv _)   = text "(proof irrel.)"
+  ppr (PluginProv str cvs) = parens (text "plugin" <+> brackets (text str) <+> ppr cvs)
 
 -- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
 data CoercionHole
@@ -1690,6 +1693,50 @@ Here,
   where
     co5 :: (a1 ~ Bool) ~ (a2 ~ Bool)
     co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>]
+
+
+Note [The importance of tracking free coercion variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is vital that `UnivCo` (a coercion that lacks a proper proof)
+tracks its free coercion variables. To see why, consider this program:
+
+    type S :: Nat -> Nat
+
+    data T (a::Nat) where
+      T1 :: T 0
+      T2 :: ...
+
+    f :: T a -> S (a+1) -> S 1
+    f = /\a (x:T a) (y:a).
+        case x of
+          T1 (gco : a ~# 0) -> y |> wco
+
+For this to typecheck we need `wco :: S (a+1) ~# S 1`, given that `gco : a ~# 0`.
+To prove that we need to know that `a+1 = 1` if `a=0`, which a plugin might know.
+So it solves `wco` by providing a `UnivCo (PluginProv "my-plugin" gcvs) (a+1) 1`.
+
+    But the `gcvs` in `PluginProv` must mention `gco`.
+
+Why? Otherwise we might float the entire expression (y |> wco) out of the
+the case alternative for `T1` which brings `gco` into scope. If this
+happens then we aren't far from a segmentation fault or much worse.
+See #23923 for a real-world example of this happening.
+
+So it is /crucial/ for the `PluginProv` to mention, in `gcvs`, the coercion
+variables used by the plugin to justify the `UnivCo` that it builds.
+
+Note that we don't need to track
+* the coercion's free *type* variables
+* coercion variables free in kinds (we only need the "shallow" free covars)
+
+This means that we may float past type variables which the original
+proof had as free variables. While surprising, this doesn't jeopardise
+the validity of the coercion, which only depends upon the scoping
+relative to the free coercion variables.
+
+(The free coercion variables are kept as a DCoVarSet in UnivCo,
+since these sets are included in interface files.)
+
 -}
 
 
@@ -1856,7 +1903,9 @@ foldTyCo (TyCoFolder { tcf_view       = view
 
     go_prov env (PhantomProv co)    = go_co env co
     go_prov env (ProofIrrelProv co) = go_co env co
-    go_prov _   (PluginProv _)      = mempty
+    go_prov _   (PluginProv _ cvs)  = go_cvs env cvs
+
+    go_cvs env cvs = foldl' (\ !acc cv -> acc `mappend` covar env cv) mempty (dVarSetElems cvs)
 
 -- | A view function that looks through nothing.
 noView :: Type -> Maybe Type
@@ -1922,7 +1971,7 @@ coercionSize (AxiomRuleCo _ cs)  = 1 + sum (map coercionSize cs)
 provSize :: UnivCoProvenance -> Int
 provSize (PhantomProv co)    = 1 + coercionSize co
 provSize (ProofIrrelProv co) = 1 + coercionSize co
-provSize (PluginProv _)      = 1
+provSize (PluginProv _ _)    = 1
 
 {-
 ************************************************************************


=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -41,7 +41,7 @@ module GHC.Core.TyCo.Subst
         cloneTyVarBndr, cloneTyVarBndrs,
         substVarBndr, substVarBndrs,
         substTyVarBndr, substTyVarBndrs,
-        substCoVarBndr,
+        substCoVarBndr, substDCoVarSet,
         substTyVar, substTyVars, substTyVarToTyVar,
         substTyCoVars,
         substTyCoBndr, substForAllCoBndr,
@@ -910,12 +910,18 @@ subst_co subst co
 
     go_prov (PhantomProv kco)    = PhantomProv (go kco)
     go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
-    go_prov p@(PluginProv _)     = p
+    go_prov (PluginProv s cvs)   = PluginProv s $ substDCoVarSet subst cvs
 
     -- See Note [Substituting in a coercion hole]
     go_hole h@(CoercionHole { ch_co_var = cv })
       = h { ch_co_var = updateVarType go_ty cv }
 
+-- | Perform a substitution within a 'DVarSet' of free variables,
+-- returning the shallow free coercion variables.
+substDCoVarSet :: Subst -> DCoVarSet -> DCoVarSet
+substDCoVarSet subst cvs = coVarsOfCosDSet $ map (substCoVar subst) $
+                           dVarSetElems cvs
+
 substForAllCoBndr :: Subst -> TyCoVar -> KindCoercion
                   -> (Subst, TyCoVar, Coercion)
 substForAllCoBndr subst


=====================================
compiler/GHC/Core/TyCo/Tidy.hs
=====================================
@@ -20,9 +20,11 @@ import GHC.Data.FastString
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.FVs (tyCoVarsOfTypesWellScoped, tyCoVarsOfTypeList)
 
+import GHC.Data.Maybe (orElse)
 import GHC.Types.Name hiding (varName)
 import GHC.Types.Var
 import GHC.Types.Var.Env
+import GHC.Types.Var.Set
 import GHC.Utils.Misc (strictMap)
 
 import Data.List (mapAccumL)
@@ -233,9 +235,7 @@ tidyCo env@(_, subst) co
             -- the case above duplicates a bit of work in tidying h and the kind
             -- of tv. But the alternative is to use coercionKind, which seems worse.
     go (FunCo r afl afr w co1 co2) = ((FunCo r afl afr $! go w) $! go co1) $! go co2
-    go (CoVarCo cv)          = case lookupVarEnv subst cv of
-                                 Nothing  -> CoVarCo cv
-                                 Just cv' -> CoVarCo cv'
+    go (CoVarCo cv)          = CoVarCo $! go_cv cv
     go (HoleCo h)            = HoleCo h
     go (AxiomInstCo con ind cos) = AxiomInstCo con ind $! strictMap go cos
     go (UnivCo p r t1 t2)    = (((UnivCo $! (go_prov p)) $! r) $!
@@ -249,9 +249,11 @@ tidyCo env@(_, subst) co
     go (SubCo co)            = SubCo $! go co
     go (AxiomRuleCo ax cos)  = AxiomRuleCo ax $ strictMap go cos
 
+    go_cv cv = lookupVarEnv subst cv `orElse` cv
+
     go_prov (PhantomProv co)    = PhantomProv $! go co
     go_prov (ProofIrrelProv co) = ProofIrrelProv $! go co
-    go_prov p@(PluginProv _)    = p
+    go_prov (PluginProv s cvs)  = PluginProv s $ mapDVarSet go_cv cvs
 
 tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
 tidyCos env = strictMap (tidyCo env)


=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -580,7 +580,7 @@ expandTypeSynonyms ty
 
     go_prov subst (PhantomProv co)    = PhantomProv (go_co subst co)
     go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
-    go_prov _     p@(PluginProv _)    = p
+    go_prov _     p@(PluginProv _ _)  = p
 
       -- the "False" and "const" are to accommodate the type of
       -- substForAllCoBndrUsing, which is general enough to
@@ -912,7 +912,8 @@ mapTyCo mapper
         -> (go_ty (), go_tys (), go_co (), go_cos ())
 
 {-# INLINE mapTyCoX #-}  -- See Note [Specialising mappers]
-mapTyCoX :: Monad m => TyCoMapper env m
+mapTyCoX :: forall m env. Monad m
+         => TyCoMapper env m
          -> ( env -> Type       -> m Type
             , env -> [Type]     -> m [Type]
             , env -> Coercion   -> m Coercion
@@ -960,6 +961,7 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
     go_mco !_   MRefl    = return MRefl
     go_mco !env (MCo co) = MCo <$> (go_co env co)
 
+    go_co :: env -> Coercion -> m Coercion
     go_co !env (Refl ty)                  = Refl <$> go_ty env ty
     go_co !env (GRefl r ty mco)           = mkGReflCo r <$> go_ty env ty <*> go_mco env mco
     go_co !env (AppCo c1 c2)              = mkAppCo <$> go_co env c1 <*> go_co env c2
@@ -999,7 +1001,14 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
 
     go_prov !env (PhantomProv co)    = PhantomProv <$> go_co env co
     go_prov !env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
-    go_prov !_   p@(PluginProv _)    = return p
+    go_prov !env (PluginProv s cvs)  = PluginProv s <$> strictFoldDVarSet (do_cv env)
+                                                          (return emptyDVarSet) cvs
+
+    do_cv :: env -> CoVar -> m DTyCoVarSet -> m DTyCoVarSet
+    do_cv env v mfvs = do { fvs <- mfvs
+                          ; co  <- covar env v
+                          ; return (tyCoVarsOfCoDSet co `unionDVarSet` fvs) }
+
 
 
 {- *********************************************************************


=====================================
compiler/GHC/CoreToIface.hs
=====================================
@@ -88,6 +88,7 @@ import GHC.Utils.Panic
 import GHC.Utils.Misc
 
 import Data.Maybe ( isNothing, catMaybes )
+import Data.List ( partition )
 
 {- Note [Avoiding space leaks in toIface*]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -318,9 +319,11 @@ toIfaceCoercionX fr co
                             fr' = fr `delVarSet` tv
 
     go_prov :: UnivCoProvenance -> IfaceUnivCoProv
-    go_prov (PhantomProv co)    = IfacePhantomProv (go co)
-    go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co)
-    go_prov (PluginProv str)    = IfacePluginProv str
+    go_prov (PhantomProv co)     = IfacePhantomProv (go co)
+    go_prov (ProofIrrelProv co)  = IfaceProofIrrelProv (go co)
+    go_prov (PluginProv str cvs) = IfacePluginProv str (map toIfaceCoVar bound_cvs) free_cvs
+      where
+        (free_cvs, bound_cvs) = partition (`elemVarSet` fr) (dVarSetElems cvs)
 
 toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
 toIfaceTcArgs = toIfaceTcArgsX emptyVarSet


=====================================
compiler/GHC/Iface/Rename.hs
=====================================
@@ -678,6 +678,8 @@ rnIfaceCo (IfaceAxiomInstCo n i cs)
     = IfaceAxiomInstCo <$> rnIfaceGlobal n <*> pure i <*> mapM rnIfaceCo cs
 rnIfaceCo (IfaceUnivCo s r t1 t2)
     = IfaceUnivCo s r <$> rnIfaceType t1 <*> rnIfaceType t2
+        -- Renaming affects only type constructors, not coercion variables,
+        -- so no need to recurs into the provenance.
 rnIfaceCo (IfaceSymCo c)
     = IfaceSymCo <$> rnIfaceCo c
 rnIfaceCo (IfaceTransCo c1 c2)


=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -1795,7 +1795,7 @@ freeNamesIfCoercion (IfaceAxiomRuleCo _ax cos)
 freeNamesIfProv :: IfaceUnivCoProv -> NameSet
 freeNamesIfProv (IfacePhantomProv co)    = freeNamesIfCoercion co
 freeNamesIfProv (IfaceProofIrrelProv co) = freeNamesIfCoercion co
-freeNamesIfProv (IfacePluginProv _)      = emptyNameSet
+freeNamesIfProv (IfacePluginProv _ _ _)  = emptyNameSet
 
 freeNamesIfVarBndr :: VarBndr IfaceBndr vis -> NameSet
 freeNamesIfVarBndr (Bndr bndr _) = freeNamesIfBndr bndr


=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -399,7 +399,10 @@ data IfaceCoercion
 data IfaceUnivCoProv
   = IfacePhantomProv IfaceCoercion
   | IfaceProofIrrelProv IfaceCoercion
-  | IfacePluginProv String
+  | IfacePluginProv String [IfLclName] [Var]
+    -- Local covars and open (free) covars resp
+    -- See Note [Free tyvars in IfaceType]
+
 
 {- Note [Holes in IfaceCoercion]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -620,7 +623,7 @@ substIfaceType env ty
 
     go_prov (IfacePhantomProv co)    = IfacePhantomProv (go_co co)
     go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
-    go_prov co@(IfacePluginProv _)   = co
+    go_prov co@(IfacePluginProv _ _ _) = co
 
 substIfaceAppArgs :: IfaceTySubst -> IfaceAppArgs -> IfaceAppArgs
 substIfaceAppArgs env args
@@ -1954,8 +1957,8 @@ pprIfaceUnivCoProv (IfacePhantomProv co)
   = text "phantom" <+> pprParendIfaceCoercion co
 pprIfaceUnivCoProv (IfaceProofIrrelProv co)
   = text "irrel" <+> pprParendIfaceCoercion co
-pprIfaceUnivCoProv (IfacePluginProv s)
-  = text "plugin" <+> doubleQuotes (text s)
+pprIfaceUnivCoProv (IfacePluginProv s cvs fcvs)
+  = hang (text "plugin") 2 (sep [doubleQuotes (text s), ppr cvs, ppr fcvs])
 
 -------------------
 instance Outputable IfaceTyCon where
@@ -2324,9 +2327,11 @@ instance Binary IfaceUnivCoProv where
   put_ bh (IfaceProofIrrelProv a) = do
           putByte bh 2
           put_ bh a
-  put_ bh (IfacePluginProv a) = do
+  put_ bh (IfacePluginProv a cvs fcvs) = do
           putByte bh 3
           put_ bh a
+          assertPpr (null fcvs) (ppr cvs $$ ppr fcvs) $
+            put_ bh cvs
 
   get bh = do
       tag <- getByte bh
@@ -2336,7 +2341,8 @@ instance Binary IfaceUnivCoProv where
            2 -> do a <- get bh
                    return $ IfaceProofIrrelProv a
            3 -> do a <- get bh
-                   return $ IfacePluginProv a
+                   cvs <- get bh
+                   return $ IfacePluginProv a cvs []
            _ -> panic ("get IfaceUnivCoProv " ++ show tag)
 
 


=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -1491,7 +1491,10 @@ tcIfaceCo = go
 tcIfaceUnivCoProv :: IfaceUnivCoProv -> IfL UnivCoProvenance
 tcIfaceUnivCoProv (IfacePhantomProv kco)    = PhantomProv <$> tcIfaceCo kco
 tcIfaceUnivCoProv (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tcIfaceCo kco
-tcIfaceUnivCoProv (IfacePluginProv str)     = return $ PluginProv str
+tcIfaceUnivCoProv (IfacePluginProv str cvs fcvs) =
+  assertPpr (null fcvs) (ppr fcvs) $ do
+    cvs' <- mapM tcIfaceLclId cvs
+    return $ PluginProv str $ mkDVarSet cvs'
 
 {-
 ************************************************************************


=====================================
compiler/GHC/Tc/TyCl/Utils.hs
=====================================
@@ -156,7 +156,7 @@ synonymTyConsOfType ty
 
      go_prov (PhantomProv co)     = go_co co
      go_prov (ProofIrrelProv co)  = go_co co
-     go_prov (PluginProv _)       = emptyNameEnv
+     go_prov (PluginProv _ _)     = emptyNameEnv
 
      go_tc tc | isTypeSynonymTyCon tc = unitNameEnv (tyConName tc) tc
               | otherwise             = emptyNameEnv


=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -1592,7 +1592,10 @@ collect_cand_qtvs_co orig_ty cur_lvl bound = go_co
 
     go_prov dv (PhantomProv co)    = go_co dv co
     go_prov dv (ProofIrrelProv co) = go_co dv co
-    go_prov dv (PluginProv _)      = return dv
+    go_prov dv (PluginProv _ cvs)  = strictFoldDVarSet zt_cv (return dv) cvs
+
+    zt_cv :: CoVar -> TcM CandidatesQTvs -> TcM CandidatesQTvs
+    zt_cv cv mdvs = do { dvs <- mdvs; go_cv dvs cv }
 
     go_cv :: CandidatesQTvs -> CoVar -> TcM CandidatesQTvs
     go_cv dv@(DV { dv_cvs = cvs }) cv


=====================================
compiler/GHC/Types/Unique/DSet.hs
=====================================
@@ -33,7 +33,7 @@ module GHC.Types.Unique.DSet (
         lookupUniqDSet,
         uniqDSetToList,
         partitionUniqDSet,
-        mapUniqDSet
+        mapUniqDSet, strictFoldUniqDSet
     ) where
 
 import GHC.Prelude
@@ -125,7 +125,15 @@ partitionUniqDSet p = coerce . partitionUDFM p . getUniqDSet
 
 -- See Note [UniqSet invariant] in GHC.Types.Unique.Set
 mapUniqDSet :: Uniquable b => (a -> b) -> UniqDSet a -> UniqDSet b
-mapUniqDSet f = mkUniqDSet . map f . uniqDSetToList
+mapUniqDSet f (UniqDSet m) = UniqDSet $ unsafeCastUDFMKey $ mapUDFM f m
+-- Simply apply `f` to each element, retaining all the structure unchanged.
+-- The identification of keys and elements prevents a derived Functor
+-- instance, but `unsafeCastUDFMKey` makes it possible to apply the strict
+-- mapping from DFM.
+
+strictFoldUniqDSet :: (a -> r -> r) -> r -> UniqDSet a -> r
+strictFoldUniqDSet k r s = foldl' (\ !r e -> k e r) r $
+                           uniqDSetToList s
 
 -- Two 'UniqDSet's are considered equal if they contain the same
 -- uniques.


=====================================
compiler/GHC/Types/Var/Set.hs
=====================================
@@ -26,7 +26,7 @@ module GHC.Types.Var.Set (
         nonDetStrictFoldVarSet,
 
         -- * Deterministic Var set types
-        DVarSet, DIdSet, DTyVarSet, DTyCoVarSet,
+        DVarSet, DIdSet, DTyVarSet, DCoVarSet, DTyCoVarSet,
 
         -- ** Manipulating these sets
         emptyDVarSet, unitDVarSet, mkDVarSet,
@@ -38,7 +38,7 @@ module GHC.Types.Var.Set (
         isEmptyDVarSet, delDVarSet, delDVarSetList,
         minusDVarSet,
         nonDetStrictFoldDVarSet,
-        filterDVarSet, mapDVarSet,
+        filterDVarSet, mapDVarSet, strictFoldDVarSet,
         dVarSetMinusVarSet, anyDVarSet, allDVarSet,
         transCloDVarSet,
         sizeDVarSet, seqDVarSet,
@@ -232,6 +232,9 @@ type DIdSet      = UniqDSet Id
 -- | Deterministic Type Variable Set
 type DTyVarSet   = UniqDSet TyVar
 
+-- | Deterministic Coercion Variable Set
+type DCoVarSet   = UniqDSet CoVar
+
 -- | Deterministic Type or Coercion Variable Set
 type DTyCoVarSet = UniqDSet TyCoVar
 
@@ -308,6 +311,9 @@ allDVarSet p = allUDFM p . getUniqDSet
 mapDVarSet :: Uniquable b => (a -> b) -> UniqDSet a -> UniqDSet b
 mapDVarSet = mapUniqDSet
 
+strictFoldDVarSet :: (a -> r -> r) -> r -> UniqDSet a -> r
+strictFoldDVarSet = strictFoldUniqDSet
+
 filterDVarSet :: (Var -> Bool) -> DVarSet -> DVarSet
 filterDVarSet = filterUniqDSet
 


=====================================
compiler/GHC/Utils/FV.hs
=====================================
@@ -21,6 +21,7 @@ module GHC.Utils.FV (
         delFVs,
         filterFV,
         mapUnionFV,
+        fvDVarSetSome,
     ) where
 
 import GHC.Prelude
@@ -195,3 +196,7 @@ mkFVs :: [Var] -> FV
 mkFVs vars fv_cand in_scope acc =
   mapUnionFV unitFV vars fv_cand in_scope acc
 {-# INLINE mkFVs #-}
+
+fvDVarSetSome :: InterestingVarFun -> FV -> DVarSet
+fvDVarSetSome interesting_var fv =
+  mkDVarSet $ fst $ fv interesting_var emptyVarSet ([], emptyVarSet)


=====================================
docs/users_guide/extending_ghc.rst
=====================================
@@ -760,10 +760,33 @@ This evidence is ignored for Given constraints, which GHC
 "solves" simply by discarding them; typically this is used when they are
 uninformative (e.g. reflexive equations). For Wanted constraints, the
 evidence will form part of the Core term that is generated after
-typechecking, and can be checked by ``-dcore-lint``. It is possible for
-the plugin to create equality axioms for use in evidence terms, but GHC
-does not check their consistency, and inconsistent axiom sets may lead
-to segfaults or other runtime misbehaviour.
+typechecking, and can be checked by ``-dcore-lint``.
+
+When solving a Wanted equality constraint (of type ``t1 ~N# t2``
+or ``t1 ~R# t2`` for nominal and representation equalities respectively),
+the evidence (of type ``EvTerm``) will take the form ``EvExpr (Coercion co)``,
+where the coercion ``co`` has type ``co :: t1 ~N# t2`` or ``co :: t1 ~R# t2``
+respectively.
+
+It is up to the plugin to construct a suitable coercion ``co``.
+However, one possibility is to construct one of form ::
+
+    UnivCo (PluginProv "my-plugin" gcvs) role t1 t2
+
+A ``UnivCo`` of this form says "trust me: my-plugin has solved this Wanted
+using (only) ``gcvs``".
+
+Here
+
+* The ``role`` should be the role of the original equality constraint
+  (nominal or representational).
+* The ``gcvs`` is a set of "given coercion variables"; these are the coercion
+  variable bound by enclosing Given constraints, which the plugin has used
+  to justify solving the Wanted.
+
+For soundness, it is very important to include the ``gcvs``; otherwise
+GHC may transform the program into a form that seg-faults.
+See #23923 for a long dicussion.
 
 Evidence is required also when creating new Given constraints, which are
 usually implied by old ones. It is not uncommon that the evidence of a new


=====================================
testsuite/tests/tcplugins/CtIdPlugin.hs
=====================================
@@ -21,6 +21,7 @@ import GHC.Tc.Plugin
 import GHC.Tc.Types
 import GHC.Tc.Types.Constraint
 import GHC.Tc.Types.Evidence
+import GHC.Types.Unique.DSet
 
 -- common
 import Common
@@ -41,7 +42,7 @@ solver :: [String]
        -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct]
        -> TcPluginM TcPluginSolveResult
 solver _args defs ev givens wanteds = do
-  let pluginCo = mkUnivCo (PluginProv "CtIdPlugin") Representational
+  let pluginCo = mkUnivCo (PluginProv "CtIdPlugin" emptyUniqDSet) Representational  -- Empty is fine. This plugin does not use "givens".
   let substEvidence ct ct' =
         evCast (ctEvExpr $ ctEvidence ct') $ pluginCo (ctPred ct') (ctPred ct)
 


=====================================
testsuite/tests/tcplugins/RewritePlugin.hs
=====================================
@@ -45,6 +45,8 @@ import GHC.Tc.Types.Constraint
   )
 import GHC.Tc.Types.Evidence
   ( EvTerm(EvExpr), Role(Nominal) )
+import GHC.Types.Unique.DSet
+  ( emptyUniqDSet )
 import GHC.Types.Unique.FM
   ( UniqFM, listToUFM )
 
@@ -85,5 +87,5 @@ mkTyFamReduction :: TyCon -> [ Type ] -> Type -> Reduction
 mkTyFamReduction tyCon args res = Reduction co res
   where
     co :: Coercion
-    co = mkUnivCo ( PluginProv "RewritePlugin" ) Nominal
+    co = mkUnivCo ( PluginProv "RewritePlugin" emptyUniqDSet) Nominal  -- Empty is fine. This plugin does not use "givens".
            ( mkTyConApp tyCon args ) res


=====================================
testsuite/tests/tcplugins/TyFamPlugin.hs
=====================================
@@ -39,6 +39,8 @@ import GHC.Tc.Types.Constraint
   )
 import GHC.Tc.Types.Evidence
   ( EvBindsVar, EvTerm(EvExpr), Role(Nominal) )
+import GHC.Types.Unique.DSet
+  ( emptyUniqDSet )
 
 -- common
 import Common
@@ -78,6 +80,6 @@ solveCt ( PluginDefs {..} ) ct@( classifyPredType . ctPred -> EqPred NomEq lhs r
   , let
       evTerm :: EvTerm
       evTerm = EvExpr . Coercion
-             $ mkUnivCo ( PluginProv "TyFamPlugin" ) Nominal lhs rhs
+             $ mkUnivCo ( PluginProv "TyFamPlugin" emptyUniqDSet) Nominal lhs rhs  -- Empty is fine. This plugin does not use "givens".
   = pure $ Just ( evTerm, ct )
 solveCt _ ct = pure Nothing



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/c4b131133e4cee35d2140eedfcf3b4e573a43a8a...053fdb81f509cc6158c5d645ef2402e24ca3c115

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/c4b131133e4cee35d2140eedfcf3b4e573a43a8a...053fdb81f509cc6158c5d645ef2402e24ca3c115
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/20240307/286e1cd8/attachment-0001.html>


More information about the ghc-commits mailing list