diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # ghc-typelits-knownnat -[![Build Status](https://secure.travis-ci.org/clash-lang/ghc-typelits-knownnat.png?branch=master)](http://travis-ci.org/clash-lang/ghc-typelits-knownnat) +[![Build Status](https://secure.travis-ci.org/clash-lang/ghc-typelits-knownnat.svg?branch=master)](http://travis-ci.org/clash-lang/ghc-typelits-knownnat) [![Hackage](https://img.shields.io/hackage/v/ghc-typelits-knownnat.svg)](https://hackage.haskell.org/package/ghc-typelits-knownnat) [![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-knownnat.svg?style=flat)](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` 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 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.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\@ 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 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 @@ -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 #-} 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 @@ -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\@ 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\@ 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 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 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 diff --git a/src/GHC/TypeLits/KnownNat/TH.hs b/src/GHC/TypeLits/KnownNat/TH.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits/KnownNat/TH.hs @@ -0,0 +1,16 @@ +{-| +Copyright : (C) 2016, University of Twente +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij +-} + +{-# 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 diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -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" ] ] diff --git a/tests/TestFunctions.hs b/tests/TestFunctions.hs new file mode 100644 --- /dev/null +++ b/tests/TestFunctions.hs @@ -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