packages feed

if-instance 0.2.0.0 → 0.2.1.0

raw patch · 4 files changed

+78/−33 lines, 4 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 view
@@ -1,10 +1,14 @@+# Version 0.2.1.0 (2021-08-31)
+
+- Require `ghc-tcplugin-api >= 0.5.1.0`.
+
 # Version 0.2.0.0 (2021-08-31)
 
-- Add a type family 'IsSat :: Constraint -> Bool'
+- Add a type family `IsSat :: Constraint -> Bool`
   that computes whether a type-family is satisfied in
   the current context.
 
-- Rename 'IfCt' to 'IfSat'
+- Rename `IfCt` to `IfSat`.
 
 # Version 0.1.0.0 (2021-08-30)
if-instance.cabal view
@@ -1,6 +1,6 @@ cabal-version:  3.0
 name:           if-instance
-version:        0.2.0.0
+version:        0.2.1.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.5.0.0 && < 0.6,
+      >= 0.5.1.0 && < 0.6,
 
   exposed-modules:
     Data.Constraint.If
src/IfSat/Plugin.hs view
@@ -183,15 +183,15 @@   let
     r, a, b :: CoreBndr
     r = mkTyVar r_name liftedTypeKind
-    a = mkLocalId a_name Many ( mkInvisFunTyMany (sat_eqTy defs ct_ty tru) $ mkInvisFunTyMany ct_ty r_ty )
-    b = mkWildValBinder  Many ( mkInvisFunTyMany (sat_eqTy defs ct_ty fls) r_ty )
+    a = mkLocalId a_name Many ( mkInvisFunTyMany (sat_eqTy defs ct_ty True ) $ mkInvisFunTyMany ct_ty r_ty )
+    b = mkWildValBinder  Many ( mkInvisFunTyMany (sat_eqTy defs ct_ty False) r_ty )
     r_ty :: Type
     r_ty = mkTyVarTy r
   pure . EvExpr $
     mkCoreConApps ( classDataCon ifSatClass )
       [ Type ct_ty
       , mkCoreLams [ r, a, b ]
-        ( mkCoreApps ( Var a ) [ sat_co_expr defs ct_ty tru, ct_evTerm ] )
+        ( mkCoreApps ( Var a ) [ sat_co_expr defs ct_ty True, ct_evTerm ] )
       ]
 
 -- Evidence term for @IfSat ct@ when @ct@ isn't satisfied.
@@ -203,37 +203,46 @@   let
     r, a, b :: CoreBndr
     r = mkTyVar r_name liftedTypeKind
-    a = mkWildValBinder  Many ( mkInvisFunTyMany (sat_eqTy defs ct_ty tru) $ mkInvisFunTyMany ct_ty r_ty )
-    b = mkLocalId b_name Many ( mkInvisFunTyMany (sat_eqTy defs ct_ty fls) r_ty )
+    a = mkWildValBinder  Many ( mkInvisFunTyMany (sat_eqTy defs ct_ty True ) $ mkInvisFunTyMany ct_ty r_ty )
+    b = mkLocalId b_name Many ( mkInvisFunTyMany (sat_eqTy defs ct_ty False) r_ty )
     r_ty :: Type
     r_ty = mkTyVarTy r
   pure . EvExpr $
     mkCoreConApps ( classDataCon ifSatClass )
       [ Type ct_ty
       , mkCoreLams [ r, a, b ]
-        ( mkCoreApps ( Var b ) [ sat_co_expr defs ct_ty fls ] )
+        ( mkCoreApps ( Var b ) [ sat_co_expr defs ct_ty False ] )
       ]
 
-fls, tru :: Type
-fls = mkTyConTy promotedFalseDataCon
-tru = mkTyConTy promotedTrueDataCon
-
--- @ sat_eqTy defs ct_ty rhs @ represents the type @ IsSat ct ~ rhs @.
-sat_eqTy :: PluginDefs -> Type -> Type -> Type
-sat_eqTy ( PluginDefs { isSatTyCon } ) ct_ty rhs
+-- @ sat_eqTy defs ct_ty b @ represents the type @ IsSat ct ~ b @.
+sat_eqTy :: PluginDefs -> Type -> Bool -> Type
+sat_eqTy ( PluginDefs { isSatTyCon } ) ct_ty booly
   = mkTyConApp eqTyCon
       [ boolTy, mkTyConApp isSatTyCon [ct_ty], rhs ]
+  where
+    rhs :: Type
+    rhs = if booly then tru else fls
 
