v 0.13.0.0, with proper GHC 9.12 support

changelog.md

@@ -1,6 +1,22 @@
+# Version 0.13.0.0 (2024-30-10)
+
+- Update to changes in the type of GHC's `mkUnivCo`
+  in order to (properly) add support for GHC 9.12.
+
+- Change `mkPluginUnivCo`, `mkPluginUnivEvTerm` and `mkTyFamAppReduction`
+  to take a `[Coercion]` rather than a `DVarSet` for specifying dependencies.
+
+- Stop re-exporting `DVarSet`, `emptyDVarSet`, `extendDVarSet`, `unionDVarSet`,
+  `unitDVarSet`, and `mkDVarSet`.
+
+- Update documentation to suggest using `ctEvCoercion`
+  rather than `ctEvId` to specify coercions that a `UnivCo` depends on.
+
+- Re-export `ctEvCoercion`, and stop re-exporting `ctEvId`.
+
 # Version 0.12.0.0 (2024-22-10)
 
-- Add support for GHC 9.12.
+- Add preliminary support for GHC 9.12.
 
 - `mkPluginUnivCo`, `mkPluginUnivEvTerm` and `mkTyFamAppReduction` now all take
   an additional `DVarSet` argument which allows specifying evidence that we

examples/SystemF/src/SystemF/Plugin.hs

@@ -98,27 +98,27 @@ pattern NoReduction = False
 pattern DidRewrite :: RewriteQ
 pattern DidRewrite = True
 
-type RewriteM = StateT ( RewriteQ, DVarSet ) ( TcPluginM Rewrite )
+type RewriteM = StateT ( RewriteQ, [ Coercion ] ) ( TcPluginM Rewrite )
 
-runRewriteM :: RewriteM a -> TcPluginM Rewrite ( Maybe ( a, DVarSet ) )
+runRewriteM :: RewriteM a -> TcPluginM Rewrite ( Maybe ( a, [ Coercion ] ) )
 runRewriteM ma = do
-  ( a, ( didRewrite, deps ) ) <- State.runStateT ma ( NoReduction, emptyDVarSet )
+  ( a, ( didRewrite, deps ) ) <- State.runStateT ma ( NoReduction, [] )
   pure $
     if didRewrite
     then Just ( a, deps )
     else Nothing
 
-rewrote :: DVarSet -> RewriteM ()
-rewrote deps = State.modify ( \ ( _, deps0 ) -> ( DidRewrite, deps0 `unionDVarSet` deps ) )
+rewrote :: [ Coercion ] -> RewriteM ()
+rewrote deps = State.modify ( \ ( _, deps0 ) -> ( DidRewrite, deps0 ++ deps ) )
 
 askIfRewrote :: RewriteM a -> RewriteM ( a, RewriteQ )
 askIfRewrote ma = do
   ( before, deps1 ) <- State.get
-  State.put ( NoReduction, emptyDVarSet )
+  State.put ( NoReduction, [] )
   a <- ma
   ( didRewrite, deps2 ) <- State.get
   State.put
-    ( before || didRewrite, deps1 `unionDVarSet` deps2 )
+    ( before || didRewrite, deps1 ++ deps2 )
   pure ( a, didRewrite )
 
 pluginRewrite :: PluginDefs -> UniqFM TyCon TcPluginRewriter
@@ -139,7 +139,7 @@ rewriteSub defs@( PluginDefs { .. } ) givens applySubArgs
   = pure $ TcPluginNoRewrite
   where
 
-    finish :: Maybe ( Type, DVarSet ) -> TcPluginRewriteResult
+    finish :: Maybe ( Type, [ Coercion ] ) -> TcPluginRewriteResult
     finish ( Just ( ty, deps ) ) =
       TcPluginRewriteTo
         ( mkTyFamAppReduction "SystemF.Plugin" Nominal deps applySubTyCon applySubArgs ty )
@@ -185,7 +185,7 @@ canonicaliseSub defs@( PluginDefs { .. } ) givens kϕ kψ k = go
       , tc2 == composeTyCon
       = do
         lift $ tcPluginTrace "AssEnv" ( ppr t $$ ppr s $$ ppr r )
