diff --git a/changelog.md b/changelog.md index 2f34145..fc2d5c1 100644 --- a/changelog.md +++ b/changelog.md @@ -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. diff --git a/if-instance.cabal b/if-instance.cabal index 7432f59..a4c0dbd 100644 --- a/if-instance.cabal +++ b/if-instance.cabal @@ -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 @@ library build-depends: ghc-tcplugin-api - >= 0.9 && < 0.10, + >= 0.10 && < 0.11, exposed-modules: Data.Constraint.If @@ -135,3 +135,7 @@ test-suite if-instance-test main-is: Main.hs + + other-modules: + Framework + Tests diff --git a/src/IfSat/Plugin.hs b/src/IfSat/Plugin.hs index 4494c3c..9ee2549 100644 --- a/src/IfSat/Plugin.hs +++ b/src/IfSat/Plugin.hs @@ -86,7 +86,9 @@ data PluginDefs 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 @@ solveWanted defs@( PluginDefs { orClass } ) givens wanted 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 @@ solveWanted defs@( PluginDefs { orClass } ) givens wanted _ -> 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 diff --git a/test/Framework.hs b/test/Framework.hs new file mode 100644 index 0000000..4b4fb56 --- /dev/null +++ b/test/Framework.hs @@ -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 diff --git a/test/Main.hs b/test/Main.hs index f18dd25..26481a0 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -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 ) +-- IfSat: tests +import Framework + ( Test(..), runTests ) +import Tests + ( test1, test1b + , test2, test2b #if MIN_VERSION_ghc(9,3,0) -import GHC.Exts - ( withDict ) + , test3, test3b #endif - --- IfSat -import Data.Constraint.If - ( IfSat, ifSat, IsSat ) + , test4, test4b + ) -------------------------------------------------------------------------------- -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 _ = "<>" - --- 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 ) ) - --------------------------------------------------------------------------------- - -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 @@ tests = ] main :: IO () -main = do - let - results :: [ String ] - results = mapMaybe runTest tests - case results of - [] -> exitSuccess - _ -> putStrLn ( unlines results ) *> exitFailure +main = runTests tests diff --git a/test/Tests.hs b/test/Tests.hs new file mode 100644 index 0000000..7a380a4 --- /dev/null +++ b/test/Tests.hs @@ -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 _ = "<>" + +-- 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 ) )