packages feed

if-instance 0.4.0.0 → 0.5.0.0

raw patch · 6 files changed

+74/−7 lines, 6 filesdep ~basedep ~ghcdep ~ghc-tcplugin-apiPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, ghc, ghc-tcplugin-api

API changes (from Hackage documentation)

Files

changelog.md view
@@ -1,7 +1,17 @@ 
+# Version 0.5.0.0 (2023-08-09)
+
+- Add a fixity declaration for `(||)` (`infixr 2`, matching term-level disjunction).
+
+- Reset the GHC solver monad state after failing to solve the LHS constraint in
+  a disjunction.
+
+- Require `ghc-tcplugin-api >= 0.11`.
+
 # Version 0.4.0.0 (2023-08-09)
 
 - Only consider a constraint solved when there are no residual constraints.
+
 - Bump version bounds for `ghc-tcplugin-api`.
 
 # Version 0.3.1.0 (2023-01-24)
if-instance.cabal view
@@ -1,6 +1,6 @@ cabal-version:  3.0
 name:           if-instance
-version:        0.4.0.0
+version:        0.5.0.0
 synopsis:       Branch on whether a constraint is satisfied
 license:        BSD-3-Clause
 build-type:     Simple
@@ -85,7 +85,7 @@ 
   build-depends:
     ghc-tcplugin-api
-      >= 0.10 && < 0.11,
+      >= 0.11 && < 0.12,
 
   exposed-modules:
     Data.Constraint.If
src/Data/Constraint/If.hs view
@@ -135,7 +135,7 @@ 
 --------------------------------------------------------------------------------
 
-
+infixr 2 ||
 type (||) :: Constraint -> Constraint -> Constraint
 class c || d where
   -- | @dispatch \@c \@d a b@ returns @a@ if the constraint @c@ is satisfied,
src/IfSat/Plugin.hs view
@@ -10,6 +10,10 @@   where
 
 -- base
+import Control.Monad
+  ( filterM )
+import Data.Foldable
+  ( for_ )
 import Data.Maybe
   ( catMaybes )
 #if !MIN_VERSION_ghc(9,2,0)
@@ -22,11 +26,15 @@   hiding ( TcPlugin, (<>) )
 import GHC.Data.Bag
   ( unitBag )
+#if MIN_VERSION_ghc(9,8,0)
+import GHC.Tc.Solver.Solve
+  ( solveSimpleGivens, solveSimpleWanteds )
+#else
 import GHC.Tc.Solver.Interact
   ( solveSimpleGivens, solveSimpleWanteds )
+#endif
 import GHC.Tc.Solver.Monad
-  ( TcS
-  , getTcEvBindsMap, readTcRef, runTcS, runTcSWithEvBinds, traceTcS
+  ( runTcS, runTcSWithEvBinds, traceTcS
 #if MIN_VERSION_ghc(9,2,0)
   , wrapTcS
 #endif
@@ -35,6 +43,12 @@   ( TcM )
 import GHC.Tc.Types.Constraint
   ( isEmptyWC )
+import GHC.Tc.Utils.TcType
+  ( MetaDetails(..), metaTyVarRef
+  , tyCoVarsOfTypeList
+  )
+import GHC.Tc.Utils.TcMType
+  ( isUnfilledMetaTyVar )
 
 -- ghc-tcplugin-api
 import GHC.TcPlugin.API
@@ -131,12 +145,22 @@       ct_l_ev_dest, ct_r_ev_dest :: TcEvDest
       ct_l_ev_dest = ctev_dest ct_l_ev
       ct_r_ev_dest = ctev_dest ct_r_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
+
+      -- Keep track of the current solver state in order to backtrack
+      -- in the event that our attempt at solving 'ct_l' fails.
+      ct_l_unfilled_metas <- wrapTcS
+                           $ filterM isUnfilledMetaTyVar
+                           $ tyCoVarsOfTypeList ct_l_ty
+      inert_givens <- getInertSet
+      ev_binds0 <- getTcEvBindsMap evBindsVar
+
       -- Try to solve 'ct_l', using both Givens and top-level instances.
       residual_ct_l <- solveSimpleWanteds ( unitBag ct_l )
       -- Now look up whether GHC has managed to produce evidence for 'ct_l'.
@@ -159,6 +183,17 @@           traceTcS "IfSat solver: LHS constraint could not be solved" $
             vcat [ text "ct_l =" <+> ppr ct_l_ty
                  , text "residual_ct_l =" <+> ppr residual_ct_l ]
+
+          -- Reset the solver state to before we attempted to solve 'ct_l':
+          --
+          --  - reset the inert set,
+          --  - reset the EvBinds,
+          --  - undo any type variable unifications that happened.
+          setInertSet inert_givens
+          setTcEvBindsMap evBindsVar ev_binds0
+          wrapTcS $ for_ ct_l_unfilled_metas \ meta ->
+            writeTcRef ( metaTyVarRef meta ) Flexi
+
           -- Try to solve 'ct_r', using both Givens and top-level instances.
           residual_ct_r <- solveSimpleWanteds ( unitBag ct_r )
           mb_ct_r_evTerm <- lookupEvTerm evBindsVar ct_r_ev_dest
@@ -186,7 +221,7 @@ -- | Look up whether a 'TcEvDest' has been filled with evidence.
 lookupEvTerm :: EvBindsVar -> TcEvDest -> TcS ( Maybe EvTerm )
 lookupEvTerm _ ( HoleDest ( CoercionHole { ch_ref = ref } ) ) = do
-  mb_co <- readTcRef ref
+  mb_co <- wrapTcS $ readTcRef ref
   traceTcS "IfSat solver: coercion hole" ( ppr mb_co )
   case mb_co of
     Nothing -> pure Nothing
test/Main.hs view
@@ -12,6 +12,7 @@   , test3, test3b
 #endif
   , test4, test4b
+  , test5
   )
 
 --------------------------------------------------------------------------------
@@ -28,6 +29,7 @@ #endif
   , Test "test4"  test4  "<<no MyShow instance>>"
   , Test "test4b" test4b False
+  , Test "test5"  test5  'x'
   ]
 
 main :: IO ()
test/Tests.hs view
@@ -3,9 +3,13 @@ {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE NamedWildCards #-}
+{-# LANGUAGE PartialTypeSignatures #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 
 {-# OPTIONS_GHC -fplugin=IfSat.Plugin #-}
 {-# OPTIONS_GHC -dcore-lint #-}
@@ -19,6 +23,7 @@   , test3, test3b
 #endif
   , test4, test4b
+  , test5
   )
   where
 
@@ -32,7 +37,7 @@ 
 -- IfSat
 import Data.Constraint.If
-  ( IfSat, ifSat, IsSat )
+  ( type (||), IfSat, ifSat, IsSat )
 
 --------------------------------------------------------------------------------
 
@@ -99,3 +104,18 @@ 
 test4b :: Bool
 test4b = boolI @( IsSat ( MyShow A ) )
+
+--------------------------------------------------------------------------------
+
+type Stuck :: Type -> Type
+type family Stuck a where
+
+test5_aux :: forall a
+          .  ( ( a ~ Bool, Stuck a ~ Int ) || ( a ~ Char ) )
+          => a -> a
+test5_aux x = x
+
+test5 :: Char
+test5 = test5_aux 'x'
+  -- Check that we correctly backtrack out of "a ~ Bool" and end up
+  -- unifying "a := Char".