if-instance 0.3.1.0 → 0.4.0.0
raw patch · 6 files changed
+187/−135 lines, 6 filesdep ~ghc-tcplugin-apiPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: ghc-tcplugin-api
API changes (from Hackage documentation)
Files
- changelog.md +5/−0
- if-instance.cabal +6/−2
- src/IfSat/Plugin.hs +21/−15
- test/Framework.hs +44/−0
- test/Main.hs +10/−118
- test/Tests.hs +101/−0
changelog.md view
@@ -1,4 +1,9 @@ +# 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) - Bumping of version bounds, and support for GHC 9.4 and GHC 9.6.
if-instance.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: if-instance -version: 0.3.1.0 +version: 0.4.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.9 && < 0.10, + >= 0.10 && < 0.11, exposed-modules: Data.Constraint.If @@ -135,3 +135,7 @@ main-is: Main.hs + + other-modules: + Framework + Tests
src/IfSat/Plugin.hs view
@@ -86,7 +86,9 @@ findModule :: MonadTcPlugin m => String -> m Module findModule modName = do - findResult <- findImportedModule ( mkModuleName modName ) NoPkgQual + let mod_name = mkModuleName modName + pkg_qual <- resolveImport mod_name Nothing + findResult <- findImportedModule mod_name pkg_qual case findResult of Found _ res -> pure res FoundMultiple _ -> error $ "IfSat plugin: found multiple modules named " <> modName <> "." @@ -136,11 +138,13 @@ traceTcS "IfSat solver: adding Givens to the inert set" (ppr givens) solveSimpleGivens givens -- Try to solve 'ct_l', using both Givens and top-level instances. - _ <- solveSimpleWanteds ( unitBag ct_l ) + 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 - Just ( EvExpr ct_l_evExpr ) -> do + Just ( EvExpr ct_l_evExpr ) + | isEmptyWC residual_ct_l + -> do -- We've managed to solve 'ct_l': use the evidence and take the 'True' branch. traceTcS "IfSat solver: LHS constraint could be solved" ( vcat @@ -152,26 +156,28 @@ _ -> do -- We couldn't solve 'ct_l': this means we must solve 'ct_r', -- to provide evidence needed for the 'False' branch. - traceTcS "IfSat solver: LHS constraint could not be solved" - ( text "ct_l =" <+> ppr ct_l_ty ) + 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 ] -- Try to solve 'ct_r', using both Givens and top-level instances. - _ <- solveSimpleWanteds ( unitBag ct_r ) + residual_ct_r <- solveSimpleWanteds ( unitBag ct_r ) mb_ct_r_evTerm <- lookupEvTerm evBindsVar ct_r_ev_dest case mb_ct_r_evTerm of - Just ( EvExpr ct_r_evExpr ) -> do + Just ( EvExpr ct_r_evExpr ) + | isEmptyWC residual_ct_r + -> do -- We've managed to solve 'ct_r': use the evidence and take the 'False' branch. - traceTcS "IfSat solver: RHS constraint could be solved" - ( vcat - [ text "ct_r =" <+> ppr ct_r_ty - , text "ev =" <+> ppr ct_r_evExpr - ] - ) + traceTcS "IfSat solver: RHS constraint could be solved" $ + vcat [ text "ct_r =" <+> ppr ct_r_ty + , text "ev =" <+> ppr ct_r_evExpr + ] wrapTcS $ ( Just <$> dispatchFalseEvTerm defs ct_l_ty ct_r_ty ct_r_evExpr ) _ -> do -- We could solve neither 'ct_l' not 'ct_r'. -- This means we can't solve the disjunction constraint. - traceTcS "IfSat solver: RHS constraint could not be solved" - ( text "ct_r =" <+> ppr ct_r_ty ) + 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 ] pure Nothing pure $ ( , wanted ) <$> mb_wanted_evTerm | otherwise
+ test/Framework.hs view
@@ -0,0 +1,44 @@+ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NamedFieldPuns #-} + +module Framework + ( Test(..), runTest, runTests ) + where + +-- base +import Data.Maybe + ( mapMaybe ) +import System.Exit + ( exitFailure, exitSuccess ) + +-------------------------------------------------------------------------------- + +data Test where + Test + :: ( Show a, Eq a ) + => { testName :: String + , testActual :: a + , testExpected :: a + } + -> Test + +runTest :: Test -> Maybe String +runTest ( Test { testName, testActual, testExpected } ) + | testActual == testExpected + = Nothing + | otherwise + = Just $ + "\n" <> + "Test '" <> testName <> "' failed.\n" <> + "Expected: " <> show testExpected <> "\n" <> + " Actual: " <> show testActual + +runTests :: [ Test ] -> IO () +runTests tests = do + let + results :: [ String ] + results = mapMaybe runTest tests + case results of + [] -> exitSuccess + _ -> putStrLn ( unlines results ) *> exitFailure
test/Main.hs view
@@ -1,123 +1,21 @@- -{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE CPP #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneKindSignatures #-} -{-# LANGUAGE TypeApplications #-} -{-# OPTIONS_GHC -fplugin=IfSat.Plugin #-} -{-# OPTIONS_GHC -dcore-lint #-} - module Main where --- base -import Data.Maybe - ( mapMaybe ) -import Data.Kind - ( Constraint, Type ) -import System.Exit - ( exitFailure, exitSuccess ) -#if MIN_VERSION_ghc(9,3,0) -import GHC.Exts - ( withDict ) -#endif - --- IfSat -import Data.Constraint.If - ( IfSat, ifSat, IsSat ) - --------------------------------------------------------------------------------- - -type BoolI :: Bool -> Constraint -class BoolI b where - boolI :: Bool -instance BoolI True where - boolI = True -instance BoolI False where - boolI = False - -type MyShow :: Type -> Constraint -class MyShow a where - myShow :: a -> String - -instance MyShow Int where - myShow = show - -myShowAnything :: forall a. IfSat ( MyShow a ) => a -> String -myShowAnything = ifSat @( MyShow a ) yes no - where - yes :: MyShow a => a -> String - yes = myShow - no :: a -> String - no _ = "<<no MyShow instance>>" - --- Should use the "MyShow Int" instance. -test1 :: String -test1 = myShowAnything ( 123 :: Int ) - -test1b :: Bool -test1b = boolI @( IsSat ( MyShow Int ) ) - --- No "MyShow ( Int -> Int -> Int )" instance. -test2 :: String -test2 = myShowAnything ( (+) :: Int -> Int -> Int ) - -test2b :: Bool -test2b = boolI @( IsSat ( MyShow ( Int -> Int -> Int ) ) ) - -data A = A - -myShowA :: IfSat ( MyShow A ) => String -myShowA = myShowAnything A - +-- IfSat: tests +import Framework + ( Test(..), runTests ) +import Tests + ( test1, test1b + , test2, test2b #if MIN_VERSION_ghc(9,3,0) --- Should use the instance locally provided by "withDict". -test3 :: String -test3 = - withDict @( MyShow A ) @( A -> String ) - ( \ _ -> "A" ) - myShowA - -test3b :: Bool -test3b = - withDict @( MyShow A ) @( A -> String ) - ( \ _ -> "A" ) - ( boolI @( IsSat ( MyShow A ) ) ) + , test3, test3b #endif - --- No "MyShow A" instance. -test4 :: String -test4 = myShowA - -test4b :: Bool -test4b = boolI @( IsSat ( MyShow A ) ) + , test4, test4b + ) -------------------------------------------------------------------------------- -data Test where - Test - :: ( Show a, Eq a ) - => { testName :: String - , testActual :: a - , testExpected :: a - } - -> Test - -runTest :: Test -> Maybe String -runTest ( Test { testName, testActual, testExpected } ) - | testActual == testExpected - = Nothing - | otherwise - = Just $ - "\n" <> - "Test '" <> testName <> "' failed.\n" <> - "Expected: " <> show testExpected <> "\n" <> - " Actual: " <> show testActual - tests :: [ Test ] tests = [ Test "test1" test1 "123" @@ -133,10 +31,4 @@ ] main :: IO () -main = do - let - results :: [ String ] - results = mapMaybe runTest tests - case results of - [] -> exitSuccess - _ -> putStrLn ( unlines results ) *> exitFailure +main = runTests tests
+ test/Tests.hs view
@@ -0,0 +1,101 @@+ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeApplications #-} + +{-# OPTIONS_GHC -fplugin=IfSat.Plugin #-} +{-# OPTIONS_GHC -dcore-lint #-} + +{-# OPTIONS_GHC -fno-specialise #-} + +module Tests + ( test1, test1b + , test2, test2b +#if MIN_VERSION_ghc(9,3,0) + , test3, test3b +#endif + , test4, test4b + ) + where + +-- base +import Data.Kind + ( Constraint, Type ) +#if MIN_VERSION_ghc(9,3,0) +import GHC.Exts + ( withDict ) +#endif + +-- IfSat +import Data.Constraint.If + ( IfSat, ifSat, IsSat ) + +-------------------------------------------------------------------------------- + +type BoolI :: Bool -> Constraint +class BoolI b where + boolI :: Bool +instance BoolI True where + boolI = True +instance BoolI False where + boolI = False + +type MyShow :: Type -> Constraint +class MyShow a where + myShow :: a -> String + +instance MyShow Int where + myShow = show + +myShowAnything :: forall a. IfSat ( MyShow a ) => a -> String +myShowAnything = ifSat @( MyShow a ) yes no + where + yes :: MyShow a => a -> String + yes = myShow + no :: a -> String + no _ = "<<no MyShow instance>>" + +-- Should use the "MyShow Int" instance. +test1 :: String +test1 = myShowAnything ( 123 :: Int ) + +test1b :: Bool +test1b = boolI @( IsSat ( MyShow Int ) ) + +-- No "MyShow ( Int -> Int -> Int )" instance. +test2 :: String +test2 = myShowAnything ( (+) :: Int -> Int -> Int ) + +test2b :: Bool +test2b = boolI @( IsSat ( MyShow ( Int -> Int -> Int ) ) ) + +data A = A + +myShowA :: IfSat ( MyShow A ) => String +myShowA = myShowAnything A + +#if MIN_VERSION_ghc(9,3,0) +-- Should use the instance locally provided by "withDict". +test3 :: String +test3 = + withDict @( MyShow A ) @( A -> String ) + ( \ _ -> "A" ) + myShowA + +test3b :: Bool +test3b = + withDict @( MyShow A ) @( A -> String ) + ( \ _ -> "A" ) + ( boolI @( IsSat ( MyShow A ) ) ) +#endif + +-- No "MyShow A" instance. +test4 :: String +test4 = myShowA + +test4b :: Bool +test4b = boolI @( IsSat ( MyShow A ) )