ghc-typelits-knownnat 0.6 → 0.7

raw patch · 5 files changed

+302/−54 lines, 5 filesdep +ghc-primdep ~ghcdep ~ghc-typelits-natnormalisedep ~template-haskellPVP ok

version bump matches the API change (PVP)

Dependencies added: ghc-prim

Dependency ranges changed: ghc, ghc-typelits-natnormalise, template-haskell

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• ghc-typelits-knownnat.cabal +7/−6
• src/GHC/TypeLits/KnownNat.hs +87/−3
• src/GHC/TypeLits/KnownNat/Solver.hs +168/−44
• tests/Main.hs +37/−1

@@ -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` 

@@ -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

@@ -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))

@@ -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

@@ -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)),