if-instance 0.5.0.0 → 0.5.1.0
raw patch · 6 files changed
+174/−37 lines, 6 filesdep ~ghcPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: ghc
API changes (from Hackage documentation)
Files
- changelog.md +7/−1
- if-instance.cabal +6/−3
- src/IfSat/Plugin.hs +41/−28
- src/IfSat/Plugin/Compat.hs +110/−0
- test/Main.hs +3/−2
- test/Tests.hs +7/−3
changelog.md view
@@ -1,5 +1,11 @@ -# Version 0.5.0.0 (2023-08-09) +# Version 0.5.1.0 (2023-08-30) + +- Be more thorough when resetting GHC solver monad state. This should ensure + transparent backtracking after giving up on the LHS of a disjunction + constraint. + +# Version 0.5.0.0 (2023-08-29) - Add a fixity declaration for `(||)` (`infixr 2`, matching term-level disjunction).
if-instance.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: if-instance -version: 0.5.0.0 +version: 0.5.1.0 synopsis: Branch on whether a constraint is satisfied license: BSD-3-Clause build-type: Simple @@ -60,9 +60,9 @@ build-depends: base - >= 4.15.0 && < 4.19, + >= 4.15.0 && < 4.20, ghc - >= 9.0 && < 9.8, + >= 9.0 && < 9.10, default-language: Haskell2010 @@ -90,6 +90,9 @@ exposed-modules: Data.Constraint.If IfSat.Plugin + + other-modules: + IfSat.Plugin.Compat default-language: Haskell2010
src/IfSat/Plugin.hs view
@@ -16,17 +16,13 @@ ( for_ ) import Data.Maybe ( catMaybes ) -#if !MIN_VERSION_ghc(9,2,0) -import Unsafe.Coerce - ( unsafeCoerce ) -#endif -- ghc import GHC.Plugins hiding ( TcPlugin, (<>) ) import GHC.Data.Bag ( unitBag ) -#if MIN_VERSION_ghc(9,8,0) +#if MIN_VERSION_ghc(9,7,0) import GHC.Tc.Solver.Solve ( solveSimpleGivens, solveSimpleWanteds ) #else @@ -34,11 +30,7 @@ ( solveSimpleGivens, solveSimpleWanteds ) #endif import GHC.Tc.Solver.Monad - ( runTcS, runTcSWithEvBinds, traceTcS -#if MIN_VERSION_ghc(9,2,0) - , wrapTcS -#endif - ) + ( runTcS, runTcSWithEvBinds, traceTcS ) import GHC.Tc.Types ( TcM ) import GHC.Tc.Types.Constraint @@ -55,6 +47,10 @@ import GHC.TcPlugin.API.Internal ( unsafeLiftTcM ) +-- if-instance +import IfSat.Plugin.Compat + ( wrapTcS, getRestoreTcS ) + -------------------------------------------------------------------------------- -- Plugin definition. @@ -147,7 +143,7 @@ ct_r_ev_dest = ctev_dest ct_r_ev evBindsVar <- askEvBinds - -- Start a new Solver run. + -- Start a new constraint solver run. unsafeLiftTcM $ runTcSWithEvBinds evBindsVar $ do -- Add back all the Givens. traceTcS "IfSat solver: adding Givens to the inert set" (ppr givens) @@ -158,11 +154,11 @@ ct_l_unfilled_metas <- wrapTcS $ filterM isUnfilledMetaTyVar $ tyCoVarsOfTypeList ct_l_ty - inert_givens <- getInertSet - ev_binds0 <- getTcEvBindsMap evBindsVar + restoreTcS <- getRestoreTcS -- 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'. mb_ct_l_evTerm <- lookupEvTerm evBindsVar ct_l_ev_dest mb_wanted_evTerm <- case mb_ct_l_evTerm of @@ -184,15 +180,14 @@ 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 + -- Reset the solver state to before we attempted to solve 'ct_l', + -- and undo any type variable unifications that happened. + restoreTcS wrapTcS $ for_ ct_l_unfilled_metas \ meta -> writeTcRef ( metaTyVarRef meta ) Flexi + ct_r_unfilled_metas <- wrapTcS + $ filterM isUnfilledMetaTyVar + $ tyCoVarsOfTypeList ct_r_ty -- Try to solve 'ct_r', using both Givens and top-level instances. residual_ct_r <- solveSimpleWanteds ( unitBag ct_r ) @@ -212,7 +207,14 @@ -- This means we can't solve the disjunction constraint. traceTcS "IfSat solver: RHS constraint could not be solved" $ vcat [ text "ct_r =" <+> ppr ct_r_ty - , text "residual ct_r =" <+> ppr residual_ct_r ] + , text "residualct_r =" <+> ppr residual_ct_r ] + + -- Reset the solver state to before we attempted to solve 'ct_r', + -- and undo any type variable unifications that happened. + restoreTcS + wrapTcS $ for_ ct_r_unfilled_metas \ meta -> + writeTcRef ( metaTyVarRef meta ) Flexi + pure Nothing pure $ ( , wanted ) <$> mb_wanted_evTerm | otherwise @@ -346,11 +348,27 @@ 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 + + -- Keep track of the current solver state in order to undo any + -- side-effects after calling 'solveSimpleWanteds' on 'ct'. + ct_unfilled_metas <- wrapTcS + $ filterM isUnfilledMetaTyVar + $ tyCoVarsOfTypeList ct_ty + restoreTcS <- getRestoreTcS + -- Try to solve 'ct', using both Givens and top-level instances. residual_wc <- solveSimpleWanteds ( unitBag ct ) + + -- Reset the solver state to before we attempted to solve 'ct', + -- and undo any type variable unifications that happened. + restoreTcS + wrapTcS $ for_ ct_unfilled_metas \ meta -> + writeTcRef ( metaTyVarRef meta ) Flexi + -- When there are residual Wanteds, we couldn't solve the constraint. let is_sat :: Bool @@ -362,13 +380,8 @@ | otherwise = mkTyConTy promotedFalseDataCon pure $ mkTyFamAppReduction ( "IsSat: " <> show is_sat ) Nominal isSatTyCon [ct_ty] sat + tcPluginTrace "IfSat rewriter }" ( ppr redn ) pure $ TcPluginRewriteTo redn [] -isSatRewriter _ _ _ = pure TcPluginNoRewrite --------------------------------------------------------------------------------- - -#if !MIN_VERSION_ghc(9,2,0) -wrapTcS :: TcM a -> TcS a -wrapTcS = unsafeCoerce const -#endif +isSatRewriter _ _ _ = pure TcPluginNoRewrite
+ src/IfSat/Plugin/Compat.hs view
@@ -0,0 +1,110 @@+{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE CPP #-} + +{-# OPTIONS_GHC -Wno-unused-top-binds #-} + +module IfSat.Plugin.Compat + ( wrapTcS, getRestoreTcS ) + where + +-- base +import Unsafe.Coerce + ( unsafeCoerce ) + +-- ghc +#if MIN_VERSION_ghc(9,4,0) +import GHC.Tc.Solver.InertSet + ( WorkList, InertSet ) +#endif +import GHC.Tc.Solver.Monad + ( TcS +#if MIN_VERSION_ghc(9,1,0) + , TcLevel, wrapTcS +#endif +#if !MIN_VERSION_ghc(9,4,0) + , WorkList, InertSet +#endif + ) +import GHC.Tc.Types + ( TcM, TcRef ) +import GHC.Tc.Types.Evidence + ( EvBindsVar(..) ) + +-- ghc-tcplugin-api +import GHC.TcPlugin.API + ( readTcRef, writeTcRef ) + +-------------------------------------------------------------------------------- + +-- | Capture the current 'TcS' state, returning an action which restores +-- the fields of 'TcSEnv' as appropriate after running a test-run +-- of 'solveSimpleWanteds' and deciding to backtrack. +getRestoreTcS :: TcS (TcS ()) +getRestoreTcS = do + shim_tcs_env <- getShimTcSEnv + let ev_binds_var = shim_tcs_ev_binds shim_tcs_env + unif_var = shim_tcs_unified shim_tcs_env +#if MIN_VERSION_ghc(9,1,0) + unif_lvl_var = shim_tcs_unif_lvl shim_tcs_env +#endif + unit_count_var = shim_tcs_count shim_tcs_env + wrapTcS $ do + restore_evBinds <- case ev_binds_var of + EvBindsVar { ebv_binds = ev_binds_ref + , ebv_tcvs = ev_cvs_ref } -> + do ev_binds <- readTcRef ev_binds_ref + ev_cvs <- readTcRef ev_cvs_ref + return do + writeTcRef ev_binds_ref ev_binds + writeTcRef ev_cvs_ref ev_cvs + CoEvBindsVar { ebv_tcvs = ev_cvs_ref } -> + do ev_cvs <- readTcRef ev_cvs_ref + return do + writeTcRef ev_cvs_ref ev_cvs + + unif <- readTcRef unif_var +#if MIN_VERSION_ghc(9,1,0) + unif_lvl <- readTcRef unif_lvl_var +#endif + count <- readTcRef unit_count_var + return $ wrapTcS $ do + restore_evBinds + writeTcRef unif_var unif +#if MIN_VERSION_ghc(9,1,0) + writeTcRef unif_lvl_var unif_lvl +#endif + writeTcRef unit_count_var count + + -- NB: no need to reset 'tcs_inerts' or 'tcs_worklist', because + -- 'solveSimpleWanteds' calls 'nestTcS', which appropriately resets + -- both of those fields. + +#if !MIN_VERSION_ghc(9,1,0) +wrapTcS :: TcM a -> TcS a +wrapTcS = unsafeCoerce const +#endif + + +-- Obtain the 'TcSEnv' underlying the 'TcS' monad (in the form of a 'ShimTcSEnv'). +getShimTcSEnv :: TcS ShimTcSEnv +getShimTcSEnv = unsafeCoerce ( return :: ShimTcSEnv -> TcM ShimTcSEnv ) + +-- | A shim copy of "GHC.Tc.Solver.Monad.TcSEnv", to work around the +-- fact that it isn't exported. +-- +-- Needs to be manually kept in sync with 'TcSEnv' to avoid segfaults due +-- to the use of 'unsafeCoerce' in 'getShimTcSEnv'. +data ShimTcSEnv + = ShimTcSEnv + { shim_tcs_ev_binds :: EvBindsVar + , shim_tcs_unified :: TcRef Int +#if MIN_VERSION_ghc(9,1,0) + , shim_tcs_unif_lvl :: TcRef (Maybe TcLevel) +#endif + , shim_tcs_count :: TcRef Int + , shim_tcs_inerts :: TcRef InertSet +#if MIN_VERSION_ghc(9,3,0) + , shim_tcs_abort_on_insoluble :: Bool +#endif + , shim_tcs_worklist :: TcRef WorkList + }
test/Main.hs view
@@ -12,7 +12,7 @@ , test3, test3b #endif , test4, test4b - , test5 + , test5a, test5b ) -------------------------------------------------------------------------------- @@ -29,7 +29,8 @@ #endif , Test "test4" test4 "<<no MyShow instance>>" , Test "test4b" test4b False - , Test "test5" test5 'x' + , Test "test5a" test5a 'x' + , Test "test5b" (test5b 'y') 'y' ] main :: IO ()
test/Tests.hs view
@@ -16,6 +16,8 @@ {-# OPTIONS_GHC -fno-specialise #-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} + module Tests ( test1, test1b , test2, test2b @@ -23,7 +25,7 @@ , test3, test3b #endif , test4, test4b - , test5 + , test5a, test5b ) where @@ -115,7 +117,9 @@ => a -> a test5_aux x = x -test5 :: Char -test5 = test5_aux 'x' +test5a :: Char +test5a = test5_aux 'x' +test5b :: _char -> _char +test5b = test5_aux -- Check that we correctly backtrack out of "a ~ Bool" and end up -- unifying "a := Char".