ghc-typelits-knownnat 0.7.12 → 0.7.13
raw patch · 12 files changed
+3043/−3031 lines, 12 filesdep ~ghcdep ~ghc-primdep ~template-haskellsetup-changedPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: ghc, ghc-prim, template-haskell
API changes (from Hackage documentation)
Files
- CHANGELOG.md +99/−96
- LICENSE +28/−28
- README.md +82/−82
- Setup.hs +2/−2
- ghc-typelits-knownnat.cabal +136/−135
- src-ghc-9.4/GHC/TypeLits/KnownNat.hs +277/−277
- src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs +822/−814
- src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs +308/−308
- src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs +883/−883
- src/GHC/TypeLits/KnownNat/TH.hs +16/−16
- tests/Main.hs +320/−320
- tests/TestFunctions.hs +70/−70
CHANGELOG.md view
@@ -1,96 +1,99 @@-# 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 +# Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package++## 0.7.13 *March 4th 2025*+* Support for GHC 9.12.1++## 0.7.12 *May 22nd, 2024*+* Support for GHC 9.10.1++## 0.7.11+* Fix infinite loop between plugin and solver pipeline++## 0.7.10 *November 14th 2023*+* Work around [GHC issue 23109](https://gitlab.haskell.org/ghc/ghc/-/issues/23109)++## 0.7.9 *October 10th 2023*+* Support for GHC 9.8.1++## 0.7.8 *February 20th 2023*+* Support for GHC-9.6.0.20230210++## 0.7.7 *October 10th 2022*+* Add support for GHC 9.4++## 0.7.6 *June 18th 2021*+* Add support for GHC 9.2.0.20210422++## 0.7.5 *February 10th 2021*+* Raise upper limit for TH dep to allow building on ghc-9.0.1++## 0.7.4 *January 1st 2021*+* Add support for GHC 9.0.1-rc1++## 0.7.3 *July 25th 2020*+* Fix https://github.com/clash-lang/clash-compiler/issues/1454++## 0.7.2 *February 6th 2020*+ * Add support for GHC 8.10.0-alpha2++## 0.7.1 *October 8th 2019*+* Fix [#29](https://github.com/clash-lang/ghc-typelits-knownnat/issues/29)+* Fix [#30](https://github.com/clash-lang/ghc-typelits-knownnat/issues/30)++## 0.7 *August 26th 2018*+* Solve "known" type-level Booleans, also inside `If` (GHC 8.6+)++## 0.6 *September 14th 2018*+* Move `KnownNat2` instances for `Div` and `Mod` from `ghc-typelits-extra` to `ghc-typelits-knownnat`++## 0.5 *May 9th 2018*+* Fix Inferred constraint is too strong [#19](https://github.com/clash-lang/ghc-typelits-knownnat/issues/19)++## 0.4.2 *April 15th 2018*+* Add support for GHC 8.5.20180306++## 0.4.1 *March 17th, 2018*+* Add support for GHC 8.4.1++## 0.4 *January 4th, 2018*+* Add partial GHC 8.4.1-alpha1 support+* Drop `singletons` dependency [#15](https://github.com/clash-lang/ghc-typelits-knownnat/issues/15)+ * `KnownNatN` classes no longer have the `KnownNatFN` associated type family++## 0.3.1 *August 17th 2017*+* Fix testsuite for GHC 8.2.1++## 0.3 *May 15th 2017*+* GHC 8.2.1 support: Underlying representation for `KnownNat` in GHC 8.2 is `Natural`, meaning users of this plugin will need to update their code to use `Natural` for GHC 8.2 as well.++## 0.2.4 *April 10th 2017*+* New features:+ * Derive constraints for unary functions via a `KnownNat1` instance; thanks to @nshepperd [#11](https://github.com/clash-lang/ghc-typelits-knownnat/pull/11)+ * 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,136 @@-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 +name: ghc-typelits-knownnat+version: 0.7.13+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.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1,+ GHC == 9.12.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.13,+ ghc-prim >= 0.4.0.0 && <0.14,+ 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.24+ 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.13)+ 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,814 +1,822 @@-{-| -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 +{-|+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]+#if MIN_VERSION_ghc(9,11,0)+ kn_co_co = mkUnivCo (PluginProv "ghc-typelits-knownnat") []+#else+ kn_co_co = mkUnivCo (PluginProv "ghc-typelits-knownnat")+#endif+ 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")+#if MIN_VERSION_ghc(9,11,0)+ , let kn_co_rep = mkUnivCo (PluginProv "ghc-typelits-knownnat") []+#else+ , let kn_co_rep = mkUnivCo (PluginProv "ghc-typelits-knownnat")+#endif+ 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,883 +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 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 +{-|+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)