ghc-typelits-knownnat 0.7.10 → 0.7.12
raw patch · 12 files changed
+3031/−3010 lines, 12 filesdep ~ghcdep ~template-haskellsetup-changedPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: ghc, template-haskell
API changes (from Hackage documentation)
- GHC.TypeLits.KnownNat: instance (GHC.TypeNats.KnownNat a, GHC.TypeNats.KnownNat b, b Data.Type.Ord.<= a) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeNats.-" a b
- GHC.TypeLits.KnownNat: instance (GHC.TypeNats.KnownNat x, GHC.TypeNats.KnownNat y, 1 Data.Type.Ord.<= y) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeNats.Div" x y
- GHC.TypeLits.KnownNat: instance (GHC.TypeNats.KnownNat x, GHC.TypeNats.KnownNat y, 1 Data.Type.Ord.<= y) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeNats.Mod" x y
+ GHC.TypeLits.KnownNat: instance (GHC.TypeNats.KnownNat a, GHC.TypeNats.KnownNat b, (b Data.Type.Ord.<= a) GHC.Types.~ (() :: Constraint)) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeNats.-" a b
+ GHC.TypeLits.KnownNat: instance (GHC.TypeNats.KnownNat x, GHC.TypeNats.KnownNat y, (1 Data.Type.Ord.<= y) GHC.Types.~ (() :: Constraint)) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeNats.Div" x y
+ GHC.TypeLits.KnownNat: instance (GHC.TypeNats.KnownNat x, GHC.TypeNats.KnownNat y, (1 Data.Type.Ord.<= y) GHC.Types.~ (() :: Constraint)) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeNats.Mod" x y
Files
- CHANGELOG.md +96/−90
- LICENSE +28/−28
- README.md +82/−82
- Setup.hs +2/−2
- ghc-typelits-knownnat.cabal +135/−135
- src-ghc-9.4/GHC/TypeLits/KnownNat.hs +277/−277
- src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs +814/−800
- src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs +308/−308
- src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs +883/−882
- src/GHC/TypeLits/KnownNat/TH.hs +16/−16
- tests/Main.hs +320/−320
- tests/TestFunctions.hs +70/−70
CHANGELOG.md view
@@ -1,90 +1,96 @@-# Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package--## 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)- * Use type-substituted [G]iven KnownNats (partial solve for [#13](https://github.com/clash-lang/ghc-typelits-knownnat/issues/13))--## 0.2.3 *January 15th 2017*-* Solve normalised literal constraints, i.e.:- * `KnownNat (((addrSize + 1) - (addrSize - 1))) ~ KnownNat 2`--## 0.2.2 *September 29th 2016*-* New features:- * Derive smaller constraints from larger constraints when they differ by a single variable, i.e. `KnownNat (a + b), KnownNat b` implies `KnownNat a`.--## 0.2.1 *August 19th 2016*-* Fixes bugs:- * Source location of derived wanted constraints is, erroneously, always set to line 1, column 1--## 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--## 0.1 *August 10th 2016*-* Initial release+# Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package + +## 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) + * Use type-substituted [G]iven KnownNats (partial solve for [#13](https://github.com/clash-lang/ghc-typelits-knownnat/issues/13)) + +## 0.2.3 *January 15th 2017* +* Solve normalised literal constraints, i.e.: + * `KnownNat (((addrSize + 1) - (addrSize - 1))) ~ KnownNat 2` + +## 0.2.2 *September 29th 2016* +* New features: + * Derive smaller constraints from larger constraints when they differ by a single variable, i.e. `KnownNat (a + b), KnownNat b` implies `KnownNat a`. + +## 0.2.1 *August 19th 2016* +* Fixes bugs: + * Source location of derived wanted constraints is, erroneously, always set to line 1, column 1 + +## 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 + +## 0.1 *August 10th 2016* +* Initial release
LICENSE view
@@ -1,28 +1,28 @@-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-modification, are permitted provided that the following conditions are-met:--1. Redistributions of source code must retain the above copyright- notice, this list of conditions and the following disclaimer.--2. Redistributions in binary form must reproduce the above copyright- notice, this list of conditions and the following disclaimer in the- documentation and/or other materials provided with the- distribution.--THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS-"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT-LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR-A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT-OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,-SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT-LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,-DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY-THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT-(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE-OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+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 +modification, are permitted provided that the following conditions are +met: + +1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the + distribution. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
README.md view
@@ -1,82 +1,82 @@-# 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)--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:--```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 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:- * a matching given `KnownNat` constraint; or- * a corresponding `KnownNat<N>` instance for the type function--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- 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--```-OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver-```--Pragma to the header of your file.+# 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) + +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: + +```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 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: + * a matching given `KnownNat` constraint; or + * a corresponding `KnownNat<N>` instance for the type function + +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 + 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 + +``` +OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver +``` + +Pragma to the header of your file.
Setup.hs view
@@ -1,2 +1,2 @@-import Distribution.Simple-main = defaultMain+import Distribution.Simple +main = defaultMain
ghc-typelits-knownnat.cabal view
@@ -1,135 +1,135 @@-name: ghc-typelits-knownnat-version: 0.7.10-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-file: LICENSE-author: Christiaan Baaij-maintainer: christiaan.baaij@gmail.com-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- CHANGELOG.md-cabal-version: >=1.10-tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,- GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,- GHC == 9.4.7, GHC == 9.6.3, GHC == 9.8.1--source-repository head- type: git- location: https://github.com/clash-lang/ghc-typelits-knownnat.git--flag deverror- description:- Enables `-Werror` for development mode and TravisCI- default: False- manual: True--library- exposed-modules: GHC.TypeLits.KnownNat,- GHC.TypeLits.KnownNat.Solver- other-modules: GHC.TypeLits.KnownNat.TH- other-extensions: AllowAmbiguousTypes- DataKinds- FlexibleInstances- KindSignatures- LambdaCase- MultiParamTypeClasses- ScopedTypeVariables- TemplateHaskell- TupleSections- TypeApplications- TypeOperators- TypeFamilies- TypeInType- UndecidableInstances- ViewPatterns- build-depends: base >= 4.9 && <5,- ghc >= 8.0.1 && <9.10,- ghc-prim >= 0.4.0.0 && <0.12,- ghc-tcplugins-extra >= 0.3.1,- ghc-typelits-natnormalise >= 0.7.1 && <0.8,- transformers >= 0.5.2.0 && <0.7,- template-haskell >= 2.11.0.0 && <2.22- hs-source-dirs: src- default-language: Haskell2010- if flag(deverror)- ghc-options: -Wall -Werror- else- ghc-options: -Wall- if impl(ghc >= 8.0) && impl(ghc < 9.4)- hs-source-dirs: src-pre-ghc-9.4- if impl(ghc >= 9.4) && impl(ghc < 9.10)- hs-source-dirs: src-ghc-9.4- if impl(ghc < 8.2)- build-depends: integer-gmp >= 0.5.1.0--test-suite unittests- type: exitcode-stdio-1.0- main-is: Main.hs- Other-Modules: TestFunctions- build-depends: base >= 4.8 && <5,- ghc-typelits-knownnat,- ghc-typelits-natnormalise >= 0.7.1 && <0.8,- tasty >= 0.10,- tasty-hunit >= 0.9,- tasty-quickcheck >= 0.8- hs-source-dirs: tests- default-language: Haskell2010- other-extensions: DataKinds- FlexibleContexts- FlexibleInstances- GADTs- MultiParamTypeClasses- KindSignatures- ScopedTypeVariables,- TemplateHaskell- TypeApplications- TypeFamilies- TypeFamilyDependencies- TypeOperators- UndecidableInstances- if flag(deverror)- ghc-options: -dcore-lint+name: ghc-typelits-knownnat +version: 0.7.12 +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-file: LICENSE +author: Christiaan Baaij +maintainer: christiaan.baaij@gmail.com +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 + CHANGELOG.md +cabal-version: >=1.10 +tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5, + GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8, + GHC == 9.4.7, GHC == 9.6.3, GHC == 9.8.2, GHC == 9.10.1 + +source-repository head + type: git + location: https://github.com/clash-lang/ghc-typelits-knownnat.git + +flag deverror + description: + Enables `-Werror` for development mode and TravisCI + default: False + manual: True + +library + exposed-modules: GHC.TypeLits.KnownNat, + GHC.TypeLits.KnownNat.Solver + other-modules: GHC.TypeLits.KnownNat.TH + other-extensions: AllowAmbiguousTypes + DataKinds + FlexibleInstances + KindSignatures + LambdaCase + MultiParamTypeClasses + ScopedTypeVariables + TemplateHaskell + TupleSections + TypeApplications + TypeOperators + TypeFamilies + TypeInType + UndecidableInstances + ViewPatterns + build-depends: base >= 4.9 && <5, + ghc >= 8.0.1 && <9.12, + ghc-prim >= 0.4.0.0 && <0.12, + ghc-tcplugins-extra >= 0.3.1, + ghc-typelits-natnormalise >= 0.7.1 && <0.8, + transformers >= 0.5.2.0 && <0.7, + template-haskell >= 2.11.0.0 && <2.23 + hs-source-dirs: src + default-language: Haskell2010 + if flag(deverror) + ghc-options: -Wall -Werror + else + ghc-options: -Wall + if impl(ghc >= 8.0) && impl(ghc < 9.4) + hs-source-dirs: src-pre-ghc-9.4 + if impl(ghc >= 9.4) && impl(ghc < 9.12) + hs-source-dirs: src-ghc-9.4 + if impl(ghc < 8.2) + build-depends: integer-gmp >= 0.5.1.0 + +test-suite unittests + type: exitcode-stdio-1.0 + main-is: Main.hs + Other-Modules: TestFunctions + build-depends: base >= 4.8 && <5, + ghc-typelits-knownnat, + ghc-typelits-natnormalise >= 0.7.1 && <0.8, + tasty >= 0.10, + tasty-hunit >= 0.9, + tasty-quickcheck >= 0.8 + hs-source-dirs: tests + default-language: Haskell2010 + other-extensions: DataKinds + FlexibleContexts + FlexibleInstances + GADTs + MultiParamTypeClasses + KindSignatures + ScopedTypeVariables, + TemplateHaskell + TypeApplications + TypeFamilies + TypeFamilyDependencies + TypeOperators + UndecidableInstances + if flag(deverror) + ghc-options: -dcore-lint
src-ghc-9.4/GHC/TypeLits/KnownNat.hs view
@@ -1,277 +1,277 @@-{-|-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>--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 DataKinds, FlexibleInstances, GADTs, KindSignatures,- MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell,- TypeApplications, TypeFamilies, TypeOperators,- UndecidableInstances \#-\}--import Data.Proxy (Proxy (..))-import GHC.TypeLits.KnownNat--instance (KnownNat a, KnownNat b) => 'KnownNat2' $('nameToSymbol' ''Max) a b where- 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 #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE MagicHash #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeFamilies #-}-#if MIN_VERSION_ghc(8,6,0)-{-# LANGUAGE NoStarIsType #-}-#endif-#if !MIN_VERSION_ghc(8,2,0)-{-# LANGUAGE BangPatterns #-}-#endif--{-# LANGUAGE Trustworthy #-}--{-# OPTIONS_GHC -Wno-unused-top-binds -fexpose-all-unfoldings #-}-{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.KnownNat- ( -- * Singleton natural number- SNatKn (..)- -- * Constraint-level arithmetic classes- , KnownNat1 (..)- , KnownNat2 (..)- , KnownNat3 (..)- -- * Singleton boolean- , SBool (..)- , boolVal- -- * KnownBool- , KnownBool (..)- -- ** Constraint-level boolean functions- , SBoolKb (..)- , KnownNat2Bool (..)- , KnownBoolNat2 (..)- -- * Template Haskell helper- , nameToSymbol- )-where--import GHC.Natural (shiftLNatural)-import Data.Proxy (Proxy (..))-import Data.Type.Bool (If)-import GHC.Prim (Proxy#)-import GHC.TypeNats- (KnownNat, Nat, type (+), type (*), type (^), type (-), type (<=?), type (<=),- type Mod, type Div, natVal)-import GHC.TypeLits (Symbol)-import Numeric.Natural (Natural)-import Data.Type.Ord (OrdCond)-import GHC.Types (Constraint)--import GHC.TypeLits.KnownNat.TH---- | 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- natSing1 :: SNatKn f---- | 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- natSing2 :: SNatKn f---- | 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- natSing3 :: SNatKn f---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.+'-instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(+)) a b where- natSing2 = SNatKn (natVal (Proxy @a) + natVal (Proxy @b))- {-# NOINLINE natSing2 #-}---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.*'-instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(*)) a b where- natSing2 = SNatKn (natVal (Proxy @a) * natVal (Proxy @b))- {-# NOINLINE natSing2 #-}---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.^'-instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where- natSing2 = let x = natVal (Proxy @a)- y = natVal (Proxy @b)- z = case x of- 2 -> shiftLNatural 1 (fromIntegral y)- _ -> x ^ y- in SNatKn z- {-# NOINLINE natSing2 #-}---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.-'-instance (KnownNat a, KnownNat b, (b <= a) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''(-)) a b where- natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b))- {-# NOINLINE natSing2 #-}--instance (KnownNat x, KnownNat y, (1 <= y) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''Div) x y where- natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y)))- {-# NOINLINE natSing2 #-}--instance (KnownNat x, KnownNat y, (1 <= y) ~ (() :: Constraint)) => 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 #-}--instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''OrdCond) a b where- boolNatSing2 = SBoolKb (natVal (Proxy @a) <= natVal (Proxy @b))- {-# NOINLINE boolNatSing2 #-}---- | Class for ternary functions with a Natural result.------ The 'Symbol' /f/ must correspond to the fully qualified name of the--- type-level operation. Use 'nameToSymbol' to get the fully qualified--- TH Name as a 'Symbol'-class KnownNat2Bool (f :: Symbol) (a :: Bool) (b :: k) (c :: k) where- natBoolSing3 :: SNatKn f--instance (KnownBool a, KnownNat b, KnownNat c) => KnownNat2Bool $(nameToSymbol ''If) a b c where- natBoolSing3 = SNatKn (if boolVal (Proxy @a) then natVal (Proxy @b) else natVal (Proxy @c))- {-# NOINLINE natBoolSing3 #-}+{-| +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> + +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 DataKinds, FlexibleInstances, GADTs, KindSignatures, + MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell, + TypeApplications, TypeFamilies, TypeOperators, + UndecidableInstances \#-\} + +import Data.Proxy (Proxy (..)) +import GHC.TypeLits.KnownNat + +instance (KnownNat a, KnownNat b) => 'KnownNat2' $('nameToSymbol' ''Max) a b where + 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 #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +#if MIN_VERSION_ghc(8,6,0) +{-# LANGUAGE NoStarIsType #-} +#endif +#if !MIN_VERSION_ghc(8,2,0) +{-# LANGUAGE BangPatterns #-} +#endif + +{-# LANGUAGE Trustworthy #-} + +{-# OPTIONS_GHC -Wno-unused-top-binds -fexpose-all-unfoldings #-} +{-# OPTIONS_HADDOCK show-extensions #-} + +module GHC.TypeLits.KnownNat + ( -- * Singleton natural number + SNatKn (..) + -- * Constraint-level arithmetic classes + , KnownNat1 (..) + , KnownNat2 (..) + , KnownNat3 (..) + -- * Singleton boolean + , SBool (..) + , boolVal + -- * KnownBool + , KnownBool (..) + -- ** Constraint-level boolean functions + , SBoolKb (..) + , KnownNat2Bool (..) + , KnownBoolNat2 (..) + -- * Template Haskell helper + , nameToSymbol + ) +where + +import GHC.Natural (shiftLNatural) +import Data.Proxy (Proxy (..)) +import Data.Type.Bool (If) +import GHC.Prim (Proxy#) +import GHC.TypeNats + (KnownNat, Nat, type (+), type (*), type (^), type (-), type (<=?), type (<=), + type Mod, type Div, natVal) +import GHC.TypeLits (Symbol) +import Numeric.Natural (Natural) +import Data.Type.Ord (OrdCond) +import GHC.Types (Constraint) + +import GHC.TypeLits.KnownNat.TH + +-- | 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 + natSing1 :: SNatKn f + +-- | 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 + natSing2 :: SNatKn f + +-- | 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 + natSing3 :: SNatKn f + +-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.+' +instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(+)) a b where + natSing2 = SNatKn (natVal (Proxy @a) + natVal (Proxy @b)) + {-# NOINLINE natSing2 #-} + +-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.*' +instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(*)) a b where + natSing2 = SNatKn (natVal (Proxy @a) * natVal (Proxy @b)) + {-# NOINLINE natSing2 #-} + +-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.^' +instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where + natSing2 = let x = natVal (Proxy @a) + y = natVal (Proxy @b) + z = case x of + 2 -> shiftLNatural 1 (fromIntegral y) + _ -> x ^ y + in SNatKn z + {-# NOINLINE natSing2 #-} + +-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.-' +instance (KnownNat a, KnownNat b, (b <= a) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''(-)) a b where + natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b)) + {-# NOINLINE natSing2 #-} + +instance (KnownNat x, KnownNat y, (1 <= y) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''Div) x y where + natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y))) + {-# NOINLINE natSing2 #-} + +instance (KnownNat x, KnownNat y, (1 <= y) ~ (() :: Constraint)) => 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 #-} + +instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''OrdCond) a b where + boolNatSing2 = SBoolKb (natVal (Proxy @a) <= natVal (Proxy @b)) + {-# NOINLINE boolNatSing2 #-} + +-- | Class for ternary functions with a Natural result. +-- +-- The 'Symbol' /f/ must correspond to the fully qualified name of the +-- type-level operation. Use 'nameToSymbol' to get the fully qualified +-- TH Name as a 'Symbol' +class KnownNat2Bool (f :: Symbol) (a :: Bool) (b :: k) (c :: k) where + natBoolSing3 :: SNatKn f + +instance (KnownBool a, KnownNat b, KnownNat c) => KnownNat2Bool $(nameToSymbol ''If) a b c where + natBoolSing3 = SNatKn (if boolVal (Proxy @a) then natVal (Proxy @b) else natVal (Proxy @c)) + {-# NOINLINE natBoolSing3 #-}
src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs view
@@ -1,800 +1,814 @@-{-|-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>--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:- * a matching given @KnownNat@ constraint; or- * a corresponding @KnownNat\<N\>@ instance for the type function--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- 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--@-OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver-@--Pragma to the header of your file.---}--{-# LANGUAGE CPP #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE ViewPatterns #-}--{-# LANGUAGE Trustworthy #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.KnownNat.Solver- ( plugin )-where---- external-import Control.Arrow ((&&&), first)-import Control.Monad.Trans.Maybe (MaybeT (..))-import Control.Monad.Trans.Writer.Strict-import Data.Maybe (catMaybes, fromMaybe, 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 GHC.Builtin.Names (knownNatClassName)-import GHC.Builtin.Types (boolTy)-import GHC.Builtin.Types.Literals (typeNatAddTyCon, typeNatDivTyCon, typeNatSubTyCon)-import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)-import GHC.Builtin.Types.Literals (typeNatCmpTyCon)-import GHC.Core.Class (Class, classMethods, className, classTyCon)-import GHC.Core.Coercion- (Coercion, Role (Nominal, Representational), coercionRKind, mkNomReflCo,- mkTyConAppCo, mkUnivCo)-import GHC.Core.InstEnv (instanceDFunId, lookupUniqueInstEnv)-import GHC.Core.Make (mkNaturalExpr)-import GHC.Core.Predicate- (EqRel (NomEq), Pred (ClassPred,EqPred), classifyPredType)-import GHC.Core.TyCo.Rep (Type (..), TyLit (..), UnivCoProvenance (PluginProv))-import GHC.Core.TyCon (tyConName)-#if MIN_VERSION_ghc(9,6,0)-import GHC.Core.Type- (PredType, dropForAlls, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,- piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind,- irrelevantMult)-import GHC.Core.TyCo.Compare- (eqType)-#else-import GHC.Core.Type- (PredType, dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,- piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind,- irrelevantMult)-#endif-import GHC.Data.FastString (fsLit)-import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)-import GHC.Tc.Instance.Family (tcInstNewTyCon_maybe)-import GHC.Tc.Plugin (TcPluginM, tcLookupClass, getInstEnvs, unsafeTcPluginTcM)-import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), getPlatform)-import GHC.Tc.Types.Constraint- (Ct, ctEvExpr, ctEvidence, ctEvPred, ctLoc, mkNonCanonical)-#if MIN_VERSION_ghc(9,6,0)-import GHC.Tc.Types.Evidence- (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast, evTermCoercion_maybe)-import GHC.Plugins- (mkSymCo, mkTransCo)-#else-import GHC.Tc.Types.Evidence- (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo,- evTermCoercion_maybe)-#endif-import GHC.Types.Id (idType)-import GHC.Types.Name (nameModule_maybe, nameOccName)-import GHC.Types.Name.Occurrence (mkTcOcc, occNameString)-import GHC.Types.Unique.FM (emptyUFM)-import GHC.Types.Var (DFunId)-import GHC.Unit.Module (mkModuleName, moduleName, moduleNameString)--#if MIN_VERSION_ghc(9,6,0)-mkTcSymCo :: Coercion -> Coercion-mkTcSymCo = mkSymCo--mkTcTransCo :: Coercion -> Coercion -> Coercion-mkTcTransCo = mkTransCo-#endif---- | Classes and instances from "GHC.TypeLits.KnownNat"-data KnownNatDefs- = KnownNatDefs- { knownBool :: Class- , knownBoolNat2 :: Class- , knownNat2Bool :: Class- , knownNatN :: Int -> Maybe Class -- ^ KnownNat{N}- }---- | 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- )--{-|-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:- * a matching given @KnownNat@ constraint; or- * a corresponding @KnownNat\<N\>@ instance for the type function--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--$(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)- 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--@-OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver-@--Pragma to the header of your file.---}-plugin :: Plugin-plugin- = defaultPlugin- { tcPlugin = const $ Just normalisePlugin-#if MIN_VERSION_ghc(8,6,0)- , pluginRecompile = purePlugin-#endif- }--normalisePlugin :: TcPlugin-normalisePlugin = tracePlugin "ghc-typelits-knownnat"- TcPlugin { tcPluginInit = lookupKnownNatDefs- , tcPluginSolve = solveKnownNat- , tcPluginRewrite = const emptyUFM- , tcPluginStop = const (return ())- }--solveKnownNat :: KnownNatDefs -> EvBindsVar -> [Ct] -> [Ct]- -> TcPluginM TcPluginSolveResult-solveKnownNat _defs _ _givens [] = return (TcPluginOk [] [])-solveKnownNat defs _ givens wanteds = do- let 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- 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)- return (TcPluginOk solved (concat new))---- | Get the KnownNat constraints-toKnConstraint :: KnownNatDefs -> Ct -> Maybe KnConstraint-toKnConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- ClassPred 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,EvExpr)-toGivenEntry ct = let ct_ev = ctEvidence ct- c_ty = ctEvPred ct_ev- ev = ctEvExpr ct_ev- in (CType c_ty,ev)---- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat"-lookupKnownNatDefs :: TcPluginM KnownNatDefs-lookupKnownNatDefs = do- md <- lookupModule myModule myPackage- kbC <- look md "KnownBool"- kbn2C <- look md "KnownBoolNat2"- kn2bC <- look md "KnownNat2Bool"- kn1C <- look md "KnownNat1"- kn2C <- look md "KnownNat2"- kn3C <- look md "KnownNat3"- return KnownNatDefs- { knownBool = kbC- , knownBoolNat2 = kbn2C- , knownNat2Bool = kn2bC- , knownNatN = \case { 1 -> Just kn1C- ; 2 -> Just kn2C- ; 3 -> Just kn3C- ; _ -> Nothing- }- }- where- look md s = do- nm <- lookupName md (mkTcOcc s)- 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,EvExpr)]- -- ^ All the [G]iven constraints- -> KnConstraint- -> TcPluginM (Maybe ((EvTerm,Ct),[Ct]))-constraintToEvTerm defs 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 (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, Maybe Coercion) -> TcPluginM (Maybe (EvTerm,[Ct]))- go (go_other -> Just ev, _) = return (Just (ev,[]))- go (ty@(TyConApp tc args0), sM)- | let tcNm = tyConName tc- , Just m <- nameModule_maybe tcNm- = do- ienv <- getInstEnvs- let mS = moduleNameString (moduleName m)- tcS = occNameString (nameOccName tcNm)- fn0 = mS ++ "." ++ tcS- fn1 = mkStrLitTy (fsLit fn0)- args1 = fn1:args0- instM = case () of- () | Just knN_cls <- knownNatN defs (length args0)- , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1- -> Just (inst,knN_cls,args0,args1)- | fn0 == "Data.Type.Ord.OrdCond"- , [_,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)- | [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- , length args0Rest == 3- , fn0 == "Data.Type.Bool.If"- , 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) evs)- else return ((,concat new) <$> makeOpDict df cls args1N args0N (unOrig orig) evs (fmap (ty,) sM))- _ -> return ((,[]) <$> go_other ty)-- go ((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- = (fmap (,[])) <$> makeLitDict cls op 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 (EvExpr,[Ct])- go_arg ty = case lookup (CType ty) givens of- Just ev -> return (ev,[])- _ -> do- (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 =- let knClsTc = classTyCon cls- kn = mkTyConApp knClsTc [ty]- cast = if CType ty == CType op- then Just . EvExpr- 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 -- Get the knownnat contraints- unKn ty' = case classifyPredType ty' of- ClassPred cls' [ty'']- | className cls' == knownNatClassName- -> Just ty''- _ -> Nothing- -- Get the rewrites- 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,ev)- | ty1 `eqType` tyK- = Just (ty2,Just (tyK,evTermCoercion_maybe (EvExpr ev)))- | ty2 `eqType` tyK- = Just (ty1,Just (tyK,fmap mkTcSymCo (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 :: [()]- 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 _ _ = Nothing- interesting = mapMaybe (uncurry examineDiff) exploded- -- convert the first suitable evidence- (((h,sM),corr):_) <- 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 x)--makeWantedEv- :: Ct- -> Type- -> TcPluginM (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:--* A "magic" class, and corresponding instance dictionary function, for a- type-level arithmetic operation-* Two KnownNat dictionaries--makeOpDict instantiates the dictionary function with the KnownNat dictionaries,-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. 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)--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 for the Class- -> [Type]- -- ^ Argument types for the Instance- -> Type- -- ^ Type of the result- -> [EvExpr]- -- ^ Evidence arguments- -> Maybe (Type, Coercion)- -> Maybe EvTerm-makeOpDict (opCls,dfid) knCls tyArgsC tyArgsI z evArgs sM- | let z1 = maybe z fst sM- , Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z1]- -- 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 [z1]- -- SNat n ~ Integer- , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgsC- -- KnownNatAdd a b ~ SNatKn (a+b)- , [ op_meth ] <- classMethods opCls- , Just (op_tcRep,op_args) <- splitTyConApp_maybe -- (SNatKn, [KnownNatF2 f x y])- $ funResultTy -- SNatKn (KnownNatF2 f x y)- $ (`piResultTys` tyArgsC) -- KnownNatAdd f x y => SNatKn (KnownNatF2 f x y)- $ idType op_meth -- forall f a b . KnownNat2 f a b => SNatKn (KnownNatF2 f a b)- , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args- -- SNatKn (a+b) ~ Integer- , EvExpr dfun_inst <- evDFunApp dfid tyArgsI evArgs- -- KnownNatAdd a b- , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep)- (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep))- -- KnownNatAdd a b ~ KnownNat (a+b)- , let op_to_kn1 = case sM of- Nothing -> op_to_kn- Just (_,rw) ->- let kn_co_rw = mkTyConAppCo Representational (classTyCon knCls) [rw]- kn_co_co = mkUnivCo (PluginProv "ghc-typelits-knownnat")- Representational- (coercionRKind kn_co_rw)- (mkTyConApp (classTyCon knCls) [z])- in mkTcTransCo op_to_kn (mkTcTransCo kn_co_rw kn_co_co)- , let ev_tm = mkEvCast dfun_inst op_to_kn1- = 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- -> 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---- | 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 -> TcPluginM (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- = do- platform <- unsafeTcPluginTcM getPlatform- let et = mkNaturalExpr platform i- ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))- return (Just ev_tm)- | otherwise- = return Nothing--{- |-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- -> [EvExpr]- -- ^ Evidence arguments- -> Maybe EvTerm-makeOpDictByFiat (opCls,dfid) knCls tyArgsC tyArgsI z evArgs- -- KnownBool b ~ SBool b- | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z]- , [ kn_meth ] <- classMethods knCls- , Just kn_tcRep <- tyConAppTyCon_maybe -- SBool- $ funResultTy -- SBool b- $ dropForAlls -- KnownBool b => SBool b- $ idType kn_meth -- forall b. KnownBool b => SBool b- -- SBool b R~ Bool (The "Lie")- , let kn_co_rep = mkUnivCo (PluginProv "ghc-typelits-knownnat")- Representational- (mkTyConApp kn_tcRep [z]) boolTy- -- KnownBoolNat2 f a b ~ SBool f- , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgsC- , [ op_meth ] <- classMethods opCls- , Just (op_tcRep,op_args) <- splitTyConApp_maybe -- (SBool, [f])- $ funResultTy -- SBool f- $ (`piResultTys` tyArgsC) -- KnownBoolNat2 f x y => SBool f- $ idType op_meth -- forall f x y . KnownBoolNat2 f a b => SBoolf f- -- SBoolF f ~ Bool- , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args- , EvExpr dfun_inst <- evDFunApp dfid tyArgsI evArgs- -- KnownBoolNat2 f x y ~ KnownBool b- , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep)- (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep))- ev_tm = mkEvCast dfun_inst op_to_kn- = Just ev_tm- | otherwise- = Nothing+{-| +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> + +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: + * a matching given @KnownNat@ constraint; or + * a corresponding @KnownNat\<N\>@ instance for the type function + +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 + 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 + +@ +OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver +@ + +Pragma to the header of your file. + +-} + +{-# LANGUAGE CPP #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TemplateHaskellQuotes #-} +{-# LANGUAGE Trustworthy #-} + +{-# OPTIONS_HADDOCK show-extensions #-} + +module GHC.TypeLits.KnownNat.Solver + ( plugin ) +where + +-- external +import Control.Arrow ((&&&), first) +import Control.Monad.Trans.Maybe (MaybeT (..)) +import Control.Monad.Trans.Writer.Strict +import Data.Maybe (catMaybes, fromMaybe, mapMaybe) +import Data.Type.Ord (OrdCond) +import Data.Type.Bool (If) +import GHC.TcPluginM.Extra (newWanted, tracePlugin) +import GHC.TypeLits.Normalise.SOP (SOP (..), Product (..), Symbol (..)) +import GHC.TypeLits.Normalise.Unify (CType (..),normaliseNat,reifySOP) + +-- GHC API +import GHC.Builtin.Names (knownNatClassName) +import GHC.Builtin.Types (boolTy) +import GHC.Builtin.Types.Literals (typeNatAddTyCon, typeNatDivTyCon, typeNatSubTyCon) +import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon) +import GHC.Builtin.Types.Literals (typeNatCmpTyCon) +import GHC.Core.Class (Class, classMethods, className, classTyCon) +import GHC.Core.Coercion + (Coercion, Role (Nominal, Representational), coercionRKind, mkNomReflCo, + mkTyConAppCo, mkUnivCo) +import GHC.Core.InstEnv (instanceDFunId, lookupUniqueInstEnv) +import GHC.Core.Make (mkNaturalExpr) +import GHC.Core.Predicate + (EqRel (NomEq), Pred (ClassPred,EqPred), classifyPredType) +import GHC.Core.TyCo.Rep (Type (..), TyLit (..), UnivCoProvenance (PluginProv)) +import GHC.Core.TyCon (tyConName) +#if MIN_VERSION_ghc(9,6,0) +import GHC.Core.Type + (PredType, dropForAlls, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, + piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind, + irrelevantMult) +import GHC.Core.TyCo.Compare + (eqType) +#else +import GHC.Core.Type + (PredType, dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, + piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind, + irrelevantMult) +#endif +import GHC.Data.FastString (fsLit) +import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin) +import GHC.Tc.Instance.Family (tcInstNewTyCon_maybe) +import GHC.Tc.Plugin (TcPluginM, tcLookupClass, getInstEnvs, unsafeTcPluginTcM, tcPluginIO, tcLookupTyCon) +import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), getPlatform, env_top) +import GHC.Tc.Types.Constraint + (Ct, ctEvExpr, ctEvidence, ctEvPred, ctLoc, mkNonCanonical) +#if MIN_VERSION_ghc(9,6,0) +import GHC.Tc.Types.Evidence + (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast, evTermCoercion_maybe) +import GHC.Plugins + (mkSymCo, mkTransCo) +#else +import GHC.Tc.Types.Evidence + (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo, + evTermCoercion_maybe) +#endif +import GHC.Types.Id (idType) +import GHC.Types.Name (nameModule_maybe, nameOccName, Name) +import GHC.Types.Name.Occurrence (occNameString) +import GHC.Types.Unique.FM (emptyUFM) +import GHC.Types.Var (DFunId) +import GHC.Unit.Module (moduleName, moduleNameString) +import qualified Language.Haskell.TH as TH +import GHC.Plugins (thNameToGhcNameIO, TyCon) +import GHC.Driver.Env (hsc_NC) +import GHC.Data.IOEnv (getEnv) +import GHC.TypeLits.KnownNat + +#if MIN_VERSION_ghc(9,6,0) +mkTcSymCo :: Coercion -> Coercion +mkTcSymCo = mkSymCo + +mkTcTransCo :: Coercion -> Coercion -> Coercion +mkTcTransCo = mkTransCo +#endif + +-- | Classes and instances from "GHC.TypeLits.KnownNat" +data KnownNatDefs + = KnownNatDefs + { knownBool :: Class + , knownBoolNat2 :: Class + , knownNat2Bool :: Class + , knownNatN :: Int -> Maybe Class -- ^ KnownNat{N} + , ordCondTyCon :: TyCon + , ifTyCon :: TyCon + } + +-- | 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 + ) + +{-| +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: + * a matching given @KnownNat@ constraint; or + * a corresponding @KnownNat\<N\>@ instance for the type function + +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 + +$(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) + 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 + +@ +OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver +@ + +Pragma to the header of your file. + +-} +plugin :: Plugin +plugin + = defaultPlugin + { tcPlugin = const $ Just normalisePlugin +#if MIN_VERSION_ghc(8,6,0) + , pluginRecompile = purePlugin +#endif + } + +normalisePlugin :: TcPlugin +normalisePlugin = tracePlugin "ghc-typelits-knownnat" + TcPlugin { tcPluginInit = lookupKnownNatDefs + , tcPluginSolve = solveKnownNat + , tcPluginRewrite = const emptyUFM + , tcPluginStop = const (return ()) + } + +solveKnownNat :: KnownNatDefs -> EvBindsVar -> [Ct] -> [Ct] + -> TcPluginM TcPluginSolveResult +solveKnownNat _defs _ _givens [] = return (TcPluginOk [] []) +solveKnownNat defs _ givens wanteds = do + let 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 + 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) + return (TcPluginOk solved (concat new)) + +-- | Get the KnownNat constraints +toKnConstraint :: KnownNatDefs -> Ct -> Maybe KnConstraint +toKnConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of + ClassPred 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,EvExpr) +toGivenEntry ct = let ct_ev = ctEvidence ct + c_ty = ctEvPred ct_ev + ev = ctEvExpr ct_ev + in (CType c_ty,ev) + +-- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat" +lookupKnownNatDefs :: TcPluginM KnownNatDefs +lookupKnownNatDefs = do + kbC <- look ''KnownBool + kbn2C <- look ''KnownBoolNat2 + kn2bC <- look ''KnownNat2Bool + kn1C <- look ''KnownNat1 + kn2C <- look ''KnownNat2 + kn3C <- look ''KnownNat3 + ordcond <- lookupTHName ''OrdCond >>= tcLookupTyCon + ifTc <- lookupTHName ''If >>= tcLookupTyCon + return KnownNatDefs + { knownBool = kbC + , knownBoolNat2 = kbn2C + , knownNat2Bool = kn2bC + , knownNatN = \case { 1 -> Just kn1C + ; 2 -> Just kn2C + ; 3 -> Just kn3C + ; _ -> Nothing + } + , ordCondTyCon = ordcond + , ifTyCon = ifTc + } + where + look nm = lookupTHName nm >>= tcLookupClass + +lookupTHName :: TH.Name -> TcPluginM Name +lookupTHName th = do + nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv) + res <- tcPluginIO $ thNameToGhcNameIO nc th + maybe (fail $ "Failed to lookup " ++ show th) return res + +-- | Try to create evidence for a wanted constraint +constraintToEvTerm + :: KnownNatDefs + -- ^ The "magic" KnownNatN classes + -> [(CType,EvExpr)] + -- ^ All the [G]iven constraints + -> KnConstraint + -> TcPluginM (Maybe ((EvTerm,Ct),[Ct])) +constraintToEvTerm defs 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 (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, Maybe Coercion) -> TcPluginM (Maybe (EvTerm,[Ct])) + go (go_other -> Just ev, _) = return (Just (ev,[])) + go (ty@(TyConApp tc args0), sM) + | let tcNm = tyConName tc + , Just m <- nameModule_maybe tcNm + = do + ienv <- getInstEnvs + let mS = moduleNameString (moduleName m) + tcS = occNameString (nameOccName tcNm) + fn0 = mS ++ "." ++ tcS + fn1 = mkStrLitTy (fsLit fn0) + args1 = fn1:args0 + instM = case () of + () | Just knN_cls <- knownNatN defs (length args0) + , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1 + -> Just (inst,knN_cls,args0,args1) + | 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) + | [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 + , length args0Rest == 3 + , 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) evs) + else return ((,concat new) <$> makeOpDict df cls args1N args0N (unOrig orig) evs (fmap (ty,) sM)) + _ -> return ((,[]) <$> go_other ty) + + go ((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 + = (fmap (,[])) <$> makeLitDict cls op 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 (EvExpr,[Ct]) + go_arg ty = case lookup (CType ty) givens of + Just ev -> return (ev,[]) + _ -> do + (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 = + let knClsTc = classTyCon cls + kn = mkTyConApp knClsTc [ty] + cast = if CType ty == CType op + then Just . EvExpr + 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 LitTy{} = pure Nothing + offset want = runMaybeT $ do + let -- Get the knownnat contraints + unKn ty' = case classifyPredType ty' of + ClassPred cls' [ty''] + | className cls' == knownNatClassName + -> Just ty'' + _ -> Nothing + -- Get the rewrites + 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,ev) + | ty1 `eqType` tyK + = Just (ty2,Just (tyK,evTermCoercion_maybe (EvExpr ev))) + | ty2 `eqType` tyK + = Just (ty1,Just (tyK,fmap mkTcSymCo (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 :: [()] + 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 _ _ = Nothing + interesting = mapMaybe (uncurry examineDiff) exploded + -- convert the first suitable evidence + (((h,sM),corr):_) <- 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 x) + +makeWantedEv + :: Ct + -> Type + -> TcPluginM (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: + +* A "magic" class, and corresponding instance dictionary function, for a + type-level arithmetic operation +* Two KnownNat dictionaries + +makeOpDict instantiates the dictionary function with the KnownNat dictionaries, +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. 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) + +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 for the Class + -> [Type] + -- ^ Argument types for the Instance + -> Type + -- ^ Type of the result + -> [EvExpr] + -- ^ Evidence arguments + -> Maybe (Type, Coercion) + -> Maybe EvTerm +makeOpDict (opCls,dfid) knCls tyArgsC tyArgsI z evArgs sM + | let z1 = maybe z fst sM + , Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z1] + -- 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 [z1] + -- SNat n ~ Integer + , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgsC + -- KnownNatAdd a b ~ SNatKn (a+b) + , [ op_meth ] <- classMethods opCls + , Just (op_tcRep,op_args) <- splitTyConApp_maybe -- (SNatKn, [KnownNatF2 f x y]) + $ funResultTy -- SNatKn (KnownNatF2 f x y) + $ (`piResultTys` tyArgsC) -- KnownNatAdd f x y => SNatKn (KnownNatF2 f x y) + $ idType op_meth -- forall f a b . KnownNat2 f a b => SNatKn (KnownNatF2 f a b) + , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args + -- SNatKn (a+b) ~ Integer + , EvExpr dfun_inst <- evDFunApp dfid tyArgsI evArgs + -- KnownNatAdd a b + , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep) + (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep)) + -- KnownNatAdd a b ~ KnownNat (a+b) + , let op_to_kn1 = case sM of + Nothing -> op_to_kn + Just (_,rw) -> + let kn_co_rw = mkTyConAppCo Representational (classTyCon knCls) [rw] + kn_co_co = mkUnivCo (PluginProv "ghc-typelits-knownnat") + Representational + (coercionRKind kn_co_rw) + (mkTyConApp (classTyCon knCls) [z]) + in mkTcTransCo op_to_kn (mkTcTransCo kn_co_rw kn_co_co) + , let ev_tm = mkEvCast dfun_inst op_to_kn1 + = 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 + -> 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 + +-- | 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 -> TcPluginM (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 + = do + platform <- unsafeTcPluginTcM getPlatform + let et = mkNaturalExpr platform i + ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep)) + return (Just ev_tm) + | otherwise + = return Nothing + +{- | +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 + -> [EvExpr] + -- ^ Evidence arguments + -> Maybe EvTerm +makeOpDictByFiat (opCls,dfid) knCls tyArgsC tyArgsI z evArgs + -- KnownBool b ~ SBool b + | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z] + , [ kn_meth ] <- classMethods knCls + , Just kn_tcRep <- tyConAppTyCon_maybe -- SBool + $ funResultTy -- SBool b + $ dropForAlls -- KnownBool b => SBool b + $ idType kn_meth -- forall b. KnownBool b => SBool b + -- SBool b R~ Bool (The "Lie") + , let kn_co_rep = mkUnivCo (PluginProv "ghc-typelits-knownnat") + Representational + (mkTyConApp kn_tcRep [z]) boolTy + -- KnownBoolNat2 f a b ~ SBool f + , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgsC + , [ op_meth ] <- classMethods opCls + , Just (op_tcRep,op_args) <- splitTyConApp_maybe -- (SBool, [f]) + $ funResultTy -- SBool f + $ (`piResultTys` tyArgsC) -- KnownBoolNat2 f x y => SBool f + $ idType op_meth -- forall f x y . KnownBoolNat2 f a b => SBoolf f + -- SBoolF f ~ Bool + , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args + , EvExpr dfun_inst <- evDFunApp dfid tyArgsI evArgs + -- KnownBoolNat2 f x y ~ KnownBool b + , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep) + (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep)) + ev_tm = mkEvCast dfun_inst op_to_kn + = Just ev_tm + | otherwise + = Nothing
src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs view
@@ -1,308 +1,308 @@-{-|-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>--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 DataKinds, FlexibleInstances, GADTs, KindSignatures,- MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell,- TypeApplications, TypeFamilies, TypeOperators,- UndecidableInstances \#-\}--import Data.Proxy (Proxy (..))-import GHC.TypeLits.KnownNat--instance (KnownNat a, KnownNat b) => 'KnownNat2' $('nameToSymbol' ''Max) a b where- 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 #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE MagicHash #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeFamilies #-}-#if MIN_VERSION_ghc(8,6,0)-{-# LANGUAGE NoStarIsType #-}-#endif-#if !MIN_VERSION_ghc(8,2,0)-{-# LANGUAGE BangPatterns #-}-#endif--{-# LANGUAGE Trustworthy #-}--{-# OPTIONS_GHC -Wno-unused-top-binds -fexpose-all-unfoldings #-}-{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.KnownNat- ( -- * Singleton natural number- SNatKn (..)- -- * Constraint-level arithmetic classes- , KnownNat1 (..)- , KnownNat2 (..)- , KnownNat3 (..)- -- * Singleton boolean- , SBool (..)- , boolVal- -- * KnownBool- , KnownBool (..)- -- ** Constraint-level boolean functions- , SBoolKb (..)- , KnownNat2Bool (..)- , KnownBoolNat2 (..)- -- * Template Haskell helper- , nameToSymbol- )-where--#if MIN_VERSION_ghc(8,6,0)-import GHC.Natural (shiftLNatural)-#elif MIN_VERSION_ghc(8,2,0)-import Data.Bits (shiftL)-#else-import GHC.Int (Int (..))-import GHC.Integer (shiftLInteger)-#endif-import Data.Proxy (Proxy (..))-import Data.Type.Bool (If)-import GHC.Prim (Proxy#)-#if MIN_VERSION_ghc(8,2,0)-import GHC.TypeNats- (KnownNat, Nat, type (+), type (*), type (^), type (-), type (<=?), type (<=),- natVal)-#if MIN_VERSION_base(4,11,0)-import GHC.TypeNats (Div, Mod)-#endif-import GHC.TypeLits (Symbol)-import Numeric.Natural (Natural)-#else-import GHC.TypeLits- (KnownNat, Nat, Symbol, type (+), type (*), type (^), type (-), type (<=?),- type (<=), natVal)-#endif-#if MIN_VERSION_base(4,16,0)-import Data.Type.Ord (OrdCond)-#endif--import GHC.TypeLits.KnownNat.TH---- | Singleton natural number-newtype SNatKn (f :: Symbol) =-#if MIN_VERSION_ghc(8,2,0)- SNatKn Natural-#else- SNatKn Integer-#endif---- | 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- natSing1 :: SNatKn f---- | 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- natSing2 :: SNatKn f---- | 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- natSing3 :: SNatKn f---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.+'-instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(+)) a b where- natSing2 = SNatKn (natVal (Proxy @a) + natVal (Proxy @b))- {-# INLINE natSing2 #-}---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.*'-instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(*)) a b where- natSing2 = SNatKn (natVal (Proxy @a) * natVal (Proxy @b))- {-# INLINE natSing2 #-}---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.^'-instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where- natSing2 = let x = natVal (Proxy @a)- y = natVal (Proxy @b)- z = case x of- 2 ->-#if MIN_VERSION_ghc(8,6,0)- shiftLNatural 1 (fromIntegral y)-#elif MIN_VERSION_ghc(8,2,0)- shiftL 1 (fromIntegral y)-#else- let !(I# y#) = fromIntegral y- in shiftLInteger 1 y#-#endif- _ -> x ^ y- in SNatKn z- {-# INLINE natSing2 #-}---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.-'-instance (KnownNat a, KnownNat b, b <= a) => KnownNat2 $(nameToSymbol ''(-)) a b where- natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b))- {-# INLINE natSing2 #-}--#if MIN_VERSION_base(4,11,0)-instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x y where- natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y)))--instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x y where- natSing2 = SNatKn (rem (natVal (Proxy @x)) (natVal (Proxy @y)))-#endif---- | Singleton version of 'Bool'-data SBool (b :: Bool) where- SFalse :: SBool 'False- STrue :: SBool 'True--class KnownBool (b :: Bool) where- boolSing :: SBool b--instance KnownBool 'False where- boolSing = SFalse--instance KnownBool 'True where- boolSing = STrue---- | Get the 'Bool' value associated with a type-level 'Bool'------ Use 'boolVal' if you want to perform the standard boolean operations on the--- reified type-level 'Bool'.------ Use 'boolSing' if you need a context in which the type-checker needs the--- type-level 'Bool' to be either 'True' or 'False'------ @--- f :: forall proxy b r . KnownBool b => r--- f = case boolSing @b of--- SFalse -> -- context with b ~ False--- STrue -> -- context with b ~ True--- @-boolVal :: forall b proxy . KnownBool b => proxy b -> Bool-boolVal _ = case boolSing :: SBool b of- SFalse -> False- _ -> True---- | Get the `Bool` value associated with a type-level `Bool`. See also--- 'boolVal' and 'Proxy#'.-boolVal' :: forall b . KnownBool b => Proxy# b -> Bool-boolVal' _ = case boolSing :: SBool b of- SFalse -> False- _ -> True---- | A type "representationally equal" to 'SBool', used for simpler--- implementation of constraint-level functions that need to create instances of--- 'KnownBool'-newtype SBoolKb (f :: Symbol) = SBoolKb Bool---- | Class for binary functions with a Boolean result.------ The 'Symbol' /f/ must correspond to the fully qualified name of the--- type-level operation. Use 'nameToSymbol' to get the fully qualified--- TH Name as a 'Symbol'-class KnownBoolNat2 (f :: Symbol) (a :: k) (b :: k) where- boolNatSing2 :: SBoolKb f--instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''(<=?)) a b where- boolNatSing2 = SBoolKb (natVal (Proxy @a) <= natVal (Proxy @b))- {-# INLINE boolNatSing2 #-}--#if MIN_VERSION_base(4,16,0)-instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''OrdCond) a b where- boolNatSing2 = SBoolKb (natVal (Proxy @a) <= natVal (Proxy @b))- {-# INLINE 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))+{-| +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> + +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 DataKinds, FlexibleInstances, GADTs, KindSignatures, + MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell, + TypeApplications, TypeFamilies, TypeOperators, + UndecidableInstances \#-\} + +import Data.Proxy (Proxy (..)) +import GHC.TypeLits.KnownNat + +instance (KnownNat a, KnownNat b) => 'KnownNat2' $('nameToSymbol' ''Max) a b where + 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 #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +#if MIN_VERSION_ghc(8,6,0) +{-# LANGUAGE NoStarIsType #-} +#endif +#if !MIN_VERSION_ghc(8,2,0) +{-# LANGUAGE BangPatterns #-} +#endif + +{-# LANGUAGE Trustworthy #-} + +{-# OPTIONS_GHC -Wno-unused-top-binds -fexpose-all-unfoldings #-} +{-# OPTIONS_HADDOCK show-extensions #-} + +module GHC.TypeLits.KnownNat + ( -- * Singleton natural number + SNatKn (..) + -- * Constraint-level arithmetic classes + , KnownNat1 (..) + , KnownNat2 (..) + , KnownNat3 (..) + -- * Singleton boolean + , SBool (..) + , boolVal + -- * KnownBool + , KnownBool (..) + -- ** Constraint-level boolean functions + , SBoolKb (..) + , KnownNat2Bool (..) + , KnownBoolNat2 (..) + -- * Template Haskell helper + , nameToSymbol + ) +where + +#if MIN_VERSION_ghc(8,6,0) +import GHC.Natural (shiftLNatural) +#elif MIN_VERSION_ghc(8,2,0) +import Data.Bits (shiftL) +#else +import GHC.Int (Int (..)) +import GHC.Integer (shiftLInteger) +#endif +import Data.Proxy (Proxy (..)) +import Data.Type.Bool (If) +import GHC.Prim (Proxy#) +#if MIN_VERSION_ghc(8,2,0) +import GHC.TypeNats + (KnownNat, Nat, type (+), type (*), type (^), type (-), type (<=?), type (<=), + natVal) +#if MIN_VERSION_base(4,11,0) +import GHC.TypeNats (Div, Mod) +#endif +import GHC.TypeLits (Symbol) +import Numeric.Natural (Natural) +#else +import GHC.TypeLits + (KnownNat, Nat, Symbol, type (+), type (*), type (^), type (-), type (<=?), + type (<=), natVal) +#endif +#if MIN_VERSION_base(4,16,0) +import Data.Type.Ord (OrdCond) +#endif + +import GHC.TypeLits.KnownNat.TH + +-- | Singleton natural number +newtype SNatKn (f :: Symbol) = +#if MIN_VERSION_ghc(8,2,0) + SNatKn Natural +#else + SNatKn Integer +#endif + +-- | 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 + natSing1 :: SNatKn f + +-- | 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 + natSing2 :: SNatKn f + +-- | 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 + natSing3 :: SNatKn f + +-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.+' +instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(+)) a b where + natSing2 = SNatKn (natVal (Proxy @a) + natVal (Proxy @b)) + {-# INLINE natSing2 #-} + +-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.*' +instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(*)) a b where + natSing2 = SNatKn (natVal (Proxy @a) * natVal (Proxy @b)) + {-# INLINE natSing2 #-} + +-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.^' +instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where + natSing2 = let x = natVal (Proxy @a) + y = natVal (Proxy @b) + z = case x of + 2 -> +#if MIN_VERSION_ghc(8,6,0) + shiftLNatural 1 (fromIntegral y) +#elif MIN_VERSION_ghc(8,2,0) + shiftL 1 (fromIntegral y) +#else + let !(I# y#) = fromIntegral y + in shiftLInteger 1 y# +#endif + _ -> x ^ y + in SNatKn z + {-# INLINE natSing2 #-} + +-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.-' +instance (KnownNat a, KnownNat b, b <= a) => KnownNat2 $(nameToSymbol ''(-)) a b where + natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b)) + {-# INLINE natSing2 #-} + +#if MIN_VERSION_base(4,11,0) +instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x y where + natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y))) + +instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x y where + natSing2 = SNatKn (rem (natVal (Proxy @x)) (natVal (Proxy @y))) +#endif + +-- | Singleton version of 'Bool' +data SBool (b :: Bool) where + SFalse :: SBool 'False + STrue :: SBool 'True + +class KnownBool (b :: Bool) where + boolSing :: SBool b + +instance KnownBool 'False where + boolSing = SFalse + +instance KnownBool 'True where + boolSing = STrue + +-- | Get the 'Bool' value associated with a type-level 'Bool' +-- +-- Use 'boolVal' if you want to perform the standard boolean operations on the +-- reified type-level 'Bool'. +-- +-- Use 'boolSing' if you need a context in which the type-checker needs the +-- type-level 'Bool' to be either 'True' or 'False' +-- +-- @ +-- f :: forall proxy b r . KnownBool b => r +-- f = case boolSing @b of +-- SFalse -> -- context with b ~ False +-- STrue -> -- context with b ~ True +-- @ +boolVal :: forall b proxy . KnownBool b => proxy b -> Bool +boolVal _ = case boolSing :: SBool b of + SFalse -> False + _ -> True + +-- | Get the `Bool` value associated with a type-level `Bool`. See also +-- 'boolVal' and 'Proxy#'. +boolVal' :: forall b . KnownBool b => Proxy# b -> Bool +boolVal' _ = case boolSing :: SBool b of + SFalse -> False + _ -> True + +-- | A type "representationally equal" to 'SBool', used for simpler +-- implementation of constraint-level functions that need to create instances of +-- 'KnownBool' +newtype SBoolKb (f :: Symbol) = SBoolKb Bool + +-- | Class for binary functions with a Boolean result. +-- +-- The 'Symbol' /f/ must correspond to the fully qualified name of the +-- type-level operation. Use 'nameToSymbol' to get the fully qualified +-- TH Name as a 'Symbol' +class KnownBoolNat2 (f :: Symbol) (a :: k) (b :: k) where + boolNatSing2 :: SBoolKb f + +instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''(<=?)) a b where + boolNatSing2 = SBoolKb (natVal (Proxy @a) <= natVal (Proxy @b)) + {-# INLINE boolNatSing2 #-} + +#if MIN_VERSION_base(4,16,0) +instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''OrdCond) a b where + boolNatSing2 = SBoolKb (natVal (Proxy @a) <= natVal (Proxy @b)) + {-# INLINE 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))
src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs view
@@ -1,882 +1,883 @@-{-|-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>--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:- * a matching given @KnownNat@ constraint; or- * a corresponding @KnownNat\<N\>@ instance for the type function--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- 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--@-OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver-@--Pragma to the header of your file.---}--{-# LANGUAGE CPP #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE ViewPatterns #-}--{-# LANGUAGE Trustworthy #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.KnownNat.Solver- ( plugin )-where---- external-import Control.Arrow ((&&&), first)-import Control.Monad.Trans.Maybe (MaybeT (..))-import Control.Monad.Trans.Writer.Strict-import Data.Maybe (catMaybes,mapMaybe)-import GHC.TcPluginM.Extra (lookupModule, lookupName, newWanted,- tracePlugin)-#if MIN_VERSION_ghc(8,4,0)-import GHC.TcPluginM.Extra (flattenGivens, mkSubst', substType)-#endif-import GHC.TypeLits.Normalise.SOP (SOP (..), Product (..), Symbol (..))-import GHC.TypeLits.Normalise.Unify (CType (..),normaliseNat,reifySOP)---- GHC API-#if MIN_VERSION_ghc(9,0,0)-import GHC.Builtin.Names (knownNatClassName)-import GHC.Builtin.Types (boolTy)-import GHC.Builtin.Types.Literals (typeNatAddTyCon, typeNatDivTyCon, typeNatSubTyCon)-#if MIN_VERSION_ghc(9,2,0)-import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)-import GHC.Builtin.Types.Literals (typeNatCmpTyCon)-#endif-import GHC.Core.Class (Class, classMethods, className, classTyCon)-import GHC.Core.Coercion (Role (Representational), mkUnivCo)-import GHC.Core.InstEnv (instanceDFunId, lookupUniqueInstEnv)-import GHC.Core.Make (mkNaturalExpr)-import GHC.Core.Predicate- (EqRel (NomEq), Pred (ClassPred,EqPred), classifyPredType)-import GHC.Core.TyCo.Rep (Type (..), TyLit (..), UnivCoProvenance (PluginProv))-import GHC.Core.TyCon (tyConName)-import GHC.Core.Type- (PredType, dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,- piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind,- irrelevantMult)-import GHC.Data.FastString (fsLit)-import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)-import GHC.Tc.Instance.Family (tcInstNewTyCon_maybe)-import GHC.Tc.Plugin (TcPluginM, tcLookupClass, getInstEnvs)-import GHC.Tc.Types (TcPlugin(..), TcPluginResult (..))-import GHC.Tc.Types.Constraint- (Ct, ctEvExpr, ctEvidence, ctEvLoc, ctEvPred, ctLoc, ctLocSpan, isWanted,- mkNonCanonical, setCtLoc, setCtLocSpan)-import GHC.Tc.Types.Evidence- (EvTerm (..), EvExpr, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo)-import GHC.Types.Id (idType)-import GHC.Types.Name (nameModule_maybe, nameOccName)-import GHC.Types.Name.Occurrence (mkTcOcc, occNameString)-import GHC.Types.Var (DFunId)-import GHC.Unit.Module (mkModuleName, moduleName, moduleNameString)-#else-import Class (Class, classMethods, className, classTyCon)-#if MIN_VERSION_ghc(8,6,0)-import Coercion (Role (Representational), mkUnivCo)-#endif-import FamInst (tcInstNewTyCon_maybe)-import FastString (fsLit)-import Id (idType)-import InstEnv (instanceDFunId,lookupUniqueInstEnv)-#if MIN_VERSION_ghc(8,5,0)-import MkCore (mkNaturalExpr)-#endif-import Module (mkModuleName, moduleName, moduleNameString)-import Name (nameModule_maybe, nameOccName)-import OccName (mkTcOcc, occNameString)-import Plugins (Plugin (..), defaultPlugin)-#if MIN_VERSION_ghc(8,6,0)-import Plugins (purePlugin)-#endif-import PrelNames (knownNatClassName)-#if MIN_VERSION_ghc(8,5,0)-import TcEvidence (EvTerm (..), EvExpr, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo)-#else-import TcEvidence (EvTerm (..), EvLit (EvNum), mkEvCast, mkTcSymCo, mkTcTransCo)-#endif-#if MIN_VERSION_ghc(8,5,0)-import TcPluginM (unsafeTcPluginTcM)-#endif-#if !MIN_VERSION_ghc(8,4,0)-import TcPluginM (zonkCt)-#endif-import TcPluginM (TcPluginM, tcLookupClass, getInstEnvs)-import TcRnTypes (TcPlugin(..), TcPluginResult (..))-import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon)-#if MIN_VERSION_ghc(8,4,0)-import TcTypeNats (typeNatDivTyCon)-#endif-import Type- (PredType,- dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,- piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind)-import TyCon (tyConName)-import TyCoRep (Type (..), TyLit (..))-#if MIN_VERSION_ghc(8,6,0)-import TyCoRep (UnivCoProvenance (PluginProv))-import TysWiredIn (boolTy)-#endif-import Var (DFunId)--#if MIN_VERSION_ghc(8,10,0)-import Constraint- (Ct, ctEvExpr, ctEvidence, ctEvLoc, ctEvPred, ctLoc, ctLocSpan, isWanted,- mkNonCanonical, setCtLoc, setCtLocSpan)-import Predicate (EqRel (NomEq), Pred (ClassPred,EqPred), classifyPredType)-#else-import TcRnTypes- (Ct, ctEvidence, ctEvLoc, ctEvPred, ctLoc, ctLocSpan, isWanted, mkNonCanonical,- setCtLoc, setCtLocSpan)-import Type (EqRel (NomEq), PredTree (ClassPred,EqPred), classifyPredType)-#if MIN_VERSION_ghc(8,5,0)-import TcRnTypes (ctEvExpr)-#else-import TcRnTypes (ctEvTerm)-#endif-#endif-#endif---- | Classes and instances from "GHC.TypeLits.KnownNat"-data KnownNatDefs- = KnownNatDefs- { knownBool :: Class- , knownBoolNat2 :: Class- , knownNat2Bool :: Class- , knownNatN :: Int -> Maybe Class -- ^ KnownNat{N}- }---- | 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- )--{-|-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:- * a matching given @KnownNat@ constraint; or- * a corresponding @KnownNat\<N\>@ instance for the type function--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--$(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)- 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--@-OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver-@--Pragma to the header of your file.---}-plugin :: Plugin-plugin- = defaultPlugin- { tcPlugin = const $ Just normalisePlugin-#if MIN_VERSION_ghc(8,6,0)- , pluginRecompile = purePlugin-#endif- }--normalisePlugin :: TcPlugin-normalisePlugin = tracePlugin "ghc-typelits-knownnat"- TcPlugin { tcPluginInit = lookupKnownNatDefs- , tcPluginSolve = solveKnownNat- , tcPluginStop = 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-#if MIN_VERSION_ghc(8,4,0)- subst = map fst- $ mkSubst' givens- kn_wanteds = map (\(x,y,z,orig) -> (x,y,substType subst z,orig))- $ mapMaybe (toKnConstraint defs) wanteds'-#else- kn_wanteds = mapMaybe (toKnConstraint defs) wanteds'-#endif- case kn_wanteds of- [] -> return (TcPluginOk [] [])- _ -> do- -- Make a lookup table for all the [G]iven constraints-#if MIN_VERSION_ghc(8,4,0)- let given_map = map toGivenEntry (flattenGivens givens)-#else- given_map <- mapM (fmap toGivenEntry . zonkCt) givens-#endif- -- Try to solve the wanted KnownNat constraints given the [G]iven- -- KnownNat constraints- (solved,new) <- (unzip . catMaybes) <$> (mapM (constraintToEvTerm defs given_map) kn_wanteds)- return (TcPluginOk solved (concat new))---- | Get the KnownNat constraints-toKnConstraint :: KnownNatDefs -> Ct -> Maybe KnConstraint-toKnConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- ClassPred 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.-#if MIN_VERSION_ghc(8,5,0)-toGivenEntry :: Ct -> (CType,EvExpr)-#else-toGivenEntry :: Ct -> (CType,EvTerm)-#endif-toGivenEntry ct = let ct_ev = ctEvidence ct- c_ty = ctEvPred ct_ev-#if MIN_VERSION_ghc(8,5,0)- ev = ctEvExpr ct_ev-#else- ev = ctEvTerm ct_ev-#endif- in (CType c_ty,ev)---- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat"-lookupKnownNatDefs :: TcPluginM KnownNatDefs-lookupKnownNatDefs = do- md <- lookupModule myModule myPackage- kbC <- look md "KnownBool"- kbn2C <- look md "KnownBoolNat2"- kn2bC <- look md "KnownNat2Bool"- kn1C <- look md "KnownNat1"- kn2C <- look md "KnownNat2"- kn3C <- look md "KnownNat3"- return KnownNatDefs- { knownBool = kbC- , knownBoolNat2 = kbn2C- , knownNat2Bool = kn2bC- , knownNatN = \case { 1 -> Just kn1C- ; 2 -> Just kn2C- ; 3 -> Just kn3C- ; _ -> Nothing- }- }- where- look md s = do- nm <- lookupName md (mkTcOcc s)- 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-#if MIN_VERSION_ghc(8,5,0)- -> [(CType,EvExpr)]-#else- -> [(CType,EvTerm)]-#endif- -- All the [G]iven constraints-- -> KnConstraint- -> TcPluginM (Maybe ((EvTerm,Ct),[Ct]))-constraintToEvTerm defs 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 op- 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 args0)- | let tcNm = tyConName tc- , Just m <- nameModule_maybe tcNm- = do- ienv <- getInstEnvs- let mS = moduleNameString (moduleName m)- tcS = occNameString (nameOccName tcNm)- fn0 = mS ++ "." ++ tcS- fn1 = mkStrLitTy (fsLit fn0)- args1 = fn1:args0- instM = case () of- () | Just knN_cls <- knownNatN defs (length args0)- , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1- -> Just (inst,knN_cls,args0,args1)-#if MIN_VERSION_base(4,16,0)- | fn0 == "Data.Type.Ord.OrdCond"- , [_,cmpNat,TyConApp t1 [],TyConApp t2 [],TyConApp f1 []] <- args0- , TyConApp cmpNatTc args2 <- cmpNat- , cmpNatTc == typeNatCmpTyCon- , t1 == promotedTrueDataCon- , t2 == promotedTrueDataCon- , f1 == promotedFalseDataCon- , let knN_cls = knownBoolNat2 defs- ki = typeKind (head args2)- args1N = ki:fn1:args2- , Right (inst,_) <- lookupUniqueInstEnv ienv knN_cls args1N- -> Just (inst,knN_cls,args2,args1N)-#endif- | length args0 == 2- , let knN_cls = knownBoolNat2 defs- ki = typeKind (head args0)- args1N = ki:args1- , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N- -> Just (inst,knN_cls,args0,args1N)- | length args0 == 4- , fn0 == "Data.Type.Bool.If"- , let args0N = tail args0- args1N = head args0:fn1:tail args0- knN_cls = knownNat2Bool defs- , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N- -> Just (inst,knN_cls,args0N,args1N)- | otherwise- -> Nothing- case instM of- Just (inst,knN_cls,args0N,args1N) -> do- let df_id = instanceDFunId inst- df = (knN_cls,df_id)- df_args = fst -- [KnownNat x, KnownNat y]- . splitFunTys -- ([KnownNat x, KnowNat y], DKnownNat2 "+" x y)- . (`piResultTys` args0N) -- (KnowNat x, KnownNat y) => DKnownNat2 "+" x y- $ idType df_id -- forall a b . (KnownNat a, KnownNat b) => DKnownNat2 "+" a b-#if MIN_VERSION_ghc(9,0,0)- (evs,new) <- unzip <$> mapM (go_arg . irrelevantMult) df_args-#else- (evs,new) <- unzip <$> mapM go_arg df_args-#endif- 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) evs)- else return ((,concat new) <$> makeOpDict df cls args1N args0N (unOrig orig) evs)- _ -> return ((,[]) <$> go_other ty)-- go (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-#if MIN_VERSION_ghc(8,5,0)- = (fmap (,[])) <$> makeLitDict cls op i-#else- = return ((,[]) <$> makeLitDict cls op i)-#endif- 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-#if MIN_VERSION_ghc(8,5,0)- go_arg :: PredType -> TcPluginM (EvExpr,[Ct])-#else- go_arg :: PredType -> TcPluginM (EvTerm,[Ct])-#endif- go_arg ty = case lookup (CType ty) givens of- Just ev -> return (ev,[])- _ -> do- (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 =- let knClsTc = classTyCon cls- kn = mkTyConApp knClsTc [ty]- cast = if CType ty == CType op-#if MIN_VERSION_ghc(8,6,0)- then Just . EvExpr-#else- then Just-#endif- 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 -- Get the knownnat contraints- unKn ty' = case classifyPredType ty' of- ClassPred cls' [ty'']- | className cls' == knownNatClassName- -> 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- -- Rewrite- rewriteTy tyK (ty1,ty2) | ty1 `eqType` tyK = Just ty2- | ty2 `eqType` tyK = Just ty1- | 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 = knowns ++ knownsR- -- pair up the sum-of-products KnownNat constraints- -- with the original Nat operation- subWant = mkTyConApp typeNatSubTyCon . (:[want])- exploded = map (fst . runWriter . normaliseNat . subWant &&& 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 _ _ = Nothing- interesting = mapMaybe (uncurry examineDiff) exploded- -- convert the first suitable evidence- ((h,corr):_) <- pure interesting- x <- case corr of- I 0 -> pure h- I i | i < 0- -> pure (mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate i)])- | otherwise- -> pure (mkTyConApp typeNatSubTyCon [h,mkNumLitTy i])- -- 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 ->-#if MIN_VERSION_ghc(8,4,0)- pure (mkTyConApp typeNatDivTyCon [h,reifySOP (S [P [I 2]])])-#else- MaybeT (pure Nothing)-#endif- -- 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)) knownsX- -> MaybeT (pure Nothing)- _ -> pure (mkTyConApp typeNatSubTyCon [h,reifySOP (S [P [corr]])])- MaybeT (go x)--makeWantedEv- :: Ct- -> Type-#if MIN_VERSION_ghc(8,5,0)- -> TcPluginM (EvExpr,Ct)-#else- -> TcPluginM (EvTerm,Ct)-#endif-makeWantedEv ct ty = do- -- Create a new wanted constraint- wantedCtEv <- newWanted (ctLoc ct) ty-#if MIN_VERSION_ghc(8,5,0)- let ev = ctEvExpr wantedCtEv-#else- let ev = ctEvTerm wantedCtEv-#endif- 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- ct_ls = ctLocSpan (ctLoc ct)- ctl = ctEvLoc wantedCtEv- wanted' = setCtLoc wanted (setCtLocSpan ctl ct_ls)- return (ev,wanted')--{- |-Given:--* A "magic" class, and corresponding instance dictionary function, for a- type-level arithmetic operation-* Two KnownNat dictionaries--makeOpDict instantiates the dictionary function with the KnownNat dictionaries,-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. 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)--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 for the Class- -> [Type]- -- ^ Argument types for the Instance- -> Type -- ^ Type of the result-#if MIN_VERSION_ghc(8,5,0)- -> [EvExpr]-#else- -> [EvTerm]-#endif- -- ^ Evidence arguments- -> Maybe EvTerm-makeOpDict (opCls,dfid) knCls tyArgsC tyArgsI z evArgs- | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z]- -- KnownNat n ~ SNat n- , [ kn_meth ] <- classMethods knCls- , 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) tyArgsC- -- KnownNatAdd a b ~ SNatKn (a+b)- , [ op_meth ] <- classMethods opCls- , Just (op_tcRep,op_args) <- splitTyConApp_maybe -- (SNatKn, [KnownNatF2 f x y])- $ funResultTy -- SNatKn (KnownNatF2 f x y)- $ (`piResultTys` tyArgsC) -- KnownNatAdd f x y => SNatKn (KnownNatF2 f x y)- $ idType op_meth -- forall f a b . KnownNat2 f a b => SNatKn (KnownNatF2 f a b)- , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args- -- SNatKn (a+b) ~ Integer-#if MIN_VERSION_ghc(8,5,0)- , EvExpr dfun_inst <- evDFunApp dfid tyArgsI evArgs-#else- , let dfun_inst = EvDFunApp dfid tyArgsI evArgs-#endif- -- KnownNatAdd a b- , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep)- (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep))- -- KnownNatAdd a b ~ KnownNat (a+b)- ev_tm = mkEvCast dfun_inst op_to_kn- = 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-#if MIN_VERSION_ghc(8,5,0)- -> EvExpr-#else- -> EvTerm-#endif- -- ^ 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---- | 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-#if MIN_VERSION_ghc(8,5,0)-makeLitDict :: Class -> Type -> Integer -> TcPluginM (Maybe EvTerm)-#else-makeLitDict :: Class -> Type -> Integer -> Maybe EvTerm-#endif-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-#if MIN_VERSION_ghc(8,5,0)- = do-#if MIN_VERSION_ghc(9,0,0)- let et = mkNaturalExpr i-#else- et <- unsafeTcPluginTcM (mkNaturalExpr i)-#endif- let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))- return (Just ev_tm)- | otherwise- = return Nothing-#else- , let ev_tm = mkEvCast (EvLit (EvNum i)) (mkTcSymCo (mkTcTransCo co_dict co_rep))- = Just ev_tm- | otherwise- = Nothing-#endif--{- |-Given:--* A "magic" class, and corresponding instance dictionary function, for a- type-level boolean operation-* Two KnownBool dictionaries--makeOpDictByFiat instantiates the dictionary function with the KnownBool-dictionaries, and coerces it to a KnownBool dictionary. i.e. for KnownBoolNat2,-the "magic" dictionary for binary functions, the coercion happens in the-following steps:--1. KnownBoolNat2 "<=?" x y -> SBoolF "<=?"-2. SBoolF "<=?" -> Bool-3. Bool -> SNat (x <=? y) THE BY FIAT PART!-4. SBool (x <=? y) -> KnownBool (x <=? y)--this process is mirrored for the dictionary functions of a higher arity--}-makeOpDictByFiat- :: (Class,DFunId)- -- ^ "magic" class function and dictionary function id- -> Class- -- ^ KnownNat class- -> [Type]- -- ^ Argument types for the Class- -> [Type]- -- ^ Argument types for the Instance- -> Type- -- ^ Type of the result-#if MIN_VERSION_ghc(8,6,0)- -> [EvExpr]-#else- -> [EvTerm]-#endif- -- ^ Evidence arguments- -> Maybe EvTerm-#if MIN_VERSION_ghc(8,6,0)-makeOpDictByFiat (opCls,dfid) knCls tyArgsC tyArgsI z evArgs- -- KnownBool b ~ SBool b- | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z]- , [ kn_meth ] <- classMethods knCls- , Just kn_tcRep <- tyConAppTyCon_maybe -- SBool- $ funResultTy -- SBool b- $ dropForAlls -- KnownBool b => SBool b- $ idType kn_meth -- forall b. KnownBool b => SBool b- -- SBool b R~ Bool (The "Lie")- , let kn_co_rep = mkUnivCo (PluginProv "ghc-typelits-knownnat")- Representational- (mkTyConApp kn_tcRep [z]) boolTy- -- KnownBoolNat2 f a b ~ SBool f- , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgsC- , [ op_meth ] <- classMethods opCls- , Just (op_tcRep,op_args) <- splitTyConApp_maybe -- (SBool, [f])- $ funResultTy -- SBool f- $ (`piResultTys` tyArgsC) -- KnownBoolNat2 f x y => SBool f- $ idType op_meth -- forall f x y . KnownBoolNat2 f a b => SBoolf f- -- SBoolF f ~ Bool- , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args- , EvExpr dfun_inst <- evDFunApp dfid tyArgsI evArgs- -- KnownBoolNat2 f x y ~ KnownBool b- , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep)- (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep))- ev_tm = mkEvCast dfun_inst op_to_kn- = Just ev_tm- | otherwise- = Nothing-#else-makeOpDictByFiat _ _ _ _ _ _ = Nothing-#endif+{-| +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> + +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: + * a matching given @KnownNat@ constraint; or + * a corresponding @KnownNat\<N\>@ instance for the type function + +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 + 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 + +@ +OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver +@ + +Pragma to the header of your file. + +-} + +{-# LANGUAGE CPP #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE ViewPatterns #-} + +{-# LANGUAGE Trustworthy #-} + +{-# OPTIONS_HADDOCK show-extensions #-} + +module GHC.TypeLits.KnownNat.Solver + ( plugin ) +where + +-- external +import Control.Arrow ((&&&), first) +import Control.Monad.Trans.Maybe (MaybeT (..)) +import Control.Monad.Trans.Writer.Strict +import Data.Maybe (catMaybes,mapMaybe) +import GHC.TcPluginM.Extra (lookupModule, lookupName, newWanted, + tracePlugin) +#if MIN_VERSION_ghc(8,4,0) +import GHC.TcPluginM.Extra (flattenGivens, mkSubst', substType) +#endif +import GHC.TypeLits.Normalise.SOP (SOP (..), Product (..), Symbol (..)) +import GHC.TypeLits.Normalise.Unify (CType (..),normaliseNat,reifySOP) + +-- GHC API +#if MIN_VERSION_ghc(9,0,0) +import GHC.Builtin.Names (knownNatClassName) +import GHC.Builtin.Types (boolTy) +import GHC.Builtin.Types.Literals (typeNatAddTyCon, typeNatDivTyCon, typeNatSubTyCon) +#if MIN_VERSION_ghc(9,2,0) +import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon) +import GHC.Builtin.Types.Literals (typeNatCmpTyCon) +#endif +import GHC.Core.Class (Class, classMethods, className, classTyCon) +import GHC.Core.Coercion (Role (Representational), mkUnivCo) +import GHC.Core.InstEnv (instanceDFunId, lookupUniqueInstEnv) +import GHC.Core.Make (mkNaturalExpr) +import GHC.Core.Predicate + (EqRel (NomEq), Pred (ClassPred,EqPred), classifyPredType) +import GHC.Core.TyCo.Rep (Type (..), TyLit (..), UnivCoProvenance (PluginProv)) +import GHC.Core.TyCon (tyConName) +import GHC.Core.Type + (PredType, dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, + piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind, + irrelevantMult) +import GHC.Data.FastString (fsLit) +import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin) +import GHC.Tc.Instance.Family (tcInstNewTyCon_maybe) +import GHC.Tc.Plugin (TcPluginM, tcLookupClass, getInstEnvs) +import GHC.Tc.Types (TcPlugin(..), TcPluginResult (..)) +import GHC.Tc.Types.Constraint + (Ct, ctEvExpr, ctEvidence, ctEvLoc, ctEvPred, ctLoc, ctLocSpan, isWanted, + mkNonCanonical, setCtLoc, setCtLocSpan) +import GHC.Tc.Types.Evidence + (EvTerm (..), EvExpr, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo) +import GHC.Types.Id (idType) +import GHC.Types.Name (nameModule_maybe, nameOccName) +import GHC.Types.Name.Occurrence (mkTcOcc, occNameString) +import GHC.Types.Var (DFunId) +import GHC.Unit.Module (mkModuleName, moduleName, moduleNameString) +#else +import Class (Class, classMethods, className, classTyCon) +#if MIN_VERSION_ghc(8,6,0) +import Coercion (Role (Representational), mkUnivCo) +#endif +import FamInst (tcInstNewTyCon_maybe) +import FastString (fsLit) +import Id (idType) +import InstEnv (instanceDFunId,lookupUniqueInstEnv) +#if MIN_VERSION_ghc(8,5,0) +import MkCore (mkNaturalExpr) +#endif +import Module (mkModuleName, moduleName, moduleNameString) +import Name (nameModule_maybe, nameOccName) +import OccName (mkTcOcc, occNameString) +import Plugins (Plugin (..), defaultPlugin) +#if MIN_VERSION_ghc(8,6,0) +import Plugins (purePlugin) +#endif +import PrelNames (knownNatClassName) +#if MIN_VERSION_ghc(8,5,0) +import TcEvidence (EvTerm (..), EvExpr, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo) +#else +import TcEvidence (EvTerm (..), EvLit (EvNum), mkEvCast, mkTcSymCo, mkTcTransCo) +#endif +#if MIN_VERSION_ghc(8,5,0) +import TcPluginM (unsafeTcPluginTcM) +#endif +#if !MIN_VERSION_ghc(8,4,0) +import TcPluginM (zonkCt) +#endif +import TcPluginM (TcPluginM, tcLookupClass, getInstEnvs) +import TcRnTypes (TcPlugin(..), TcPluginResult (..)) +import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon) +#if MIN_VERSION_ghc(8,4,0) +import TcTypeNats (typeNatDivTyCon) +#endif +import Type + (PredType, + dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, + piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind) +import TyCon (tyConName) +import TyCoRep (Type (..), TyLit (..)) +#if MIN_VERSION_ghc(8,6,0) +import TyCoRep (UnivCoProvenance (PluginProv)) +import TysWiredIn (boolTy) +#endif +import Var (DFunId) + +#if MIN_VERSION_ghc(8,10,0) +import Constraint + (Ct, ctEvExpr, ctEvidence, ctEvLoc, ctEvPred, ctLoc, ctLocSpan, isWanted, + mkNonCanonical, setCtLoc, setCtLocSpan) +import Predicate (EqRel (NomEq), Pred (ClassPred,EqPred), classifyPredType) +#else +import TcRnTypes + (Ct, ctEvidence, ctEvLoc, ctEvPred, ctLoc, ctLocSpan, isWanted, mkNonCanonical, + setCtLoc, setCtLocSpan) +import Type (EqRel (NomEq), PredTree (ClassPred,EqPred), classifyPredType) +#if MIN_VERSION_ghc(8,5,0) +import TcRnTypes (ctEvExpr) +#else +import TcRnTypes (ctEvTerm) +#endif +#endif +#endif + +-- | Classes and instances from "GHC.TypeLits.KnownNat" +data KnownNatDefs + = KnownNatDefs + { knownBool :: Class + , knownBoolNat2 :: Class + , knownNat2Bool :: Class + , knownNatN :: Int -> Maybe Class -- ^ KnownNat{N} + } + +-- | 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 + ) + +{-| +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: + * a matching given @KnownNat@ constraint; or + * a corresponding @KnownNat\<N\>@ instance for the type function + +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 + +$(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) + 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 + +@ +OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver +@ + +Pragma to the header of your file. + +-} +plugin :: Plugin +plugin + = defaultPlugin + { tcPlugin = const $ Just normalisePlugin +#if MIN_VERSION_ghc(8,6,0) + , pluginRecompile = purePlugin +#endif + } + +normalisePlugin :: TcPlugin +normalisePlugin = tracePlugin "ghc-typelits-knownnat" + TcPlugin { tcPluginInit = lookupKnownNatDefs + , tcPluginSolve = solveKnownNat + , tcPluginStop = 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 +#if MIN_VERSION_ghc(8,4,0) + subst = map fst + $ mkSubst' givens + kn_wanteds = map (\(x,y,z,orig) -> (x,y,substType subst z,orig)) + $ mapMaybe (toKnConstraint defs) wanteds' +#else + kn_wanteds = mapMaybe (toKnConstraint defs) wanteds' +#endif + case kn_wanteds of + [] -> return (TcPluginOk [] []) + _ -> do + -- Make a lookup table for all the [G]iven constraints +#if MIN_VERSION_ghc(8,4,0) + let given_map = map toGivenEntry (flattenGivens givens) +#else + given_map <- mapM (fmap toGivenEntry . zonkCt) givens +#endif + -- Try to solve the wanted KnownNat constraints given the [G]iven + -- KnownNat constraints + (solved,new) <- (unzip . catMaybes) <$> (mapM (constraintToEvTerm defs given_map) kn_wanteds) + return (TcPluginOk solved (concat new)) + +-- | Get the KnownNat constraints +toKnConstraint :: KnownNatDefs -> Ct -> Maybe KnConstraint +toKnConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of + ClassPred 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. +#if MIN_VERSION_ghc(8,5,0) +toGivenEntry :: Ct -> (CType,EvExpr) +#else +toGivenEntry :: Ct -> (CType,EvTerm) +#endif +toGivenEntry ct = let ct_ev = ctEvidence ct + c_ty = ctEvPred ct_ev +#if MIN_VERSION_ghc(8,5,0) + ev = ctEvExpr ct_ev +#else + ev = ctEvTerm ct_ev +#endif + in (CType c_ty,ev) + +-- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat" +lookupKnownNatDefs :: TcPluginM KnownNatDefs +lookupKnownNatDefs = do + md <- lookupModule myModule myPackage + kbC <- look md "KnownBool" + kbn2C <- look md "KnownBoolNat2" + kn2bC <- look md "KnownNat2Bool" + kn1C <- look md "KnownNat1" + kn2C <- look md "KnownNat2" + kn3C <- look md "KnownNat3" + return KnownNatDefs + { knownBool = kbC + , knownBoolNat2 = kbn2C + , knownNat2Bool = kn2bC + , knownNatN = \case { 1 -> Just kn1C + ; 2 -> Just kn2C + ; 3 -> Just kn3C + ; _ -> Nothing + } + } + where + look md s = do + nm <- lookupName md (mkTcOcc s) + 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 +#if MIN_VERSION_ghc(8,5,0) + -> [(CType,EvExpr)] +#else + -> [(CType,EvTerm)] +#endif + -- All the [G]iven constraints + + -> KnConstraint + -> TcPluginM (Maybe ((EvTerm,Ct),[Ct])) +constraintToEvTerm defs 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 op + 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 args0) + | let tcNm = tyConName tc + , Just m <- nameModule_maybe tcNm + = do + ienv <- getInstEnvs + let mS = moduleNameString (moduleName m) + tcS = occNameString (nameOccName tcNm) + fn0 = mS ++ "." ++ tcS + fn1 = mkStrLitTy (fsLit fn0) + args1 = fn1:args0 + instM = case () of + () | Just knN_cls <- knownNatN defs (length args0) + , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1 + -> Just (inst,knN_cls,args0,args1) +#if MIN_VERSION_base(4,16,0) + | fn0 == "Data.Type.Ord.OrdCond" + , [_,cmpNat,TyConApp t1 [],TyConApp t2 [],TyConApp f1 []] <- args0 + , TyConApp cmpNatTc args2 <- cmpNat + , cmpNatTc == typeNatCmpTyCon + , t1 == promotedTrueDataCon + , t2 == promotedTrueDataCon + , f1 == promotedFalseDataCon + , let knN_cls = knownBoolNat2 defs + ki = typeKind (head args2) + args1N = ki:fn1:args2 + , Right (inst,_) <- lookupUniqueInstEnv ienv knN_cls args1N + -> Just (inst,knN_cls,args2,args1N) +#endif + | length args0 == 2 + , let knN_cls = knownBoolNat2 defs + ki = typeKind (head args0) + args1N = ki:args1 + , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N + -> Just (inst,knN_cls,args0,args1N) + | length args0 == 4 + , fn0 == "Data.Type.Bool.If" + , let args0N = tail args0 + args1N = head args0:fn1:tail args0 + knN_cls = knownNat2Bool defs + , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N + -> Just (inst,knN_cls,args0N,args1N) + | otherwise + -> Nothing + case instM of + Just (inst,knN_cls,args0N,args1N) -> do + let df_id = instanceDFunId inst + df = (knN_cls,df_id) + df_args = fst -- [KnownNat x, KnownNat y] + . splitFunTys -- ([KnownNat x, KnowNat y], DKnownNat2 "+" x y) + . (`piResultTys` args0N) -- (KnowNat x, KnownNat y) => DKnownNat2 "+" x y + $ idType df_id -- forall a b . (KnownNat a, KnownNat b) => DKnownNat2 "+" a b +#if MIN_VERSION_ghc(9,0,0) + (evs,new) <- unzip <$> mapM (go_arg . irrelevantMult) df_args +#else + (evs,new) <- unzip <$> mapM go_arg df_args +#endif + 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) evs) + else return ((,concat new) <$> makeOpDict df cls args1N args0N (unOrig orig) evs) + _ -> return ((,[]) <$> go_other ty) + + go (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 +#if MIN_VERSION_ghc(8,5,0) + = (fmap (,[])) <$> makeLitDict cls op i +#else + = return ((,[]) <$> makeLitDict cls op i) +#endif + 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 +#if MIN_VERSION_ghc(8,5,0) + go_arg :: PredType -> TcPluginM (EvExpr,[Ct]) +#else + go_arg :: PredType -> TcPluginM (EvTerm,[Ct]) +#endif + go_arg ty = case lookup (CType ty) givens of + Just ev -> return (ev,[]) + _ -> do + (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 = + let knClsTc = classTyCon cls + kn = mkTyConApp knClsTc [ty] + cast = if CType ty == CType op +#if MIN_VERSION_ghc(8,6,0) + then Just . EvExpr +#else + then Just +#endif + 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 LitTy{} = pure Nothing + offset want = runMaybeT $ do + let -- Get the knownnat contraints + unKn ty' = case classifyPredType ty' of + ClassPred cls' [ty''] + | className cls' == knownNatClassName + -> 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 + -- Rewrite + rewriteTy tyK (ty1,ty2) | ty1 `eqType` tyK = Just ty2 + | ty2 `eqType` tyK = Just ty1 + | 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 = knowns ++ knownsR + -- pair up the sum-of-products KnownNat constraints + -- with the original Nat operation + subWant = mkTyConApp typeNatSubTyCon . (:[want]) + exploded = map (fst . runWriter . normaliseNat . subWant &&& 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 _ _ = Nothing + interesting = mapMaybe (uncurry examineDiff) exploded + -- convert the first suitable evidence + ((h,corr):_) <- pure interesting + x <- case corr of + I 0 -> pure h + I i | i < 0 + -> pure (mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate i)]) + | otherwise + -> pure (mkTyConApp typeNatSubTyCon [h,mkNumLitTy i]) + -- 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 -> +#if MIN_VERSION_ghc(8,4,0) + pure (mkTyConApp typeNatDivTyCon [h,reifySOP (S [P [I 2]])]) +#else + MaybeT (pure Nothing) +#endif + -- 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)) knownsX + -> MaybeT (pure Nothing) + _ -> pure (mkTyConApp typeNatSubTyCon [h,reifySOP (S [P [corr]])]) + MaybeT (go x) + +makeWantedEv + :: Ct + -> Type +#if MIN_VERSION_ghc(8,5,0) + -> TcPluginM (EvExpr,Ct) +#else + -> TcPluginM (EvTerm,Ct) +#endif +makeWantedEv ct ty = do + -- Create a new wanted constraint + wantedCtEv <- newWanted (ctLoc ct) ty +#if MIN_VERSION_ghc(8,5,0) + let ev = ctEvExpr wantedCtEv +#else + let ev = ctEvTerm wantedCtEv +#endif + 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 + ct_ls = ctLocSpan (ctLoc ct) + ctl = ctEvLoc wantedCtEv + wanted' = setCtLoc wanted (setCtLocSpan ctl ct_ls) + return (ev,wanted') + +{- | +Given: + +* A "magic" class, and corresponding instance dictionary function, for a + type-level arithmetic operation +* Two KnownNat dictionaries + +makeOpDict instantiates the dictionary function with the KnownNat dictionaries, +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. 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) + +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 for the Class + -> [Type] + -- ^ Argument types for the Instance + -> Type -- ^ Type of the result +#if MIN_VERSION_ghc(8,5,0) + -> [EvExpr] +#else + -> [EvTerm] +#endif + -- ^ Evidence arguments + -> Maybe EvTerm +makeOpDict (opCls,dfid) knCls tyArgsC tyArgsI z evArgs + | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z] + -- KnownNat n ~ SNat n + , [ kn_meth ] <- classMethods knCls + , 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) tyArgsC + -- KnownNatAdd a b ~ SNatKn (a+b) + , [ op_meth ] <- classMethods opCls + , Just (op_tcRep,op_args) <- splitTyConApp_maybe -- (SNatKn, [KnownNatF2 f x y]) + $ funResultTy -- SNatKn (KnownNatF2 f x y) + $ (`piResultTys` tyArgsC) -- KnownNatAdd f x y => SNatKn (KnownNatF2 f x y) + $ idType op_meth -- forall f a b . KnownNat2 f a b => SNatKn (KnownNatF2 f a b) + , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args + -- SNatKn (a+b) ~ Integer +#if MIN_VERSION_ghc(8,5,0) + , EvExpr dfun_inst <- evDFunApp dfid tyArgsI evArgs +#else + , let dfun_inst = EvDFunApp dfid tyArgsI evArgs +#endif + -- KnownNatAdd a b + , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep) + (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep)) + -- KnownNatAdd a b ~ KnownNat (a+b) + ev_tm = mkEvCast dfun_inst op_to_kn + = 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 +#if MIN_VERSION_ghc(8,5,0) + -> EvExpr +#else + -> EvTerm +#endif + -- ^ 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 + +-- | 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 +#if MIN_VERSION_ghc(8,5,0) +makeLitDict :: Class -> Type -> Integer -> TcPluginM (Maybe EvTerm) +#else +makeLitDict :: Class -> Type -> Integer -> Maybe EvTerm +#endif +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 +#if MIN_VERSION_ghc(8,5,0) + = do +#if MIN_VERSION_ghc(9,0,0) + let et = mkNaturalExpr i +#else + et <- unsafeTcPluginTcM (mkNaturalExpr i) +#endif + let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep)) + return (Just ev_tm) + | otherwise + = return Nothing +#else + , let ev_tm = mkEvCast (EvLit (EvNum i)) (mkTcSymCo (mkTcTransCo co_dict co_rep)) + = Just ev_tm + | otherwise + = Nothing +#endif + +{- | +Given: + +* A "magic" class, and corresponding instance dictionary function, for a + type-level boolean operation +* Two KnownBool dictionaries + +makeOpDictByFiat instantiates the dictionary function with the KnownBool +dictionaries, and coerces it to a KnownBool dictionary. i.e. for KnownBoolNat2, +the "magic" dictionary for binary functions, the coercion happens in the +following steps: + +1. KnownBoolNat2 "<=?" x y -> SBoolF "<=?" +2. SBoolF "<=?" -> Bool +3. Bool -> SNat (x <=? y) THE BY FIAT PART! +4. SBool (x <=? y) -> KnownBool (x <=? y) + +this process is mirrored for the dictionary functions of a higher arity +-} +makeOpDictByFiat + :: (Class,DFunId) + -- ^ "magic" class function and dictionary function id + -> Class + -- ^ KnownNat class + -> [Type] + -- ^ Argument types for the Class + -> [Type] + -- ^ Argument types for the Instance + -> Type + -- ^ Type of the result +#if MIN_VERSION_ghc(8,6,0) + -> [EvExpr] +#else + -> [EvTerm] +#endif + -- ^ Evidence arguments + -> Maybe EvTerm +#if MIN_VERSION_ghc(8,6,0) +makeOpDictByFiat (opCls,dfid) knCls tyArgsC tyArgsI z evArgs + -- KnownBool b ~ SBool b + | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z] + , [ kn_meth ] <- classMethods knCls + , Just kn_tcRep <- tyConAppTyCon_maybe -- SBool + $ funResultTy -- SBool b + $ dropForAlls -- KnownBool b => SBool b + $ idType kn_meth -- forall b. KnownBool b => SBool b + -- SBool b R~ Bool (The "Lie") + , let kn_co_rep = mkUnivCo (PluginProv "ghc-typelits-knownnat") + Representational + (mkTyConApp kn_tcRep [z]) boolTy + -- KnownBoolNat2 f a b ~ SBool f + , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgsC + , [ op_meth ] <- classMethods opCls + , Just (op_tcRep,op_args) <- splitTyConApp_maybe -- (SBool, [f]) + $ funResultTy -- SBool f + $ (`piResultTys` tyArgsC) -- KnownBoolNat2 f x y => SBool f + $ idType op_meth -- forall f x y . KnownBoolNat2 f a b => SBoolf f + -- SBoolF f ~ Bool + , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args + , EvExpr dfun_inst <- evDFunApp dfid tyArgsI evArgs + -- KnownBoolNat2 f x y ~ KnownBool b + , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep) + (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep)) + ev_tm = mkEvCast dfun_inst op_to_kn + = Just ev_tm + | otherwise + = Nothing +#else +makeOpDictByFiat _ _ _ _ _ _ = Nothing +#endif
src/GHC/TypeLits/KnownNat/TH.hs view
@@ -1,16 +1,16 @@-{-|-Copyright : (C) 2016, University of Twente-License : BSD2 (see the file LICENSE)-Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>--}--{-# OPTIONS_GHC -Wno-unused-imports #-}--module GHC.TypeLits.KnownNat.TH where--import GHC.TypeLits (Symbol) -- haddock only-import Language.Haskell.TH (Name, TypeQ, litT, strTyLit)---- | Convert a TH 'Name' to a type-level 'Symbol'-nameToSymbol :: Name -> TypeQ-nameToSymbol = litT . strTyLit . show+{-| +Copyright : (C) 2016, University of Twente +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> +-} + +{-# OPTIONS_GHC -Wno-unused-imports #-} + +module GHC.TypeLits.KnownNat.TH where + +import GHC.TypeLits (Symbol) -- haddock only +import Language.Haskell.TH (Name, TypeQ, litT, strTyLit) + +-- | Convert a TH 'Name' to a type-level 'Symbol' +nameToSymbol :: Name -> TypeQ +nameToSymbol = litT . strTyLit . show
tests/Main.hs view
@@ -1,320 +1,320 @@-{-# 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--#if __GLASGOW_HASKELL__ >= 802-instance Arbitrary Natural where- arbitrary = fromInteger . abs <$> arbitrary-#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 :: Number -> Number -> Number-subT a b- | a >= b = withNat a $- \(Proxy :: Proxy a) ->- withNat b $- \(Proxy :: Proxy b) ->- case unsafeCoerce Refl of- (Refl :: (b <=? a) :~: True) ->- natVal (Proxy :: Proxy (a - b))- | otherwise = error "a - b < 0"--mulT :: Number -> Number -> Number-mulT a b = withNat a $- \(Proxy :: Proxy a) ->- withNat b $- \(Proxy :: Proxy b) ->- natVal (Proxy :: Proxy (a * b))--maxT :: Number -> Number -> Number-maxT a b = withNat a $- \(Proxy :: Proxy a) ->- withNat b $- \(Proxy :: Proxy b) ->- natVal (Proxy :: Proxy (Max a b))--logT :: Number -> Number-logT n = withNat n $ \(Proxy :: Proxy n) ->- natVal (Proxy :: Proxy (Log n))--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 -> Number-test2 _ = natVal (Proxy :: Proxy (n*3))--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 -> Number-test4 _ _ = natVal (Proxy :: Proxy (n*m))--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 -> Number-test6 _ _ = natVal (Proxy :: Proxy ((n^m)+(n*m)))--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 -> Number-test8 _ _ = natVal (Proxy :: Proxy (Min n m + 1))--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, n <= m) => Proxy m -> Proxy n -> Number-test10 _ _ = natVal (Proxy :: Proxy (m-n+n))--test11 :: forall m . (KnownNat m) => Proxy m -> Number-test11 _ = natVal (Proxy @(m*m))--test12 :: forall m . (KnownNat (m+1)) => Proxy m -> Number-test12 = natVal--test13 :: forall m . (KnownNat (m+3)) => Proxy m -> Number-test13 = natVal--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) -> Number-test15 _ _ = natVal (Proxy @(Foo 1 + 7))--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) -> Number-test17 _ _ = natVal (Proxy @(2 * Foo 1 + 7 + Foo 1))--data SNat :: Nat -> Type 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 -> Number-test20 _ = natVal (Proxy @(2 * a))--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 -> Number-test22 _ _ = natVal (Proxy :: Proxy (y*x*y))--test23 :: (1 <= addrSize) => SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1))-test23 SNat = SNat--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--tests :: TestTree-tests = testGroup "ghc-typelits-natnormalise"- [ testGroup "Basic functionality"- [ testCase "KnownNat 4 + KnownNat 6 ~ 10" $- show (test1 (Proxy @4)) @?=- "10"- , testCase "KnownNat 4 * KnownNat 3 ~ 12" $- show (test2 (Proxy @4)) @?=- "12"- , testCase "KnownNat 2 + KnownNat 7 ~ 9" $- show (test3 (Proxy @2) (Proxy @7)) @?=- "9"- , testCase "KnownNat 2 * KnownNat 7 ~ 14" $- show (test4 (Proxy @2) (Proxy @7)) @?=- "14"- , testCase "KnownNat 2 ^ KnownNat 7 ~ 128" $- show (test5 (Proxy @2) (Proxy @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"- , 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)) @?=- "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"- , testCase "KnownNat (a + b), KnownNat b => KnownNat a; @(a+b) ~ 8, b ~ 6" $- show (test21 (Proxy @8) (Proxy @6)) @?=- "2"- ],- 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"- , testCase "SNat ((addrSize + 1) - (addrSize - 1)) = SNat 2" $- 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)),- testProperty "mulT = (*)" $ (\a b -> (a >= 0 && b >= 0) ==> (mulT a b === a * b)),- testProperty "maxT = max" $ (\a b -> (a >= 0 && b >= 0) ==> (maxT a b === max a b)),- testProperty "logT = logInt" $ (\a -> (a > 0) ==> (logT a == logInt a))- ]- ]--main :: IO ()-main = defaultMain tests+{-# 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 + +#if __GLASGOW_HASKELL__ >= 802 +instance Arbitrary Natural where + arbitrary = fromInteger . abs <$> arbitrary +#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 :: Number -> Number -> Number +subT a b + | a >= b = withNat a $ + \(Proxy :: Proxy a) -> + withNat b $ + \(Proxy :: Proxy b) -> + case unsafeCoerce Refl of + (Refl :: (b <=? a) :~: True) -> + natVal (Proxy :: Proxy (a - b)) + | otherwise = error "a - b < 0" + +mulT :: Number -> Number -> Number +mulT a b = withNat a $ + \(Proxy :: Proxy a) -> + withNat b $ + \(Proxy :: Proxy b) -> + natVal (Proxy :: Proxy (a * b)) + +maxT :: Number -> Number -> Number +maxT a b = withNat a $ + \(Proxy :: Proxy a) -> + withNat b $ + \(Proxy :: Proxy b) -> + natVal (Proxy :: Proxy (Max a b)) + +logT :: Number -> Number +logT n = withNat n $ \(Proxy :: Proxy n) -> + natVal (Proxy :: Proxy (Log n)) + +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 -> Number +test2 _ = natVal (Proxy :: Proxy (n*3)) + +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 -> Number +test4 _ _ = natVal (Proxy :: Proxy (n*m)) + +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 -> Number +test6 _ _ = natVal (Proxy :: Proxy ((n^m)+(n*m))) + +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 -> Number +test8 _ _ = natVal (Proxy :: Proxy (Min n m + 1)) + +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, n <= m) => Proxy m -> Proxy n -> Number +test10 _ _ = natVal (Proxy :: Proxy (m-n+n)) + +test11 :: forall m . (KnownNat m) => Proxy m -> Number +test11 _ = natVal (Proxy @(m*m)) + +test12 :: forall m . (KnownNat (m+1)) => Proxy m -> Number +test12 = natVal + +test13 :: forall m . (KnownNat (m+3)) => Proxy m -> Number +test13 = natVal + +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) -> Number +test15 _ _ = natVal (Proxy @(Foo 1 + 7)) + +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) -> Number +test17 _ _ = natVal (Proxy @(2 * Foo 1 + 7 + Foo 1)) + +data SNat :: Nat -> Type 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 -> Number +test20 _ = natVal (Proxy @(2 * a)) + +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 -> Number +test22 _ _ = natVal (Proxy :: Proxy (y*x*y)) + +test23 :: (1 <= addrSize) => SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1)) +test23 SNat = SNat + +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 + +tests :: TestTree +tests = testGroup "ghc-typelits-natnormalise" + [ testGroup "Basic functionality" + [ testCase "KnownNat 4 + KnownNat 6 ~ 10" $ + show (test1 (Proxy @4)) @?= + "10" + , testCase "KnownNat 4 * KnownNat 3 ~ 12" $ + show (test2 (Proxy @4)) @?= + "12" + , testCase "KnownNat 2 + KnownNat 7 ~ 9" $ + show (test3 (Proxy @2) (Proxy @7)) @?= + "9" + , testCase "KnownNat 2 * KnownNat 7 ~ 14" $ + show (test4 (Proxy @2) (Proxy @7)) @?= + "14" + , testCase "KnownNat 2 ^ KnownNat 7 ~ 128" $ + show (test5 (Proxy @2) (Proxy @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" + , 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)) @?= + "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" + , testCase "KnownNat (a + b), KnownNat b => KnownNat a; @(a+b) ~ 8, b ~ 6" $ + show (test21 (Proxy @8) (Proxy @6)) @?= + "2" + ], + 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" + , testCase "SNat ((addrSize + 1) - (addrSize - 1)) = SNat 2" $ + 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)), + testProperty "mulT = (*)" $ (\a b -> (a >= 0 && b >= 0) ==> (mulT a b === a * b)), + testProperty "maxT = max" $ (\a b -> (a >= 0 && b >= 0) ==> (maxT a b === max a b)), + testProperty "logT = logInt" $ (\a -> (a > 0) ==> (logT a == logInt a)) + ] + ] + +main :: IO () +main = defaultMain tests
tests/TestFunctions.hs view
@@ -1,70 +1,70 @@-{-# LANGUAGE CPP, DataKinds, FlexibleInstances, GADTs, KindSignatures,- MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TemplateHaskell,- TypeApplications, TypeFamilies, TypeOperators,- UndecidableInstances #-}--module TestFunctions where--import Data.Proxy (Proxy (..))-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--instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''Max) a b where- 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---- 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--#if __GLASGOW_HASKELL__ >= 802-logInt :: Natural -> Natural-#else-logInt :: Integer -> Integer-#endif-logInt 0 = error "log 0"-logInt n = go 0- where- go k = case compare (2^k) n of- LT -> go (k + 1)- EQ -> k- GT -> k - 1--instance (KnownNat a) => KnownNat1 $(nameToSymbol ''Log) a where- natSing1 = let x = natVal (Proxy @a)- in SNatKn (logInt x)+{-# LANGUAGE CPP, DataKinds, FlexibleInstances, GADTs, KindSignatures, + MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TemplateHaskell, + TypeApplications, TypeFamilies, TypeOperators, + UndecidableInstances #-} + +module TestFunctions where + +import Data.Proxy (Proxy (..)) +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 + +instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''Max) a b where + 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 + +-- 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 + +#if __GLASGOW_HASKELL__ >= 802 +logInt :: Natural -> Natural +#else +logInt :: Integer -> Integer +#endif +logInt 0 = error "log 0" +logInt n = go 0 + where + go k = case compare (2^k) n of + LT -> go (k + 1) + EQ -> k + GT -> k - 1 + +instance (KnownNat a) => KnownNat1 $(nameToSymbol ''Log) a where + natSing1 = let x = natVal (Proxy @a) + in SNatKn (logInt x)