diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,82 +1,82 @@ -# ghc-typelits-knownnat - -[![Build Status](https://github.com/clash-lang/ghc-typelits-knownnat/actions/workflows/haskell-ci.yml/badge.svg?branch=master)](https://github.com/clash-lang/ghc-typelits-knownnat/actions) -[![Hackage](https://img.shields.io/hackage/v/ghc-typelits-knownnat.svg)](https://hackage.haskell.org/package/ghc-typelits-knownnat) -[![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-knownnat.svg?style=flat)](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-knownnat) - -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` 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 + +[![Build Status](https://github.com/clash-lang/ghc-typelits-knownnat/actions/workflows/haskell-ci.yml/badge.svg?branch=master)](https://github.com/clash-lang/ghc-typelits-knownnat/actions) +[![Hackage](https://img.shields.io/hackage/v/ghc-typelits-knownnat.svg)](https://hackage.haskell.org/package/ghc-typelits-knownnat) +[![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-knownnat.svg?style=flat)](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-knownnat) + +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` 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. diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -1,2 +1,2 @@ -import Distribution.Simple -main = defaultMain +import Distribution.Simple +main = defaultMain diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal --- a/ghc-typelits-knownnat.cabal +++ b/ghc-typelits-knownnat.cabal @@ -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\@ 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\@ 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 diff --git a/src-ghc-9.4/GHC/TypeLits/KnownNat.hs b/src-ghc-9.4/GHC/TypeLits/KnownNat.hs --- a/src-ghc-9.4/GHC/TypeLits/KnownNat.hs +++ b/src-ghc-9.4/GHC/TypeLits/KnownNat.hs @@ -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 - -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 + +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 #-} diff --git a/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs b/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs --- a/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs +++ b/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs @@ -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 - -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\@ 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\@ 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 instance. - _ -> go (op,Nothing) - return ((first (,ct)) <$> evM) - where - -- Determine whether the outer type-level operation has a corresponding - -- KnownNat instance, where /N/ corresponds to the arity of the - -- type-level operation - go :: (Type, 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 + +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\@ 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\@ 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 instance. + _ -> go (op,Nothing) + return ((first (,ct)) <$> evM) + where + -- Determine whether the outer type-level operation has a corresponding + -- KnownNat instance, where /N/ corresponds to the arity of the + -- type-level operation + go :: (Type, 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 diff --git a/src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs b/src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs --- a/src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs +++ b/src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs @@ -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 - -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 + +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)) diff --git a/src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs b/src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs --- a/src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs +++ b/src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs @@ -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 - -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\@ 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\@ 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 instance. - _ -> go op - return ((first (,ct)) <$> evM) - where - -- Determine whether the outer type-level operation has a corresponding - -- KnownNat instance, where /N/ corresponds to the arity of the - -- type-level operation - go :: Type -> TcPluginM (Maybe (EvTerm,[Ct])) - go (go_other -> Just ev) = return (Just (ev,[])) - go ty@(TyConApp tc 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 + +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\@ 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\@ 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 instance. + _ -> go op + return ((first (,ct)) <$> evM) + where + -- Determine whether the outer type-level operation has a corresponding + -- KnownNat instance, where /N/ corresponds to the arity of the + -- type-level operation + go :: Type -> TcPluginM (Maybe (EvTerm,[Ct])) + go (go_other -> Just ev) = return (Just (ev,[])) + go ty@(TyConApp tc 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 diff --git a/src/GHC/TypeLits/KnownNat/TH.hs b/src/GHC/TypeLits/KnownNat/TH.hs --- a/src/GHC/TypeLits/KnownNat/TH.hs +++ b/src/GHC/TypeLits/KnownNat/TH.hs @@ -1,16 +1,16 @@ -{-| -Copyright : (C) 2016, University of Twente -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij --} - -{-# OPTIONS_GHC -Wno-unused-imports #-} - -module GHC.TypeLits.KnownNat.TH where - -import GHC.TypeLits (Symbol) -- haddock only -import Language.Haskell.TH (Name, TypeQ, litT, strTyLit) - --- | Convert a TH 'Name' to a type-level 'Symbol' -nameToSymbol :: Name -> TypeQ -nameToSymbol = litT . strTyLit . show +{-| +Copyright : (C) 2016, University of Twente +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij +-} + +{-# OPTIONS_GHC -Wno-unused-imports #-} + +module GHC.TypeLits.KnownNat.TH where + +import GHC.TypeLits (Symbol) -- haddock only +import Language.Haskell.TH (Name, TypeQ, litT, strTyLit) + +-- | Convert a TH 'Name' to a type-level 'Symbol' +nameToSymbol :: Name -> TypeQ +nameToSymbol = litT . strTyLit . show diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -1,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 diff --git a/tests/TestFunctions.hs b/tests/TestFunctions.hs --- a/tests/TestFunctions.hs +++ b/tests/TestFunctions.hs @@ -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)