diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.7 *August 26th 2018* +* Solve "known" type-level Booleans, also inside `If` (GHC 8.6+) + ## 0.6 *September 14th 2018* * Move `KnownNat2` instances for `Div` and `Mod` from `ghc-typelits-extra` to `ghc-typelits-knownnat` diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal --- a/ghc-typelits-knownnat.cabal +++ b/ghc-typelits-knownnat.cabal @@ -1,5 +1,5 @@ name: ghc-typelits-knownnat -version: 0.6 +version: 0.7 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@ @@ -53,8 +53,8 @@ extra-source-files: README.md CHANGELOG.md cabal-version: >=1.10 -tested-with: GHC==8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.4.2, - GHC == 8.6 +tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5, + GHC == 8.8.1 source-repository head type: git @@ -86,9 +86,10 @@ UndecidableInstances ViewPatterns build-depends: base >= 4.9 && <5, - ghc >= 8.0.1 && <8.8, + ghc >= 8.0.1 && <8.9, + ghc-prim >= 0.4.0.0 && <0.6, ghc-tcplugins-extra >= 0.3, - ghc-typelits-natnormalise >= 0.6 && <0.7, + ghc-typelits-natnormalise >= 0.6 && <0.8, transformers >= 0.5.2.0 && <0.6, template-haskell >= 2.11.0.0 && <2.15 hs-source-dirs: src @@ -104,7 +105,7 @@ Other-Modules: TestFunctions build-depends: base >= 4.8 && <5, ghc-typelits-knownnat, - ghc-typelits-natnormalise >= 0.6 && <0.7, + ghc-typelits-natnormalise >= 0.6 && <0.8, tasty >= 0.10, tasty-hunit >= 0.9, tasty-quickcheck >= 0.8 diff --git a/src/GHC/TypeLits/KnownNat.hs b/src/GHC/TypeLits/KnownNat.hs --- a/src/GHC/TypeLits/KnownNat.hs +++ b/src/GHC/TypeLits/KnownNat.hs @@ -86,8 +86,11 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} @@ -109,6 +112,15 @@ , KnownNat1 (..) , KnownNat2 (..) , KnownNat3 (..) + -- * Singleton boolean + , SBool (..) + , boolVal + -- * KnownBool + , KnownBool (..) + -- ** Constraint-level boolean functions + , SBoolKb (..) + , KnownNat2Bool (..) + , KnownBoolNat2 (..) -- * Template Haskell helper , nameToSymbol ) @@ -116,17 +128,21 @@ import Data.Bits (shiftL) import Data.Proxy (Proxy (..)) +import Data.Type.Bool (If) +import GHC.Prim (Proxy#) #if MIN_VERSION_ghc(8,2,0) import GHC.TypeNats - (KnownNat, Nat, type (+), type (*), type (^), type (-), natVal, type (<=)) + (KnownNat, Nat, type (+), type (*), type (^), type (-), type (<=?), type (<=), + natVal) #if MIN_VERSION_base(4,11,0) import GHC.TypeNats (Div, Mod) #endif import GHC.TypeLits (Symbol) import Numeric.Natural (Natural) #else -import GHC.TypeLits (KnownNat, Nat, Symbol, type (+), type (*), - type (^), type (-), natVal, type (<=)) +import GHC.TypeLits + (KnownNat, Nat, Symbol, type (+), type (*), type (^), type (-), type (<=?), + type (<=), natVal) #endif import GHC.TypeLits.KnownNat.TH @@ -195,3 +211,71 @@ instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x y where natSing2 = SNatKn (rem (natVal (Proxy @x)) (natVal (Proxy @y))) #endif + +-- | Singleton version of 'Bool' +data SBool (b :: Bool) where + SFalse :: SBool 'False + STrue :: SBool 'True + +class KnownBool (b :: Bool) where + boolSing :: SBool b + +instance KnownBool 'False where + boolSing = SFalse + +instance KnownBool 'True where + boolSing = STrue + +-- | Get the 'Bool' value associated with a type-level 'Bool' +-- +-- Use 'boolVal' if you want to perform the standard boolean operations on the +-- reified type-level 'Bool'. +-- +-- Use 'boolSing' if you need a context in which the type-checker needs the +-- type-level 'Bool' to be either 'True' or 'False' +-- +-- @ +-- f :: forall proxy b r . KnownBool b => r +-- f = case boolSing @ b of +-- SFalse -> -- context with b ~ False +-- STrue -> -- context with b ~ True +-- @ +boolVal :: forall b proxy . KnownBool b => proxy b -> Bool +boolVal _ = case boolSing :: SBool b of + SFalse -> False + _ -> True + +-- | Get the `Bool` value associated with a type-level `Bool`. See also +-- 'boolVal' and 'Proxy#'. +boolVal' :: forall b . KnownBool b => Proxy# b -> Bool +boolVal' _ = case boolSing :: SBool b of + SFalse -> False + _ -> True + +-- | A type "representationally equal" to 'SBool', used for simpler +-- implementation of constraint-level functions that need to create instances of +-- 'KnownBool' +newtype SBoolKb (f :: Symbol) = SBoolKb Bool + +-- | Class for binary functions with a Boolean result. +-- +-- The 'Symbol' /f/ must correspond to the fully qualified name of the +-- type-level operation. Use 'nameToSymbol' to get the fully qualified +-- TH Name as a 'Symbol' +class KnownBoolNat2 (f :: Symbol) (a :: k) (b :: k) where + boolNatSing2 :: SBoolKb f + +instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''(<=?)) a b where + boolNatSing2 = SBoolKb (natVal (Proxy @a) <= natVal (Proxy @b)) + {-# INLINE boolNatSing2 #-} + +-- | Class for ternary functions with a Natural result. +-- +-- The 'Symbol' /f/ must correspond to the fully qualified name of the +-- type-level operation. Use 'nameToSymbol' to get the fully qualified +-- TH Name as a 'Symbol' +class KnownNat2Bool (f :: Symbol) (a :: Bool) (b :: k) (c :: k) where + natBoolSing3 :: SNatKn f + +instance (KnownBool a, KnownNat b, KnownNat c) => KnownNat2Bool $(nameToSymbol ''If) a b c where + natBoolSing3 = SNatKn (if boolVal (Proxy @a) then natVal (Proxy @b) else natVal (Proxy @c)) diff --git a/src/GHC/TypeLits/KnownNat/Solver.hs b/src/GHC/TypeLits/KnownNat/Solver.hs --- a/src/GHC/TypeLits/KnownNat/Solver.hs +++ b/src/GHC/TypeLits/KnownNat/Solver.hs @@ -93,7 +93,9 @@ {-# OPTIONS_HADDOCK show-extensions #-} -module GHC.TypeLits.KnownNat.Solver (plugin) where +module GHC.TypeLits.KnownNat.Solver + ( plugin ) +where -- external import Control.Arrow ((&&&), first) @@ -110,6 +112,9 @@ -- GHC API import Class (Class, classMethods, className, classTyCon) +#if MIN_VERSION_ghc(8,6,0) +import Coercion (Role (Representational), mkUnivCo) +#endif import FamInst (tcInstNewTyCon_maybe) import FastString (fsLit) import Id (idType) @@ -148,13 +153,23 @@ import Type (EqRel (NomEq), PredTree (ClassPred,EqPred), PredType, classifyPredType, dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, - piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe) + piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind) import TyCon (tyConName) import TyCoRep (Type (..), TyLit (..)) +#if MIN_VERSION_ghc(8,6,0) +import TyCoRep (UnivCoProvenance (PluginProv)) +import TysWiredIn (boolTy) +#endif import Var (DFunId) -- | Classes and instances from "GHC.TypeLits.KnownNat" -type KnownNatDefs = Int -> Maybe Class -- ^ KnownNatN class +data KnownNatDefs + = KnownNatDefs + { knownBool :: Class + , knownBoolNat2 :: Class + , knownNat2Bool :: Class + , knownNatN :: Int -> Maybe Class -- ^ KnownNat{N} + } -- | KnownNat constraints type KnConstraint = (Ct -- The constraint @@ -270,9 +285,9 @@ subst = map fst $ mkSubst' givens kn_wanteds = map (\(x,y,z) -> (x,y,substType subst z)) - $ mapMaybe toKnConstraint wanteds' + $ mapMaybe (toKnConstraint defs) wanteds' #else - kn_wanteds = mapMaybe toKnConstraint wanteds' + kn_wanteds = mapMaybe (toKnConstraint defs) wanteds' #endif case kn_wanteds of [] -> return (TcPluginOk [] []) @@ -289,10 +304,11 @@ return (TcPluginOk solved (concat new)) -- | Get the KnownNat constraints -toKnConstraint :: Ct -> Maybe KnConstraint -toKnConstraint ct = case classifyPredType $ ctEvPred $ ctEvidence ct of +toKnConstraint :: KnownNatDefs -> Ct -> Maybe KnConstraint +toKnConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of ClassPred cls [ty] - | className cls == knownNatClassName + | className cls == knownNatClassName || + className cls == className (knownBool defs) -> Just (ct,cls,ty) _ -> Nothing @@ -315,14 +331,22 @@ lookupKnownNatDefs :: TcPluginM KnownNatDefs lookupKnownNatDefs = do md <- lookupModule myModule myPackage + kbC <- look md "KnownBool" + kbn2C <- look md "KnownBoolNat2" + kn2bC <- look md "KnownNat2Bool" kn1C <- look md "KnownNat1" kn2C <- look md "KnownNat2" kn3C <- look md "KnownNat3" - return $ (\case { 1 -> Just kn1C - ; 2 -> Just kn2C - ; 3 -> Just kn3C - ; _ -> Nothing - }) + return KnownNatDefs + { knownBool = kbC + , knownBoolNat2 = kbn2C + , knownNat2Bool = kn2bC + , knownNatN = \case { 1 -> Just kn1C + ; 2 -> Just kn2C + ; 3 -> Just kn3C + ; _ -> Nothing + } + } where look md s = do nm <- lookupName md (mkTcOcc s) @@ -359,26 +383,49 @@ -- type-level operation go :: Type -> TcPluginM (Maybe (EvTerm,[Ct])) go (go_other -> Just ev) = return (Just (ev,[])) - go ty@(TyConApp tc args) + go ty@(TyConApp tc args0) | let tcNm = tyConName tc , Just m <- nameModule_maybe tcNm - , Just knN_cls <- defs (length args) - = do let mS = moduleNameString (moduleName m) - tcS = occNameString (nameOccName tcNm) - fn = mkStrLitTy (fsLit (mS ++ "." ++ tcS)) - args' = fn:args - ienv <- getInstEnvs - case lookupUniqueInstEnv ienv knN_cls args' of - Right (inst, _) -> do - let df_id = instanceDFunId inst - df = (knN_cls,df_id) - df_args = fst -- [KnownNat x, KnownNat y] - . splitFunTys -- ([KnownNat x, KnowNat y], DKnownNat2 "+" x y) - . (`piResultTys` args) -- (KnowNat x, KnownNat y) => DKnownNat2 "+" x y - $ idType df_id -- forall a b . (KnownNat a, KnownNat b) => DKnownNat2 "+" a b - (evs,new) <- unzip <$> mapM go_arg df_args - return ((,concat new) <$> makeOpDict df cls args' op evs) - _ -> return ((,[]) <$> go_other ty) + = do + ienv <- getInstEnvs + let mS = moduleNameString (moduleName m) + tcS = occNameString (nameOccName tcNm) + fn0 = mS ++ "." ++ tcS + fn1 = mkStrLitTy (fsLit fn0) + args1 = fn1:args0 + instM = case () of + () | Just knN_cls <- knownNatN defs (length args0) + , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1 + -> Just (inst,knN_cls,args0,args1) + | length args0 == 2 + , let knN_cls = knownBoolNat2 defs + ki = typeKind (head args0) + args1N = ki:args1 + , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N + -> Just (inst,knN_cls,args0,args1N) + | length args0 == 4 + , fn0 == "Data.Type.Bool.If" + , let args0N = tail args0 + args1N = head args0:fn1:tail args0 + knN_cls = knownNat2Bool defs + , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N + -> Just (inst,knN_cls,args0N,args1N) + | otherwise + -> Nothing + case instM of + Just (inst,knN_cls,args0N,args1N) -> do + let df_id = instanceDFunId inst + df = (knN_cls,df_id) + df_args = fst -- [KnownNat x, KnownNat y] + . splitFunTys -- ([KnownNat x, KnowNat y], DKnownNat2 "+" x y) + . (`piResultTys` args0N) -- (KnowNat x, KnownNat y) => DKnownNat2 "+" x y + $ idType df_id -- forall a b . (KnownNat a, KnownNat b) => DKnownNat2 "+" a b + (evs,new) <- unzip <$> mapM go_arg df_args + if className cls == className (knownBool defs) + then return ((,concat new) <$> makeOpDictByFiat df cls args1N args0N op evs) + else return ((,concat new) <$> makeOpDict df cls args1N args0N op evs) + _ -> return ((,[]) <$> go_other ty) + go (LitTy (NumTyLit i)) -- Let GHC solve simple Literal constraints | LitTy _ <- op @@ -506,18 +553,24 @@ this process is mirrored for the dictionary functions of a higher arity -} -makeOpDict :: (Class,DFunId) -- ^ "magic" class function and dictionary function id - -> Class -- ^ KnownNat class - -> [Type] -- ^ Argument types - -> Type -- ^ Type of the result +makeOpDict + :: (Class,DFunId) + -- ^ "magic" class function and dictionary function id + -> Class + -- ^ KnownNat class + -> [Type] + -- ^ Argument types for the Class + -> [Type] + -- ^ Argument types for the Instance + -> Type -- ^ Type of the result #if MIN_VERSION_ghc(8,5,0) - -> [EvExpr] + -> [EvExpr] #else - -> [EvTerm] + -> [EvTerm] #endif - -- ^ Evidence arguments - -> Maybe EvTerm -makeOpDict (opCls,dfid) knCls tyArgs z evArgs + -- ^ Evidence arguments + -> Maybe EvTerm +makeOpDict (opCls,dfid) knCls tyArgsC tyArgsI z evArgs | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z] -- KnownNat n ~ SNat n , [ kn_meth ] <- classMethods knCls @@ -527,19 +580,19 @@ $ idType kn_meth -- forall n. KnownNat n => SNat n , Just (_, kn_co_rep) <- tcInstNewTyCon_maybe kn_tcRep [z] -- SNat n ~ Integer - , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgs + , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgsC -- KnownNatAdd a b ~ SNatKn (a+b) , [ op_meth ] <- classMethods opCls , Just (op_tcRep,op_args) <- splitTyConApp_maybe -- (SNatKn, [KnownNatF2 f x y]) $ funResultTy -- SNatKn (KnownNatF2 f x y) - $ (`piResultTys` tyArgs) -- KnownNatAdd f x y => SNatKn (KnownNatF2 f x y) + $ (`piResultTys` tyArgsC) -- KnownNatAdd f x y => SNatKn (KnownNatF2 f x y) $ idType op_meth -- forall f a b . KnownNat2 f a b => SNatKn (KnownNatF2 f a b) , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args -- SNatKn (a+b) ~ Integer #if MIN_VERSION_ghc(8,5,0) - , let EvExpr dfun_inst = evDFunApp dfid (tail tyArgs) evArgs + , let EvExpr dfun_inst = evDFunApp dfid tyArgsI evArgs #else - , let dfun_inst = EvDFunApp dfid (tail tyArgs) evArgs + , let dfun_inst = EvDFunApp dfid tyArgsI evArgs #endif -- KnownNatAdd a b op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep) @@ -626,4 +679,75 @@ = Just ev_tm | otherwise = Nothing +#endif + +{- | +Given: + +* A "magic" class, and corresponding instance dictionary function, for a + type-level boolean operation +* Two KnownBool dictionaries + +makeOpDictByFiat instantiates the dictionary function with the KnownBool +dictionaries, and coerces it to a KnownBool dictionary. i.e. for KnownBoolNat2, +the "magic" dictionary for binary functions, the coercion happens in the +following steps: + +1. KnownBoolNat2 "<=?" x y -> SBoolF "<=?" +2. SBoolF "<=?" -> Bool +3. Bool -> SNat (x <=? y) THE BY FIAT PART! +4. SBool (x <=? y) -> KnownBool (x <=? y) + +this process is mirrored for the dictionary functions of a higher arity +-} +makeOpDictByFiat + :: (Class,DFunId) + -- ^ "magic" class function and dictionary function id + -> Class + -- ^ KnownNat class + -> [Type] + -- ^ Argument types for the Class + -> [Type] + -- ^ Argument types for the Instance + -> Type + -- ^ Type of the result +#if MIN_VERSION_ghc(8,6,0) + -> [EvExpr] +#else + -> [EvTerm] +#endif + -- ^ Evidence arguments + -> Maybe EvTerm +#if MIN_VERSION_ghc(8,6,0) +makeOpDictByFiat (opCls,dfid) knCls tyArgsC tyArgsI z evArgs + -- KnownBool b ~ SBool b + | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z] + , [ kn_meth ] <- classMethods knCls + , Just kn_tcRep <- tyConAppTyCon_maybe -- SBool + $ funResultTy -- SBool b + $ dropForAlls -- KnownBool b => SBool b + $ idType kn_meth -- forall b. KnownBool b => SBool b + -- SBool b R~ Bool (The "Lie") + , let kn_co_rep = mkUnivCo (PluginProv "ghc-typelits-knownnat") + Representational + (mkTyConApp kn_tcRep [z]) boolTy + -- KnownBoolNat2 f a b ~ SBool f + , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgsC + , [ op_meth ] <- classMethods opCls + , Just (op_tcRep,op_args) <- splitTyConApp_maybe -- (SBool, [f]) + $ funResultTy -- SBool f + $ (`piResultTys` tyArgsC) -- KnownBoolNat2 f x y => SBool f + $ idType op_meth -- forall f x y . KnownBoolNat2 f a b => SBoolf f + -- SBoolF f ~ Bool + , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args + , EvExpr dfun_inst <- evDFunApp dfid tyArgsI evArgs + -- KnownBoolNat2 f x y ~ KnownBool b + , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep) + (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep)) + ev_tm = mkEvCast dfun_inst op_to_kn + = Just ev_tm + | otherwise + = Nothing +#else +makeOpDictByFiat _ _ _ _ _ _ = Nothing #endif diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -24,6 +24,10 @@ import Test.Tasty.HUnit import Test.Tasty.QuickCheck import Unsafe.Coerce (unsafeCoerce) +#if __GLASGOW_HASKELL__ >= 806 +import Data.Type.Bool (If) +import GHC.TypeLits.KnownNat +#endif import TestFunctions @@ -168,6 +172,17 @@ test24 :: (KnownNat n, n ~ (m+1)) => proxy m -> Number test24 = natVal +#if __GLASGOW_HASKELL__ >= 806 +test25 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Bool +test25 _ _ = boolVal (Proxy :: Proxy (n <=? m)) + +test26 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Natural +test26 _ _ = natVal (Proxy :: Proxy (If (n <=? m) m n)) + +test27 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Natural +test27 _ _ = natVal (Proxy :: Proxy (If (n <=? m) n m)) +#endif + tests :: TestTree tests = testGroup "ghc-typelits-natnormalise" [ testGroup "Basic functionality" @@ -256,8 +271,29 @@ , testCase "(KnownNat n, n ~ m + 1) ~ KnownNat m" $ show (test24 (Proxy @4)) @?= "4" - ], +#if __GLASGOW_HASKELL__ >= 806 + testGroup "KnownBool" + [ testCase "KnownBool (X <=? Y) @2 @3 ~ True" $ + show (test25 (Proxy @2) (Proxy @3)) @?= + "True" + , testCase "KnownBool (X <=? Y) @3 @2 ~ False" $ + show (test25 (Proxy @3) (Proxy @2)) @?= + "False" + , testCase "KnownNat (If (X <=? Y) Y X) @2 @3 ~ 3" $ + show (test26 (Proxy @2) (Proxy @3)) @?= + "3" + , testCase "KnownNat (If (X <=? Y) Y X) @3 @2 ~ 3" $ + show (test26 (Proxy @3) (Proxy @2)) @?= + "3" + , testCase "KnownNat (If (X <=? Y) X Y) @2 @3 ~ 2" $ + show (test27 (Proxy @2) (Proxy @3)) @?= + "2" + , testCase "KnownNat (If (X <=? Y) X Y) @3 @2 ~ 2" $ + show (test27 (Proxy @3) (Proxy @2)) @?= + "2" + ], +#endif testGroup "QuickCheck" [ testProperty "addT = (+)" $ (\a b -> (a >= 0 && b >= 0) ==> (addT a b === a + b)), testProperty "subT = (-)" $ (\a b -> (a >= b && b >= 0) ==> (subT a b === a - b)),