-        rewrote emptyDVarSet
+        rewrote []
         go $
           mkTyConApp composeTyCon
             [ kϕ1, kψ2, kξ1
@@ -200,7 +200,7 @@ canonicaliseSub defs@( PluginDefs { .. } ) givens kϕ kψ k = go
       , tc2 == extendTyCon
       = do
         lift $ tcPluginTrace "MapEnv" ( ppr t $$ ppr s )
-        rewrote emptyDVarSet
+        rewrote []
         go $
           mkTyConApp extendTyCon
             [ kϕ2, kψ, l
@@ -217,7 +217,7 @@ canonicaliseSub defs@( PluginDefs { .. } ) givens kϕ kψ k = go
       , tc3 == bindTyCon
       = do
         lift $ tcPluginTrace "ShiftCons" ( ppr s )
-        rewrote emptyDVarSet
+        rewrote []
         go s
       -- (ShiftLift1) KUnder s :.: KBind
       --         ===> KBind :.: s
@@ -229,7 +229,7 @@ canonicaliseSub defs@( PluginDefs { .. } ) givens kϕ kψ k = go
       , tc3 == underTyCon
       = do
         lift $ tcPluginTrace "ShiftLift1" ( ppr s )
-        rewrote emptyDVarSet
+        rewrote []
         go $
           mkTyConApp composeTyCon
             [ kϕ, kψ0, kψ
@@ -248,7 +248,7 @@ canonicaliseSub defs@( PluginDefs { .. } ) givens kϕ kψ k = go
       , tc4 == underTyCon
       = do
         lift $ tcPluginTrace "ShiftLift2" ( ppr t $$ ppr s )
-        rewrote emptyDVarSet
+        rewrote []
         go $
           mkTyConApp composeTyCon
             [ kϕ, kψ1, kψ
@@ -269,7 +269,7 @@ canonicaliseSub defs@( PluginDefs { .. } ) givens kϕ kψ k = go
       , tc3 == underTyCon
       = do
         lift $ tcPluginTrace "Lift1" ( ppr t $$ ppr s )
-        rewrote emptyDVarSet
+        rewrote []
         go $
           mkTyConApp underTyCon
           [ kϕ2, kψ1, l
@@ -287,7 +287,7 @@ canonicaliseSub defs@( PluginDefs { .. } ) givens kϕ kψ k = go
       , tc4 == underTyCon
       = do
         lift $ tcPluginTrace "Lift2" ( ppr u $$ ppr t $$ ppr s )
-        rewrote emptyDVarSet
+        rewrote []
         go $
           mkTyConApp composeTyCon
             [ kϕ, kψ0, kψ
@@ -313,7 +313,7 @@ canonicaliseSub defs@( PluginDefs { .. } ) givens kϕ kψ k = go
               rewrote deps
               return s
             Nothing -> do
-              rewrote emptyDVarSet
+              rewrote []
               return $ mkTyConApp composeTyCon [kϕ0, kψ0, kψ1, t, s]
         go $
           mkTyConApp extendTyCon
@@ -326,7 +326,7 @@ canonicaliseSub defs@( PluginDefs { .. } ) givens kϕ kψ k = go
       , tc2 == idTyCon
       = do
         lift $ tcPluginTrace "IdL" ( ppr s )
-        rewrote emptyDVarSet
+        rewrote []
         go s
       -- (IdR) s :.: KId
       --  ===> s
@@ -336,7 +336,7 @@ canonicaliseSub defs@( PluginDefs { .. } ) givens kϕ kψ k = go
       , tc2 == idTyCon
       = do
         lift $ tcPluginTrace "IdR" ( ppr s )
-        rewrote emptyDVarSet
+        rewrote []
         go s
       -- (LiftId) KUnder KId
       --     ===> KId
@@ -346,7 +346,7 @@ canonicaliseSub defs@( PluginDefs { .. } ) givens kϕ kψ k = go
       , tc2 == idTyCon
       = do
         lift $ tcPluginTrace "LiftId" empty
-        rewrote emptyDVarSet
+        rewrote []
         pure $ i
       -- Recur under KUnder.
       | Just ( tc1, [ kϕ0, kψ0, k0, s ] ) <- splitTyConApp_maybe sub
@@ -385,7 +385,7 @@ canonicaliseSub defs@( PluginDefs { .. } ) givens kϕ kψ k = go
       | otherwise
       = pure sub
 
-detectApplySub :: PluginDefs -> [ Ct ] -> Type -> Maybe ( ( Type, Type, Type, Type, Type ), DVarSet )
+detectApplySub :: PluginDefs -> [ Ct ] -> Type -> Maybe ( ( Type, Type, Type, Type, Type ), [ Coercion ] )
 detectApplySub ( PluginDefs { applySubTyCon } ) =
   recognise \ ty ->
     case splitTyConApp_maybe ty of
@@ -399,21 +399,23 @@ detectApplySub ( PluginDefs { applySubTyCon } ) =
 --
 -- Useful to check whether some type is a type-family application in the presence of
 -- Givens.
-recognise :: forall r. ( Type -> Maybe r ) -> [ Ct ] -> Type -> Maybe ( r, DVarSet )
+recognise :: forall r. ( Type -> Maybe r ) -> [ Ct ] -> Type -> Maybe ( r, [ Coercion ] )
 recognise f givens ty
   | Just r <- f ty
-  = Just ( r, emptyDVarSet )
+  = Just ( r, [] )
   | otherwise
-  = case ( `State.runState` emptyDVarSet ) $ go [ ty ] givens of
+  = case ( `State.runState` [] ) $ go [ ty ] givens of
       ( Nothing, _ ) -> Nothing
       ( Just ty', deps ) -> Just ( ty', deps )
   where
-    go :: [ Type ] -> [ Ct ] -> State DVarSet ( Maybe r )
+    go :: [ Type ] -> [ Ct ] -> State [ Coercion ] ( Maybe r )
     go _   [] = return Nothing
     go tys ( g : gs )
       | let ctTy = ctPred g
       , EqPred NomEq lhs rhs <- classifyPredType ctTy
-      , let declareDeps = State.modify ( \ deps -> extendDVarSet deps ( ctEvId g ) )
+      , let
+          co = ctEvCoercion $ ctEvidence g
+          declareDeps = State.modify ( \ deps -> co : deps )
       = if
           | any ( eqType lhs ) tys
           -> case f rhs of
@@ -442,7 +444,7 @@ recognise f givens ty
       | otherwise
       = go tys gs
 
-isId :: PluginDefs -> [ Ct ] -> Type -> Maybe DVarSet
+isId :: PluginDefs -> [ Ct ] -> Type -> Maybe [ Coercion ]
 isId ( PluginDefs { .. } ) givens s = snd <$> recognise isIdTyCon givens s
   where
     isIdTyCon :: Type -> Maybe ()

ghc-tcplugin-api.cabal

@@ -1,6 +1,6 @@
 cabal-version:  3.0
 name:           ghc-tcplugin-api
-version:        0.12.0.0
+version:        0.13.0.0
 synopsis:       An API for type-checker plugins.
 license:        BSD-3-Clause
 build-type:     Simple
@@ -37,7 +37,7 @@ library
     containers
       >= 0.6    && < 0.8,
     ghc
-      >= 8.8    && < 9.13,
+      >= 8.8    && < 9.14,
     transformers
       >= 0.5    && < 0.7,
 

src/GHC/TcPlugin/API.hs

@@ -246,7 +246,6 @@ module GHC.TcPlugin.API
     -- | == Some further functions for inspecting constraints
   , eqType
   , ctLoc, ctEvidence, ctFlavour, ctEqRel, ctOrigin
-  , ctEvId
 
     -- ** Constraint evidence
 
@@ -263,16 +262,16 @@ module GHC.TcPlugin.API
     -- *** Depending on outer Givens
 
     -- | When a plugin returns a coercion that depends on outer Given constraints,
-    -- it should declare this dependency using the 'DVarSet' argument to
+    -- it should declare this dependency using the '[Coercion]' argument to
     -- functions such as 'mkPluginUnivCo', 'mkPluginUnivEvTerm' and 'mkTyFamAppReduction'
     -- in order to avoid this coercion getting floated out past such enclosing
     -- Givens.
     --
-    -- You can use 'ctEvId' to obtain the evidence variable corresponding to
-    -- a Given constraint, and functions such as 'emptyDVarSet', 'unitDVarSet',
-    -- 'unionDVarSet' and 'extendDVarSet' to construct the appropriate 'DVarSet's.
-  , DVarSet
-  , emptyDVarSet, unitDVarSet, unionDVarSet, extendDVarSet, mkDVarSet
+    -- You can use 'ctEvCoercion' to obtain the coercion underlying an equality
+    -- constraint (whether Given or Wanted). It is not possible to declare
+    -- a dependency on non-equality constraints, and calling 'ctEvCoercion'
+    -- on a non-equality constraint will cause a crash.
+  , ctEvCoercion
 
     -- *** Evidence terms
 
@@ -623,13 +622,20 @@ import GHC.Tc.Types
   , RewriteEnv(..)
 #endif
   )
+#if MIN_VERSION_ghc(9,11,0)
+import GHC.Tc.Types.CtLoc
+  ( CtLoc(..), bumpCtLocDepth )
+#endif
 import GHC.Tc.Types.Constraint
-  ( Ct(..), CtLoc(..), CtEvidence(..), CtFlavour(..)
+  ( Ct(..), CtEvidence(..), CtFlavour(..)
   , QCInst(..), TcEvDest(..)
-  , ctPred, ctLoc, ctEvidence, ctEvId, ctEvExpr
+  , ctPred, ctLoc, ctEvidence, ctEvExpr
+  , ctEvCoercion
   , ctFlavour, ctEqRel, ctOrigin
-  , bumpCtLocDepth
   , mkNonCanonical
+#if !MIN_VERSION_ghc(9,11,0)
+  , CtLoc(..), bumpCtLocDepth
+#endif
   )
 import GHC.Tc.Types.Evidence
   ( EvBind(..), EvTerm(..), EvExpr, EvBindsVar(..)
@@ -664,11 +670,6 @@ import GHC.Types.Name.Occurrence
   ( OccName(..)
   , mkVarOcc, mkDataOcc, mkTyVarOcc, mkTcOcc, mkClsOcc
   )
-import GHC.Types.Var.Set
-  ( mkDVarSet, emptyDVarSet, extendDVarSet
-  , unitDVarSet, extendDVarSet, unionDVarSet
-  , DVarSet
-  )
 #if MIN_VERSION_ghc(9,3,0)
 import GHC
   ( HscEnv )
@@ -1029,18 +1030,19 @@ setEvBind ev_bind = do
 mkPluginUnivCo
   :: String  -- ^ Name of equality (for the plugin's internal use, or for debugging)
   -> Role
-  -> DVarSet -- ^ Evidence that this proof term depends on (use e.g. 'ctEvId' for a Given)
+  -> [Coercion] -- ^ Evidence that this proof term depends on (use 'ctEvCoercion')
   -> TcType  -- ^ LHS
   -> TcType  -- ^ RHS
   -> Coercion
 mkPluginUnivCo str role _deps lhs rhs =
-  let prov =
-        PluginProv
-          str
-#if MIN_VERSION_ghc(9,11,0)
-          _deps
+  mkUnivCo
+    ( PluginProv str )
+#if MIN_VERSION_ghc(9,12,0)
+    _deps
 #endif
-  in mkUnivCo prov role lhs rhs
+    role
+    lhs
+    rhs
 
 -- | Conjure up an evidence term for an equality between two types
 -- at the given 'Role' ('Nominal' or 'Representational').
@@ -1050,11 +1052,11 @@ mkPluginUnivCo str role _deps lhs rhs =
 -- The plugin is responsible for not emitting any unsound equalities,
 -- such as an equality between 'Int' and 'Float'.
 mkPluginUnivEvTerm
-  :: String  -- ^ Name of equality (for the plugin's internal use, or for debugging)
+  :: String     -- ^ Name of equality (for the plugin's internal use, or for debugging)
   -> Role
-  -> DVarSet -- ^ Evidence that this proof term depends on (use e.g. 'ctEvId' for a Given)
-  -> TcType  -- ^ LHS
-  -> TcType  -- ^ RHS
+  -> [Coercion] -- ^ Evidence that this proof term depends on (use 'ctEvCoercion')
+  -> TcType     -- ^ LHS
+  -> TcType     -- ^ RHS
   -> EvTerm
 mkPluginUnivEvTerm str role deps lhs rhs =
   evCoercion $ mkPluginUnivCo str role deps lhs rhs
@@ -1065,12 +1067,12 @@ mkPluginUnivEvTerm str role deps lhs rhs =
 -- The result can be passed to 'TcPluginRewriteTo' to specify the outcome
 -- of rewriting a type family application.
 mkTyFamAppReduction
-  :: String    -- ^ Name of reduction (for debugging)
-  -> Role      -- ^ Role of reduction ('Nominal' or 'Representational')
-  -> DVarSet   -- ^ Evidence that this reduction depends on (use e.g. 'ctEvId' for a Given)
-  -> TyCon     -- ^ Type family 'TyCon'
-  -> [TcType]  -- ^ Type family arguments
-  -> TcType    -- ^ The type that the type family application reduces to
+  :: String     -- ^ Name of reduction (for debugging)
+  -> Role       -- ^ Role of reduction ('Nominal' or 'Representational')
+  -> [Coercion] -- ^ Evidence that this reduction depends on (use 'ctEvCoercion')
+  -> TyCon      -- ^ Type family 'TyCon'
+  -> [TcType]   -- ^ Type family arguments
+  -> TcType     -- ^ The type that the type family application reduces to
   -> Reduction
 mkTyFamAppReduction str role deps tc args ty =
   Reduction ( mkPluginUnivCo str role deps ( mkTyConApp tc args ) ty ) ty