ghc-typelits-knownnat 0.2.4 → 0.8.4
raw patch · 9 files changed
Files
- CHANGELOG.md +84/−0
- LICENSE +3/−3
- README.md +3/−6
- ghc-typelits-knownnat.cabal +78/−36
- src/GHC/TypeLits/KnownNat.hs +142/−31
- src/GHC/TypeLits/KnownNat/Compat.hs +160/−0
- src/GHC/TypeLits/KnownNat/Solver.hs +478/−215
- tests/Main.hs +165/−70
- tests/TestFunctions.hs +19/−12
CHANGELOG.md view
@@ -1,5 +1,89 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.8.4 *May 13th 2026*+* Bump ghc-tcplugin-api to prepare for inclusion into stackage++## 0.8.3 *March 20th 2026*+* Unfix -fdefer-type-errors regression as it caused more regressions++## 0.8.2 *October 17th 2025*+* Fix -fdefer-type-errors regression++## 0.8.1 *October 10th 2025*+* Fix [#53](https://github.com/clash-lang/ghc-typelits-knownnat/issues/53) The plugin sometimes doesn't look through type aliases+* Fix [#13](https://github.com/clash-lang/ghc-typelits-knownnat/issues/13) Type equality constraints aren't used by solver+* Fix [#42](https://github.com/clash-lang/ghc-typelits-knownnat/issues/42) Intermediate type variable stops derivation of `KnownNat` constraint++## 0.8.0 *September 8th 2025*+* Support for GHC 9.14.1.+* Drop support for GHC 8.0, 8.2, 8.4, 8.6.++## 0.7.13 *March 4th 2025*+* Support for GHC 9.12.1++## 0.7.12 *May 22nd, 2024*+* Support for GHC 9.10.1++## 0.7.11+* Fix infinite loop between plugin and solver pipeline++## 0.7.10 *November 14th 2023*+* Work around [GHC issue 23109](https://gitlab.haskell.org/ghc/ghc/-/issues/23109)++## 0.7.9 *October 10th 2023*+* Support for GHC 9.8.1++## 0.7.8 *February 20th 2023*+* Support for GHC-9.6.0.20230210++## 0.7.7 *October 10th 2022*+* Add support for GHC 9.4++## 0.7.6 *June 18th 2021*+* Add support for GHC 9.2.0.20210422++## 0.7.5 *February 10th 2021*+* Raise upper limit for TH dep to allow building on ghc-9.0.1++## 0.7.4 *January 1st 2021*+* Add support for GHC 9.0.1-rc1++## 0.7.3 *July 25th 2020*+* Fix https://github.com/clash-lang/clash-compiler/issues/1454++## 0.7.2 *February 6th 2020*+ * Add support for GHC 8.10.0-alpha2++## 0.7.1 *October 8th 2019*+* Fix [#29](https://github.com/clash-lang/ghc-typelits-knownnat/issues/29)+* Fix [#30](https://github.com/clash-lang/ghc-typelits-knownnat/issues/30)++## 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`++## 0.5 *May 9th 2018*+* Fix Inferred constraint is too strong [#19](https://github.com/clash-lang/ghc-typelits-knownnat/issues/19)++## 0.4.2 *April 15th 2018*+* Add support for GHC 8.5.20180306++## 0.4.1 *March 17th, 2018*+* Add support for GHC 8.4.1++## 0.4 *January 4th, 2018*+* Add partial GHC 8.4.1-alpha1 support+* Drop `singletons` dependency [#15](https://github.com/clash-lang/ghc-typelits-knownnat/issues/15)+ * `KnownNatN` classes no longer have the `KnownNatFN` associated type family++## 0.3.1 *August 17th 2017*+* Fix testsuite for GHC 8.2.1++## 0.3 *May 15th 2017*+* GHC 8.2.1 support: Underlying representation for `KnownNat` in GHC 8.2 is `Natural`, meaning users of this plugin will need to update their code to use `Natural` for GHC 8.2 as well.+ ## 0.2.4 *April 10th 2017* * New features: * Derive constraints for unary functions via a `KnownNat1` instance; thanks to @nshepperd [#11](https://github.com/clash-lang/ghc-typelits-knownnat/pull/11)
LICENSE view
@@ -1,6 +1,6 @@-Copyright (c) 2015-2016, University of Twente,- 2017, QBayLogic,- 2017, Google Inc.+Copyright (c) 2016 , University of Twente,+ 2017-2018, QBayLogic B.V.,+ 2017 , Google Inc. All rights reserved. Redistribution and use in source and binary forms, with or without
README.md view
@@ -1,6 +1,6 @@ # ghc-typelits-knownnat -[](http://travis-ci.org/clash-lang/ghc-typelits-knownnat)+[](https://github.com/clash-lang/ghc-typelits-knownnat/actions) [](https://hackage.haskell.org/package/ghc-typelits-knownnat) [](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-knownnat) @@ -52,17 +52,14 @@ type family Max (a :: Nat) (b :: Nat) :: Nat where Max 0 b = b Max a b = If (a <=? b) b a--$(genDefunSymbols [''Max]) -- creates the 'MaxSym0' symbol ``` and corresponding `KnownNat2` instance: ```haskell instance (KnownNat a, KnownNat b) => KnownNat2 "TestFunctions.Max" a b where- type KnownNatF2 "TestFunctions.Max" = MaxSym0- natSing2 = let x = natVal (Proxy @ a)- y = natVal (Proxy @ b)+ natSing2 = let x = natVal (Proxy @a)+ y = natVal (Proxy @b) z = max x y in SNatKn z {-# INLINE natSing2 #-}
ghc-typelits-knownnat.cabal view
@@ -1,56 +1,61 @@+cabal-version: 3.0 name: ghc-typelits-knownnat-version: 0.2.4+version: 0.8.4 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@ constraints from other simple/variable @KnownNat@ constraints. i.e. without this plugin, you must have both a @KnownNat n@ and a @KnownNat (n+2)@ constraint in the type signature of the following function:- .+ @ 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:- .+ @ f :: forall n . KnownNat n => Proxy n -> Integer f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) @- .+ The plugin can derive @KnownNat@ constraints for types consisting of:- .+ * Type variables, when there is a corresponding @KnownNat@ constraint- .+ * Type-level naturals- .+ * Applications of the arithmetic expression: +,-,*,^- .+ * Type functions, when there is either:- .+ 1. a matching given @KnownNat@ constraint; or- .+ 2. a corresponding @KnownNat\<N\>@ instance for the type function- .+ To use the plugin, add the- .+ @ OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver @- .+ Pragma to the header of your file. homepage: http://clash-lang.org/-license: BSD2+license: BSD-2-Clause license-file: LICENSE author: Christiaan Baaij maintainer: christiaan.baaij@gmail.com-copyright: Copyright © 2016, University of Twente, 2017 QBayLogic+copyright: Copyright © 2016 , University of Twente,+ 2017-2018, QBayLogic B.V.,+ 2017 , Google Inc. category: Type System build-type: Simple-extra-source-files: README.md+extra-doc-files: README.md CHANGELOG.md-cabal-version: >=1.10+tested-with: GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,+ GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1,+ GHC == 9.12.1 source-repository head type: git@@ -63,9 +68,10 @@ manual: True library- exposed-modules: GHC.TypeLits.KnownNat,+ exposed-modules: GHC.TypeLits.KnownNat GHC.TypeLits.KnownNat.Solver- other-modules: GHC.TypeLits.KnownNat.TH+ other-modules: GHC.TypeLits.KnownNat.Compat+ GHC.TypeLits.KnownNat.TH other-extensions: AllowAmbiguousTypes DataKinds FlexibleInstances@@ -81,31 +87,67 @@ 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.2 && <0.6,- singletons >= 2.2 && <3.0,- transformers >= 0.5.2.0 && <0.6,- template-haskell >= 2.11.0.0 && <2.13+ build-depends: base >= 4.9 && <5,+ ghc >= 8.0.1 && <9.17,+ ghc-tcplugin-api >= 0.19 && <0.20,+ ghc-typelits-natnormalise >= 0.9.0 && <0.10,+ transformers >= 0.5.2.0 && <0.7,+ template-haskell >= 2.11.0.0 && <2.26 hs-source-dirs: src default-language: Haskell2010+ ghc-options: -Wall -Wno-unticked-promoted-constructors if flag(deverror)- ghc-options: -Wall -Werror+ ghc-options: -Werror++ if impl(ghc >= 9.0.0)+ build-depends: ghc-bignum >=1.0 && <1.6 else- ghc-options: -Wall+ build-depends: integer-gmp >=1.0 && <1.1+ mixins:+ ghc+ ( TcTypeNats as GHC.Builtin.Types.Literals+ , CoreSyn as GHC.Core+ , Class as GHC.Core.Class+ , Coercion as GHC.Core.Coercion+ , DataCon as GHC.Core.DataCon+ , InstEnv as GHC.Core.InstEnv+ , TyCoRep as GHC.Core.TyCo.Rep+ , Type as GHC.Core.Type+ , CoreUtils as GHC.Core.Utils+ , Pair as GHC.Data.Pair+ , Plugins as GHC.Driver.Plugins+ , TcEvidence as GHC.Tc.Types.Evidence+ , Id as GHC.Types.Id+ , Name as GHC.Types.Name+ , OccName as GHC.Types.Name.Occurrence+ , Var as GHC.Types.Var+ , Module as GHC.Unit.Module+ ) -test-suite test-ghc-typelits-knownnat+ if impl(ghc >= 8.9)+ mixins:+ ghc+ ( Predicate as GHC.Core.Predicate+ , TyCoSubst as GHC.Core.TyCo.Subst+ )+ else+ mixins:+ ghc+ ( Type as GHC.Core.Predicate+ , Type as GHC.Core.TyCo.Subst+ )++test-suite unittests type: exitcode-stdio-1.0 main-is: Main.hs 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,+ ghc-typelits-knownnat,+ ghc-typelits-natnormalise >= 0.8.0 && <0.10, tasty >= 0.10, tasty-hunit >= 0.9,- tasty-quickcheck >= 0.8+ tasty-quickcheck >= 0.8,+ QuickCheck >= 2.10 hs-source-dirs: tests default-language: Haskell2010 other-extensions: DataKinds@@ -114,7 +156,7 @@ GADTs MultiParamTypeClasses KindSignatures- ScopedTypeVariables,+ ScopedTypeVariables TemplateHaskell TypeApplications TypeFamilies@@ -122,4 +164,4 @@ TypeOperators UndecidableInstances if flag(deverror)- ghc-options: -O0 -dcore-lint+ ghc-options: -dcore-lint
src/GHC/TypeLits/KnownNat.hs view
@@ -1,5 +1,7 @@ {-|-Copyright : (C) 2016, University of Twente+Copyright : (C) 2016 , University of Twente,+ 2017-2018, QBayLogic B.V.,+ 2017 , Google Inc. License : BSD2 (see the file LICENSE) Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> @@ -30,13 +32,9 @@ UndecidableInstances \#-\} import Data.Proxy (Proxy (..))-import Data.Singletons.TH (genDefunSymbols) import GHC.TypeLits.KnownNat -$(genDefunSymbols [''Max]) -- creates the \'MaxSym0\' symbol- instance (KnownNat a, KnownNat b) => 'KnownNat2' $('nameToSymbol' ''Max) a b where- type 'KnownNatF2' $('nameToSymbol' ''Max) = MaxSym0 natSing2 = let x = natVal (Proxy @a) y = natVal (Proxy @b) z = max x y@@ -84,17 +82,23 @@ @ -} +{-# LANGUAGE CPP #-}+ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BangPatterns #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE Trustworthy #-}@@ -109,31 +113,61 @@ , KnownNat1 (..) , KnownNat2 (..) , KnownNat3 (..)+ -- * Singleton boolean+ , SBool (..)+ , boolVal+ -- * KnownBool+ , KnownBool (..)+ -- ** Constraint-level boolean functions+ , SBoolKb (..)+ , KnownNat2Bool (..)+ , KnownBoolNat2 (..) -- * Template Haskell helper , nameToSymbol ) where -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 (:-$))+-- base+import Data.Proxy+ ( Proxy (..) )+import Data.Type.Bool+ ( If )+import GHC.Exts+ ( Proxy# )+import GHC.TypeLits+ ( Symbol )+import GHC.TypeNats+ ( KnownNat, Nat+ , type (+), type (*), type (^), type (-), type (<=?), type (<=)+ , type Mod, type Div+ , natVal+ )+import Numeric.Natural+ ( Natural )+#if MIN_VERSION_ghc(9,1,0)+import Data.Type.Ord+ ( OrdCond )+#endif +-- ghc+import GHC.Natural+ ( shiftLNatural )++-- ghc-typelits-knownnat import GHC.TypeLits.KnownNat.TH --- | Singleton natural number (represented by an integer)-newtype SNatKn (n :: Nat) = SNatKn Integer+-------------------------------------------------------------------------------- +-- | Singleton natural number+newtype SNatKn (f :: Symbol) = SNatKn Natural+ -- | Class for arithmetic functions with /one/ argument. -- -- 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 KnownNat1 (f :: Symbol) (a :: Nat) where- type KnownNatF1 f :: Nat ~> Nat- natSing1 :: SNatKn (KnownNatF1 f @@ a)+ natSing1 :: SNatKn f -- | Class for arithmetic functions with /two/ arguments. --@@ -141,8 +175,7 @@ -- 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)+ natSing2 :: SNatKn f -- | Class for arithmetic functions with /three/ arguments. --@@ -150,34 +183,112 @@ -- 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)+ natSing3 :: SNatKn f -- | '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 #-}+ {-# NOINLINE natSing2 #-} -- | '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 #-}+ {-# NOINLINE natSing2 #-} -- | '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)+ natSing2 = let x = natVal (Proxy @a)+ y = natVal (Proxy @b) z = case x of- 2 -> shiftL 1 (fromInteger y)+ 2 -> shiftLNatural 1 (fromIntegral y) _ -> x ^ y in SNatKn z- {-# INLINE natSing2 #-}+ {-# NOINLINE natSing2 #-} -- | '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 #-}+ {-# NOINLINE natSing2 #-}++instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x y where+ natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y)))+ {-# NOINLINE natSing2 #-}++instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x y where+ natSing2 = SNatKn (rem (natVal (Proxy @x)) (natVal (Proxy @y)))+ {-# NOINLINE natSing2 #-}++-- | 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))+ {-# NOINLINE boolNatSing2 #-}++#if MIN_VERSION_ghc(9,1,0)+instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''OrdCond) a b where+ boolNatSing2 = SBoolKb (natVal (Proxy @a) <= natVal (Proxy @b))+ {-# NOINLINE boolNatSing2 #-}+#endif++-- | 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))+ {-# NOINLINE natBoolSing3 #-}
+ src/GHC/TypeLits/KnownNat/Compat.hs view
@@ -0,0 +1,160 @@+{-# LANGUAGE CPP #-}++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TemplateHaskellQuotes #-}++module GHC.TypeLits.KnownNat.Compat+ ( KnownNatDefs(..), lookupKnownNatDefs+ , mkNaturalExpr++ , coercionRKind, classMethodTy+ , irrelevantMult+ )+ where++-- base+import Data.Type.Bool+ ( If )+#if MIN_VERSION_ghc(9,1,0)+import Data.Type.Ord+ ( OrdCond )+#else+import GHC.TypeNats+ ( type (<=) )+#endif+++-- ghc-tcplugin-api+import GHC.TcPlugin.API+#if MIN_VERSION_ghc(9,3,0)+import GHC.TcPlugin.API.Internal ( unsafeLiftTcM )+#endif++-- ghc+import qualified GHC.Core.Make as GHC+ ( mkNaturalExpr )+#if MIN_VERSION_ghc(9,3,0)+import GHC.Tc.Utils.Monad+ ( getPlatform )+#endif+#if MIN_VERSION_ghc(8,11,0)+import GHC.Core.Coercion+ ( coercionRKind )+import GHC.Core.Predicate+ ( classMethodTy )+import GHC.Core.Type+ ( irrelevantMult )+#else+import GHC.Core.Coercion+ ( coercionKind )+import GHC.Core.Type+ ( dropForAlls, funResultTy, varType )+import GHC.Data.Pair+ ( Pair(..) )+#endif++-- ghc-typelits-knownnat+import GHC.TypeLits.KnownNat+ ( KnownNat1, KnownNat2, KnownNat3+ , KnownBool, KnownBoolNat2, KnownNat2Bool+ )++-- template-haskell+import qualified Language.Haskell.TH as TH+ ( Name )++--------------------------------------------------------------------------------++-- | Classes and instances from "GHC.TypeLits.KnownNat"+data KnownNatDefs+ = KnownNatDefs+ { knownBool :: Class+ , knownBoolNat2 :: Class+ , knownNat2Bool :: Class+ , knownNatN :: Int -> Maybe Class -- ^ KnownNat{N}+#if MIN_VERSION_ghc(9,1,0)+ , ordCondTyCon :: TyCon+#else+ -- | @<= :: Nat -> Nat -> Constraint@+ , leqNatTyCon :: TyCon+#endif+ , ifTyCon :: TyCon+ }++-- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat"+lookupKnownNatDefs :: TcPluginM Init KnownNatDefs+lookupKnownNatDefs = do+ kbC <- look ''KnownBool+ kbn2C <- look ''KnownBoolNat2+ kn2bC <- look ''KnownNat2Bool+ kn1C <- look ''KnownNat1+ kn2C <- look ''KnownNat2+ kn3C <- look ''KnownNat3+#if MIN_VERSION_ghc(9,1,0)+ ordcond <- lookupTHName ''OrdCond >>= tcLookupTyCon+#else+ leq <- lookupTHName ''(<=) >>= tcLookupTyCon+#endif+ ifTc <- lookupTHName ''If >>= tcLookupTyCon+ return KnownNatDefs+ { knownBool = kbC+ , knownBoolNat2 = kbn2C+ , knownNat2Bool = kn2bC+ , knownNatN = \case { 1 -> Just kn1C+ ; 2 -> Just kn2C+ ; 3 -> Just kn3C+ ; _ -> Nothing+ }+#if MIN_VERSION_ghc(9,1,0)+ , ordCondTyCon = ordcond+#else+ , leqNatTyCon = leq+#endif+ , ifTyCon = ifTc+ }+ where+ look :: TH.Name -> TcPluginM Init Class+ look nm = lookupTHName nm >>= tcLookupClass++--------------------------------------------------------------------------------++mkNaturalExpr :: Integer -> TcPluginM Solve CoreExpr+mkNaturalExpr i = do+#if MIN_VERSION_ghc(9,3,0)+ platform <- unsafeLiftTcM getPlatform+ return $ GHC.mkNaturalExpr platform i+#elif MIN_VERSION_ghc(8,11,0)+ return $ GHC.mkNaturalExpr i+#else+ GHC.mkNaturalExpr i+#endif++--------------------------------------------------------------------------------++#if !MIN_VERSION_ghc(8,11,0)+coercionRKind :: Coercion -> Type+coercionRKind co = rhs+ where+ Pair _ rhs = coercionKind co+#endif++--------------------------------------------------------------------------------++#if !MIN_VERSION_ghc(8,11,0)+classMethodTy :: Id -> Type+classMethodTy sel_id+ = funResultTy $ -- meth_ty+ dropForAlls $ -- C a => meth_ty+ varType sel_id -- forall a. C n => meth_ty+#endif++--------------------------------------------------------------------------------++#if !MIN_VERSION_ghc(8,11,0)+irrelevantMult :: a -> a+irrelevantMult = id+#endif++--------------------------------------------------------------------------------
src/GHC/TypeLits/KnownNat/Solver.hs view
@@ -1,5 +1,7 @@ {-|-Copyright : (C) 2016, University of Twente+Copyright : (C) 2016 , University of Twente,+ 2017-2018, QBayLogic B.V.,+ 2017 , Google Inc. License : BSD2 (see the file LICENSE) Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> @@ -51,17 +53,14 @@ type family Max (a :: Nat) (b :: Nat) :: Nat where Max 0 b = b Max a b = If (a <=? b) b a--$(genDefunSymbols [''Max]) -- creates the 'MaxSym0' symbol @ and corresponding @KnownNat2@ instance: @ instance (KnownNat a, KnownNat b) => KnownNat2 \"TestFunctions.Max\" a b where- type KnownNatF2 \"TestFunctions.Max\" = MaxSym0- natSing2 = let x = natVal (Proxy @ a)- y = natVal (Proxy @ b)+ natSing2 = let x = natVal (Proxy @a)+ y = natVal (Proxy @b) z = max x y in SNatKn z \{\-# INLINE natSing2 \#-\}@@ -85,57 +84,115 @@ -} +{-# LANGUAGE CPP #-}++{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE TemplateHaskellQuotes #-} {-# LANGUAGE Trustworthy #-} {-# OPTIONS_HADDOCK show-extensions #-} -module GHC.TypeLits.KnownNat.Solver (plugin) where+module GHC.TypeLits.KnownNat.Solver+ ( plugin )+where --- external-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)+-- base+import Control.Arrow+ ( (&&&), first )+import Data.Foldable+ ( asum )+import Data.List.NonEmpty as NE+ ( filter )+import Data.Maybe+ ( catMaybes, fromMaybe, mapMaybe ) --- GHC API-import Class (Class, classMethods, className, classTyCon)-import FamInst (tcInstNewTyCon_maybe)-import FastString (fsLit)-import Id (idType)-import InstEnv (instanceDFunId,lookupUniqueInstEnv)-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 TcPluginM (TcPluginM, tcLookupClass, getInstEnvs, zonkCt)-import TcRnTypes (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvLoc,- ctEvPred, ctEvTerm, ctLoc, ctLocSpan, isWanted,- mkNonCanonical, setCtLoc, setCtLocSpan)-import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon)-import Type- (EqRel (NomEq), PredTree (ClassPred,EqPred), PredType, classifyPredType,- dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,- piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe)-import TyCon (tyConName)-import TyCoRep (Type (..), TyLit (..))-import Var (DFunId)+-- transformers+import Control.Monad.Trans.Maybe+ ( MaybeT (..) )+import Control.Monad.Trans.Writer.Strict --- | Classes and instances from "GHC.TypeLits.KnownNat"-type KnownNatDefs = Int -> Maybe Class -- ^ KnownNatN class+-- ghc-typelits-natnormalise+import GHC.TypeLits.Normalise.SOP+ ( SOP (..), Product (..), Symbol (..) )+import GHC.TypeLits.Normalise.Unify+ ( CType (..),normaliseNat, reifySOP ) +-- ghc-tcplugin-api+import GHC.TcPlugin.API+import GHC.TcPlugin.API.TyConSubst++-- ghc-typelits-knownnat+import GHC.TypeLits.KnownNat.Compat+ ( KnownNatDefs(..), lookupKnownNatDefs, mkNaturalExpr+ , coercionRKind, classMethodTy+ , irrelevantMult+ )++-- ghc+import GHC.Builtin.Names+ ( knownNatClassName )+#if MIN_VERSION_ghc(9,1,0)+import GHC.Builtin.Types+ ( promotedFalseDataCon, promotedTrueDataCon )+import GHC.Builtin.Types.Literals+ ( typeNatCmpTyCon )+#endif+import GHC.Builtin.Types.Literals+ ( typeNatAddTyCon, typeNatDivTyCon, typeNatSubTyCon )+import GHC.Core+ ( mkApps, mkTyApps )+import GHC.Core.Class+ ( classMethods, classTyVars )+import GHC.Core.Coercion+ ( instNewTyCon_maybe, mkNomReflCo, mkTyConAppCo )+import GHC.Core.DataCon+ ( dataConWrapId )+import GHC.Core.InstEnv+ ( instanceDFunId, lookupUniqueInstEnv )+import GHC.Core.TyCo.Rep+ ( Type(..), TyLit(..) )+import GHC.Core.TyCo.Subst+ ( substTyWithUnchecked )+import GHC.Core.Type+ ( coreView, piResultTys, splitFunTys )+import GHC.Core.Utils+ ( exprType, mkCast )+import GHC.Driver.Plugins+ ( Plugin (..), defaultPlugin, purePlugin )+import GHC.Plugins+ ( HasDebugCallStack )+import GHC.Tc.Types.Evidence+ ( evTermCoercion_maybe, evSelector )+import GHC.Types.Id+ ( idType )+import GHC.Types.Name+ ( nameModule_maybe, nameOccName )+import GHC.Types.Name.Occurrence+ ( occNameString )+import GHC.Types.Var+ ( DFunId )+import GHC.Unit.Module+ ( moduleName, moduleNameString )+import GHC.Utils.Outputable+ ( (<+>), vcat, text )++--------------------------------------------------------------------------------++-- | Simple newtype wrapper to distinguish the original (flattened) argument of+-- knownnat from the un-flattened version that we work with internally.+newtype Orig a = Orig { unOrig :: a }+ -- | KnownNat constraints type KnConstraint = (Ct -- The constraint ,Class -- KnownNat class ,Type -- The argument to KnownNat+ ,Orig Type -- Original, flattened, argument to KnownNat ) {-|@@ -221,156 +278,222 @@ -} plugin :: Plugin-plugin = defaultPlugin { tcPlugin = const $ Just normalisePlugin }+plugin+ = defaultPlugin+ { tcPlugin = \ _ -> Just $ mkTcPlugin normalisePlugin+ , pluginRecompile = purePlugin+ } normalisePlugin :: TcPlugin-normalisePlugin = tracePlugin "ghc-typelits-knownnat"- TcPlugin { tcPluginInit = lookupKnownNatDefs- , tcPluginSolve = solveKnownNat- , tcPluginStop = const (return ())+normalisePlugin =+ TcPlugin { tcPluginInit = lookupKnownNatDefs+ , tcPluginSolve = solveKnownNat+ , tcPluginRewrite = const emptyUFM+ , tcPluginPostTc = const (return ())+ , tcPluginShutdown = const (return ()) } -solveKnownNat :: KnownNatDefs -> [Ct] -> [Ct] -> [Ct]- -> TcPluginM TcPluginResult-solveKnownNat _defs _givens _deriveds [] = return (TcPluginOk [] [])-solveKnownNat defs givens _deriveds wanteds = do- -- GHC 7.10 puts deriveds with the wanteds, so filter them out- let wanteds' = filter (isWanted . ctEvidence) wanteds- kn_wanteds = mapMaybe toKnConstraint wanteds'+solveKnownNat :: KnownNatDefs -> [Ct] -> [Ct]+ -> TcPluginM Solve TcPluginSolveResult+solveKnownNat _defs _givens [] = return (TcPluginOk [] [])+solveKnownNat defs givens wanteds = do+ let givensTyConSubst = mkTyConSubst givens+ kn_wanteds = map (\(x,y,z,orig) -> (x,y,z,orig))+ $ mapMaybe (toKnConstraint defs) wanteds case kn_wanteds of [] -> return (TcPluginOk [] []) _ -> do -- Make a lookup table for all the [G]iven constraints- given_map <- mapM (fmap toGivenEntry . zonkCt) givens+ let given_map = map toGivenEntry givens+ -- Try to solve the wanted KnownNat constraints given the [G]iven -- KnownNat constraints- (solved,new) <- (unzip . catMaybes) <$> (mapM (constraintToEvTerm defs given_map) kn_wanteds)+ (solved,new) <- (unzip . catMaybes) <$> (mapM (constraintToEvTerm defs givensTyConSubst 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+toKnConstraint :: KnownNatDefs -> Ct -> Maybe KnConstraint+toKnConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of ClassPred cls [ty]- | className cls == knownNatClassName- -> Just (ct,cls,ty)+ | className cls == knownNatClassName ||+ className cls == className (knownBool defs)+ -> Just (ct,cls,ty,Orig ty) _ -> Nothing -- | Create a look-up entry for a [G]iven constraint.-toGivenEntry :: Ct -> (CType,EvTerm)+toGivenEntry :: Ct -> (CType,EvExpr) toGivenEntry ct = let ct_ev = ctEvidence ct c_ty = ctEvPred ct_ev- ev = ctEvTerm ct_ev+ ev = ctEvExpr ct_ev in (CType c_ty,ev) --- | 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- kn1C <- look md "KnownNat1"- kn2C <- look md "KnownNat2"- kn3C <- look md "KnownNat3"- return $ (\case { 1 -> Just kn1C- ; 2 -> Just kn2C- ; 3 -> Just kn3C- ; _ -> Nothing- })- where- look md s = do- nm <- lookupName md (mkTcOcc s)- tcLookupClass nm-- myModule = mkModuleName "GHC.TypeLits.KnownNat"- myPackage = fsLit "ghc-typelits-knownnat"- -- | Try to create evidence for a wanted constraint-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+constraintToEvTerm+ :: KnownNatDefs+ -- ^ The "magic" KnownNatN classes+ -> TyConSubst+ -> [(CType,EvExpr)]+ -- ^ All the [G]iven constraints+ -> KnConstraint+ -> TcPluginM Solve (Maybe ((EvTerm,Ct),[Ct]))+constraintToEvTerm defs givensTyConSubst givens (ct,cls,op,orig) = do+ -- 1. Determine if we are an offset apart from a [G]iven constraint+ offsetM <- offset op 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)+ _ -> go [] (op,Nothing)+ return ((first (,ct)) <$> evM) where -- 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)+ go :: [Coercion] -> (Type, Maybe Coercion) -> TcPluginM Solve (Maybe (EvTerm,[Ct]))+ -- Look through type aliases+ go deps (coreView -> Just tyN, coM) = go deps (tyN, coM)+ -- Look through rewrites+ go deps0 (ty, coM)+ | Just tcapps <- splitTyConApp_upTo givensTyConSubst ty+ -- We are only interested in the splitTyConApp_upTo result that used a+ -- rewrite+ , withDeps@(_:_) <- NE.filter (\(_,_,deps) -> not (null deps)) tcapps+ = do results <- traverse (\(tc, args, deps1) -> go (deps0 <> deps1)+ (TyConApp tc args, coM))+ withDeps+ return (asum results)+ -- See whether there is a given that matches it (after having looked through+ -- type aliases and rewrites)+ go deps (go_other deps -> Just ev, _) = return (Just (ev,[]))+ -- And if there isn't, see whether we can construct it using a KnownNat<N>+ -- instance+ go deps (ty@(TyConApp tc args0), sM) | 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 (LitTy (NumTyLit i))+ = do+ ienv <- getInstEnvs+ let mS = moduleNameString (moduleName m)+ tcS = occNameString (nameOccName tcNm)+ fn0 = mS ++ "." ++ tcS+ fn1 = mkStrLitTy (fsLit fn0)+ args1 = fn1:args0+ instM =+ if | Just knN_cls <- knownNatN defs (length args0)+ , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1+ -> Just (inst,knN_cls,args0,args1)+ -- TODO: we should re-use the parsing functionality+ -- that is in GHC.TypeLits.NatNormalise.Compat.+#if MIN_VERSION_ghc(9,1,0)+ | tc == ordCondTyCon defs+ , [_,cmpNat,TyConApp t1 [],TyConApp t2 [],TyConApp f1 []] <- args0+ , TyConApp cmpNatTc args2@(arg2:_) <- cmpNat+ , cmpNatTc == typeNatCmpTyCon+ , t1 == promotedTrueDataCon+ , t2 == promotedTrueDataCon+ , f1 == promotedFalseDataCon+ , let knN_cls = knownBoolNat2 defs+ ki = typeKind arg2+ args1N = ki:fn1:args2+ , Right (inst,_) <- lookupUniqueInstEnv ienv knN_cls args1N+ -> Just (inst,knN_cls,args2,args1N)+#endif+ | [arg0,_] <- args0+ , let knN_cls = knownBoolNat2 defs+ ki = typeKind arg0+ args1N = ki:args1+ , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N+ -> Just (inst,knN_cls,args0,args1N)+ | (arg0:args0Rest@[_,_,_]) <- args0+ , tc == ifTyCon defs+ , let args1N = arg0:fn1:args0Rest+ knN_cls = knownNat2Bool defs+ , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N+ -> Just (inst,knN_cls,args0Rest,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 . irrelevantMult) df_args+ if className cls == className (knownBool defs)+ -- Create evidence using the original, flattened, argument of+ -- the KnownNat we're trying to solve. Not doing this results in+ -- GHC panics for:+ -- https://gist.github.com/christiaanb/0d204fe19f89b28f1f8d24feb63f1e63+ --+ -- That's because the flattened KnownNat we're asked to solve is+ -- [W] KnownNat fsk+ -- given:+ -- [G] fsk ~ CLog 2 n + 1+ -- [G] fsk2 ~ n+ -- [G] fsk2 ~ n + m+ --+ -- Our flattening picks one of the solution, so we try to solve+ -- [W] KnownNat (CLog 2 n + 1)+ --+ -- Turns out, GHC wanted us to solve:+ -- [W] KnownNat (CLog 2 (n + m) + 1)+ --+ -- But we have no way of knowing this! Solving the "wrong" expansion+ -- of 'fsk' results in:+ --+ -- ghc: panic! (the 'impossible' happened)+ -- (GHC version 8.6.5 for x86_64-unknown-linux):+ -- buildKindCoercion+ -- CLog 2 (n_a681K + m_a681L)+ -- CLog 2 n_a681K+ -- n_a681K + m_a681L+ -- n_a681K+ --+ -- down the line.+ --+ -- So while the "shape" of the KnownNat evidence that we return+ -- follows 'CLog 2 n + 1', the type of the evidence will be+ -- 'KnownNat fsk'; the one GHC originally asked us to solve.+ then return ((,concat new) <$> makeOpDictByFiat df cls args1N args0N (unOrig orig) deps evs)+ else return ((,concat new) <$> makeOpDict df cls args1N args0N (unOrig orig) deps evs (fmap (ty,) sM))+ _ -> return ((,[]) <$> go_other deps ty)++ go deps ((LitTy (NumTyLit i)), _) -- Let GHC solve simple Literal constraints | LitTy _ <- op = return Nothing -- This plugin only solves Literal KnownNat's that needed to be normalised -- first | otherwise- = return ((,[]) <$> makeLitDict cls op i)- go _ = return Nothing+ = (fmap (,[])) <$> makeLitDict cls op deps i+ 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 :: PredType -> TcPluginM Solve (EvExpr,[Ct]) go_arg ty = case lookup (CType ty) givens of Just ev -> return (ev,[]) _ -> do- -- Create a new wanted constraint- wantedCtEv <- newWanted (ctLoc ct) ty- let ev = ctEvTerm wantedCtEv- wanted = mkNonCanonical wantedCtEv- -- Set the source-location of the new wanted constraint to the source- -- location of the [W]anted constraint we are currently trying to solve- let ct_ls = ctLocSpan (ctLoc ct)- ctl = ctEvLoc wantedCtEv- wanted' = setCtLoc wanted (setCtLocSpan ctl ct_ls)- return (ev,[wanted'])+ (ev,wanted) <- makeWantedEv ct ty+ return (ev,[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 =+ go_other :: [Coercion] -> Type -> Maybe EvTerm+ go_other deps ty = let knClsTc = classTyCon cls kn = mkTyConApp knClsTc [ty] cast = if CType ty == CType op- then Just- else makeKnCoercion cls ty op+ then Just . EvExpr+ else makeKnCoercion cls ty op deps 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 :: Type -> TcPluginM Solve (Maybe (EvTerm,[Ct]))+ offset LitTy{} = pure Nothing offset want = runMaybeT $ do let -- Get the knownnat contraints unKn ty' = case classifyPredType ty' of@@ -379,37 +502,105 @@ -> Just ty'' _ -> Nothing -- Get the rewrites- unEq ty' = case classifyPredType ty' of- EqPred NomEq ty1 ty2 -> Just (ty1,ty2)- _ -> Nothing- rewrites = mapMaybe (unEq . unCType . fst) givens+ unEq (ty',ev) = case classifyPredType ty' of+ EqPred NomEq ty1 ty2 -> Just (ty1,ty2,ev)+ _ -> Nothing+ rewrites :: [(Type,Type,EvExpr)]+ rewrites = mapMaybe (unEq . first unCType) givens -- Rewrite- rewriteTy tyK (ty1,ty2) | ty1 `eqType` tyK = Just ty2- | ty2 `eqType` tyK = Just ty1- | otherwise = Nothing+ rewriteTy tyK (ty1,ty2,ev)+ | ty1 `eqType` tyK+ = Just (ty2,Just (tyK,evTermCoercion_maybe (EvExpr ev)))+ | ty2 `eqType` tyK+ = Just (ty1,Just (tyK,fmap mkSymCo (evTermCoercion_maybe (EvExpr ev))))+ | otherwise+ = Nothing -- Get only the [G]iven KnownNat constraints knowns = mapMaybe (unKn . unCType . fst) givens -- Get all the rewritten KNs knownsR = catMaybes $ concatMap (\t -> map (rewriteTy t) rewrites) knowns+ knownsX :: [(Type, Maybe (Type, Maybe Coercion))]+ knownsX = fmap (,Nothing) knowns ++ knownsR -- pair up the sum-of-products KnownNat constraints -- with the original Nat operation subWant = mkTyConApp typeNatSubTyCon . (:[want])- exploded = map (normaliseNat . subWant &&& id) (knowns ++ knownsR)+ -- exploded :: [()]+ exploded = map (fst . runWriter . normaliseNat . subWant . fst &&& id)+ knownsX -- interesting cases for us are those where -- wanted and given only differ by a constant- examineDiff (S [P [I n]]) entire = Just (entire,I n)- examineDiff (S [P [V v]]) entire = Just (entire,V v)+ examineDiff ((S [P [I n]]),deps) entire = Just (entire,I n,deps)+ examineDiff ((S [P [V v]]),deps) entire = Just (entire,V v,deps) examineDiff _ _ = Nothing interesting = mapMaybe (uncurry examineDiff) exploded -- convert the first suitable evidence- ((h,corr):_) <- pure interesting- let x = case corr of- I 0 -> h- I i | i < 0 -> mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate i)]- | otherwise -> mkTyConApp typeNatSubTyCon [h,mkNumLitTy i]- _ -> mkTyConApp typeNatSubTyCon [h,reifySOP (S [P [corr]])]- MaybeT (go x)+ (((h,sM),corr,deps):_) <- pure interesting+ x <- case corr of+ I 0 -> pure (fromMaybe (h,Nothing) sM)+ I i | i < 0+ , let l1 = mkNumLitTy (negate i)+ -> case sM of+ Just (q,cM) -> pure+ ( mkTyConApp typeNatAddTyCon [q,l1]+ , fmap (mkTyConAppCo Nominal typeNatAddTyCon . (:[mkNomReflCo l1])) cM+ )+ Nothing -> pure+ ( mkTyConApp typeNatAddTyCon [h,l1]+ , Nothing+ )+ | otherwise+ , let l1 = mkNumLitTy i+ -> case sM of+ Just (q,cM) -> pure+ ( mkTyConApp typeNatSubTyCon [q,l1]+ , fmap (mkTyConAppCo Nominal typeNatSubTyCon . (:[mkNomReflCo l1])) cM+ )+ Nothing -> pure+ ( mkTyConApp typeNatSubTyCon [h,l1]+ , Nothing+ )+ -- If the offset between a given and a wanted is again the wanted+ -- then the given is twice the wanted; so we can just divide+ -- the given by two. Only possible in GHC 8.4+; for 8.2 we simply+ -- fail because we don't know how to divide.+ c | CType (reifySOP (S [P [c]])) == CType want+ , let l2 = mkNumLitTy 2+ -> case sM of+ Just (q,cM) -> pure+ ( mkTyConApp typeNatDivTyCon [q,l2]+ , fmap (mkTyConAppCo Nominal typeNatDivTyCon . (:[mkNomReflCo l2])) cM+ )+ Nothing -> pure+ ( mkTyConApp typeNatDivTyCon [h,l2]+ , Nothing+ )+ -- Only solve with a variable offset if we have [G]iven knownnat for it+ -- Failing to do this check results in #30+ V v | all (not . eqType (TyVarTy v) . fst) knownsX+ -> MaybeT (pure Nothing)+ _ -> let lC = reifySOP (S [P [corr]]) in+ case sM of+ Just (q,cM) -> pure+ ( mkTyConApp typeNatSubTyCon [q,lC]+ , fmap (mkTyConAppCo Nominal typeNatSubTyCon . (:[mkNomReflCo lC])) cM+ )+ Nothing -> pure+ ( mkTyConApp typeNatSubTyCon [h,lC]+ , Nothing+ )+ MaybeT (go deps x) +makeWantedEv+ :: Ct+ -> Type+ -> TcPluginM Solve (EvExpr,Ct)+makeWantedEv ct ty = do+ -- Create a new wanted constraint+ wantedCtEv <- newWanted (ctLoc ct) ty+ let ev = ctEvExpr wantedCtEv+ wanted = mkNonCanonical wantedCtEv+ return (ev,wanted)+ {- | Given: @@ -428,40 +619,44 @@ 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- -> [EvTerm] -- ^ Evidence arguments- -> Maybe EvTerm-makeOpDict (opCls,dfid) knCls tyArgs z evArgs- | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z]- -- KnownNat n ~ SNat n- , [ 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) <- tcInstNewTyCon_maybe kn_tcRep [z]- -- SNat n ~ Integer- , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgs- -- 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)- $ 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++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+ -> [Coercion]+ -- ^ Dependent coercions+ -> [EvExpr]+ -- ^ Evidence arguments+ -> Maybe (Type, Coercion)+ -> Maybe EvTerm+makeOpDict (opCls,dfid) knCls tyArgsC tyArgsI z deps evArgs sM+ | let z1 = maybe z fst sM -- SNatKn (a+b) ~ Integer- , let dfun_inst = EvDFunApp dfid (tail tyArgs) evArgs+ , let dfun_inst = evDFunApp dfid tyArgsI evArgs -- KnownNatAdd a b- op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep)- (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep))+ , let op_to_kn :: EvExpr -> EvExpr+ op_to_kn ev+ = wrapUnaryClassByFiat knCls [z1] deps+ $ unwrapUnaryClassOverNewtype opCls tyArgsC ev -- KnownNatAdd a b ~ KnownNat (a+b)- ev_tm = mkEvCast dfun_inst op_to_kn- = Just ev_tm- | otherwise- = Nothing+ , let op_to_kn1 ev = case sM of+ Nothing -> op_to_kn ev+ Just (_,rw) ->+ let kn_co_rw = mkTyConAppCo Representational (classTyCon knCls) [rw]+ kn_co_co = mkPluginUnivCo "ghc-typelits-knownnat" Representational+ deps+ (coercionRKind kn_co_rw)+ (mkTyConApp (classTyCon knCls) [z])+ in mkCast (op_to_kn ev) (mkTransCo kn_co_rw kn_co_co)+ = Just $ EvExpr $ op_to_kn1 dfun_inst {- Given:@@ -479,24 +674,13 @@ makeKnCoercion :: Class -- ^ KnownNat class -> Type -- ^ Type of the argument -> Type -- ^ Type of the result- -> EvTerm -- ^ KnownNat dictionary for the argument+ -> [Coercion] -- ^ Dependent coercions+ -> EvExpr+ -- ^ 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+makeKnCoercion knCls x z deps knownNat_x+ = Just $ EvExpr $ wrapUnaryClassByFiat knCls [z] deps+ $ unwrapUnaryClassOverNewtype knCls [x] knownNat_x -- | THIS CODE IS COPIED FROM: -- https://github.com/ghc/ghc/blob/8035d1a5dc7290e8d3d61446ee4861e0b460214e/compiler/typecheck/TcInteract.hs#L1973@@ -507,18 +691,97 @@ -- -- 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+makeLitDict :: Class+ -> Type+ -> [Coercion]+ -- ^ dependent coercions+ -> Integer+ -> TcPluginM Solve (Maybe EvTerm)+makeLitDict clas ty deps i+ = do+ et <- mkNaturalExpr i+ let+ ev_tm = wrapUnaryClassByFiat clas [ty] deps et+ return (Just $ EvExpr ev_tm)++{- |+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+ -> [Coercion]+ -- ^ Dependent coercions+ -> [EvExpr]+ -- ^ Evidence arguments+ -> Maybe EvTerm+makeOpDictByFiat (opCls,dfid) knCls tyArgsC tyArgsI z deps evArgs+ = Just $ EvExpr $ wrapUnaryClassByFiat knCls [z] deps+ $ unwrapUnaryClassOverNewtype opCls tyArgsC ev0+ where+ ev0 = evDFunApp dfid tyArgsI evArgs++-- | Given a class of the form @class C a b c where { meth :: ... }@ with+-- a single method, construct a dictionary of the class using an 'UnivCo'.+wrapUnaryClassByFiat :: HasDebugCallStack => Class -> [Type] -> [Coercion] -> EvExpr -> EvExpr+wrapUnaryClassByFiat cls tys deps et+ | Just dc <- tyConSingleDataCon_maybe (classTyCon cls)+ , [meth] <- classMethods cls+ , let meth_ty = subst $ classMethodTy meth+ = let+ by_fiat =+ mkPluginUnivCo "ghc-typelits-knownnat" Representational+ deps+ (exprType et)+ meth_ty+ in+ Var (dataConWrapId dc) `mkTyApps` tys `mkApps` [mkCast et by_fiat] | otherwise- = Nothing+ = pprPanic "wrapUnaryClassByFiat: class not of expected form" $+ vcat [ text "cls:" <+> ppr cls+ , text "tys:" <+> ppr tys+ ]++ where+ subst = substTyWithUnchecked (classTyVars cls) tys++-- | Given a class of the form @class C a b c where { meth :: N x y }@+-- in which @N@ is a newtype, and a dictionary for this class, unwraps **both**+-- the class and the newtype to obtain the value inside the newtype.+unwrapUnaryClassOverNewtype :: HasDebugCallStack => Class -> [Type] -> EvExpr -> EvExpr+unwrapUnaryClassOverNewtype cls tys et+ | [sel] <- classMethods cls+ , Just (rep_tc, rep_args) <- splitTyConApp_maybe (subst $ classMethodTy sel)+ , Just (_, co) <- instNewTyCon_maybe rep_tc rep_args+ = mkCast (evSelector sel tys [et]) co+ | otherwise+ = pprPanic "unwrapUnaryClassOverNewtype: class not of expected form" $+ vcat [ text "cls:" <+> ppr cls+ , text "tys:" <+> ppr tys+ ]+ where+ subst = substTyWithUnchecked (classTyVars cls) tys
tests/Main.hs view
@@ -1,29 +1,60 @@-{-# LANGUAGE DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TypeOperators,+{-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies, FlexibleContexts #-}-+#if __GLASGOW_HASKELL__ >= 805+{-# LANGUAGE NoStarIsType #-}+#endif {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}+#if __GLASGOW_HASKELL__ >= 802+{-# OPTIONS_GHC -fno-warn-orphans #-}+#endif module Main where +import Data.Kind (Type) import Data.Proxy import Data.Type.Equality ((:~:)(..))+#if __GLASGOW_HASKELL__ >= 802+import GHC.TypeNats+#if __GLASGOW_HASKELL__ >= 906+ hiding (type SNat)+#endif+import Numeric.Natural+#else import GHC.TypeLits+#endif import Test.Tasty 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 -addT :: Integer -> Integer -> Integer+#if __GLASGOW_HASKELL__ >= 802+#if !MIN_VERSION_QuickCheck(2,17,0)+instance Arbitrary Natural where+ arbitrary = fromInteger . abs <$> arbitrary+#endif+#endif++#if __GLASGOW_HASKELL__ >= 802+type Number = Natural+#else+type Number = Integer+#endif++addT :: Number -> Number -> Number addT a b = withNat a $ \(Proxy :: Proxy a) -> withNat b $ \(Proxy :: Proxy b) -> natVal (Proxy :: Proxy (a + b)) -subT :: Integer -> Integer -> Integer+subT :: Number -> Number -> Number subT a b | a >= b = withNat a $ \(Proxy :: Proxy a) ->@@ -34,80 +65,80 @@ natVal (Proxy :: Proxy (a - b)) | otherwise = error "a - b < 0" -mulT :: Integer -> Integer -> Integer+mulT :: Number -> Number -> Number mulT a b = withNat a $ \(Proxy :: Proxy a) -> withNat b $ \(Proxy :: Proxy b) -> natVal (Proxy :: Proxy (a * b)) -maxT :: Integer -> Integer -> Integer+maxT :: Number -> Number -> Number maxT a b = withNat a $ \(Proxy :: Proxy a) -> withNat b $ \(Proxy :: Proxy b) -> natVal (Proxy :: Proxy (Max a b)) -logT :: Integer -> Integer+logT :: Number -> Number logT n = withNat n $ \(Proxy :: Proxy n) -> natVal (Proxy :: Proxy (Log n)) -test1 :: forall n . KnownNat n => Proxy n -> Integer+test1 :: forall n . KnownNat n => Proxy n -> Number test1 _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) -test2 :: forall n . KnownNat n => Proxy n -> Integer+test2 :: forall n . KnownNat n => Proxy n -> Number test2 _ = natVal (Proxy :: Proxy (n*3)) -test3 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer+test3 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test3 _ _ = natVal (Proxy :: Proxy (n+m)) -test4 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer+test4 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test4 _ _ = natVal (Proxy :: Proxy (n*m)) -test5 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer+test5 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test5 _ _ = natVal (Proxy :: Proxy (n^m)) -test6 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer+test6 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test6 _ _ = natVal (Proxy :: Proxy ((n^m)+(n*m))) -test7 :: forall n m . (KnownNat m, KnownNat n) => Proxy n -> Proxy m -> Integer+test7 :: forall n m . (KnownNat m, KnownNat n) => Proxy n -> Proxy m -> Number test7 _ _ = natVal (Proxy :: Proxy (Max n m + 1)) -test8 :: forall n m . (KnownNat (Min n m)) => Proxy n -> Proxy m -> Integer+test8 :: forall n m . (KnownNat (Min n m)) => Proxy n -> Proxy m -> Number test8 _ _ = natVal (Proxy :: Proxy (Min n m + 1)) -test9 :: forall n m . (KnownNat m, KnownNat n, n <= m) => Proxy m -> Proxy n -> Integer+test9 :: forall n m . (KnownNat m, KnownNat n, n <= m) => Proxy m -> Proxy n -> Number test9 _ _ = natVal (Proxy :: Proxy (m-n)) -test10 :: forall (n :: Nat) m . (KnownNat m) => Proxy m -> Proxy n -> Integer+test10 :: forall (n :: Nat) m . (KnownNat m, n <= m) => Proxy m -> Proxy n -> Number test10 _ _ = natVal (Proxy :: Proxy (m-n+n)) -test11 :: forall m . (KnownNat m) => Proxy m -> Integer-test11 _ = natVal (Proxy @ (m*m))+test11 :: forall m . (KnownNat m) => Proxy m -> Number+test11 _ = natVal (Proxy @(m*m)) -test12 :: forall m . (KnownNat (m+1)) => Proxy m -> Integer+test12 :: forall m . (KnownNat (m+1)) => Proxy m -> Number test12 = natVal -test13 :: forall m . (KnownNat (m+3)) => Proxy m -> Integer+test13 :: forall m . (KnownNat (m+3)) => Proxy m -> Number test13 = natVal -test14 :: forall m . (KnownNat (4+m)) => Proxy (7+m) -> Integer+test14 :: forall m . (KnownNat (4+m)) => Proxy (7+m) -> Number 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))+test15 :: KnownNat (4 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1) -> Number+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))+test16 :: KnownNat (4 + Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1 + Foo 1) -> Number+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))+test17 :: KnownNat (4 + 2 * Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + 2 * Foo 1 + Foo 1) -> Number+test17 _ _ = natVal (Proxy @(2 * Foo 1 + 7 + Foo 1)) -data SNat :: Nat -> * where+data SNat :: Nat -> Type where SNat :: KnownNat n => SNat n instance Show (SNat n) where@@ -131,111 +162,175 @@ 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))+test20 :: forall a . (KnownNat (3 * a - a)) => Proxy a -> Number+test20 _ = natVal (Proxy @(2 * a)) -test21 :: forall m n . (KnownNat (m+n), KnownNat m) => Proxy (m+n) -> Proxy m -> Integer+test21 :: forall m n . (KnownNat (m+n), KnownNat m) => Proxy (m+n) -> Proxy m -> Number test21 _ _ = natVal (Proxy :: Proxy n) -test22 :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer+test22 :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Number test22 _ _ = natVal (Proxy :: Proxy (y*x*y)) -test23 :: SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1))+test23 :: (1 <= addrSize) => SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1)) test23 SNat = SNat -test24 :: (KnownNat n, n ~ (m+1)) => proxy m -> Integer+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++#if __GLASGOW_HASKELL__ >= 804+test28 :: forall m n . (KnownNat m, (2*n) ~ m) => Proxy m -> Natural+test28 _ = natVal @n Proxy+#endif++type Bar (x::Nat) = x+type NatTimes2 (x :: Nat) = Bar (x * 2)++data Vec (n::Nat) a+repeatV :: KnownNat n => a -> Vec n a+repeatV = undefined++test29 :: KnownNat x => Vec (NatTimes2 x) Bool+test29 = repeatV False++test30 :: forall a b . (b ~ (2^a)) => SNat a -> SNat (Log b)+test30 SNat = SNat @(Log b)++test31 :: (KnownNat n, KnownNat m, k ~ (n + m)) => proxy n -> proxy m -> proxy k -> Natural+test31 _ _ = natVal+ tests :: TestTree tests = testGroup "ghc-typelits-natnormalise" [ testGroup "Basic functionality" [ testCase "KnownNat 4 + KnownNat 6 ~ 10" $- show (test1 (Proxy @ 4)) @?=+ show (test1 (Proxy @4)) @?= "10" , testCase "KnownNat 4 * KnownNat 3 ~ 12" $- show (test2 (Proxy @ 4)) @?=+ show (test2 (Proxy @4)) @?= "12" , testCase "KnownNat 2 + KnownNat 7 ~ 9" $- show (test3 (Proxy @ 2) (Proxy @ 7)) @?=+ show (test3 (Proxy @2) (Proxy @7)) @?= "9" , testCase "KnownNat 2 * KnownNat 7 ~ 14" $- show (test4 (Proxy @ 2) (Proxy @ 7)) @?=+ show (test4 (Proxy @2) (Proxy @7)) @?= "14" , testCase "KnownNat 2 ^ KnownNat 7 ~ 128" $- show (test5 (Proxy @ 2) (Proxy @ 7)) @?=+ show (test5 (Proxy @2) (Proxy @7)) @?= "128" , testCase "KnownNat 3 ^ KnownNat 7 ~ 2187" $- show (test5 (Proxy @ 3) (Proxy @ 7)) @?=+ show (test5 (Proxy @3) (Proxy @7)) @?= "2187" , testCase "(KnownNat 2 ^ KnownNat 7) + (KnownNat 2 * KnownNat 7) ~ 142" $- show (test6 (Proxy @ 2) (Proxy @ 7)) @?=+ show (test6 (Proxy @2) (Proxy @7)) @?= "142" , testCase "KnownNat (Max 7 5 + 1) ~ 8" $- show (test7 (Proxy @ 7) (Proxy @ 5)) @?=+ show (test7 (Proxy @7) (Proxy @5)) @?= "8" , testCase "KnownNat (Min 7 5 + 1) ~ 6" $- show (test8 (Proxy @ 7) (Proxy @ 5)) @?=+ show (test8 (Proxy @7) (Proxy @5)) @?= "6" , testCase "KnownNat (7 - 5) ~ 2" $- show (test9 (Proxy @ 7) (Proxy @ 5)) @?=+ show (test9 (Proxy @7) (Proxy @5)) @?= "2" , testCase "KnownNat (y*x*y), x=3 y=4 ~ 48" $ show (test22 (Proxy @3) (Proxy @4))@?= "48"+#if __GLASGOW_HASKELL__ >= 804+ , testCase "KnownNat m, 2 * n ~ m, m = 10 ~ 5" $+ show (test28 (Proxy @10)) @?=+ "5"+#endif ], testGroup "Implications"- [ testCase "KnownNat m => KnownNat (m*m); @ 5" $- show (test11 (Proxy @ 5)) @?=+ [ testCase "KnownNat m => KnownNat (m*m); @5" $+ show (test11 (Proxy @5)) @?= "25"- , testCase "KnownNat (m+1) => KnownNat m; @ m ~ 5" $- show (test12 (Proxy @ 5)) @?=+ , 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)) @?=+ , 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)) @?=+ , 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)) @?=+ , 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" $+ , 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))) @?=+ 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" $+ , 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))) @?=+ 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" $+ , 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))) @?=+ 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)) @?=+ , testCase "KnownNat (3 * a - a) => KnownNat (2 * a); @a ~ 4" $+ show (test20 (Proxy @4)) @?= "8"- , testCase "KnownNat (a + b), KnownNat b => KnownNat a; @ (a+b) ~ 8, b ~ 6" $- show (test21 (Proxy @ 8) (Proxy @ 6)) @?=+ , testCase "KnownNat (a + b), KnownNat b => KnownNat a; @(a+b) ~ 8, b ~ 6" $+ show (test21 (Proxy @8) (Proxy @6)) @?= "2"+ , testCase "b ~ 2 ^ a, KnownNat a => KnownNat (Log b)" $+ show (test30 (SNat @8)) @?=+ "8"+ , testCase "k ~ m + n, KnownNat m, KnownNat n => KnownNat k" $+ show (test31 (Proxy @2) (Proxy @6) Proxy) @?=+ "8" ], testGroup "Normalisation" [ testCase "KnownNat (m-n+n) ~ KnownNat m" $- show (test10 (Proxy @ 12) (Proxy @8)) @?=+ show (test10 (Proxy @12) (Proxy @8)) @?= "12" , testCase "SNat (a+1) - SNat a = SNat 1" $- show (test18 (SNat @ 11) (SNat @10)) @?=+ show (test18 (SNat @11) (SNat @10)) @?= "1" , testCase "SNat (a+b) - SNat b = SNat a" $- show (test19 (SNat @ 16) (SNat @10)) @?=+ show (test19 (SNat @16) (SNat @10)) @?= "6" , testCase "SNat ((addrSize + 1) - (addrSize - 1)) = SNat 2" $- show (test23 (SNat @ 8)) @?=+ show (test23 (SNat @8)) @?= "2" , 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)),
tests/TestFunctions.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures,+{-# LANGUAGE CPP, DataKinds, FlexibleInstances, GADTs, KindSignatures, MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}@@ -6,21 +6,22 @@ module TestFunctions where import Data.Proxy (Proxy (..))-import Data.Singletons.TH (genDefunSymbols) import Data.Type.Bool (If) import GHC.TypeLits.KnownNat+#if __GLASGOW_HASKELL__ >= 802+import GHC.TypeNats+import Numeric.Natural+#else import GHC.TypeLits+#endif 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 -genDefunSymbols [''Max]- instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''Max) a b where- type KnownNatF2 $(nameToSymbol ''Max) = MaxSym0- natSing2 = let x = natVal (Proxy @ a)- y = natVal (Proxy @ b)+ natSing2 = let x = natVal (Proxy @a)+ y = natVal (Proxy @b) z = max x y in SNatKn z {-# INLINE natSing2 #-}@@ -38,17 +39,24 @@ Min a b = If (a <=? b) a b -- Unary functions.-+#if __GLASGOW_HASKELL__ >= 802+withNat :: Natural -> (forall n. (KnownNat n) => Proxy n -> r) -> r+withNat n f = case someNatVal n of+ SomeNat proxy -> f proxy+#else withNat :: Integer -> (forall n. (KnownNat n) => Proxy n -> r) -> r withNat n f = case someNatVal n of Just (SomeNat proxy) -> f proxy Nothing -> error ("withNat: negative value (" ++ show n ++ ")")+#endif type family Log (n :: Nat) :: Nat where -genDefunSymbols [''Log]-+#if __GLASGOW_HASKELL__ >= 802+logInt :: Natural -> Natural+#else logInt :: Integer -> Integer+#endif logInt 0 = error "log 0" logInt n = go 0 where@@ -58,6 +66,5 @@ GT -> k - 1 instance (KnownNat a) => KnownNat1 $(nameToSymbol ''Log) a where- type KnownNatF1 $(nameToSymbol ''Log) = LogSym0- natSing1 = let x = natVal (Proxy @ a)+ natSing1 = let x = natVal (Proxy @a) in SNatKn (logInt x)