Helper for computing fix-point Given substitution

changelog.md

@@ -1,4 +1,14 @@
 
+# Version 0.18.2.0 (2025-01-14)
+
+- Add a new function `ctsSubst` which computes a fix-point substitution from
+  a collection of constraints which define a terminating generalised
+  substitution. Mainly for use with the set of inert Given constraints.
+
+- Re-export several functions to deal with substitutions: `substTy`,
+  `substTys`, `extendTvSubst` and `mkTvSubstPrs`. Also re-export the `Subst`
+  type (alias for `TCvSubst` on GHC <= 9.6).
+
 # Version 0.18.1.0 (2025-10-09)
 
 - Bugfix for v0.18.0.0: deal with constraints generated by unflattening

ghc-tcplugin-api.cabal

@@ -1,6 +1,6 @@
 cabal-version:  3.0
 name:           ghc-tcplugin-api
-version:        0.18.1.0
+version:        0.18.2.0
 synopsis:       An API for type-checker plugins.
 license:        BSD-3-Clause
 build-type:     Simple
@@ -153,6 +153,7 @@ library
         , Module     as GHC.Unit.Module.Name
         , Module     as GHC.Unit.Types
 
+        , FV         as GHC.Utils.FV
         , Util       as GHC.Utils.Misc
         , TcRnMonad  as GHC.Utils.Monad
         , Outputable as GHC.Utils.Outputable
@@ -167,6 +168,7 @@ library
           , Constraint as GHC.Tc.Types.Constraint
           , TcOrigin   as GHC.Tc.Types.Origin
           , GHC.ThToHs as GHC.ThToHs
+             -- I forget what this last line does, but it is needed on GHC 9.10
           )
 
     else

src/GHC/TcPlugin/API.hs

@@ -450,6 +450,12 @@ module GHC.TcPlugin.API
   , pattern OneTy, pattern ManyTy
 #endif
 
+    -- ** Substitution
+  , Subst
+  , substTy, substTys
+  , mkTvSubstPrs, extendTvSubst
+  , ctsSubst
+
     -- ** Zonking
 
     -- | Zonking is the operation in which GHC actually switches out mutable unification variables
@@ -539,10 +545,16 @@ module GHC.TcPlugin.API
 -- base
 import Prelude
   hiding ( cos )
+#if !MIN_VERSION_base(4,20,0)
+import Data.Foldable
+  ( foldl' )
+#endif
 #if !MIN_VERSION_ghc(8,11,0)
 import Data.List.NonEmpty
   ( NonEmpty(..) )
 #endif
+import Data.Maybe
+  ( mapMaybe )
 
 -- ghc
 import GHC
@@ -661,6 +673,12 @@ import GHC.Core.Type
   , pattern OneTy, pattern ManyTy
 #elif MIN_VERSION_ghc(9,0,0)
   , pattern One, pattern Many
+#endif
+  , TvSubstEnv
+#if MIN_VERSION_ghc(9,6,0)
+  , Subst
+#else
+  , TCvSubst
 #endif
   )
 import GHC.Data.FastString
@@ -748,6 +766,10 @@ import GHC.Tc.Utils.TcType
   ( TcType, TcLevel, MetaDetails, MetaInfo
   , isSkolemTyVar, isMetaTyVar
   , nonDetCmpType
+  , tyCoFVsOfTypes, mkTvSubst, extendTvSubst
+  , substTy, substTys, mkTvSubstPrs
+  , tyCoVarsOfTypes
+  , scopedSort
   )
 import GHC.Tc.Utils.TcMType
   ( isFilledMetaTyVar_maybe, writeMetaTyVar )
@@ -793,21 +815,27 @@ import GHC.Types.SrcLoc
   )
 import GHC.Types.Unique
   ( Unique )
+-- UniqFM didn't have the first argument in GHC < 9.0.
+-- This adds a little compatibility shim for that.
 #if MIN_VERSION_ghc(9,0,0)
 import GHC.Types.Unique.FM as UniqFM
