ghc-typelits-knownnat 0.1.1 → 0.2
raw patch · 8 files changed
+714/−211 lines, 8 filesdep +ghc-typelits-natnormalisedep +singletonsdep +template-haskell
Dependencies added: ghc-typelits-natnormalise, singletons, template-haskell, transformers
Files
- CHANGELOG.md +9/−0
- README.md +52/−8
- ghc-typelits-knownnat.cabal +42/−15
- src/GHC/TypeLits/KnownNat.hs +139/−25
- src/GHC/TypeLits/KnownNat/Solver.hs +289/−161
- src/GHC/TypeLits/KnownNat/TH.hs +16/−0
- tests/Main.hs +126/−2
- tests/TestFunctions.hs +41/−0
CHANGELOG.md view
@@ -1,5 +1,14 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.2 *August 17th 2016*+* New features:+ * Handle `GHC.TypeLits.-`+ * Handle custom, user-defined, type-level operations+ * Thanks to Gabor Greif (@ggreif): derive smaller from larger constraints, i.e. `KnownNat (n+1)` implies `KnownNat n`++## 0.1.2+* New features: Solve "complex" KnownNat constraints involving arbitrary type-functions, as long as there is a given KnownNat constraint for this type functions.+ ## 0.1.1 *August 11th 2016* * Fixes bug: panic on a non-given KnownNat constraint variable
README.md view
@@ -1,6 +1,6 @@ # ghc-typelits-knownnat -[](http://travis-ci.org/clash-lang/ghc-typelits-knownnat)+[](http://travis-ci.org/clash-lang/ghc-typelits-knownnat) [](https://hackage.haskell.org/package/ghc-typelits-knownnat) [](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-knownnat) @@ -9,26 +9,70 @@ plugin, you must have both a `KnownNat n` and a `KnownNat (n+2)` constraint in the type signature of the following function: -```+```haskell f :: forall n . (KnownNat n, KnownNat (n+2)) => Proxy n -> Integer f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) ``` Using the plugin you can omit the `KnownNat (n+2)` constraint: -```+```haskell f :: forall n . KnownNat n => Proxy n -> Integer f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) ``` -The plugin can only derive `KnownNat` constraints consisting of:+The plugin can derive `KnownNat` constraints for types consisting of: +* Type variables, when there is a corresponding `KnownNat` constraint * Type-level naturals-* Type variables-* Applications of the arithmetic expression: `{+,*,^}`.+* Applications of the arithmetic expression: `{+,-,*,^}`+* Type functions, when there is either:+ * a matching given `KnownNat` constraint; or+ * a corresponding `KnownNat<N>` instance for the type function -i.e. it _cannot_ derive a `KnownNat (n-1)` constraint from a `KnownNat n`-constraint+To elaborate the latter points, given the type family `Min`:++```haskell+type family Min (a :: Nat) (b :: Nat) :: Nat where+ Min 0 b = 0+ Min a b = If (a <=? b) a b+```++the plugin can derive a `KnownNat (Min x y + 1)` constraint given only a+`KnownNat (Min x y)` constraint:++```haskell+g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer+g _ _ = natVal (Proxy :: Proxy (Min x y + 1))+```++And, given the type family `Max`:++```haskell+type family Max (a :: Nat) (b :: Nat) :: Nat where+ Max 0 b = b+ Max a b = If (a <=? b) b a+```++and corresponding `KnownNat2` instance:++```haskell+instance (KnownNat a, KnownNat b) => KnownNat2 "TestFunctions.Max" a b where+ type KnownNatF2 "TestFunctions.Max" = MaxSym2+ natSing2 = let x = natVal (Proxy @ a)+ y = natVal (Proxy @ b)+ z = max x y+ in SNatKn z+ {-# INLINE natSing2 #-}+```++the plugin can derive a `KnownNat (Max x y + 1)` constraint given only a+`KnownNat x` and `KnownNat y` constraint:++```haskell+h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer+h _ _ = natVal (Proxy :: Proxy (Max x y + 1))+``` To use the plugin, add the
ghc-typelits-knownnat.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-knownnat-version: 0.1.1+version: 0.2 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@@@ -19,17 +19,20 @@ f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) @ .- The plugin can only derive @KnownNat@ constraints consisting of:+ The plugin can derive @KnownNat@ constraints for types consisting of: .+ * Type variables, when there is a corresponding @KnownNat@ constraint+ . * Type-level naturals .- * Type variables+ * Applications of the arithmetic expression: +,-,*,^ .- * Applications of the arithmetic expression: +,*,^+ * Type functions, when there is either: .- i.e. it /cannot/ derive a @KnownNat (n-1)@ constraint from a @KnownNat n@- constraint+ 1. a matching given @KnownNat@ constraint; or .+ 2. a corresponding @KnownNat\<N\>@ instance for the type function+ . To use the plugin, add the . @@@ -60,20 +63,31 @@ manual: True library- exposed-modules: GHC.TypeLits.KnownNat.Solver,- GHC.TypeLits.KnownNat+ exposed-modules: GHC.TypeLits.KnownNat,+ GHC.TypeLits.KnownNat.Solver+ other-modules: GHC.TypeLits.KnownNat.TH other-extensions: AllowAmbiguousTypes DataKinds FlexibleInstances- MultiParamTypeClasses KindSignatures+ LambdaCase+ MultiParamTypeClasses ScopedTypeVariables+ TemplateHaskell TupleSections TypeApplications TypeOperators- build-depends: base >= 4.9 && <4.10,- ghc >= 8.0.1 && <8.2,- ghc-tcplugins-extra >= 0.2+ TypeFamilies+ TypeInType+ UndecidableInstances+ ViewPatterns+ build-depends: base >= 4.9 && <4.10,+ ghc >= 8.0.1 && <8.2,+ ghc-tcplugins-extra >= 0.2,+ ghc-typelits-natnormalise >= 0.5 && <0.6,+ singletons >= 2.2 && <3.0,+ transformers >= 0.5.2.0 && <0.6,+ template-haskell >= 2.11.0.0 && <2.13 hs-source-dirs: src default-language: Haskell2010 if flag(deverror)@@ -81,18 +95,31 @@ else ghc-options: -Wall -test-suite test-ghc-typelits-knownat+test-suite test-ghc-typelits-knownnat type: exitcode-stdio-1.0 main-is: Main.hs- build-depends: base >= 4.8 && <5,+ Other-Modules: TestFunctions+ build-depends: base >= 4.8 && <5, ghc-typelits-knownnat >= 0.1,+ ghc-typelits-natnormalise >= 0.5 && <0.6,+ singletons >= 2.2 && <3.0, tasty >= 0.10, tasty-hunit >= 0.9 hs-source-dirs: tests default-language: Haskell2010 other-extensions: DataKinds- ScopedTypeVariables+ FlexibleContexts+ FlexibleInstances+ GADTs+ MultiParamTypeClasses+ KindSignatures+ ScopedTypeVariables,+ TemplateHaskell TypeApplications+ TypeFamilies+ TypeFamilyDependencies+ TypeInType TypeOperators+ UndecidableInstances if flag(deverror) ghc-options: -O0 -dcore-lint
src/GHC/TypeLits/KnownNat.hs view
@@ -5,6 +5,80 @@ Some \"magic\" classes and instances to get the "GHC.TypeLits.KnownNat.Solver" type checker plugin working.++= Usage++Let's say you defined a closed type family @Max@:++@+import Data.Type.Bool (If)+import GHC.TypeLits++type family Max (a :: Nat) (b :: Nat) :: Nat where+ Max 0 b = b+ Max a b = If (a <=? b) b a+@++if you then want the "GHC.TypeLits.KnownNat.Solver" to solve 'KnownNat'+constraints over @Max@, given just 'KnownNat' constraints for the arguments+of @Max@, then you must define:++@+\{\-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables,+ TypeApplications, TypeFamilies, TypeInType, TypeOperators,+ UndecidableInstances, TemplateHaskell \#-\}++import Data.Proxy (Proxy (..))+import Data.Singletons (Apply, type (~>))+import GHC.TypeLits.KnownNat++instance (KnownNat a, KnownNat b) => 'KnownNat2' $('nameToSymbol' ''Max) a b where+ type 'KnownNatF2' $('nameToSymbol' ''Max) = MaxSym2+ natSing2 = let x = natVal (Proxy @a)+ y = natVal (Proxy @b)+ z = max x y+ in 'SNatKn' z+ \{\-# INLINE natSing2 \#-\}+@++= FAQ++==== 1. "GHC.TypeLits.KnownNat.Solver" does not seem to find the corresponding 'KnownNat2' instance for my type-level operation+At the Core-level, GHCs internal mini-Haskell, type families that only have a+single equation are treated like type synonyms.++For example, let's say we defined a closed type family @Max@:++@+import Data.Type.Bool (If)+import GHC.TypeLits++type family Max (a :: Nat) (b :: Nat) :: Nat where+ Max a b = If (a <=? b) b a+@++Now, a Haskell-level program might contain a constraint++@+KnownNat (Max a b)+@++, however, at the Core-level, this constraint is expanded to:++@+KnownNat (If (a <=? b) b a)+@++"GHC.TypeLits.KnownNat.Solver" never sees any reference to the @Max@ type+family, so it will not look for the corresponding 'KnownNat2' instance either.+To fix this, ensure that your type-level operations always have at+least two equations. For @Max@ this means we have to redefine it as:++@+type family Max (a :: Nat) (b :: Nat) :: Nat where+ Max 0 b = b+ Max a b = If (a <=? b) b a+@ -} {-# LANGUAGE AllowAmbiguousTypes #-}@@ -13,44 +87,84 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE Safe #-}+{-# LANGUAGE Trustworthy #-} {-# OPTIONS_GHC -Wno-unused-top-binds -fexpose-all-unfoldings #-} {-# OPTIONS_HADDOCK show-extensions #-} -module GHC.TypeLits.KnownNat () where+module GHC.TypeLits.KnownNat+ ( -- * Singleton natural number+ SNatKn (..)+ -- * Constraint-level arithmetic classes+ , KnownNat2 (..)+ , KnownNat3 (..)+ -- * Template Haskell helper+ , nameToSymbol+ )+where -import Data.Bits (shiftL)-import Data.Proxy (Proxy (..))-import GHC.TypeLits (KnownNat, Nat, type (+), type (*), type (^), natVal)+import Data.Bits (shiftL)+import Data.Proxy (Proxy (..))+import GHC.TypeLits (KnownNat, Nat, Symbol, type (+), type (*),+ type (^), type (-), type (<=), natVal)+import Data.Singletons (type (~>), type (@@))+import Data.Promotion.Prelude (type (:+$), type (:*$), type (:^$), type (:-$)) +import GHC.TypeLits.KnownNat.TH++-- | Singleton natural number (represented by an integer) newtype SNatKn (n :: Nat) = SNatKn Integer -class KnownNatAdd (a :: Nat) (b :: Nat) where- natSingAdd :: SNatKn (a + b)+-- | Class for arithmetic functions with /two/ arguments.+--+-- 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 KnownNat2 (f :: Symbol) (a :: Nat) (b :: Nat) where+ type KnownNatF2 f :: Nat ~> Nat ~> Nat+ natSing2 :: SNatKn (KnownNatF2 f @@ a @@ b) -instance (KnownNat a, KnownNat b) => KnownNatAdd a b where- natSingAdd = SNatKn (natVal (Proxy @ a) + natVal (Proxy @ b))- {-# INLINE natSingAdd #-}+-- | Class for arithmetic functions with /three/ arguments.+--+-- 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 KnownNat3 (f :: Symbol) (a :: Nat) (b :: Nat) (c :: Nat) where+ type KnownNatF3 f :: Nat ~> Nat ~> Nat ~> Nat+ natSing3 :: SNatKn (KnownNatF3 f @@ a @@ b @@ c) -class KnownNatMul (a :: Nat) (b :: Nat) where- natSingMul :: SNatKn (a * b)+-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.+'+instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(+)) a b where+ type KnownNatF2 $(nameToSymbol ''(+)) = (:+$)+ natSing2 = SNatKn (natVal (Proxy @a) + natVal (Proxy @b))+ {-# INLINE natSing2 #-} -instance (KnownNat a, KnownNat b) => KnownNatMul a b where- natSingMul = SNatKn (natVal (Proxy @ a) * natVal (Proxy @ b))- {-# INLINE natSingMul #-}+-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.*'+instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(*)) a b where+ type KnownNatF2 $(nameToSymbol ''(*)) = (:*$)+ natSing2 = SNatKn (natVal (Proxy @a) * natVal (Proxy @b))+ {-# INLINE natSing2 #-} -class KnownNatExp (a :: Nat) (b :: Nat) where- natSingExp :: SNatKn (a ^ b)+-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.^'+instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where+ type KnownNatF2 $(nameToSymbol ''(^)) = (:^$)+ natSing2 = let x = natVal (Proxy @ a)+ y = natVal (Proxy @ b)+ z = case x of+ 2 -> shiftL 1 (fromInteger y)+ _ -> x ^ y+ in SNatKn z+ {-# INLINE natSing2 #-} -instance (KnownNat a, KnownNat b) => KnownNatExp a b where- natSingExp = let x = natVal (Proxy @ a)- y = natVal (Proxy @ b)- z = case x of- 2 -> shiftL 1 (fromInteger y)- _ -> x ^ y- in SNatKn z- {-# INLINE natSingExp #-}+-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.-'+instance (KnownNat a, KnownNat b, b <= a) => KnownNat2 $(nameToSymbol ''(-)) a b where+ type KnownNatF2 $(nameToSymbol ''(-)) = (:-$)+ natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b))+ {-# INLINE natSing2 #-}
src/GHC/TypeLits/KnownNat/Solver.hs view
@@ -20,15 +20,59 @@ f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) @ -The plugin can only derive @KnownNat@ constraints consisting of:+The plugin can derive @KnownNat@ constraints for types consisting of: +* Type variables, when there is a corresponding @KnownNat@ constraint * Type-level naturals-* Type variables-* Applications of the arithmetic expression: @{+,*,^}@+* Applications of the arithmetic expression: @{+,-,*,^}@+* Type functions, when there is either:+ * a matching given @KnownNat@ constraint; or+ * a corresponding @KnownNat\<N\>@ instance for the type function -i.e. it /cannot/ derive a @KnownNat (n-1)@ constraint from a @KnownNat n@-constraint+To elaborate the latter points, given the type family @Min@: +@+type family Min (a :: Nat) (b :: Nat) :: Nat where+ Min 0 b = 0+ Min a b = If (a <=? b) a b+@++the plugin can derive a @KnownNat (Min x y + 1)@ constraint given only a+@KnownNat (Min x y)@ constraint:++@+g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer+g _ _ = natVal (Proxy :: Proxy (Min x y + 1))+@++And, given the type family @Max@:++@+type family Max (a :: Nat) (b :: Nat) :: Nat where+ Max 0 b = b+ Max a b = If (a <=? b) b a+@++and corresponding @KnownNat2@ instance:++@+instance (KnownNat a, KnownNat b) => KnownNat2 \"TestFunctions.Max\" a b where+ type KnownNatF2 \"TestFunctions.Max\" = MaxSym2+ natSing2 = let x = natVal (Proxy @ a)+ y = natVal (Proxy @ b)+ z = max x y+ in SNatKn z+ \{\-# INLINE natSing2 \#-\}+@++the plugin can derive a @KnownNat (Max x y + 1)@ constraint given only a+@KnownNat x@ and @KnownNat y@ constraint:++@+h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer+h _ _ = natVal (Proxy :: Proxy (Max x y + 1))+@+ To use the plugin, add the @@@ -39,7 +83,9 @@ -} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE TupleSections #-}+{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE Trustworthy #-} @@ -48,8 +94,13 @@ module GHC.TypeLits.KnownNat.Solver (plugin) where -- external-import Data.Maybe (catMaybes,mapMaybe)-import GHC.TcPluginM.Extra (lookupModule, lookupName, tracePlugin)+import Control.Arrow ((&&&), first)+import Control.Monad.Trans.Maybe (MaybeT (..))+import Data.Maybe (catMaybes,mapMaybe)+import GHC.TcPluginM.Extra (lookupModule, lookupName, newWanted,+ tracePlugin)+import GHC.TypeLits.Normalise.SOP (SOP (..), Product (..), Symbol (..))+import GHC.TypeLits.Normalise.Unify (CType (..),normaliseNat,reifySOP) -- GHC API import Class (Class, classMethods, className, classTyCon)@@ -57,57 +108,32 @@ import FastString (fsLit) import Id (idType) import InstEnv (instanceDFunId,lookupUniqueInstEnv)-import Module (mkModuleName)-import OccName (mkTcOcc)-import Outputable (Outputable (..), (<+>), integer, text, vcat)-import Panic (panicDoc, pgmErrorDoc)+import Module (mkModuleName, moduleName, moduleNameString)+import Name (nameModule_maybe, nameOccName)+import OccName (mkTcOcc, occNameString) import Plugins (Plugin (..), defaultPlugin) import PrelNames (knownNatClassName)-import TcEvidence (EvTerm (..), EvLit (EvNum), mkEvCast, mkTcSymCo, mkTcTransCo)+import TcEvidence (EvTerm (..), mkEvCast, mkTcSymCo, mkTcTransCo) import TcPluginM (TcPluginM, tcLookupClass, getInstEnvs, zonkCt)-import TcRnTypes (Ct, CtEvidence (..), TcPlugin(..), TcPluginResult (..),- ctEvidence, ctEvPred, isWanted)-import TcTypeNats (typeNatAddTyCon, typeNatMulTyCon, typeNatExpTyCon)-import Type (PredTree (ClassPred), TyVar, classifyPredType, dropForAlls,- funResultTy, tyConAppTyCon_maybe, mkNumLitTy, mkTyVarTy,- mkTyConApp)-import TyCoRep (Type (..), TyLit (..))+import TcRnTypes (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvPred,+ ctEvTerm, ctLoc, isWanted, mkNonCanonical)+import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon)+import Type (PredTree (ClassPred), PredType, classifyPredType, dropForAlls,+ funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, piResultTys,+ splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe)+import TyCon (tyConName)+import TyCoRep (Type (..)) import Var (DFunId) -- | Classes and instances from "GHC.TypeLits.KnownNat"-data KnownNatDefs = KnownNatDefs- { knAddDFunId :: (Class,DFunId) -- ^ KnownNatAdd class and its only instance- , knMulDFunId :: (Class,DFunId) -- ^ KnownNatMul class and its only instance- , knExpDFunId :: (Class,DFunId) -- ^ KnownNatPow class and its only instance- }--instance Outputable KnownNatDefs where- ppr d = text "{" <+> ppr (knAddDFunId d) <+>- text "," <+> ppr (knMulDFunId d) <+>- text "," <+> ppr (knExpDFunId d) <+>- text "}"+type KnownNatDefs = Int -> Maybe Class -- ^ KnownNatN class -- | KnownNat constraints type KnConstraint = (Ct -- The constraint ,Class -- KnownNat class- ,KnOp -- The argument to KnownNat+ ,Type -- The argument to KnownNat ) --- | Reified argument of a KnownNat-data KnOp- = I Integer- | V TyVar- | Add KnOp KnOp- | Mul KnOp KnOp- | Exp KnOp KnOp--instance Outputable KnOp where- ppr (I i) = integer i- ppr (V v) = ppr v- ppr (Add x y) = text "(" <+> ppr x <+> text "+" <+> ppr y <+> text ")"- ppr (Mul x y) = text "(" <+> ppr x <+> text "*" <+> ppr y <+> text ")"- ppr (Exp x y) = text "(" <+> ppr x <+> text "^" <+> ppr y <+> text ")"- {-| A type checker plugin for GHC that can derive \"complex\" @KnownNat@ constraints from other simple/variable @KnownNat@ constraints. i.e. without@@ -126,15 +152,59 @@ f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) @ -The plugin can only derive @KnownNat@ constraints consisting of:+The plugin can derive @KnownNat@ constraints for types consisting of: +* Type variables, when there is a corresponding @KnownNat@ constraint * Type-level naturals-* Type variables-* Applications of the arithmetic expression: @{+,*,^}@.+* Applications of the arithmetic expression: @{+,-,*,^}@+* Type functions, when there is either:+ * a matching given @KnownNat@ constraint; or+ * a corresponding @KnownNat\<N\>@ instance for the type function -i.e. it /cannot/ derive a @KnownNat (n-1)@ constraint from a @KnownNat n@-constraint+To elaborate the latter points, given the type family @Min@: +@+type family Min (a :: Nat) (b :: Nat) :: Nat where+ Min 0 b = 0+ Min a b = If (a <=? b) a b+@++the plugin can derive a @KnownNat (Min x y + 1)@ constraint given only a+@KnownNat (Min x y)@ constraint:++@+g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer+g _ _ = natVal (Proxy :: Proxy (Min x y + 1))+@++And, given the type family @Max@:++@+type family Max (a :: Nat) (b :: Nat) :: Nat where+ Max 0 b = b+ Max a b = If (a <=? b) b a+@++and corresponding @KnownNat2@ instance:++@+instance (KnownNat a, KnownNat b) => KnownNat2 \"TestFunctions.Max\" a b where+ type KnownNatF2 \"TestFunctions.Max\" = MaxSym2+ natSing2 = let x = natVal (Proxy @ a)+ y = natVal (Proxy @ b)+ z = max x y+ in SNatKn z+ \{\-# INLINE natSing2 \#-\}+@++the plugin can derive a @KnownNat (Max x y + 1)@ constraint given only a+@KnownNat x@ and @KnownNat y@ constraint:++@+h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer+h _ _ = natVal (Proxy :: Proxy (Max x y + 1))+@+ To use the plugin, add the @@@ -142,6 +212,7 @@ @ Pragma to the header of your file.+ -} plugin :: Plugin plugin = defaultPlugin { tcPlugin = const $ Just normalisePlugin }@@ -163,98 +234,148 @@ case kn_wanteds of [] -> return (TcPluginOk [] []) _ -> do- kn_givens <- catMaybes <$> mapM (fmap toKnConstraint . zonkCt) givens- -- Make a lookup table of the [G]iven KnownNat constraints- let kn_map = mapMaybe toKnEntry kn_givens+ -- Make a lookup table for all the [G]iven constraints+ given_map <- mapM (fmap toGivenEntry . zonkCt) givens -- Try to solve the wanted KnownNat constraints given the [G]iven -- KnownNat constraints- let solved = mapMaybe (constraintToEvTerm defs kn_map) kn_wanteds- return (TcPluginOk solved [])+ (solved,new) <- (unzip . catMaybes) <$> (mapM (constraintToEvTerm defs given_map) kn_wanteds)+ return (TcPluginOk solved (concat new)) -- | Get the KnownNat constraints toKnConstraint :: Ct -> Maybe KnConstraint toKnConstraint ct = case classifyPredType $ ctEvPred $ ctEvidence ct of ClassPred cls [ty] | className cls == knownNatClassName- -> ((ct,cls,) <$> toKnOp ty)+ -> Just (ct,cls,ty) _ -> Nothing -{- |-The plugin can only derive @KnownNat@ constraints consisting of:--* Type-level naturals-* Type variables-* Applications of the arithmetic expression: @{+,*,^}@.--}-toKnOp :: Type -> Maybe KnOp-toKnOp (LitTy (NumTyLit i)) = pure (I i)-toKnOp (TyVarTy v) = pure (V v)-toKnOp (TyConApp tc [x,y])- | tc == typeNatAddTyCon = Add <$> toKnOp x <*> toKnOp y- | tc == typeNatMulTyCon = Mul <$> toKnOp x <*> toKnOp y- | tc == typeNatExpTyCon = Exp <$> toKnOp x <*> toKnOp y-toKnOp _ = Nothing+-- | Create a look-up entry for a [G]iven constraint.+toGivenEntry :: Ct -> (CType,EvTerm)+toGivenEntry ct = let ct_ev = ctEvidence ct+ c_ty = ctEvPred ct_ev+ ev = ctEvTerm ct_ev+ in (CType c_ty,ev) --- | Create a look-up entry for @n@ given a [G]iven @KnownNat n@ constraint.-toKnEntry :: KnConstraint -> Maybe (TyVar,KnConstraint)-toKnEntry kn@(_,_,V v) = Just (v,kn)-toKnEntry _ = Nothing+-- | Normalise a type to Sum-of-Product type form as defined in the+-- `ghc-typelits-natnormalise` package.+normaliseSOP :: Type -> Type+normaliseSOP = reifySOP . normaliseNat -- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat" lookupKnownNatDefs :: TcPluginM KnownNatDefs lookupKnownNatDefs = do md <- lookupModule myModule myPackage- addDF <- look md "KnownNatAdd"- mulDF <- look md "KnownNatMul"- expDF <- look md "KnownNatExp"- return $ KnownNatDefs addDF mulDF expDF+ kn2C <- look md "KnownNat2"+ kn3C <- look md "KnownNat3"+ return $ (\case { 2 -> Just kn2C+ ; 3 -> Just kn3C+ ; _ -> Nothing+ }) where look md s = do nm <- lookupName md (mkTcOcc s)- cls <- tcLookupClass nm- ienv <- getInstEnvs- case lookupUniqueInstEnv ienv cls [mkNumLitTy 0, mkNumLitTy 0] of- Right (inst, _) -> return (cls,instanceDFunId inst)- Left err ->- pgmErrorDoc "Initialising GHC.TypeLits.KnownNat.Solver failed"- (vcat [text "Cannot find: " <+> text s- ,text "Reason: "- ,err- ])+ tcLookupClass nm myModule = mkModuleName "GHC.TypeLits.KnownNat" myPackage = fsLit "ghc-typelits-knownnat" --- | Convert a reified argument of a KnownNat constraint back to a type-reifyOp :: KnOp -> Type-reifyOp (I i) = mkNumLitTy i-reifyOp (V v) = mkTyVarTy v-reifyOp (Add x y) = mkTyConApp typeNatAddTyCon [reifyOp x, reifyOp y]-reifyOp (Mul x y) = mkTyConApp typeNatMulTyCon [reifyOp x, reifyOp y]-reifyOp (Exp x y) = mkTyConApp typeNatExpTyCon [reifyOp x, reifyOp y]- -- | Try to create evidence for a wanted constraint-constraintToEvTerm :: KnownNatDefs -> [(TyVar,KnConstraint)] -> KnConstraint- -> Maybe (EvTerm,Ct)-constraintToEvTerm defs kn_map (ct,cls,op) = (,ct) <$> go op+constraintToEvTerm :: KnownNatDefs -- ^ The "magic" KnownNatN classes+ -> [(CType,EvTerm)] -- All the [G]iven constraints+ -> KnConstraint+ -> TcPluginM (Maybe ((EvTerm,Ct),[Ct]))+constraintToEvTerm defs givens (ct,cls,op) = do+ -- 1. Normalise to SOP normal form+ let ty = normaliseSOP op+ -- 2. Determine if we are an offset apart from a [G]iven constraint+ offsetM <- offset ty+ evM <- case offsetM of+ -- 3.a If so, we are done+ found@Just {} -> return found+ -- 3.b If not, we check if the outer type-level operation+ -- has a corresponding KnownNat<N> instance.+ _ -> go ty+ return (first (,ct) <$> evM) where- go (I i) = makeLitDict cls (mkNumLitTy i) i- go (V v) = case lookup v kn_map of- Just (ct',_,_) -> let ct_ev = ctEvidence ct'- evT = ctev_evar ct_ev- in Just (EvId evT)- Nothing -> Nothing- go e = do- let (x,y,df) = case e of- Add x' y' -> (x',y',knAddDFunId defs)- Mul x' y' -> (x',y',knMulDFunId defs)- Exp x' y' -> (x',y',knExpDFunId defs)- _ -> panicDoc "GHC.TypeLits.KnownNat.Solver: not an op" (ppr e)- x' <- go x- y' <- go y- makeOpDict df cls (reifyOp x) (reifyOp y) (reifyOp e) x' y'+ -- Determine whether the outer type-level operation has a corresponding+ -- KnownNat<N> instance, where /N/ corresponds to the arity of the+ -- type-level operation+ go :: Type -> TcPluginM (Maybe (EvTerm,[Ct]))+ go (go_other -> Just ev) = return (Just (ev,[]))+ go ty@(TyConApp tc args)+ | 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)+ go _ = return Nothing -{-+ -- Get EvTerm arguments for type-level operations. If they do not exist+ -- as [G]iven constraints, then generate new [W]anted constraints+ go_arg :: PredType -> TcPluginM (EvTerm,[Ct])+ go_arg ty = case lookup (CType ty) givens of+ Just ev -> return (ev,[])+ _ -> do+ wanted <- newWanted (ctLoc ct) ty+ let ev = ctEvTerm wanted+ return (ev,[mkNonCanonical wanted])++ -- Fall through case: look up the normalised [W]anted constraint in the list+ -- of [G]iven constraints.+ go_other :: Type -> Maybe EvTerm+ go_other ty =+ let knClsTc = classTyCon cls+ kn = mkTyConApp knClsTc [ty]+ cast = if CType ty == CType op+ then Just+ else makeKnCoercion cls ty op+ in cast =<< lookup (CType kn) givens++ -- Find a known constraint for a wanted, so that (modulo normalization)+ -- the two are a constant offset apart.+ offset :: Type -> TcPluginM (Maybe (EvTerm,[Ct]))+ offset want = runMaybeT $ do+ let unKn ty' = case classifyPredType ty' of+ ClassPred cls' [ty'']+ | className cls' == knownNatClassName+ -> Just ty''+ _ -> Nothing+ -- Get only the [G]iven KnownNat constraints+ knowns = mapMaybe (unKn . unCType . fst) givens+ -- pair up the sum-of-products KnownNat constraints+ -- with the original Nat operation+ subWant = mkTyConApp typeNatSubTyCon . (:[want])+ exploded = map (normaliseNat . subWant &&& id) knowns+ -- interesting cases for us are those where+ -- wanted and given only differ by a constant+ examine (diff,entire) =+ case diff of+ S [P [I n]] -> Just (entire, n)+ _ -> Nothing+ interesting = mapMaybe examine exploded+ -- convert the first suitable evidence+ ((h,corr):_) <- pure interesting+ let x = case corr of+ 0 -> h+ _ | corr < 0 -> mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate corr)]+ | otherwise -> mkTyConApp typeNatSubTyCon [h,mkNumLitTy corr]+ MaybeT (go x)++{- | Given: * A "magic" class, and corresponding instance dictionary function, for a@@ -262,26 +383,23 @@ * Two KnownNat dictionaries makeOpDict instantiates the dictionary function with the KnownNat dictionaries,-and coerces it to a KnownNat dictionary. i.e. for KnownNatAdd, the "magic"-dictionary for addition, the coercion happens in the following steps:+and coerces it to a KnownNat dictionary. i.e. for KnownNat2, the "magic"+dictionary for binary functions, the coercion happens in the following steps: -1. KnownNatAdd a b -> SNatKn (a + b)-2. SNatKn (a + b) -> Integer-3. Integer -> SNat (a + b)-4. SNat (a + b) -> KnownNat (a + b)+1. KnownNat2 "+" a b -> SNatKn (KnownNatF2 "+" a b)+2. SNatKn (KnownNatF2 "+" a b) -> Integer+3. Integer -> SNat (a + b)+4. SNat (a + b) -> KnownNat (a + b) -The process is mirrored for KnownNatMul, and KnownNatExp, the classes-representing multiplication and exponentiation.+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 -- ^ Type of the first argument- -> Type -- ^ Type of the second argument+ -> [Type] -- ^ Argument types -> Type -- ^ Type of the result- -> EvTerm -- ^ KnownNat dictionary for the first argument- -> EvTerm -- ^ KnownNat dictionary for the second argument+ -> [EvTerm] -- ^ Evidence arguments -> Maybe EvTerm-makeOpDict (opCls,dfid) knCls x y z xEv yEv+makeOpDict (opCls,dfid) knCls tyArgs z evArgs | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z] -- KnownNat n ~ SNat n , [ kn_meth ] <- classMethods knCls@@ -291,16 +409,16 @@ $ 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) [x,y]+ , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgs -- KnownNatAdd a b ~ SNatKn (a+b) , [ op_meth ] <- classMethods opCls- , Just op_tcRep <- tyConAppTyCon_maybe -- SNatKn- $ funResultTy -- SNatKn (a+b)- $ dropForAlls -- KnownNatAdd a b => SNatKn (a + b)- $ idType op_meth -- forall a b . KnownNatAdd a b => SNatKn (a+b)- , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep [z]+ , 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)+ $ 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- , let dfun_inst = EvDFunApp dfid [x,y] [xEv,yEv]+ , let dfun_inst = EvDFunApp dfid (tail tyArgs) evArgs -- KnownNatAdd a b op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep) (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep))@@ -310,27 +428,37 @@ | otherwise = Nothing --- | THIS CODE IS COPIED FROM:--- https://github.com/ghc/ghc/blob/8035d1a5dc7290e8d3d61446ee4861e0b460214e/compiler/typecheck/TcInteract.hs#L1973------ makeLitDict adds a coercion that will convert the literal into a dictionary--- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]--- in TcEvidence. The coercion happens in 2 steps:------ Integer -> SNat n -- representation of literal to singleton--- SNat n -> KnownNat n -- singleton to dictionary-makeLitDict :: Class -> Type -> Integer -> Maybe EvTerm-makeLitDict clas ty i- | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]- -- co_dict :: KnownNat n ~ SNat n- , [ meth ] <- classMethods clas- , Just tcRep <- tyConAppTyCon_maybe -- SNat- $ funResultTy -- SNat n- $ dropForAlls -- KnownNat n => SNat n- $ idType meth -- forall n. KnownNat n => SNat n- , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]- -- SNat n ~ Integer- , let ev_tm = mkEvCast (EvLit (EvNum i)) (mkTcSymCo (mkTcTransCo co_dict co_rep))- = Just ev_tm- | otherwise- = Nothing+{-+Given:+* A KnownNat dictionary evidence over a type x+* a desired type z+makeKnCoercion assembles a coercion from a KnownNat x+dictionary to a KnownNat z dictionary and applies it+to the passed-in evidence.+The coercion happens in the following steps:+1. KnownNat x -> SNat x+2. SNat x -> Integer+3. Integer -> SNat z+4. SNat z -> KnownNat z+-}+makeKnCoercion :: Class -- ^ KnownNat class+ -> Type -- ^ Type of the argument+ -> Type -- ^ Type of the result+ -> EvTerm -- ^ KnownNat dictionary for the argument+ -> Maybe EvTerm+makeKnCoercion knCls x z xEv+ | Just (_, kn_co_dict_z) <- tcInstNewTyCon_maybe (classTyCon knCls) [z]+ -- KnownNat z ~ SNat z+ , [ kn_meth ] <- classMethods knCls+ , Just kn_tcRep <- tyConAppTyCon_maybe -- SNat+ $ funResultTy -- SNat n+ $ dropForAlls -- KnownNat n => SNat n+ $ idType kn_meth -- forall n. KnownNat n => SNat n+ , Just (_, kn_co_rep_z) <- tcInstNewTyCon_maybe kn_tcRep [z]+ -- SNat z ~ Integer+ , Just (_, kn_co_rep_x) <- tcInstNewTyCon_maybe kn_tcRep [x]+ -- Integer ~ SNat x+ , Just (_, kn_co_dict_x) <- tcInstNewTyCon_maybe (classTyCon knCls) [x]+ -- SNat x ~ KnownNat x+ = Just . mkEvCast xEv $ (kn_co_dict_x `mkTcTransCo` kn_co_rep_x) `mkTcTransCo` mkTcSymCo (kn_co_dict_z `mkTcTransCo` kn_co_rep_z)+ | otherwise = Nothing
+ src/GHC/TypeLits/KnownNat/TH.hs view
@@ -0,0 +1,16 @@+{-|+Copyright : (C) 2016, University of Twente+License : BSD2 (see the file LICENSE)+Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>+-}++{-# OPTIONS_GHC -Wno-unused-imports #-}++module GHC.TypeLits.KnownNat.TH where++import GHC.TypeLits (Symbol) -- haddock only+import Language.Haskell.TH (Name, TypeQ, litT, strTyLit)++-- | Convert a TH 'Name' to a type-level 'Symbol'+nameToSymbol :: Name -> TypeQ+nameToSymbol = litT . strTyLit . show
tests/Main.hs view
@@ -1,12 +1,20 @@-{-# LANGUAGE DataKinds, ScopedTypeVariables, TypeOperators, TypeApplications #-}+{-# LANGUAGE DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TypeOperators,+ TypeApplications, TypeFamilies, TypeFamilyDependencies, FlexibleContexts #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} +module Main where+ import Data.Proxy+import Data.Type.Equality ((:~:)(..)) import GHC.TypeLits import Test.Tasty import Test.Tasty.HUnit+import Unsafe.Coerce (unsafeCoerce) +import TestFunctions+ test1 :: forall n . KnownNat n => Proxy n -> Integer test1 _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) @@ -25,6 +33,70 @@ test6 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer test6 _ _ = natVal (Proxy :: Proxy ((n^m)+(n*m))) +test7 :: forall n m . (KnownNat m, KnownNat n) => Proxy n -> Proxy m -> Integer+test7 _ _ = natVal (Proxy :: Proxy (Max n m + 1))++test8 :: forall n m . (KnownNat (Min n m)) => Proxy n -> Proxy m -> Integer+test8 _ _ = natVal (Proxy :: Proxy (Min n m + 1))++test9 :: forall n m . (KnownNat m, KnownNat n, n <= m) => Proxy m -> Proxy n -> Integer+test9 _ _ = natVal (Proxy :: Proxy (m-n))++test10 :: forall (n :: Nat) m . (KnownNat m) => Proxy m -> Proxy n -> Integer+test10 _ _ = natVal (Proxy :: Proxy (m-n+n))++test11 :: forall m . (KnownNat m) => Proxy m -> Integer+test11 _ = natVal (Proxy @ (m*m))++test12 :: forall m . (KnownNat (m+1)) => Proxy m -> Integer+test12 = natVal++test13 :: forall m . (KnownNat (m+3)) => Proxy m -> Integer+test13 = natVal++test14 :: forall m . (KnownNat (4+m)) => Proxy (7+m) -> Integer+test14 = natVal++type family Foo (m :: Nat) = (result :: Nat) | result -> m+fakeFooEvidence :: 1 :~: Foo 1+fakeFooEvidence = unsafeCoerce Refl++test15 :: KnownNat (4 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1) -> Integer+test15 _ _ = natVal (Proxy @ (Foo 1 + 7))++test16 :: KnownNat (4 + Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1 + Foo 1) -> Integer+test16 _ _ = natVal (Proxy @ (Foo 1 + 7 + Foo 1))++test17 :: KnownNat (4 + 2 * Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + 2 * Foo 1 + Foo 1) -> Integer+test17 _ _ = natVal (Proxy @ (2 * Foo 1 + 7 + Foo 1))++data SNat :: Nat -> * where+ SNat :: KnownNat n => SNat n++instance Show (SNat n) where+ show s@SNat = show (natVal s)++addSNat :: SNat a -> SNat b -> SNat (a + b)+addSNat SNat SNat = SNat++mulSNat :: SNat a -> SNat b -> SNat (a * b)+mulSNat SNat SNat = SNat++expSNat :: SNat a -> SNat b -> SNat (a ^ b)+expSNat SNat SNat = SNat++subSNat :: (b <= a) => SNat a -> SNat b -> SNat (a - b)+subSNat SNat SNat = SNat++test18 :: SNat (a+1) -> SNat a -> SNat 1+test18 = subSNat++test19 :: SNat (a+b) -> SNat b -> SNat a+test19 = subSNat++test20 :: forall a . (KnownNat (3 * a - a)) => Proxy a -> Integer+test20 _ = natVal (Proxy @ (2 * a))+ tests :: TestTree tests = testGroup "ghc-typelits-natnormalise" [ testGroup "Basic functionality"@@ -43,12 +115,64 @@ , testCase "KnownNat 2 ^ KnownNat 7 ~ 128" $ show (test5 (Proxy @ 2) (Proxy @ 7)) @?= "128"- , testCase "KnownNat 3 ^ KnownNat 7 ~ 128" $+ , testCase "KnownNat 3 ^ KnownNat 7 ~ 2187" $ show (test5 (Proxy @ 3) (Proxy @ 7)) @?= "2187" , testCase "(KnownNat 2 ^ KnownNat 7) + (KnownNat 2 * KnownNat 7) ~ 142" $ show (test6 (Proxy @ 2) (Proxy @ 7)) @?= "142"+ , testCase "KnownNat (Max 7 5 + 1) ~ 8" $+ show (test7 (Proxy @ 7) (Proxy @ 5)) @?=+ "8"+ , testCase "KnownNat (Min 7 5 + 1) ~ 6" $+ show (test8 (Proxy @ 7) (Proxy @ 5)) @?=+ "6"+ , testCase "KnownNat (7 - 5) ~ 2" $+ show (test9 (Proxy @ 7) (Proxy @ 5)) @?=+ "2"+ ],+ testGroup "Implications"+ [ testCase "KnownNat m => KnownNat (m*m); @ 5" $+ show (test11 (Proxy @ 5)) @?=+ "25"+ , testCase "KnownNat (m+1) => KnownNat m; @ m ~ 5" $+ show (test12 (Proxy @ 5)) @?=+ "5"+ , testCase "KnownNat (m+1) => KnownNat m; @ m ~ 0" $+ show (test12 (Proxy @ 0)) @?=+ "0"+ , testCase "KnownNat (m+3) => KnownNat m; @ m ~ 0" $+ show (test13 (Proxy @ 0)) @?=+ "0"+ , testCase "KnownNat (4+m) => KnownNat (7+m); @ m ~ 1" $+ show (test14 (Proxy @ 8)) @?=+ "8"+ , testCase "KnownNat (4 + Foo 1) => KnownNat (Foo 1 + 7); @ Foo 1 ~ 1" $+ (case fakeFooEvidence of+ Refl -> show $ test15 (Proxy @ (Foo 1)) (Proxy @ (4 + Foo 1))) @?=+ "8"+ , testCase "KnownNat (4 + Foo 1 + Foo 1) => KnownNat (Foo 1 + 7 + Foo 1); @ Foo 1 ~ 1" $+ (case fakeFooEvidence of+ Refl -> show $ test16 (Proxy @ (Foo 1)) (Proxy @ (4 + Foo 1 + Foo 1))) @?=+ "9"+ , testCase "KnownNat (4 + 2 * Foo 1 + Foo 1) => KnownNat (2 * Foo 1 + 7 + Foo 1); @ Foo 1 ~ 1" $+ (case fakeFooEvidence of+ Refl -> show $ test17 (Proxy @ (Foo 1)) (Proxy @ (4 + 2 * Foo 1 + Foo 1))) @?=+ "10"+ , testCase "KnownNat (3 * a - a) => KnownNat (2 * a); @ a ~ 4" $+ show (test20 (Proxy @ 4)) @?=+ "8"+ ],+ testGroup "Normalisation"+ [ testCase "KnownNat (m-n+n) ~ KnownNat m" $+ show (test10 (Proxy @ 12) (Proxy @8)) @?=+ "12"+ , testCase "SNat (a+1) - SNat a = SNat 1" $+ show (test18 (SNat @ 11) (SNat @10)) @?=+ "1"+ , testCase "SNat (a+b) - SNat b = SNat a" $+ show (test19 (SNat @ 16) (SNat @10)) @?=+ "6" ] ]
+ tests/TestFunctions.hs view
@@ -0,0 +1,41 @@+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables,+ TypeApplications, TypeFamilies, TypeInType, TypeOperators,+ UndecidableInstances, TemplateHaskell #-}++module TestFunctions where++import Data.Proxy (Proxy (..))+import Data.Singletons (Apply, type (~>))+import Data.Type.Bool (If)+import GHC.TypeLits.KnownNat+import GHC.TypeLits++type family Max (a :: Nat) (b :: Nat) :: Nat where+ Max 0 b = b -- See [Note: single equation TFs are treated like synonyms]+ Max a b = If (a <=? b) b a++data MaxSym1 :: Nat -> Nat ~> Nat+data MaxSym2 :: Nat ~> Nat ~> Nat++type instance Apply MaxSym2 a = (MaxSym1 a)+type instance Apply (MaxSym1 a) b = Max a b++instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''Max) a b where+ type KnownNatF2 $(nameToSymbol ''Max) = MaxSym2+ natSing2 = let x = natVal (Proxy @ a)+ y = natVal (Proxy @ b)+ z = max x y+ in SNatKn z+ {-# INLINE natSing2 #-}++{- [Note: single equation TFs are treated like synonyms]+Single equation (closed) type families (TF) are treated like type synonyms, this+means that type-applications of such a TF only shows up in its expanded form.++Consequently, the KnownNat solver plugin does not have a TyCon name to look+up the corresponding instance of the KnownNat2 class.+-}++type family Min (a :: Nat) (b :: Nat) :: Nat where+ Min 0 b = 0 -- See [Note: single equation TFs are treated like synonyms]+ Min a b = If (a <=? b) a b