if-instance 0.1.0.0 → 0.2.0.0

raw patch · 8 files changed

+339/−262 lines, 8 filesdep ~ghcPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: ghc

API changes (from Hackage documentation)

Files

• changelog.md +9/−1
• example/M1.hs +4/−4
• example/M2.hs +1/−1
• if-instance.cabal +8/−8
• src/Data/Constraint/If.hs +36/−26
• src/IfCt/Plugin.hs +0/−216
• src/IfSat/Plugin.hs +275/−0
• test/Main.hs +6/−6

@@ -1,3 +1,11 @@+# Version 0.2.0.0 (2021-08-31)
+
+- Add a type family 'IsSat :: Constraint -> Bool'
+  that computes whether a type-family is satisfied in
+  the current context.
+
+- Rename 'IfCt' to 'IfSat'
+
 # Version 0.1.0.0 (2021-08-30)
 
-Initial release.+Initial release.

@@ -4,7 +4,7 @@ {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 
-{-# OPTIONS_GHC -fplugin=IfCt.Plugin #-}
+{-# OPTIONS_GHC -fplugin=IfSat.Plugin #-}
 
 module M1 where
 
@@ -14,12 +14,12 @@ 
 -- if-instance
 import Data.Constraint.If
-  ( IfCt(ifCt) )
+  ( IfSat(ifSat) )
 
 --------------------------------------------------------------------------------
 
-showFun :: forall (a :: Type). IfCt ( Show ( a -> a ) ) => ( a -> a ) -> String
-showFun = ifCt @( Show (a -> a) ) show ( \ _ -> "<<function>>" )
+showFun :: forall (a :: Type). IfSat ( Show ( a -> a ) ) => ( a -> a ) -> String
+showFun = ifSat @( Show (a -> a) ) show ( \ _ -> "<<function>>" )
 
 test1 :: ( Bool -> Bool ) -> String
 test1 fun = showFun fun

@@ -4,7 +4,7 @@ {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 
-{-# OPTIONS_GHC -fplugin=IfCt.Plugin #-}
+{-# OPTIONS_GHC -fplugin=IfSat.Plugin #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module M2 where

@@ -1,6 +1,6 @@ cabal-version:  3.0
 name:           if-instance
-version:        0.1.0.0
+version:        0.2.0.0
 synopsis:       Branch on whether a constraint is satisfied
 license:        BSD-3-Clause
 build-type:     Simple
@@ -19,14 +19,14 @@ 
   @
 
-  {-# OPTIONS_GHC -fplugin=IfCt.Plugin #-}
+  {-# OPTIONS_GHC -fplugin=IfSat.Plugin #-}
 
   module MyModule where
 
-  import Data.Constraint.If ( IfCt(ifCt) )
+  import Data.Constraint.If ( IfSat(ifSat) )
 
-  hypot :: forall a. ( Floating a, IfCt (FMA a) ) => a -> a -> a
-  hypot = ifCt @(FMA a) withFMA withoutFMA
+  hypot :: forall a. ( Floating a, IfSat (FMA a) ) => a -> a -> a
+  hypot = ifSat @(FMA a) withFMA withoutFMA
     where
       withFMA :: FMA a => a -> a -> a
       withFMA a b =
@@ -60,9 +60,9 @@ 
   build-depends:
     base
-      >= 4.14.0  && < 4.18,
+      >= 4.14.0 && < 4.18,
     ghc
-      >= 8.10    && < 9.6,
+      >= 9.0    && < 9.6,
 
   default-language:
     Haskell2010
@@ -89,7 +89,7 @@ 
   exposed-modules:
     Data.Constraint.If
-    IfCt.Plugin
+    IfSat.Plugin
 
   default-language:
     Haskell2010

@@ -1,24 +1,26 @@ {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
 
 {-|
 Module: Data.Constraint.If
 
-This module defines the typeclass 'IfCt', with method 'ifCt':
+This module defines the typeclass 'IfSat', with method 'ifSat':
 
-> ifCt :: forall (ct :: Constraint) (r :: Type). IfCt ct => ( ct => r ) -> r -> r
+> ifSat :: forall (ct :: Constraint) (r :: Type). IfSat ct => ( ct => r ) -> r -> r
 
-An expression of the form @ ifCt \@ct yes no @ denotes a selection between the two
+An expression of the form @ ifSat \@ct yes no @ denotes a selection between the two
 branches @yes@ and @no@:
 
-  - if the constraint @ct@ can be determined to hold at the point of solving @IfCt ct@,
+  - if the constraint @ct@ can be determined to hold at the point of solving @IfSat ct@,
     then the @yes@ branch is selected, which has access to the @ct@ constraint;
   - otherwise, the fallback branch @no@ is selected.
 
-To use this, you will also need to enable the corresponding 'IfCt.Plugin.plugin',
-by adding @\{\-\# OPTIONS_GHC -fplugin=IfCt.Plugin \#\-\}@
+To use this, you will also need to enable the corresponding 'IfSat.Plugin.plugin',
+by adding @\{\-\# OPTIONS_GHC -fplugin=IfSat.Plugin \#\-\}@
 to the header of your module.
 
 == Example
@@ -26,8 +28,8 @@ We can select the more efficient 'nubOrd' function when an 'Ord' instance
 is available:
 
-> myNub :: forall (a :: Type). ( Eq a, IfCt (Ord a) ) => [a] -> [a]
-> myNub = ifCt @(Ord a) nubOrd nub
+> myNub :: forall (a :: Type). ( Eq a, IfSat (Ord a) ) => [a] -> [a]
+> myNub = ifSat @(Ord a) nubOrd nub
 >  -- 'nubOrd' when 'Ord a' is satisfied, 'nub' otherwise.
 
 When a user calls @myNub@, e.g.:
@@ -35,7 +37,7 @@ > foo :: [(Int, Int)]
 > foo = myNub [(1,2), (3,3), (1,2), (2,2), (1,2), (1,4)]
 
-GHC will discharge the @IfCt (Ord (Int,Int))@ constraint by trying to solve
+GHC will discharge the @IfSat (Ord (Int,Int))@ constraint by trying to solve
 the @Ord (Int, Int)@ constraint. In this case, GHC can solve the constraint
 using the two top-level instances (which we assume are in scope):
 
@@ -43,26 +45,26 @@ > instance (Ord a, Ord b) => Ord (a,b)
 
 As the @ Ord (Int,Int) @ can be solved, GHC thus choose the first branch
-in 'ifCt', which in this case is 'nubOrd'.
+in 'ifSat', which in this case is 'nubOrd'.
 
 == When does branch selection occur?
 
 What is important to understand is that the branch selection happens
-precisely when the @IfCt ct@ constraint is solved.
+precisely when the @IfSat ct@ constraint is solved.
 
 
-> { -# OPTIONS_GHC -fplugin=IfCt.Plugin #- }
+> { -# OPTIONS_GHC -fplugin=IfSat.Plugin #- }
 > module M1 where
 >
-> showFun :: forall (a :: Type). IfCt ( Show ( a -> a ) ) => ( a -> a ) -> String
-> showFun = ifCt @( Show (a -> a) ) show ( \ _ -> "<<function>>" )
+> showFun :: forall (a :: Type). IfSat ( Show ( a -> a ) ) => ( a -> a ) -> String
+> showFun = ifSat @( Show (a -> a) ) show ( \ _ -> "<<function>>" )
 >
 > test1 :: ( Bool -> Bool ) -> String
 > test1 fun = showFun fun
 >
 > ----------------------------------------
 >
-> { -# OPTIONS_GHC -fplugin=IfCt.Plugin #- }
+> { -# OPTIONS_GHC -fplugin=IfSat.Plugin #- }
 > module M2 where
 >
 > import M1
@@ -81,14 +83,14 @@ >>> test1 not
 "<<function>>"
 
-In this example, to typecheck @test1@ we need to solve @IfCt (Show (Bool -> Bool))@.
+In this example, to typecheck @test1@ we need to solve @IfSat (Show (Bool -> Bool))@.
 As no instance for @Show (Bool -> Bool)@ is available in @M1@, we pick the second branch,
 resulting in @"\<\<function\>\>"@.
 
 >>> test2 not
 "<<function>>"
 
-In this example, we must solve @IfCt (Show (a -> a))@. There is no such instance in @M2@,
+In this example, we must solve @IfSat (Show (a -> a))@. There is no such instance in @M2@,
 so we pick the second branch.
 
 >>> test3 not
@@ -97,12 +99,12 @@ >>> showFun not
 "[True, False]"
 
-In these last two examples, we must solve @IfCt (Show (Bool -> Bool))@.
+In these last two examples, we must solve @IfSat (Show (Bool -> Bool))@.
 Such an instance is in scope in @M2@, so we choose the first branch.
 -}
 
 module Data.Constraint.If
-  ( IfCt(..) )
+  ( IfSat(..), IsSat )
   where
 
 -- base
@@ -111,15 +113,23 @@ 
 --------------------------------------------------------------------------------
 
-type IfCt :: Constraint -> Constraint
-class IfCt ct where
-  -- | @ ifCt \@ct a b@ returns @a@ if the constraint is satisfied,
+type IfSat :: Constraint -> Constraint
+class IfSat ct where
+  -- | @ IfSat \@ct a b@ returns @a@ if the constraint is satisfied,
   -- and @b@ otherwise.
   --
-  -- Requires the if-instance 'IfCt.Plugin.plugin':
-  -- add @{-# OPTIONS_GHC -fplugin=IfCt.Plugin #-}@
+  -- Requires the if-instance 'IfSat.Plugin.plugin':
+  -- add @{-# OPTIONS_GHC -fplugin=IfSat.Plugin #-}@
   -- to the header of your module.
   --
-  -- Note: the selection happens at the point in the code where the @IfCt ct@
+  -- Note: the selection happens at the point in the code where the @IfSat ct@
   -- constraint is solved.
-  ifCt :: ( ct => r ) -> r -> r
+  ifSat :: ( ( IsSat ct ~ True, ct ) => r )
+       -> ( IsSat ct ~ False => r)
+       -> r
+
+-- | @IsSat ct@ returns @True@ if @ct@ is satified, and @False@ otherwise.
+--
+-- The satisfiability check occurs at the moment of type-family reduction.
+type IsSat :: Constraint -> Bool
+type family IsSat ct where

@@ -1,216 +0,0 @@-{-# LANGUAGE BlockArguments #-}
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE PatternSynonyms #-}
-
-module IfCt.Plugin
-  ( plugin )
-  where
-
--- base
-import Data.Maybe
-  ( catMaybes )
-#if !MIN_VERSION_ghc(9,2,0)
-import Unsafe.Coerce
-  ( unsafeCoerce )
-#endif
-
--- ghc
-import GHC.Plugins
-  ( Plugin(..)
-  , defaultPlugin, purePlugin
-  )
-import GHC.Data.Bag
-  ( unitBag )
-import GHC.Tc.Solver.Interact
-  ( solveSimpleGivens, solveSimpleWanteds )
-import GHC.Tc.Solver.Monad
-  ( getTcEvBindsMap, readTcRef, runTcSWithEvBinds, traceTcS
-#if MIN_VERSION_ghc(9,2,0)
-  , wrapTcS
-#else
-  , TcS
-#endif
-  )
-import GHC.Tc.Types
-  ( TcM )
-import GHC.Utils.Outputable
-  ( (<+>), ($$), empty, text, vcat )
-
--- ghc-tcplugin-api
-import GHC.TcPlugin.API
-import GHC.TcPlugin.API.Internal
-  ( unsafeLiftTcM )
-
---------------------------------------------------------------------------------
--- Plugin definition.
-
--- | A type-checking plugin that solves @MyCt ct@ constraints.
--- Theis allows users to branch on whether @ct@ is satisfied.
---
--- To use this plugin, add @{-# OPTIONS_GHC -fplugin=IfCt.Plugin #-}@
--- to your module header.
---
--- A @MyCt ct@ instance is solved by trying to solve @ct@:
---
---   - if solving succeeds, the 'Data.Constraint.If.ifCt' function will
---     pick the first branch,
---   - otherwise, 'Data.Constraint.If.ifCt' will pick the second branch.
---
--- This means that the branch selection occurs precisely at the moment
--- at which we solve the @IfCt ct@ constraint.
--- See the documentation of 'Data.Constraint.If.IfCt' for more information.
-plugin :: Plugin
-plugin =
-  defaultPlugin
-    { tcPlugin        = \ _args -> Just $ mkTcPlugin ifCtTcPlugin
-    , pluginRecompile = purePlugin
-    }
-
-ifCtTcPlugin :: TcPlugin
-ifCtTcPlugin =
-  TcPlugin
-    { tcPluginInit    = initPlugin
-    , tcPluginSolve   = solver
-    , tcPluginRewrite = \ _ -> emptyUFM
-    , tcPluginStop    = \ _ -> pure ()
-    }
-
---------------------------------------------------------------------------------
--- Plugin initialisation.
-
-data PluginDefs
-  = PluginDefs
-    { ifCtClass :: !Class }
-
-findModule :: MonadTcPlugin m => Maybe String -> String -> m Module
-findModule mb_pkg modName = do
-  findResult <- findImportedModule ( mkModuleName modName ) ( fmap fsLit mb_pkg )
-  case findResult of
-    Found _ res     -> pure res
-    FoundMultiple _ -> error $ "IfCt plugin: found multiple modules named " <> modName <> "."
-    _               -> error $ "IfCt plugin: could not find any module named " <> modName <> "."
-
-initPlugin :: TcPluginM Init PluginDefs
-initPlugin = do
-  ifCtModule <- findModule Nothing "Data.Constraint.If"
-  ifCtClass  <- tcLookupClass =<< lookupOrig ifCtModule ( mkClsOcc "IfCt" )
-  pure $ PluginDefs { ifCtClass }
-
---------------------------------------------------------------------------------
--- Constraint solving.
-
-solver :: PluginDefs -> [ Ct ] -> [ Ct ] -> TcPluginM Solve TcPluginSolveResult
-solver defs givens wanteds
-  | null wanteds
-  = pure $ TcPluginOk [] []
-  | otherwise
-  = do
-      tcPluginTrace "IfCt plugin {" (ppr givens $$ ppr wanteds)
-      solveds <- catMaybes <$> traverse ( solveWanted defs givens ) wanteds
-      tcPluginTrace "IfCt plugin }" empty
-      pure $ TcPluginOk solveds []
-
-solveWanted :: PluginDefs -> [ Ct ] -> Ct -> TcPluginM Solve ( Maybe ( EvTerm, Ct ) )
-solveWanted defs@( PluginDefs { ifCtClass } ) givens wanted
-  | ClassPred cls [ct_ty] <- classifyPredType ( ctPred wanted )
-  , cls == ifCtClass
-  = do
-    tcPluginTrace "IfCt plugin: found IfCt constraint" ( ppr wanted )
-    ct_ev <- newWanted ( ctLoc wanted ) ct_ty
-    let
-      ct :: Ct
-      ct = mkNonCanonical ct_ev
-      ct_ev_dest :: TcEvDest
-      ct_ev_dest = ctev_dest ct_ev
-    evBindsVar <- askEvBinds
-    -- Start a new Solver run.
-    unsafeLiftTcM $ runTcSWithEvBinds evBindsVar $ do
-      -- Add back all the Givens.
-      traceTcS "IfCt plugin: adding Givens to the inert set" (ppr givens)
-      solveSimpleGivens givens
-      -- Try to solve 'ct', using both Givens and top-level instances.
-      _ <- solveSimpleWanteds ( unitBag ct )
-      -- Now look up whether GHC has managed to produce evidence for 'ct'.
-      mb_ct_evTerm <-
-        case ct_ev_dest of
-          HoleDest ( CoercionHole { ch_ref = ref } ) -> do
-            mb_co <- readTcRef ref
-            traceTcS "IfCt plugin: coercion hole" (ppr mb_co)
-            case mb_co of
-              Nothing -> pure Nothing
-              Just co -> pure . Just $ evCoercion co
-          EvVarDest ev_var -> do
-            evBindsMap <- getTcEvBindsMap evBindsVar
-            let
-              mb_evBind :: Maybe EvBind
-              mb_evBind = lookupEvBind evBindsMap ev_var
-            traceTcS "IfCt plugin: evidence binding" (ppr mb_evBind)
-            case mb_evBind of
-              Nothing      -> pure Nothing
-              Just ev_bind -> pure . Just $ eb_rhs ev_bind
-      wanted_evTerm <- case mb_ct_evTerm of
-        Just ( EvExpr ct_evExpr ) -> do
-          -- We've managed to solve 'ct': use the evidence and take the 'True' branch.
-          traceTcS "IfCt plugin: constraint could be solved"
-            ( vcat
-              [ text "ct =" <+> ppr ct_ty
-              , text "ev =" <+> ppr ct_evExpr
-              ]
-            )
-          wrapTcS $ ifCtTrueEvTerm defs ct_ty ct_evExpr
-        _ -> do
-          -- We couldn't solve 'ct': take the 'False' branch.
-          traceTcS "IfCt plugin: constraint could not be solved"
-            ( text "ct =" <+> ppr ct_ty )
-          wrapTcS $ ifCtFalseEvTerm defs ct_ty
-      pure $ Just ( wanted_evTerm, wanted )
-  | otherwise
-  = pure Nothing
-
--- Evidence term for @IfCt ct@ when @ct@ isn't satisfied.
--- ifCt = \ @r (a :: ct => r) (_ :: r) -> a ct_evTerm
-ifCtTrueEvTerm :: PluginDefs -> Type -> EvExpr -> TcM EvTerm
-ifCtTrueEvTerm ( PluginDefs { ifCtClass } ) ct_ty ct_evTerm = do
-  r_name <- newName ( mkTyVarOcc "r" )
-  a_name <- newName ( mkVarOcc   "a" )
-  let
-    r, a, b :: CoreBndr
-    r = mkTyVar r_name liftedTypeKind
-    a = mkLocalId a_name Many ( mkInvisFunTyMany ct_ty r_ty )
-    b = mkWildValBinder Many r_ty
-    r_ty :: Type
-    r_ty = mkTyVarTy r
-  pure . EvExpr $
-    mkCoreConApps ( classDataCon ifCtClass )
-      [ Type ct_ty
-      , mkCoreLams [ r, a, b ]
-        ( mkCoreApps ( Var a ) [ ct_evTerm ] )
-      ]
-
--- Evidence term for @IfCt ct@ when @ct@ isn't satisfied.
--- ifCt = \ @r (_ :: ct => r) (b :: r) -> b
-ifCtFalseEvTerm :: PluginDefs -> Type -> TcM EvTerm
-ifCtFalseEvTerm ( PluginDefs { ifCtClass } ) ct_ty = do
-  r_name <- newName ( mkTyVarOcc "r" )
-  b_name <- newName ( mkVarOcc   "b" )
-  let
-    r, a, b :: CoreBndr
-    r = mkTyVar r_name liftedTypeKind
-    a = mkWildValBinder Many ( mkInvisFunTyMany ct_ty r_ty )
-    b = mkLocalId b_name Many r_ty
-    r_ty :: Type
-    r_ty = mkTyVarTy r
-  pure . EvExpr $
-    mkCoreConApps ( classDataCon ifCtClass )
-      [ Type ct_ty
-      , mkCoreLams [ r, a, b ] ( Var b )
-      ]
-
---------------------------------------------------------------------------------
-
-#if !MIN_VERSION_ghc(9,2,0)
-wrapTcS :: TcM a -> TcS a
-wrapTcS = unsafeCoerce const
-#endif

@@ -0,0 +1,275 @@+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module IfSat.Plugin
+  ( plugin )
+  where
+
+-- base
+import Data.Maybe
+  ( catMaybes )
+#if !MIN_VERSION_ghc(9,2,0)
+import Unsafe.Coerce
+  ( unsafeCoerce )
+#endif
+
+-- ghc
+import GHC.Plugins
+  ( Plugin(..)
+  , defaultPlugin, purePlugin
+  )
+import GHC.Data.Bag
+  ( unitBag )
+import GHC.Tc.Solver.Interact
+  ( solveSimpleGivens, solveSimpleWanteds )
+import GHC.Tc.Solver.Monad
+  ( getTcEvBindsMap, readTcRef, runTcS, runTcSWithEvBinds, traceTcS
+#if MIN_VERSION_ghc(9,2,0)
+  , wrapTcS
+#else
+  , TcS
+#endif
+  )
+import GHC.Tc.Types
+  ( TcM )
+import GHC.Tc.Types.Constraint
+  ( isEmptyWC )
+import GHC.Utils.Outputable
+  ( (<+>), ($$), empty, text, vcat )
+
+-- ghc-tcplugin-api
+import GHC.TcPlugin.API
+import GHC.TcPlugin.API.Internal
+  ( unsafeLiftTcM )
+
+--------------------------------------------------------------------------------
+-- Plugin definition.
+
+-- | A type-checking plugin that solves @MyCt ct@ constraints.
+-- Theis allows users to branch on whether @ct@ is satisfied.
+--
+-- To use this plugin, add @{-# OPTIONS_GHC -fplugin=IfSat.Plugin #-}@
+-- to your module header.
+--
+-- A @MyCt ct@ instance is solved by trying to solve @ct@:
+--
+--   - if solving succeeds, the 'Data.Constraint.If.ifSat' function will
+--     pick the first branch,
+--   - otherwise, 'Data.Constraint.If.ifSat' will pick the second branch.
+--
+-- This means that the branch selection occurs precisely at the moment
+-- at which we solve the @IfSat ct@ constraint.
+-- See the documentation of 'Data.Constraint.If.IfSat' for more information.
+plugin :: Plugin
+plugin =
+  defaultPlugin
+    { tcPlugin        = \ _args -> Just $ mkTcPlugin ifSatTcPlugin
+    , pluginRecompile = purePlugin
+    }
+
+ifSatTcPlugin :: TcPlugin
+ifSatTcPlugin =
+  TcPlugin
+    { tcPluginInit    = initPlugin
+    , tcPluginSolve   = solver
+    , tcPluginRewrite = rewriter
+    , tcPluginStop    = \ _ -> pure ()
+    }
+
+--------------------------------------------------------------------------------
+-- Plugin initialisation.
+
+data PluginDefs
+  = PluginDefs
+    { ifSatClass  :: !Class
+    , isSatTyCon :: !TyCon
+    }
+
+findModule :: MonadTcPlugin m => Maybe String -> String -> m Module
+findModule mb_pkg modName = do
+  findResult <- findImportedModule ( mkModuleName modName ) ( fmap fsLit mb_pkg )
+  case findResult of
+    Found _ res     -> pure res
+    FoundMultiple _ -> error $ "IfSat plugin: found multiple modules named " <> modName <> "."
+    _               -> error $ "IfSat plugin: could not find any module named " <> modName <> "."
+
+initPlugin :: TcPluginM Init PluginDefs
+initPlugin = do
+  ifSatModule <- findModule Nothing "Data.Constraint.If"
+  ifSatClass  <- tcLookupClass =<< lookupOrig ifSatModule ( mkClsOcc "IfSat" )
+  isSatTyCon  <- tcLookupTyCon =<< lookupOrig ifSatModule ( mkTcOcc  "IsSat" )
+  pure $ PluginDefs { ifSatClass, isSatTyCon }
+
+--------------------------------------------------------------------------------
+-- Constraint solving.
+
+solver :: PluginDefs -> [ Ct ] -> [ Ct ] -> TcPluginM Solve TcPluginSolveResult
+solver defs givens wanteds
+  | null wanteds
+  = pure $ TcPluginOk [] []
+  | otherwise
+  = do
+      tcPluginTrace "IfSat solver {" (ppr givens $$ ppr wanteds)
+      solveds <- catMaybes <$> traverse ( solveWanted defs givens ) wanteds
+      tcPluginTrace "IfSat solver }" empty
+      pure $ TcPluginOk solveds []
+
+solveWanted :: PluginDefs -> [ Ct ] -> Ct -> TcPluginM Solve ( Maybe ( EvTerm, Ct ) )
+solveWanted defs@( PluginDefs { ifSatClass } ) givens wanted
+  | ClassPred cls [ct_ty] <- classifyPredType ( ctPred wanted )
+  , cls == ifSatClass
+  = do
+    tcPluginTrace "IfSat solver: found IfSat constraint" ( ppr wanted )
+    ct_ev <- newWanted ( ctLoc wanted ) ct_ty
+    let
+      ct :: Ct
+      ct = mkNonCanonical ct_ev
+      ct_ev_dest :: TcEvDest
+      ct_ev_dest = ctev_dest ct_ev
+    evBindsVar <- askEvBinds
+    -- Start a new Solver run.
+    unsafeLiftTcM $ runTcSWithEvBinds evBindsVar $ do
+      -- Add back all the Givens.
+      traceTcS "IfSat solver: adding Givens to the inert set" (ppr givens)
+      solveSimpleGivens givens
+      -- Try to solve 'ct', using both Givens and top-level instances.
+      _ <- solveSimpleWanteds ( unitBag ct )
+      -- Now look up whether GHC has managed to produce evidence for 'ct'.
+      mb_ct_evTerm <-
+        case ct_ev_dest of
+          HoleDest ( CoercionHole { ch_ref = ref } ) -> do
+            mb_co <- readTcRef ref
+            traceTcS "IfSat solver: coercion hole" (ppr mb_co)
+            case mb_co of
+              Nothing -> pure Nothing
+              Just co -> pure . Just $ evCoercion co
+          EvVarDest ev_var -> do
+            evBindsMap <- getTcEvBindsMap evBindsVar
+            let
+              mb_evBind :: Maybe EvBind
+              mb_evBind = lookupEvBind evBindsMap ev_var
+            traceTcS "IfSat solver: evidence binding" (ppr mb_evBind)
+            case mb_evBind of
+              Nothing      -> pure Nothing
+              Just ev_bind -> pure . Just $ eb_rhs ev_bind
+      wanted_evTerm <- case mb_ct_evTerm of
+        Just ( EvExpr ct_evExpr ) -> do
+          -- We've managed to solve 'ct': use the evidence and take the 'True' branch.
+          traceTcS "IfSat solver: constraint could be solved"
+            ( vcat
+              [ text "ct =" <+> ppr ct_ty
+              , text "ev =" <+> ppr ct_evExpr
+              ]
+            )
+          wrapTcS $ ifSatTrueEvTerm defs ct_ty ct_evExpr
+        _ -> do
+          -- We couldn't solve 'ct': take the 'False' branch.
+          traceTcS "IfSat solver: constraint could not be solved"
+            ( text "ct =" <+> ppr ct_ty )
+          wrapTcS $ ifSatFalseEvTerm defs ct_ty
+      pure $ Just ( wanted_evTerm, wanted )
+  | otherwise
+  = pure Nothing
+
+-- Evidence term for @IfSat ct@ when @ct@ isn't satisfied.
+-- IfSat = \ @r (a :: ( IsSat ct ~ True, ct ) => r) (_ :: IsSat ct ~ False => r) -> a isSat_co ct_evTerm
+ifSatTrueEvTerm :: PluginDefs -> Type -> EvExpr -> TcM EvTerm
+ifSatTrueEvTerm defs@( PluginDefs { ifSatClass } ) ct_ty ct_evTerm = do
+  r_name <- newName ( mkTyVarOcc "r" )
+  a_name <- newName ( mkVarOcc   "a" )
+  let
+    r, a, b :: CoreBndr
+    r = mkTyVar r_name liftedTypeKind
+    a = mkLocalId a_name Many ( mkInvisFunTyMany (sat_eqTy defs ct_ty tru) $ mkInvisFunTyMany ct_ty r_ty )
+    b = mkWildValBinder  Many ( mkInvisFunTyMany (sat_eqTy defs ct_ty fls) r_ty )
+    r_ty :: Type
+    r_ty = mkTyVarTy r
+  pure . EvExpr $
+    mkCoreConApps ( classDataCon ifSatClass )
+      [ Type ct_ty
+      , mkCoreLams [ r, a, b ]
+        ( mkCoreApps ( Var a ) [ sat_co_expr defs ct_ty tru, ct_evTerm ] )
+      ]
+
+-- Evidence term for @IfSat ct@ when @ct@ isn't satisfied.
+-- IfSat = \ @r (_ :: ( IsSat ct ~ True, ct ) => r) (b :: IsSat ct ~ False => r) -> b notSat_co
+ifSatFalseEvTerm :: PluginDefs -> Type -> TcM EvTerm
+ifSatFalseEvTerm defs@( PluginDefs { ifSatClass } ) ct_ty = do
+  r_name <- newName ( mkTyVarOcc "r" )
+  b_name <- newName ( mkVarOcc   "b" )
+  let
+    r, a, b :: CoreBndr
+    r = mkTyVar r_name liftedTypeKind
+    a = mkWildValBinder  Many ( mkInvisFunTyMany (sat_eqTy defs ct_ty tru) $ mkInvisFunTyMany ct_ty r_ty )
+    b = mkLocalId b_name Many ( mkInvisFunTyMany (sat_eqTy defs ct_ty fls) r_ty )
+    r_ty :: Type
+    r_ty = mkTyVarTy r
+  pure . EvExpr $
+    mkCoreConApps ( classDataCon ifSatClass )
+      [ Type ct_ty
+      , mkCoreLams [ r, a, b ]
+        ( mkCoreApps ( Var b ) [ sat_co_expr defs ct_ty fls ] )
+      ]
+
+fls, tru :: Type
+fls = mkTyConTy promotedFalseDataCon
+tru = mkTyConTy promotedTrueDataCon
+
+-- @ sat_eqTy defs ct_ty rhs @ represents the type @ IsSat ct ~ rhs @.
+sat_eqTy :: PluginDefs -> Type -> Type -> Type
+sat_eqTy ( PluginDefs { isSatTyCon } ) ct_ty rhs
+  = mkTyConApp eqTyCon
+      [ boolTy, mkTyConApp isSatTyCon [ct_ty], rhs ]
+
+-- @ sat_co_expr defs ct_ty rhs @ is an expression of type @ IsSat ct ~ rhs @.
+sat_co_expr :: PluginDefs -> Type -> Type -> EvExpr
+sat_co_expr ( PluginDefs { isSatTyCon } ) ct_ty rhs
+  = mkCoreConApps eqDataCon
+      [ Type boolTy
+      , Type $ mkTyConApp isSatTyCon [ ct_ty ]
+      , Type rhs
+      , Coercion $ mkPluginUnivCo "IfSat: IsSat" Nominal ( mkTyConApp isSatTyCon [ct_ty] ) rhs
+      ]
+
+--------------------------------------------------------------------------------
+
+rewriter :: PluginDefs -> UniqFM TyCon TcPluginRewriter
+rewriter defs@( PluginDefs { isSatTyCon } )
+  = listToUFM [ ( isSatTyCon, isSatRewriter defs ) ]
+
+isSatRewriter :: PluginDefs -> [Ct] -> [Type] -> TcPluginM Rewrite TcPluginRewriteResult
+isSatRewriter ( PluginDefs { isSatTyCon } ) givens [ct_ty] = do
+  tcPluginTrace "IfSat rewriter {" (ppr givens $$ ppr ct_ty)
+  rewriteEnv <- askRewriteEnv
+  ct_ev <- newWanted ( rewriteEnvCtLoc rewriteEnv ) ct_ty
+  let
+    ct :: Ct
+    ct = mkNonCanonical ct_ev
+  -- Start a new Solver run.
+  ( redn, _ ) <- unsafeLiftTcM $ runTcS $ do
+    -- Add back all the Givens.
+    traceTcS "IfSat rewriter: adding Givens to the inert set" (ppr givens)
+    solveSimpleGivens givens
+    -- Try to solve 'ct', using both Givens and top-level instances.
+    residual_wc <- solveSimpleWanteds ( unitBag ct )
+    let
+      sat :: Type
+      sat
+        | isEmptyWC residual_wc
+        = mkTyConTy promotedTrueDataCon
+        | otherwise
+        = mkTyConTy promotedFalseDataCon
+    pure $ mkTyFamAppReduction "IfSat: IsSat" Nominal isSatTyCon [ct_ty] sat
+  tcPluginTrace "IfSat rewriter }" empty
+  pure $ TcPluginRewriteTo redn []
+isSatRewriter _ _ _ = pure TcPluginNoRewrite
+
+--------------------------------------------------------------------------------
+
+#if !MIN_VERSION_ghc(9,2,0)
+wrapTcS :: TcM a -> TcS a
+wrapTcS = unsafeCoerce const
+#endif

@@ -7,7 +7,7 @@ {-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TypeApplications #-}
 
-{-# OPTIONS_GHC -fplugin=IfCt.Plugin #-}
+{-# OPTIONS_GHC -fplugin=IfSat.Plugin #-}
 {-# OPTIONS_GHC -dcore-lint #-}
 
 module Main where
@@ -24,9 +24,9 @@   ( withDict )
 #endif
 
--- IfCt
+-- IfSat
 import Data.Constraint.If
-  ( IfCt(ifCt) )
+  ( IfSat(ifSat) )
 
 --------------------------------------------------------------------------------
 
@@ -37,8 +37,8 @@ instance MyShow Int where
   myShow = show
 
-myShowAnything :: forall a. IfCt ( MyShow a ) => a -> String
-myShowAnything = ifCt @( MyShow a ) yes no
+myShowAnything :: forall a. IfSat ( MyShow a ) => a -> String
+myShowAnything = ifSat @( MyShow a ) yes no
   where
     yes :: MyShow a => a -> String
     yes = myShow
@@ -55,7 +55,7 @@ 
 data A = A
 
-myShowA :: IfCt ( MyShow A ) => String
+myShowA :: IfSat ( MyShow A ) => String
 myShowA = myShowAnything A
 
 #if MIN_VERSION_ghc(9,4,0)