-  ( UniqFM, emptyUFM, listToUFM )
+  ( UniqFM )
 #else
 import qualified GHC.Types.Unique.FM as GHC
   ( UniqFM )
-import GHC.Types.Unique.FM as UniqFM
-  ( emptyUFM, listToUFM )
 #endif
+import GHC.Types.Unique.FM
+  ( emptyUFM, listToUFM, nonDetEltsUFM )
 import GHC.Types.Unique.DFM
   ( UniqDFM, lookupUDFM, lookupUDFM_Directly, elemUDFM )
 import GHC.Types.Var
   ( TyVar, CoVar, TcTyVar, EvVar
-  , mkTyVar, DFunId
+  , mkTyVar, DFunId, isTyVar, updateTyVarKind
   )
+import GHC.Types.Var.Env
+  ( InScopeSet, mkInScopeSet, mapVarEnv, elemVarEnv )
+import GHC.Types.Var.Set
+  ( mkVarSet, unionVarSet )
 import GHC.Utils.Outputable
   ( Outputable(..), SDoc, text )
 #if MIN_VERSION_ghc(9,2,0)
@@ -839,6 +867,10 @@ import GHC.Unit.Types
 import GHC.Utils.Misc
   ( HasDebugCallStack )
 #endif
+import GHC.Utils.FV
+  ( fvVarList )
+import GHC.Utils.Misc
+  ( filterOut )
 
 -- ghc-tcplugin-api
 import GHC.TcPlugin.API.Internal
@@ -984,6 +1016,60 @@ tcLookupId = liftTcPluginM . GHC.tcLookupId
 
 --------------------------------------------------------------------------------
 
+#if !MIN_VERSION_ghc(9,6,0)
+type Subst = TCvSubst
+#endif
+
+-- | Compute an idempotent substitution from a collection of constraints, in
+-- particular from inert Givens.
+--
+-- NB: don't pass any set of constraints to this function; they should form a
+-- terminating generalised substitution as in Note [inert_eqs: the inert equalities]
+-- in GHC.Tc.Solver.InertSet.
+ctsSubst :: [Ct] -> Subst
+ctsSubst cts = niFixSubst inScope $ listToUFM prs
+  where
+    toSubstPair ct =
+      case classifyPredType (ctEvPred (ctEvidence ct)) of
+        EqPred NomEq t1 t2
+          | Just tv <- getTyVar_maybe t1
+          -- NB: deliberately don't re-orient constraints: we are only
+          -- guaranteed a terminating substitution by keeping the orientation.
+          -> Just (tv, t2)
+        _ -> Nothing
+    prs = mapMaybe toSubstPair cts
+    inScope =
+      mkInScopeSet $
+        mkVarSet (map fst prs)
+          `unionVarSet`
+        tyCoVarsOfTypes (map snd prs)
+
+-- NB: copied from GHC, as GHC doesn't export this function.
+niFixSubst :: InScopeSet -> TvSubstEnv -> Subst
+niFixSubst in_scope tenv
+  | not_fixpoint = niFixSubst in_scope (mapVarEnv (substTy subst) tenv)
+  | otherwise    = tenv_subst
+  where
+    tenv_subst = mkTvSubst in_scope tenv
+
+    range_fvs = tyCoFVsOfTypes (nonDetEltsUFM tenv)
+    range_tvs = fvVarList range_fvs
+
+    not_fixpoint  = any in_domain range_tvs
+    in_domain tv  = tv `elemVarEnv` tenv
+
+    free_tvs = scopedSort (filterOut in_domain range_tvs)
+
+    subst = foldl' add_free_tv tenv_subst free_tvs
+
+    add_free_tv subst0 tv
+      | isTyVar tv = extendTvSubst subst0 tv (mkTyVarTy tv')
+      | otherwise  = subst0
+     where
+        tv' = updateTyVarKind (substTy subst0) tv
+
+--------------------------------------------------------------------------------
+
 getTopEnv :: MonadTcPlugin m => m HscEnv
 getTopEnv = liftTcPluginM GHC.getTopEnv