--- @ sat_co_expr defs ct_ty rhs @ is an expression of type @ IsSat ct ~ rhs @.
-sat_co_expr :: PluginDefs -> Type -> Type -> EvExpr
-sat_co_expr ( PluginDefs { isSatTyCon } ) ct_ty rhs
+-- @ sat_co_expr defs ct_ty b @ is an expression of type @ IsSat ct ~ b @.
+sat_co_expr :: PluginDefs -> Type -> Bool -> EvExpr
+sat_co_expr ( PluginDefs { isSatTyCon } ) ct_ty booly
   = mkCoreConApps eqDataCon
       [ Type boolTy
       , Type $ mkTyConApp isSatTyCon [ ct_ty ]
       , Type rhs
-      , Coercion $ mkPluginUnivCo "IfSat: IsSat" Nominal ( mkTyConApp isSatTyCon [ct_ty] ) rhs
+      , Coercion $
+          mkPluginUnivCo ( "IfSat :" <> show booly )
+          Nominal
+          ( mkTyConApp isSatTyCon [ct_ty] ) rhs
       ]
+  where
+    rhs :: Type
+    rhs = if booly then tru else fls
 
+fls, tru :: Type
+fls = mkTyConTy promotedFalseDataCon
+tru = mkTyConTy promotedTrueDataCon
+
 --------------------------------------------------------------------------------
 
 rewriter :: PluginDefs -> UniqFM TyCon TcPluginRewriter
@@ -255,15 +264,18 @@     solveSimpleGivens givens
     -- Try to solve 'ct', using both Givens and top-level instances.
     residual_wc <- solveSimpleWanteds ( unitBag ct )
+    -- When there are residual Wanteds, we couldn't solve the constraint.
     let
+      is_sat :: Bool
+      is_sat = isEmptyWC residual_wc
       sat :: Type
       sat
-        | isEmptyWC residual_wc
+        | is_sat
         = mkTyConTy promotedTrueDataCon
         | otherwise
         = mkTyConTy promotedFalseDataCon
-    pure $ mkTyFamAppReduction "IfSat: IsSat" Nominal isSatTyCon [ct_ty] sat
-  tcPluginTrace "IfSat rewriter }" empty
+    pure $ mkTyFamAppReduction ( "IsSat: " <> show is_sat ) Nominal isSatTyCon [ct_ty] sat
+  tcPluginTrace "IfSat rewriter }" ( ppr redn )
   pure $ TcPluginRewriteTo redn []
 isSatRewriter _ _ _ = pure TcPluginNoRewrite
test/Main.hs view
@@ -1,7 +1,9 @@ 
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE CPP #-}
-{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
@@ -19,17 +21,25 @@   ( Constraint, Type )
 import System.Exit
   ( exitFailure, exitSuccess )
-#if MIN_VERSION_ghc(9,4,0)
+#if MIN_VERSION_ghc(9,3,0)
 import GHC.Exts
   ( withDict )
 #endif
 
 -- IfSat
 import Data.Constraint.If
-  ( IfSat(ifSat) )
+  ( 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
@@ -49,28 +59,43 @@ 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,4,0)
+#if MIN_VERSION_ghc(9,3,0)
 -- Should use the instance locally provided by "withDict".
 test3 :: String
 test3 =
   withDict @( A -> String ) @( MyShow A )
     ( \ _ -> "A" )
     myShowA
+
+test3b :: Bool
+test3b =
+  withDict @( A -> String ) @( MyShow A )
+    ( \ _ -> "A" )
+    ( boolI @( IsSat ( MyShow A ) ) )
 #endif
 
 -- No "MyShow A" instance.
 test4 :: String
 test4 = myShowA
 
+test4b :: Bool
+test4b = boolI @( IsSat ( MyShow A ) )
+
 --------------------------------------------------------------------------------
 
 data Test where
@@ -95,12 +120,16 @@ 
 tests :: [ Test ]
 tests =
-  [ Test "test1" test1 "123"
-  , Test "test2" test2 "<<no MyShow instance>>"
-#if MIN_VERSION_ghc(9,4,0)
-  , Test "test3" test3 "A"
+  [ Test "test1"  test1  "123"
+  , Test "test1b" test1b True
+  , Test "test2"  test2  "<<no MyShow instance>>"
+  , Test "test2b" test2b False
+#if MIN_VERSION_ghc(9,3,0)
+  , Test "test3"  test3  "A"
+  , Test "test3b" test3b True
 #endif
-  , Test "test4" test4 "<<no MyShow instance>>"
+  , Test "test4"  test4  "<<no MyShow instance>>"
+  , Test "test4b" test4b False
   ]
 
 main :: IO ()