v0.4.0.0

sheaf · Aug 9, 2023 · b0ad0a5 · b0ad0a5
1 parent 47bf4c6
commit b0ad0a5
Show file tree

Hide file tree

Showing 6 changed files with 187 additions and 135 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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 _ = "<<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 ) )
-
---------------------------------------------------------------------------------
-
-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
@@ -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 ) )