ghc-typelits-extra 0.3.3 → 0.5.4
raw patch · 12 files changed
Files
- CHANGELOG.md +50/−0
- README.md +4/−4
- ghc-typelits-extra.cabal +72/−37
- src/GHC/TypeLits/Extra.hs +36/−15
- src/GHC/TypeLits/Extra/Solver.hs +224/−135
- src/GHC/TypeLits/Extra/Solver/Compat.hs +101/−0
- src/GHC/TypeLits/Extra/Solver/Operations.hs +129/−103
- src/GHC/TypeLits/Extra/Solver/Unify.hs +123/−82
- tests/ErrorTests.hs +0/−217
- tests/Main.hs +163/−54
- tests/ShouldError.hs +574/−0
- tests/ShouldError/Tasty.hs +53/−0
CHANGELOG.md view
@@ -1,5 +1,55 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package +# 0.5.4 *May 13th 2026*+* Bump ghc-tcplugin-api to prepare for inclusion into stackage++# 0.5.3 *March 19th 2026*+* Do not require equality to unit constraint for wanted InEqs for `CLog` and `CLogWZ`.+* Fix wrong reification from `CLogWZ` to `CLog` causing GHC panic. [#71](https://github.com/clash-lang/ghc-typelits-extra/issues/71)+* Do not emit new wanteds for given `CLogWZ ~ CLog` equalities. [#73](https://github.com/clash-lang/ghc-typelits-extra/issues/73)++# 0.5.2 *December 3rd 2025*+* Add `CLogWZ`, an extension of 'CLog', which returns the additional third argument in case the second argument is zero+* Add rewrite rules for `Min`, `Max`, `FLog`, `CLog`, and `Log`++# 0.5.1 *October 21st 2025*+* Compatibility with `ghc-typelits-natnormalise` 0.9.1 release++# 0.5.0 *October 17th 2025*+* Add support for GHC 9.14+* Uses https://hackage.haskell.org/package/ghc-tcplugin-api to make supporting new GHC versions easier+* Support for GHC versions older than 8.8 is dropped++# 0.4.8 *March 4th 2025*+* Add support for GHC 9.12.1++# 0.4.7 *May 22nd, 2024*+* Add support for GHC 9.10.1+* Fix Plugin silently fails when normalizing <= in GHC 9.4+ [#50](https://github.com/clash-lang/ghc-typelits-extra/issues/50)+* Fix faulty lookup for `Mod` and `Div` in GHC >= 9.2++# 0.4.6 *October 10th 2023*+* Support for GHC-9.8.1++# 0.4.5 *February 20th 2023*+* Support for GHC-9.6.0.20230210++# 0.4.4 *October 21st 2022*+* Add support for GHC 9.4++# 0.4.3 *June 18th 2021*+* Add support for GHC 9.2.0.20210422++# 0.4.2 *January 1st 2021*+* Add support for GHC 9.0.1-rc1++# 0.4.1 *November 10 2020*+* Reduce `n <=? Max (n + p) p` to `True`++# 0.4 *March 9 2020*+* `Max` short-circuits on zero, but is stuckness preserving. i.e. `Max (0-1) 0` reduces to `(0-1)`+* Reduce inside arithmetic equations. e.g. `1 + a ~ Max 0 a + CLog 2 2`+ # 0.3.3 *February 6th 2020* * Add support for GHC 8.10.1-alpha2
README.md view
@@ -1,6 +1,6 @@ # ghc-typelits-extra -[](http://travis-ci.org/clash-lang/ghc-typelits-extra)+[](https://github.com/clash-lang/ghc-typelits-extra/actions) [](https://hackage.haskell.org/package/ghc-typelits-extra) [](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-extra) @@ -11,11 +11,11 @@ * `GHC.TypeLits.Extra.Min`: type-level [min](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:min) * `GHC.TypeLits.Extra.Div`: type-level [div](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:div) * `GHC.TypeLits.Extra.Mod`: type-level [mod](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:mod)-* `GHC.TypeLits.Extra.FLog`: type-level equivalent of [integerLogBase#](https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35-)+* `GHC.TypeLits.Extra.FLog`: type-level equivalent of [integerLogBase#](https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35-) .i.e. the exact integer equivalent to "`floor (logBase x y)`"-* `GHC.TypeLits.Extra.CLog`: type-level equivalent of _the ceiling of_ [integerLogBase#](https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35-)+* `GHC.TypeLits.Extra.CLog`: type-level equivalent of _the ceiling of_ [integerLogBase#](https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35-) .i.e. the exact integer equivalent to "`ceiling (logBase x y)`"-* 'GHC.TypeLits.Extra.Log': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+* 'GHC.TypeLits.Extra.Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> where the operation only reduces when "`floor (logBase b x) ~ ceiling (logBase b x)`" * `GHC.TypeLits.Extra.GCD`: a type-level [gcd](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd) * `GHC.TypeLits.Extra.LCM`: a type-level [lcm](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:lcm)
ghc-typelits-extra.cabal view
@@ -1,42 +1,45 @@+cabal-version: 3.0 name: ghc-typelits-extra-version: 0.3.3+version: 0.5.4 synopsis: Additional type-level operations on GHC.TypeLits.Nat description: Additional type-level operations on @GHC.TypeLits.Nat@:- .+ * @Max@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:max max>- .+ * @Min@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:min min>- .+ * @Div@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:div div>- .+ * @Mod@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:mod mod>- .- * @FLog@: type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>++ * @FLog@: type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> i.e. the exact integer equivalent to @floor (logBase x y)@- .- * @CLog@: type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>++ * @CLog@: type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> i.e. the exact integer equivalent to @ceiling (logBase x y)@- .- * @Log@: type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>++ * @CLogWZ@: extension of @CLog@, which returns the additional third argument in case the second argument is zero++ * @Log@: type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> where the operation only reduces when @floor (logBase b x) ~ ceiling (logBase b x)@- .+ * @GCD@: a type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd gcd>- .+ * @LCM@: a type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:lcm lcm>- .+ And a custom solver for the above operations defined in @GHC.TypeLits.Extra.Solver@ as a GHC type-checker plugin. To use the plugin, add the- .+ @ OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver @- .+ pragma to the header of your file. homepage: http://www.clash-lang.org/ bug-reports: http://github.com/clash-lang/ghc-typelits-extra/issues-license: BSD2+license: BSD-2-Clause license-file: LICENSE author: Christiaan Baaij maintainer: christiaan.baaij@gmail.com@@ -44,11 +47,11 @@ 2017-2018, QBayLogic B.V. category: Type System build-type: Simple-extra-source-files: README.md+extra-doc-files: README.md CHANGELOG.md-cabal-version: >=1.10-tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,- GHC == 8.8.1, GHC == 8.10.1+tested-with: GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,+ GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.3,+ GHC == 9.12.2 source-repository head@@ -64,17 +67,42 @@ library exposed-modules: GHC.TypeLits.Extra, GHC.TypeLits.Extra.Solver- other-modules: GHC.TypeLits.Extra.Solver.Unify+ other-modules: GHC.TypeLits.Extra.Solver.Compat+ GHC.TypeLits.Extra.Solver.Unify GHC.TypeLits.Extra.Solver.Operations- build-depends: base >= 4.8 && <5,- containers >= 0.5.7.1 && <0.7,- ghc >= 7.10 && <8.11,- ghc-prim >= 0.5 && <1.0,- ghc-tcplugins-extra >= 0.3.1,- ghc-typelits-knownnat >= 0.7.2 && <0.8,- ghc-typelits-natnormalise >= 0.7.1 && <0.8,- integer-gmp >= 1.0 && <1.1,- transformers >= 0.4.2.0 && <0.6+ build-depends: base >= 4.8 && <5,+ containers >= 0.5.7.1 && <0.9,+ ghc >= 8.8 && <9.17,+ ghc-prim >= 0.5 && <1,+ ghc-tcplugin-api >= 0.19 && <0.20,+ ghc-typelits-knownnat >= 0.7.2 && <0.9,+ ghc-typelits-natnormalise >= 0.9.5 && <0.10,+ transformers >= 0.4.2.0 && <0.7,+ template-haskell >= 2.15 && <2.25+ if impl(ghc >= 9.0.0)+ build-depends: ghc-bignum >=1.0 && <1.5+ else+ build-depends: integer-gmp >=1.0 && <1.1+ mixins:+ ghc+ ( TcTypeNats as GHC.Builtin.Types.Literals+ , DataCon as GHC.Core.DataCon+ , TyCoRep as GHC.Core.TyCo.Rep+ , Type as GHC.Core.Type+ , Plugins as GHC.Driver.Plugins+ )++ if impl(ghc >= 8.9)+ mixins:+ ghc+ ( Constraint as GHC.Tc.Types.Constraint+ )+ else+ mixins:+ ghc+ ( TcRnTypes as GHC.Tc.Types.Constraint+ )+ hs-source-dirs: src default-language: Haskell2010 other-extensions: DataKinds@@ -97,16 +125,23 @@ test-suite test-ghc-typelits-extra type: exitcode-stdio-1.0 main-is: Main.hs- Other-Modules: ErrorTests- build-depends: base >= 4.8 && <5,+ Other-Modules: ShouldError+ ShouldError.Tasty+ build-depends: base,+ directory,+ filepath, ghc-typelits-extra,- ghc-typelits-knownnat >= 0.7.2,- ghc-typelits-natnormalise >= 0.7.1,+ ghc-typelits-knownnat,+ ghc-typelits-natnormalise,+ process,+ interpolate, tasty >= 0.10,- tasty-hunit >= 0.9+ tasty-hunit >= 0.9,+ temporary hs-source-dirs: tests+ ghc-options: -Wall default-language: Haskell2010 other-extensions: DataKinds TypeOperators if flag(deverror)- ghc-options: -O0 -dcore-lint+ ghc-options: -Werror -dcore-lint
src/GHC/TypeLits/Extra.hs view
@@ -14,13 +14,15 @@ * 'Mod': type-level 'mod' - * 'FLog': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ * 'FLog': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" - * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" - * 'Log': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ * 'CLogWZ': extension of 'CLog', which returns the additional third argument in case the second argument is zero++ * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" * 'GCD': a type-level 'gcd'@@ -70,6 +72,7 @@ -- ** Logarithm , FLog , CLog+ , CLogWZ -- *** Exact logarithm , Log -- Numeric@@ -98,7 +101,8 @@ #if MIN_VERSION_ghc(8,4,0) import GHC.TypeLits (Div, Mod) #endif-import GHC.TypeLits.KnownNat (KnownNat2 (..), SNatKn (..), nameToSymbol)+import GHC.TypeLits.KnownNat (KnownNat2 (..), KnownNat3 (..),+ SNatKn (..), nameToSymbol) #if MIN_VERSION_ghc(8,2,0) intToNumber :: Int# -> Natural@@ -130,7 +134,7 @@ -- -- Note that additional equations are provided by the type-checker plugin solver -- "GHC.TypeLits.Extra.Solver".-type family Div (x :: Nat) (y :: Nat) :: Nat where+type family Div (dividend :: Nat) (divisor :: Nat) :: Nat where Div x 1 = x instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x y where@@ -155,12 +159,12 @@ -- | Type-level `divMod` type DivMod n d = '(Div n d, Mod n d) --- | Type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"+-- | Type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'floor' ('logBase' base value)@" -- -- Note that additional equations are provided by the type-checker plugin solver -- "GHC.TypeLits.Extra.Solver".-type family FLog (x :: Nat) (y :: Nat) :: Nat where+type family FLog (base :: Nat) (value :: Nat) :: Nat where FLog 2 1 = 0 -- Additional equations are provided by the custom solver instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''FLog) x y where@@ -170,12 +174,12 @@ natSing2 = SNatKn (intToNumber (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y)))) #endif --- | Type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"+-- | Type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' base value)@" -- -- Note that additional equations are provided by the type-checker plugin solver -- "GHC.TypeLits.Extra.Solver".-type family CLog (x :: Nat) (y :: Nat) :: Nat where+type family CLog (base :: Nat) (value :: Nat) :: Nat where CLog 2 1 = 0 -- Additional equations are provided by the custom solver instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where@@ -188,20 +192,37 @@ _ | isTrue# (z1 ==# z2) -> SNatKn (intToNumber (z1 +# 1#)) | otherwise -> SNatKn (intToNumber z1) --- | Type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- | Extended version of 'CLog', which is well-defined for the second, non-base argument being zero. The additional third argument argument is returned in this particular case.+type family CLogWZ (base :: Nat) (value :: Nat) (ifzero :: Nat) :: Nat where+ CLogWZ _ 0 z = z+ CLogWZ b v _ = CLog b v++instance (KnownNat x, KnownNat y, KnownNat z, 2 <= x) => KnownNat3 $(nameToSymbol ''CLogWZ) x y z where+ natSing3 = let x = natVal (Proxy @x)+ y = natVal (Proxy @y)+ z = natVal (Proxy @z)+ z1 = integerLogBase# x y+ z2 = integerLogBase# x (y-1)+ in case y of+ 0 -> SNatKn $ fromInteger z+ 1 -> SNatKn 0+ _ | isTrue# (z1 ==# z2) -> SNatKn (intToNumber (z1 +# 1#))+ | otherwise -> SNatKn (intToNumber z1)++-- | Type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> -- where the operation only reduces when: -- -- @--- 'FLog' b x ~ 'CLog' b x+-- 'FLog' base value ~ 'CLog' base value -- @ -- -- Additionally, the following property holds for 'Log': ----- > (b ^ (Log b x)) ~ x+-- > (base ^ (Log base value)) ~ value -- -- Note that additional equations are provided by the type-checker plugin solver -- "GHC.TypeLits.Extra.Solver".-type family Log (x :: Nat) (y :: Nat) :: Nat where+type family Log (base :: Nat) (value :: Nat) :: Nat where Log 2 1 = 0 -- Additional equations are provided by the custom solver instance (KnownNat x, KnownNat y, FLog x y ~ CLog x y) => KnownNat2 $(nameToSymbol ''Log) x y where
src/GHC/TypeLits/Extra/Solver.hs view
@@ -13,8 +13,9 @@ -} -{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE TupleSections #-}+{-# LANGUAGE TemplateHaskellQuotes #-} {-# OPTIONS_HADDOCK show-extensions #-} @@ -24,46 +25,25 @@ -- external import Control.Monad.Trans.Maybe (MaybeT (..))-import Data.Either (lefts)-import Data.Maybe (catMaybes)-import GHC.TcPluginM.Extra (evByFiat, lookupModule, lookupName,- tracePlugin)+import Data.Maybe (catMaybes) +-- ghc-tcplugin-api+import GHC.TcPlugin.API+import GHC.TcPlugin.API.TyConSubst+ -- GHC API-import FastString (fsLit)-import Module (mkModuleName)-import OccName (mkTcOcc)-import Outputable (Outputable (..), (<+>), ($$), text)-import Plugins (Plugin (..), defaultPlugin)-#if MIN_VERSION_ghc(8,6,0)-import Plugins (purePlugin)-#endif-import TcEvidence (EvTerm)-import TcPluginM (TcPluginM, tcLookupTyCon, tcPluginTrace)-import TcRnTypes (TcPlugin(..), TcPluginResult (..))-import Type (Kind, eqType)-import TyCoRep (Type (..))-import TysWiredIn (typeNatKind, promotedTrueDataCon, promotedFalseDataCon)-import TcTypeNats (typeNatLeqTyCon)-#if MIN_VERSION_ghc(8,4,0)-import GHC.TcPluginM.Extra (flattenGivens)-import TcTypeNats (typeNatTyCons)-#else-import TcPluginM (zonkCt)-import Control.Monad ((<=<))-#endif+import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon)+import GHC.Core.DataCon (dataConWrapId)+import GHC.Core.TyCo.Rep (Type (..), TyLit (..))+import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)+import GHC.Tc.Types.Constraint (isWantedCt)+import GHC.Utils.Outputable ((<+>), ($$), text, vcat) -#if MIN_VERSION_ghc(8,10,0)-import Constraint (Ct, ctEvidence, ctEvPred, isWantedCt)-import Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType)-import Type (typeKind)-#else-import TcRnTypes (Ct, ctEvidence, ctEvPred, isWantedCt)-import TcType (typeKind)-import Type (EqRel (NomEq), PredTree (EqPred), classifyPredType)-#endif+-- ghc-typelits-natnormalise+import GHC.TypeLits.Normalise.Compat -- internal+import GHC.TypeLits.Extra.Solver.Compat import GHC.TypeLits.Extra.Solver.Operations import GHC.TypeLits.Extra.Solver.Unify @@ -73,13 +53,15 @@ -- -- * 'Mod': type-level 'mod' ----- * 'FLog': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- * 'FLog': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> -- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" ----- * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> -- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" ----- * 'Log': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- * 'CLogWZ': extension of @CLog@, which returns the additional third argument in case the second argument is zero+--+-- * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> -- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" -- -- * 'GCD': a type-level 'gcd'@@ -96,143 +78,250 @@ plugin :: Plugin plugin = defaultPlugin- { tcPlugin = const $ Just normalisePlugin-#if MIN_VERSION_ghc(8,6,0)+ { tcPlugin = const (pure (mkTcPlugin normalisePlugin)) , pluginRecompile = purePlugin-#endif } normalisePlugin :: TcPlugin-normalisePlugin = tracePlugin "ghc-typelits-extra"- TcPlugin { tcPluginInit = lookupExtraDefs- , tcPluginSolve = decideEqualSOP- , tcPluginStop = const (return ())+normalisePlugin =+ TcPlugin { tcPluginInit = lookupExtraDefs+ , tcPluginSolve = decideEqualSOP+ , tcPluginRewrite = extraRewrite+ , tcPluginPostTc = const (return ())+ , tcPluginShutdown = const (return ()) } -decideEqualSOP :: ExtraDefs -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult-decideEqualSOP _ _givens _deriveds [] = return (TcPluginOk [] [])-decideEqualSOP defs givens _deriveds wanteds = do- -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out- let wanteds' = filter isWantedCt wanteds- unit_wanteds <- catMaybes <$> mapM (runMaybeT . toNatEquality defs) wanteds'+extraRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter+extraRewrite defs = listToUFM+ [ (minTyCon defs, minRewrite)+ , (maxTyCon defs, maxRewrite)+ , (flogTyCon defs, flogRewrite)+ , (clogTyCon defs, clogRewrite)+ , (clogWZTyCon defs, clogWZRewrite)+ , (logTyCon defs, logRewrite)+ , (gcdTyCon defs, gcdRewrite)+ , (lcmTyCon defs, lcmRewrite)+ ]+ where+ minRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ = pure $ rewriteTo (minTyCon defs) args $ min i j+ minRewrite _ _ = pure TcPluginNoRewrite++ maxRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ = pure $ rewriteTo (maxTyCon defs) args $ max i j+ maxRewrite _ _ = pure TcPluginNoRewrite++ flogRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ , i > 1+ , Just r <- flogBase i j+ = pure $ rewriteTo (flogTyCon defs) args r+ flogRewrite _ _ = pure TcPluginNoRewrite++ clogRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ , i > 1+ , Just r <- clogBase i j+ = pure $ rewriteTo (clogTyCon defs) args r+ clogRewrite _ _ = pure TcPluginNoRewrite++ clogWZRewrite _ args+ | [_, LitTy (NumTyLit 0), z] <- args+ = pure $ TcPluginRewriteTo (reduce (clogWZTyCon defs) args z) []+ clogWZRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j), _] <- args+ , i > 1+ , Just r <- clogBase i j+ = pure $ rewriteTo (clogWZTyCon defs) args r+ clogWZRewrite _ _ = pure TcPluginNoRewrite++ logRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ , i > 1+ , Just r <- exactLogBase i j+ = pure $ rewriteTo (logTyCon defs) args r+ logRewrite _ _ = pure TcPluginNoRewrite++ gcdRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ = pure $ rewriteTo (gcdTyCon defs) args (i `gcd` j)+ gcdRewrite _ _ = pure TcPluginNoRewrite++ lcmRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ = pure $ rewriteTo (lcmTyCon defs) args (i `lcm` j)+ lcmRewrite _ _ = pure TcPluginNoRewrite++ rewriteTo tyCon args x =+ TcPluginRewriteTo (reduce tyCon args (LitTy (NumTyLit x))) []++ reduce tc args res = Reduction co res+ where+ co = mkPluginUnivCo "ghc-typelits-extra" Nominal []+ (mkTyConApp tc args) res+++decideEqualSOP :: ExtraDefs -> [Ct] -> [Ct] -> TcPluginM 'Solve TcPluginSolveResult+decideEqualSOP _ _givens [] = return (TcPluginOk [] [])+decideEqualSOP defs givens wanteds = do+ let givensTyConSubst = mkTyConSubst givens+ unit_wanteds <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs givensTyConSubst) wanteds case unit_wanteds of [] -> return (TcPluginOk [] []) _ -> do-#if MIN_VERSION_ghc(8,4,0)- unit_givens <- catMaybes <$> mapM (runMaybeT . toNatEquality defs) (givens ++ flattenGivens givens)-#else- unit_givens <- catMaybes <$> mapM ((runMaybeT . toNatEquality defs) <=< zonkCt) givens-#endif- sr <- simplifyExtra (unit_givens ++ unit_wanteds)+ unit_givens <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs givensTyConSubst) givens+ sr <- simplifyExtra defs (unit_givens ++ unit_wanteds)+ tcPluginTrace "ghc-typelits-extra Wanteds {" $+ vcat [ text "givens:" <+> ppr givens+ , text "unit_givens" <+> ppr unit_givens+ , text $ replicate 80 '-'+ , text "wanteds:" <+> ppr wanteds+ , text "unit_wanteds:" <+> ppr unit_wanteds+ ] tcPluginTrace "normalised" (ppr sr) case sr of- Simplified evs -> return (TcPluginOk (filter (isWantedCt . snd) evs) [])- Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])+ Simplified evs new -> return (TcPluginOk (filter (isWantedCt . snd) evs) new)+ Impossible eq -> return (TcPluginContradiction [fromSolverConstraint eq]) -type NatEquality = (Ct,ExtraOp,ExtraOp)-type NatInEquality = (Ct,ExtraOp,ExtraOp,Bool)+data SolverConstraint+ = NatEquality Ct ExtraOp ExtraOp Normalised+ | NatInequality Ct [Coercion] ExtraOp ExtraOp Bool Normalised +instance Outputable SolverConstraint where+ ppr (NatEquality ct op1 op2 norm) =+ text "NatEquality" $$ ppr ct $$ ppr op1 $$ ppr op2 $$ ppr norm+ ppr (NatInequality _ _ op1 op2 b norm) =+ text "NatInequality" $$ ppr op1 $$ ppr op2 $$ ppr b $$ ppr norm+ data SimplifyResult- = Simplified [(EvTerm,Ct)]- | Impossible (Either NatEquality NatInEquality)+ = Simplified [(EvTerm,Ct)] [Ct]+ | Impossible SolverConstraint instance Outputable SimplifyResult where- ppr (Simplified evs) = text "Simplified" $$ ppr evs- ppr (Impossible eq) = text "Impossible" <+> ppr eq+ ppr (Simplified evs new) =+ text "Simplified" $$ text "Solved:" $$ ppr evs $$ text "New:" $$ ppr new+ ppr (Impossible sct) =+ text "Impossible" <+> ppr sct -simplifyExtra :: [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult-simplifyExtra eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] eqs+simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult+simplifyExtra defs eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] eqs where- simples :: [Maybe (EvTerm, Ct)] -> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult- simples evs [] = return (Simplified (catMaybes evs))- simples evs (eq@(Left (ct,u,v)):eqs') = do- ur <- unifyExtra ct u v- tcPluginTrace "unifyExtra result" (ppr ur)- case ur of- Win -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'- Lose -> if null evs && null eqs'- then return (Impossible eq)- else simples evs eqs'- Draw -> simples evs eqs'- simples evs (eq@(Right (ct,u,v,b)):eqs') = do+ simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult+ simples evs news [] = return (Simplified (catMaybes evs) news)+ simples evs news (eq@(NatEquality ct u v norm):eqs') = do+ let evM = evMagic (ordTyCons defs) ct (depsFromNormalised norm)+ -- transform: CLogWZ a b c ~ CLog a b+ -- to: 1 <= b+ -- which is equivalent by definition and try to solve that+ -- along with the rest of the eqs'+ wz = case (u, v) of+ (CLogWZ a b _, CLog a' b') | a == a' && b == b' -> Just b+ (CLog a' b', CLogWZ a b _) | a == a' && b == b' -> Just b+ _ -> Nothing+ case wz of+ Just x | isWantedCt ct -> do+ let x' = reifyEOP defs x+ one = reifyEOP defs (I 1)+ ev <- newWanted (ctLoc ct) $ mkLEqNat (ordTyCons defs) one x'+ let newCt = mkNonCanonical ev+ simples (fmap (,ct) evM:evs) (newCt:news) eqs'+ _ -> do+ ur <- unifyExtra ct u v+ tcPluginTrace "unifyExtra result" (ppr ur)+ case ur of+ Win -> simples (fmap (,ct) evM:evs) news eqs'+ Lose | null evs && null eqs' -> return (Impossible eq)+ _ | Normalised {} <- norm+ , isWantedCt ct -> do+ newCt <- createWantedFromNormalised defs eq+ simples (fmap (,ct) evM:evs) (newCt:news) eqs'+ Lose -> simples evs news eqs'+ Draw -> simples evs news eqs'+ simples evs news (eq@(NatInequality ct deps u v b norm):eqs') = do tcPluginTrace "unifyExtra leq result" (ppr (u,v,b))+ let evM = evMagic (ordTyCons defs) ct (deps <> depsFromNormalised norm) case (u,v) of (I i,I j)- | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'+ | (i <= j) == b+ -> simples (fmap (,ct) evM:evs) news eqs' | otherwise -> return (Impossible eq) (p, Max x y)- | b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'+ | b && (p == x || p == y)+ -> simples (fmap (,ct) evM:evs) news eqs' -- transform: q ~ Max x y => (p <=? q ~ True) -- to: (p <=? Max x y) ~ True -- and try to solve that along with the rest of the eqs' (p, q@(V _)) | b -> case findMax q eqs of- Just m -> simples evs ((Right (ct,p,m,b)):eqs')- Nothing -> simples evs eqs'- _ -> simples evs eqs'+ Just (i,m) ->+ simples evs news+ (NatInequality ct (i:deps) p m b norm:eqs')+ Nothing -> simples evs news eqs'+ _ | Normalised {} <- norm+ , isWantedCt ct -> do+ newCt <- createWantedFromNormalised defs eq+ simples (fmap (,ct) evM:evs) (newCt:news) eqs'+ _ -> simples evs news eqs' -- look for given constraint with the form: c ~ Max x y- findMax :: ExtraOp -> [Either NatEquality NatInEquality] -> Maybe ExtraOp- findMax c = go . lefts+ findMax :: ExtraOp -> [SolverConstraint] -> Maybe (Coercion, ExtraOp)+ findMax c = go where go [] = Nothing- go ((ct, a,b@(Max _ _)) :_)+ go ((NatEquality ct a b@(Max _ _) _) :_) | c == a && not (isWantedCt ct)- = Just b- go ((ct, a@(Max _ _),b) :_)+ = Just (ctEvCoercion (ctEvidence ct), b)+ go ((NatEquality ct a@(Max _ _) b _) :_) | c == b && not (isWantedCt ct)- = Just a+ = Just (ctEvCoercion (ctEvidence ct), a) go (_:rest) = go rest -- Extract the Nat equality constraints-toNatEquality :: ExtraDefs -> Ct -> MaybeT TcPluginM (Either NatEquality NatInEquality)-toNatEquality defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2- | isNatKind (typeKind t1) || isNatKind (typeKind t2)- -> Left <$> ((ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2)- | TyConApp tc [x,y] <- t1- , tc == typeNatLeqTyCon- , TyConApp tc' [] <- t2- -> if tc' == promotedTrueDataCon- then Right <$> ((ct,,,True) <$> normaliseNat defs x <*> normaliseNat defs y)- else if tc' == promotedFalseDataCon- then Right <$> ((ct,,,False) <$> normaliseNat defs x <*> normaliseNat defs y)- else fail "Nothing"- _ -> fail "Nothing"+toSolverConstraint :: ExtraDefs -> TyConSubst -> Ct -> MaybeT (TcPluginM 'Solve) SolverConstraint+toSolverConstraint defs givensTyConSubst ct =+ case isNatRel (ordTyCons defs) givensTyConSubst ty0 of+ Nothing -> fail "Nothing"+ Just (((t1,t2),leqM),deps) -> do+ (t1', n1) <- normaliseNat defs t1+ (t2', n2) <- normaliseNat defs t2+ case leqM of+ Nothing ->+ pure (NatEquality ct t1' t2' (mergeNormalised n1 n2))+ Just b ->+ pure (NatInequality ct deps t1' t2' b (mergeNormalised n1 n2)) where- isNatKind :: Kind -> Bool- isNatKind = (`eqType` typeNatKind)+ ty0 = ctEvPred (ctEvidence ct) -fromNatEquality :: Either NatEquality NatInEquality -> Ct-fromNatEquality (Left (ct, _, _)) = ct-fromNatEquality (Right (ct,_,_,_)) = ct+createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM 'Solve Ct+createWantedFromNormalised defs sct = do+ let extractCtSides (NatEquality ct t1 t2 _) = (ct, reifyEOP defs t1, reifyEOP defs t2)+ extractCtSides (NatInequality ct _ x y b _) =+ let t1 = mkLeqQNat (ordTyCons defs) (reifyEOP defs x) (reifyEOP defs y)+ tb = if b then promotedTrueDataCon else promotedFalseDataCon+ t2 = TyConApp tb []+ in (ct, t1, t2)+ let (ct, t1, t2) = extractCtSides sct+ newPredTy <- toLeqPredType (ordTyCons defs) ct t1 t2+ ev <- newWanted (ctLoc ct) newPredTy+ return (setCtEv ct ev) -lookupExtraDefs :: TcPluginM ExtraDefs-lookupExtraDefs = do- md <- lookupModule myModule myPackage- ExtraDefs <$> look md "Max"- <*> look md "Min"-#if MIN_VERSION_ghc(8,4,0)- <*> pure (typeNatTyCons !! 5)- <*> pure (typeNatTyCons !! 6)-#else- <*> look md "Div"- <*> look md "Mod"-#endif- <*> look md "FLog"- <*> look md "CLog"- <*> look md "Log"- <*> look md "GCD"- <*> look md "LCM"- where- look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)- myModule = mkModuleName "GHC.TypeLits.Extra"- myPackage = fsLit "ghc-typelits-extra"+fromSolverConstraint :: SolverConstraint -> Ct+fromSolverConstraint (NatEquality ct _ _ _) = ct+fromSolverConstraint (NatInequality ct _ _ _ _ _) = ct -- Utils-evMagic :: Ct -> Maybe EvTerm-evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-extra" t1 t2)- _ -> Nothing+evMagic :: LookedUpTyCons -> Ct -> [Coercion] -> Maybe EvTerm+evMagic tcs ct deps = case classifyPredType $ ctEvPred $ ctEvidence ct of+ EqPred NomEq t1 t2 ->+ let ctEv = mkPluginUnivCo "ghc-typelits-extra" Nominal deps t1 t2+ in Just (EvExpr (Coercion ctEv))+ IrredPred p ->+ let t1 = mkTyConApp (c0TyCon tcs) []+ co = mkPluginUnivCo "ghc-typelits-extra" Representational deps t1 p+ dcApp = evId (dataConWrapId (c0DataCon tcs))+ in Just (EvExpr (evCast dcApp co))+ _ -> Nothing
+ src/GHC/TypeLits/Extra/Solver/Compat.hs view
@@ -0,0 +1,101 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskellQuotes #-}++{-# OPTIONS_GHC -Wno-unused-matches #-}++module GHC.TypeLits.Extra.Solver.Compat where++import qualified Language.Haskell.TH as TH++import GHC.TcPlugin.API++import GHC.TypeLits.Normalise.Compat++import GHC.Builtin.Names+ ( eqPrimTyConKey, hasKey+ )+#if MIN_VERSION_ghc(9,1,0)+import GHC.Builtin.Types+ ( boolTy, promotedFalseDataCon, promotedTrueDataCon+ )+#endif+import GHC.Builtin.Types.Literals+ ( typeNatDivTyCon, typeNatModTyCon+ )+#if MIN_VERSION_ghc(9,8,0)+import GHC.Tc.Types.Constraint+ ( DictCt(..), EqCt(..), IrredCt(..)+ )+#endif+import GHC.Tc.Types.Constraint+ ( Ct (..), qci_ev+ )++import qualified GHC.TypeLits.Extra++data ExtraDefs = ExtraDefs+ { maxTyCon :: TyCon+ , minTyCon :: TyCon+ , divTyCon :: TyCon+ , modTyCon :: TyCon+ , flogTyCon :: TyCon+ , clogTyCon :: TyCon+ , clogWZTyCon :: TyCon+ , logTyCon :: TyCon+ , gcdTyCon :: TyCon+ , lcmTyCon :: TyCon+ , ordTyCons :: LookedUpTyCons+ }++-- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat"+lookupExtraDefs :: TcPluginM 'Init ExtraDefs+lookupExtraDefs = do+ ExtraDefs <$> look ''GHC.TypeLits.Extra.Max+ <*> look ''GHC.TypeLits.Extra.Min+ <*> pure typeNatDivTyCon+ <*> pure typeNatModTyCon+ <*> look ''GHC.TypeLits.Extra.FLog+ <*> look ''GHC.TypeLits.Extra.CLog+ <*> look ''GHC.TypeLits.Extra.CLogWZ+ <*> look ''GHC.TypeLits.Extra.Log+ <*> look ''GHC.TypeLits.Extra.GCD+ <*> look ''GHC.TypeLits.Extra.LCM+ <*> lookupTyCons+ where+ look :: TH.Name -> TcPluginM 'Init TyCon+ look nm = tcLookupTyCon =<< lookupTHName nm++setCtEv :: Ct -> CtEvidence -> Ct+setCtEv ct ev = case ct of+ CQuantCan qc -> CQuantCan (qc { qci_ev = ev})+#if MIN_VERSION_ghc(9,8,0)+ CDictCan di -> CDictCan (di { di_ev = ev})+ CIrredCan ir -> CIrredCan (ir { ir_ev = ev})+ CEqCan eq -> CEqCan (eq { eq_ev = ev})+ CNonCanonical _ -> CNonCanonical ev+#else+ ctX -> ctX { cc_ev = ev }+#endif++mkLeqQNat :: LookedUpTyCons -> Type -> Type -> Type+mkLeqQNat tcs x y =+#if MIN_VERSION_ghc(9,1,0)+ mkTyConApp (ordCondTyCon tcs)+ [ boolTy+ , mkTyConApp (cmpNatTyCon tcs) [x,y]+ , mkTyConApp promotedTrueDataCon []+ , mkTyConApp promotedTrueDataCon []+ , mkTyConApp promotedFalseDataCon []+ ]+#else+ mkTyConApp (leqQNatTyCon tcs) [x, y]+#endif++toLeqPredType :: Monad m => LookedUpTyCons -> Ct -> Type -> Type -> m PredType+toLeqPredType defs ct t1 t2 = case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of+ Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2])+#if MIN_VERSION_ghc(9,3,0)+ Just (tc, [_, b]) | tc == assertTyCon defs -> pure (mkTyConApp tc [t1,b])+#endif+ _ -> error "Impossible: neither (<=?) nor Assert"
src/GHC/TypeLits/Extra/Solver/Operations.hs view
@@ -7,10 +7,14 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE MagicHash #-}+{-# LANGUAGE LambdaCase #-} module GHC.TypeLits.Extra.Solver.Operations ( ExtraOp (..)- , ExtraDefs (..)+ , Normalised (..)+ , NormaliseResult+ , mergeNormalised+ , depsFromNormalised , reifyEOP , mergeMax , mergeMin@@ -18,10 +22,14 @@ , mergeMod , mergeFLog , mergeCLog+ , mergeCLogWZ , mergeLog , mergeGCD , mergeLCM , mergeExp+ , flogBase+ , clogBase+ , exactLogBase ) where @@ -36,26 +44,52 @@ import GHC.Integer.Logarithms (integerLogBase#) import GHC.TypeLits.Normalise.Unify (CType (..), normaliseNat, isNatural) +-- ghc-tcplugin-api+import GHC.TcPlugin.API+ -- GHC API-import Outputable (Outputable (..), (<+>), integer, text)-import TcTypeNats (typeNatExpTyCon, typeNatSubTyCon)-import TyCon (TyCon)-import Type (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy)+import GHC.Builtin.Types.Literals (typeNatExpTyCon, typeNatSubTyCon)+import GHC.Utils.Outputable ((<+>), integer, text) +-- internal+import GHC.TypeLits.Extra.Solver.Compat++-- | Indicates whether normalisation has occured+data Normalised = Normalised [Coercion] | Untouched++instance Outputable Normalised where+ ppr Normalised{} = text "Normalised"+ ppr Untouched = text "Untouched"++mergeNormalised :: Normalised -> Normalised -> Normalised+mergeNormalised (Normalised d1) (Normalised d2) = Normalised (d1 ++ d2)+mergeNormalised (Normalised d) _ = Normalised d+mergeNormalised _ (Normalised d) = Normalised d+mergeNormalised _ _ = Untouched++depsFromNormalised :: Normalised -> [Coercion]+depsFromNormalised (Normalised deps) = deps+depsFromNormalised Untouched = []++-- | A normalise result contains the ExtraOp and a flag that indicates whether any expression+-- | was normalised within the ExtraOp.+type NormaliseResult = (ExtraOp, Normalised)+ data ExtraOp- = I Integer- | V TyVar- | C CType- | Max ExtraOp ExtraOp- | Min ExtraOp ExtraOp- | Div ExtraOp ExtraOp- | Mod ExtraOp ExtraOp- | FLog ExtraOp ExtraOp- | CLog ExtraOp ExtraOp- | Log ExtraOp ExtraOp- | GCD ExtraOp ExtraOp- | LCM ExtraOp ExtraOp- | Exp ExtraOp ExtraOp+ = I Integer+ | V TyVar+ | C CType+ | Max ExtraOp ExtraOp+ | Min ExtraOp ExtraOp+ | Div ExtraOp ExtraOp+ | Mod ExtraOp ExtraOp+ | FLog ExtraOp ExtraOp+ | CLog ExtraOp ExtraOp+ | CLogWZ ExtraOp ExtraOp ExtraOp+ | Log ExtraOp ExtraOp+ | GCD ExtraOp ExtraOp+ | LCM ExtraOp ExtraOp+ | Exp ExtraOp ExtraOp deriving Eq instance Outputable ExtraOp where@@ -72,116 +106,108 @@ ppr (GCD x y) = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")" ppr (LCM x y) = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")" ppr (Exp x y) = text "Exp (" <+> ppr x <+> text "," <+> ppr y <+> text ")"--data ExtraDefs = ExtraDefs- { maxTyCon :: TyCon- , minTyCon :: TyCon- , divTyCon :: TyCon- , modTyCon :: TyCon- , flogTyCon :: TyCon- , clogTyCon :: TyCon- , logTyCon :: TyCon- , gcdTyCon :: TyCon- , lcmTyCon :: TyCon- }+ ppr (CLogWZ x y z) = text "CLogWZ " <+> text "(" <+> ppr x <+> text ","+ <+> ppr y <+> text "," <+> ppr z <+> text ")" reifyEOP :: ExtraDefs -> ExtraOp -> Type-reifyEOP _ (I i) = mkNumLitTy i-reifyEOP _ (V v) = mkTyVarTy v-reifyEOP _ (C (CType c)) = c-reifyEOP defs (Max x y) = mkTyConApp (maxTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (Min x y) = mkTyConApp (minTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (Div x y) = mkTyConApp (divTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (Mod x y) = mkTyConApp (modTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (CLog x y) = mkTyConApp (clogTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (FLog x y) = mkTyConApp (flogTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (Log x y) = mkTyConApp (logTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (GCD x y) = mkTyConApp (gcdTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (LCM x y) = mkTyConApp (lcmTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (Exp x y) = mkTyConApp typeNatExpTyCon [reifyEOP defs x- ,reifyEOP defs y]+reifyEOP defs = \case+ I i -> mkNumLitTy i+ V v -> mkTyVarTy v+ C (CType c) -> c+ Max x y -> mkTyConApp (maxTyCon defs) $ reifyEOP defs <$> [x, y]+ Min x y -> mkTyConApp (minTyCon defs) $ reifyEOP defs <$> [x, y]+ Div x y -> mkTyConApp (divTyCon defs) $ reifyEOP defs <$> [x, y]+ Mod x y -> mkTyConApp (modTyCon defs) $ reifyEOP defs <$> [x, y]+ CLog x y -> mkTyConApp (clogTyCon defs) $ reifyEOP defs <$> [x, y]+ CLogWZ x y z -> mkTyConApp (clogWZTyCon defs) $ reifyEOP defs <$> [x, y, z]+ FLog x y -> mkTyConApp (flogTyCon defs) $ reifyEOP defs <$> [x, y]+ Log x y -> mkTyConApp (logTyCon defs) $ reifyEOP defs <$> [x, y]+ GCD x y -> mkTyConApp (gcdTyCon defs) $ reifyEOP defs <$> [x, y]+ LCM x y -> mkTyConApp (lcmTyCon defs) $ reifyEOP defs <$> [x, y]+ Exp x y -> mkTyConApp typeNatExpTyCon $ reifyEOP defs <$> [x, y] -mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> ExtraOp+mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult+mergeMax _ (I 0) y = (y, Normalised [])+mergeMax _ x (I 0) = (x, Normalised []) mergeMax defs x y = let x' = reifyEOP defs x y' = reifyEOP defs y- z = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))-#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)+ (z,deps) = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))+ (z',deps') = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [x',y']))) in case runWriterT (isNatural z) of- Just (True , cs) | Set.null cs -> y- Just (False, cs) | Set.null cs -> x-#else- in case isNatural z of- Just True -> y- Just False -> x-#endif- _ -> Max x y+ Nothing -> case runWriterT (isNatural z') of+ Just (True ,cs) | Set.null cs -> (x, Normalised deps') -- x >= y+ Just (False,cs) | Set.null cs -> (y, Normalised deps') -- x < y+ _ -> (Max x y, Untouched)+ Just (True , cs) | Set.null cs -> (y, Normalised deps) -- y >= x+ Just (False, cs) | Set.null cs -> (x, Normalised deps) -- y < x+ _ -> (Max x y, Untouched) -mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> ExtraOp+mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult mergeMin defs x y = let x' = reifyEOP defs x y' = reifyEOP defs y- z = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))-#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)+ (z,deps) = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))+ (z',deps') = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [x',y']))) in case runWriterT (isNatural z) of- Just (True, cs) | Set.null cs -> x- Just (False,cs) | Set.null cs -> y-#else- in case isNatural z of- Just True -> x- Just False -> y-#endif- _ -> Min x y+ Nothing -> case runWriterT (isNatural z') of+ Just (True ,cs) | Set.null cs -> (y, Normalised deps') -- x >= y+ Just (False,cs) | Set.null cs -> (x, Normalised deps') -- x < y+ _ -> (Min x y, Untouched)+ Just (True, cs) | Set.null cs -> (x, Normalised deps) -- y >= x+ Just (False,cs) | Set.null cs -> (y, Normalised deps) -- y < x+ _ -> (Min x y, Untouched) -mergeDiv :: ExtraOp -> ExtraOp -> Maybe ExtraOp+mergeDiv :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeDiv _ (I 0) = Nothing-mergeDiv (I i) (I j) = Just (I (div i j))-mergeDiv x y = Just (Div x y)+mergeDiv (I i) (I j) = Just (I (div i j), Normalised [])+mergeDiv x y = Just (Div x y, Untouched) -mergeMod :: ExtraOp -> ExtraOp -> Maybe ExtraOp+mergeMod :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeMod _ (I 0) = Nothing-mergeMod (I i) (I j) = Just (I (mod i j))-mergeMod x y = Just (Mod x y)+mergeMod (I i) (I j) = Just (I (mod i j), Normalised [])+mergeMod x y = Just (Mod x y, Untouched) -mergeFLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp+mergeFLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeFLog (I i) _ | i < 2 = Nothing-mergeFLog i (Exp j k) | i == j = Just k-mergeFLog (I i) (I j) = I <$> flogBase i j-mergeFLog x y = Just (FLog x y)+mergeFLog i (Exp j k) | i == j = Just (k, Normalised [])+mergeFLog (I i) (I j) = fmap (\r -> (I r, Normalised [])) (flogBase i j)+mergeFLog x y = Just (FLog x y, Untouched) -mergeCLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp+mergeCLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeCLog (I i) _ | i < 2 = Nothing-mergeCLog i (Exp j k) | i == j = Just k-mergeCLog (I i) (I j) = I <$> clogBase i j-mergeCLog x y = Just (CLog x y)+mergeCLog i (Exp j k) | i == j = Just (k, Normalised [])+mergeCLog (I i) (I j) = fmap (\r -> (I r, Normalised [])) (clogBase i j)+mergeCLog x y = Just (CLog x y, Untouched) -mergeLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp+mergeCLogWZ :: ExtraOp -> ExtraOp -> ExtraOp -> Maybe NormaliseResult+mergeCLogWZ (I i) _ _ | i < 2 = Nothing+mergeCLogWZ _ (I 0) z = Just (z, Normalised [])+mergeCLogWZ i (Exp j k) _ | i == j = Just (k, Normalised [])+-- CLogWZ a b c = CLog a b for all b > 0 by definition, hence we can+-- elide one layer of constructor applications in this particular case+mergeCLogWZ x y@(I _) _ = do (res, _) <- mergeCLog x y+ pure (res, Normalised [])+mergeCLogWZ x y z = Just (CLogWZ x y z, Untouched)++mergeLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeLog (I i) _ | i < 2 = Nothing-mergeLog b (Exp b' y) | b == b' = Just y-mergeLog (I i) (I j) = I <$> exactLogBase i j-mergeLog x y = Just (Log x y)+mergeLog b (Exp b' y) | b == b' = Just (y, Normalised [])+mergeLog (I i) (I j) = fmap (\r -> (I r, Normalised [])) (exactLogBase i j)+mergeLog x y = Just (Log x y, Untouched) -mergeGCD :: ExtraOp -> ExtraOp -> ExtraOp-mergeGCD (I i) (I j) = I (gcd i j)-mergeGCD x y = GCD x y+mergeGCD :: ExtraOp -> ExtraOp -> NormaliseResult+mergeGCD (I i) (I j) = (I (gcd i j), Normalised [])+mergeGCD x y = (GCD x y, Untouched) -mergeLCM :: ExtraOp -> ExtraOp -> ExtraOp-mergeLCM (I i) (I j) = I (lcm i j)-mergeLCM x y = LCM x y+mergeLCM :: ExtraOp -> ExtraOp -> NormaliseResult+mergeLCM (I i) (I j) = (I (lcm i j), Normalised [])+mergeLCM x y = (LCM x y, Untouched) -mergeExp :: ExtraOp -> ExtraOp -> ExtraOp-mergeExp (I i) (I j) = I (i^j)-mergeExp b (Log b' y) | b == b' = y-mergeExp x y = Exp x y+mergeExp :: ExtraOp -> ExtraOp -> NormaliseResult+mergeExp (I i) (I j) = (I (i^j), Normalised [])+mergeExp b (Log b' y) | b == b' = (y, Normalised [])+mergeExp x y = (Exp x y, Untouched) -- | \x y -> logBase x y, x > 1 && y > 0 flogBase :: Integer -> Integer -> Maybe Integer
src/GHC/TypeLits/Extra/Solver/Unify.hs view
@@ -5,11 +5,12 @@ Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> -} -{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-} module GHC.TypeLits.Extra.Solver.Unify- ( ExtraDefs (..)- , UnifyResult (..)+ ( UnifyResult (..)+ , NormaliseResult , normaliseNat , unifyExtra )@@ -18,69 +19,106 @@ -- external import Control.Monad.Trans.Class (lift) import Control.Monad.Trans.Maybe (MaybeT (..))-import Control.Monad.Trans.Writer.Strict (runWriter)+import Data.Maybe (catMaybes) import Data.Function (on) import GHC.TypeLits.Normalise.Unify (CType (..))-import qualified GHC.TypeLits.Normalise.Unify as Normalise --- GHC API-import Outputable (Outputable (..), ($$), text)-import TcPluginM (TcPluginM, matchFam, tcPluginTrace)-import TcTypeNats (typeNatExpTyCon)-import Type (TyVar, coreView)-import TyCoRep (Type (..), TyLit (..))-import UniqSet (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)+-- ghc-tcplugin-api+import GHC.TcPlugin.API -#if MIN_VERSION_ghc(8,10,0)-import Constraint (Ct)-#else-import TcRnMonad (Ct)-#endif+-- GHC API+import GHC.Builtin.Types.Literals (typeNatExpTyCon)+import GHC.Core.TyCo.Rep (Type (..), TyLit (..))+import GHC.Core.Type (coreView)+import GHC.Types.Unique.Set (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)+import GHC.Utils.Outputable (($$), text) -- internal+import GHC.TypeLits.Extra.Solver.Compat import GHC.TypeLits.Extra.Solver.Operations -normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp-normaliseNat defs ty | Just ty1 <- coreView ty = normaliseNat defs ty1-normaliseNat _ (TyVarTy v) = pure (V v)-normaliseNat _ (LitTy (NumTyLit i)) = pure (I i)-normaliseNat defs (TyConApp tc [x,y])- | tc == maxTyCon defs = mergeMax defs <$> normaliseNat defs x- <*> normaliseNat defs y- | tc == minTyCon defs = mergeMin defs <$> normaliseNat defs x- <*> normaliseNat defs y- | tc == divTyCon defs = do x' <- normaliseNat defs x- y' <- normaliseNat defs y- MaybeT (return (mergeDiv x' y'))- | tc == modTyCon defs = do x' <- normaliseNat defs x- y' <- normaliseNat defs y- MaybeT (return (mergeMod x' y'))- | tc == flogTyCon defs = do x' <- normaliseNat defs x- y' <- normaliseNat defs y- MaybeT (return (mergeFLog x' y'))- | tc == clogTyCon defs = do x' <- normaliseNat defs x- y' <- normaliseNat defs y- MaybeT (return (mergeCLog x' y'))- | tc == logTyCon defs = do x' <- normaliseNat defs x- y' <- normaliseNat defs y- MaybeT (return (mergeLog x' y'))- | tc == gcdTyCon defs = mergeGCD <$> normaliseNat defs x- <*> normaliseNat defs y- | tc == lcmTyCon defs = mergeLCM <$> normaliseNat defs x- <*> normaliseNat defs y- | tc == typeNatExpTyCon = mergeExp <$> normaliseNat defs x- <*> normaliseNat defs y+mergeNormResWith+ :: (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)+ -> MaybeT (TcPluginM 'Solve) NormaliseResult+ -> MaybeT (TcPluginM 'Solve) NormaliseResult+ -> MaybeT (TcPluginM 'Solve) NormaliseResult+mergeNormResWith f x y = do+ (x', n1) <- x+ (y', n2) <- y+ (res, n3) <- f x' y'+ pure (res, n1 `mergeNormalised` n2 `mergeNormalised` n3) -normaliseNat defs (TyConApp tc tys) = do- tys' <- mapM (fmap (reifyEOP defs) . normaliseNat defs) tys- tyM <- lift (matchFam tc tys')- case tyM of- Just (_,ty) -> normaliseNat defs ty- _ -> let q = fst (runWriter (Normalise.normaliseNat (TyConApp tc tys)))- in return (C (CType (Normalise.reifySOP q))) -normaliseNat _ t = return (C (CType t))+normaliseNat :: ExtraDefs -> Type -> MaybeT (TcPluginM 'Solve) NormaliseResult+normaliseNat defs = go+ where+ go :: Type -> MaybeT (TcPluginM 'Solve) NormaliseResult+ go ty | Just ty1 <- coreView ty = go ty1+ go (TyVarTy v) = pure (V v, Untouched)+ go (LitTy (NumTyLit i)) = pure (I i, Untouched) + go (TyConApp tc [x,y])+ | tc == maxTyCon defs+ = mergeNormResWith (\x' y' -> return (mergeMax defs x' y'))+ (go x)+ (go y)+ | tc == minTyCon defs+ = mergeNormResWith (\x' y' -> return (mergeMin defs x' y'))+ (go x)+ (go y)+ | tc == divTyCon defs+ = mergeNormResWith (\x' y' -> MaybeT (return (mergeDiv x' y')))+ (go x)+ (go y)+ | tc == modTyCon defs+ = mergeNormResWith (\x' y' -> MaybeT (return (mergeMod x' y')))+ (go x)+ (go y)+ | tc == flogTyCon defs+ = mergeNormResWith (\x' y' -> MaybeT (return (mergeFLog x' y')))+ (go x)+ (go y)+ | tc == clogTyCon defs+ = mergeNormResWith (\x' y' -> MaybeT (return (mergeCLog x' y')))+ (go x)+ (go y)+ | tc == logTyCon defs+ = mergeNormResWith (\x' y' -> MaybeT (return (mergeLog x' y')))+ (go x)+ (go y)+ | tc == gcdTyCon defs+ = mergeNormResWith (\x' y' -> return (mergeGCD x' y'))+ (go x)+ (go y)+ | tc == lcmTyCon defs+ = mergeNormResWith (\x' y' -> return (mergeLCM x' y'))+ (go x)+ (go y)+ | tc == typeNatExpTyCon+ = mergeNormResWith (\x' y' -> return (mergeExp x' y'))+ (go x)+ (go y)++ go (TyConApp tc [x,y,z])+ | tc == clogWZTyCon defs+ = do (x', n1) <- normaliseNat defs x+ (y', n2) <- normaliseNat defs y+ (z', n3) <- normaliseNat defs z+ (res, n4) <- MaybeT $ return $ mergeCLogWZ x' y' z'+ pure (res, foldl mergeNormalised Untouched [n1,n2,n3,n4])++ go (TyConApp tc tys) = do+ let mergeExtraOp [] = []+ mergeExtraOp ((Just (op, Normalised []), _):xs) = reifyEOP defs op:mergeExtraOp xs+ mergeExtraOp ((_, ty):xs) = ty:mergeExtraOp xs++ normResults <- lift (sequence (runMaybeT . go <$> tys))+ let anyNormalised = foldr mergeNormalised Untouched (snd <$> catMaybes normResults)+ let tys' = mergeExtraOp (zip normResults tys)+ pure (C (CType (TyConApp tc tys')), anyNormalised)++ go t = return (C (CType t), Untouched)+ -- | Result of comparing two 'SOP' terms, returning a potential substitution -- list under which the two terms are equal. data UnifyResult@@ -93,7 +131,7 @@ ppr Lose = text "Lose" ppr Draw = text "Draw" -unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult+unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM 'Solve UnifyResult unifyExtra ct u v = do tcPluginTrace "unifyExtra" (ppr ct $$ ppr u $$ ppr v) return (unifyExtra' u v)@@ -121,34 +159,37 @@ commuteResult _ _ = Draw fvOP :: ExtraOp -> UniqSet TyVar-fvOP (I _) = emptyUniqSet-fvOP (V v) = unitUniqSet v-fvOP (C _) = emptyUniqSet-fvOP (Max x y) = fvOP x `unionUniqSets` fvOP y-fvOP (Min x y) = fvOP x `unionUniqSets` fvOP y-fvOP (Div x y) = fvOP x `unionUniqSets` fvOP y-fvOP (Mod x y) = fvOP x `unionUniqSets` fvOP y-fvOP (FLog x y) = fvOP x `unionUniqSets` fvOP y-fvOP (CLog x y) = fvOP x `unionUniqSets` fvOP y-fvOP (Log x y) = fvOP x `unionUniqSets` fvOP y-fvOP (GCD x y) = fvOP x `unionUniqSets` fvOP y-fvOP (LCM x y) = fvOP x `unionUniqSets` fvOP y-fvOP (Exp x y) = fvOP x `unionUniqSets` fvOP y+fvOP (I _) = emptyUniqSet+fvOP (V v) = unitUniqSet v+fvOP (C _) = emptyUniqSet+fvOP (Max x y) = fvOP x `unionUniqSets` fvOP y+fvOP (Min x y) = fvOP x `unionUniqSets` fvOP y+fvOP (Div x y) = fvOP x `unionUniqSets` fvOP y+fvOP (Mod x y) = fvOP x `unionUniqSets` fvOP y+fvOP (FLog x y) = fvOP x `unionUniqSets` fvOP y+fvOP (CLog x y) = fvOP x `unionUniqSets` fvOP y+fvOP (CLogWZ x y z) = fvOP x `unionUniqSets` fvOP y `unionUniqSets` fvOP z+fvOP (Log x y) = fvOP x `unionUniqSets` fvOP y+fvOP (GCD x y) = fvOP x `unionUniqSets` fvOP y+fvOP (LCM x y) = fvOP x `unionUniqSets` fvOP y+fvOP (Exp x y) = fvOP x `unionUniqSets` fvOP y eqFV :: ExtraOp -> ExtraOp -> Bool eqFV = (==) `on` fvOP containsConstants :: ExtraOp -> Bool-containsConstants (I _) = False-containsConstants (V _) = False-containsConstants (C _) = True-containsConstants (Max x y) = containsConstants x || containsConstants y-containsConstants (Min x y) = containsConstants x || containsConstants y-containsConstants (Div x y) = containsConstants x || containsConstants y-containsConstants (Mod x y) = containsConstants x || containsConstants y-containsConstants (FLog x y) = containsConstants x || containsConstants y-containsConstants (CLog x y) = containsConstants x || containsConstants y-containsConstants (Log x y) = containsConstants x || containsConstants y-containsConstants (GCD x y) = containsConstants x || containsConstants y-containsConstants (LCM x y) = containsConstants x || containsConstants y-containsConstants (Exp x y) = containsConstants x || containsConstants y+containsConstants = \case+ I _ -> False+ V _ -> False+ C _ -> True+ Max x y -> or $ containsConstants <$> [x, y]+ Min x y -> or $ containsConstants <$> [x, y]+ Div x y -> or $ containsConstants <$> [x, y]+ Mod x y -> or $ containsConstants <$> [x, y]+ FLog x y -> or $ containsConstants <$> [x, y]+ CLog x y -> or $ containsConstants <$> [x, y]+ CLogWZ x y z -> or $ containsConstants <$> [x, y, z]+ Log x y -> or $ containsConstants <$> [x, y]+ GCD x y -> or $ containsConstants <$> [x, y]+ LCM x y -> or $ containsConstants <$> [x, y]+ Exp x y -> or $ containsConstants <$> [x, y]
− tests/ErrorTests.hs
@@ -1,217 +0,0 @@-{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-}-#if __GLASGOW_HASKELL__ >= 805-{-# LANGUAGE NoStarIsType #-}-#endif-{-# OPTIONS_GHC -fdefer-type-errors #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}--module ErrorTests where--import Data.Proxy-import GHC.TypeLits-import GHC.TypeLits.Extra--testFail1 :: Proxy (GCD 6 8) -> Proxy 4-testFail1 = id--testFail2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9))-testFail2 = id--testFail3 :: Proxy (CLog 3 10) -> Proxy 2-testFail3 = id--testFail4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9))-testFail4 = id--testFail5 :: Proxy (CLog 0 4) -> Proxy 100-testFail5 = id--testFail6 :: Proxy (CLog 1 4) -> Proxy 100-testFail6 = id--testFail7 :: Proxy (CLog 4 0) -> Proxy 0-testFail7 = id--testFail8 :: Proxy (CLog 1 (1^y)) -> Proxy y-testFail8 = id--testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y-testFail9 = id--testFail10 :: Integer-testFail10 = natVal (Proxy :: Proxy (CLog 1 4))--testFail11 :: Integer-testFail11 = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4)))--testFail12 :: Proxy (Div 4 0) -> Proxy 4-testFail12 = id--testFail13 :: Proxy (Mod 4 0) -> Proxy 4-testFail13 = id--testFail14 :: Proxy (FLog 0 4) -> Proxy 100-testFail14 = id--testFail15 :: Proxy (FLog 1 4) -> Proxy 100-testFail15 = id--testFail16 :: Proxy (FLog 4 0) -> Proxy 0-testFail16 = id--testFail17 :: Proxy (LCM 6 8) -> Proxy 48-testFail17 = id--testFail18 :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9))-testFail18 = id--testFail19 :: Integer-testFail19 = natVal (Proxy :: Proxy (Log 3 0))--testFail20 :: Integer-testFail20 = natVal (Proxy :: Proxy (Log 3 10))--testFail21 :: Proxy a -> Proxy b -> Proxy (Min a (a*b)) -> Proxy a-testFail21 _ _ = id--testFail22 :: Proxy a -> Proxy b -> Proxy (Max a (a*b)) -> Proxy (a*b)-testFail22 _ _ = id--testFail23' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> ()-testFail23' _ _ = ()--testFail23 :: ()-testFail23 = testFail23' (Proxy @18) (Proxy @3)--testFail24 :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True-testFail24 _ _ _ = id--testFail25 :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True-testFail25 _ _ = id---- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true.-testFail26' :: ((x <=? n) ~ True) => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n-testFail26' _ _ _ = id--testFail26 = testFail26' (Proxy @4) (Proxy @6) (Proxy @6)--testFail1Errors =- ["Expected type: Proxy (GCD 6 8) -> Proxy 4"- ,"Actual type: Proxy 4 -> Proxy 4"- ]--testFail2Errors =- ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"- ,"Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)"- ]--testFail3Errors =- ["Expected type: Proxy (CLog 3 10) -> Proxy 2"- ,"Actual type: Proxy 2 -> Proxy 2"- ]--testFail4Errors =- ["Expected type: Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"- ,"Actual type: Proxy (x + CLog 2 9) -> Proxy (x + CLog 2 9)"- ]--testFail5Errors =- ["Expected type: Proxy (CLog 0 4) -> Proxy 100"- ,"Actual type: Proxy 100 -> Proxy 100"- ]--testFail6Errors =- ["Expected type: Proxy (CLog 1 4) -> Proxy 100"- ,"Actual type: Proxy 100 -> Proxy 100"- ]--testFail7Errors =- ["Expected type: Proxy (CLog 4 0) -> Proxy 0"- ,"Actual type: Proxy 0 -> Proxy 0"- ]--testFail8Errors =- ["Expected type: Proxy (CLog 1 (1 ^ y)) -> Proxy y"- ,"Actual type: Proxy y -> Proxy y"- ]--testFail9Errors =- ["Expected type: Proxy (CLog 0 (0 ^ y)) -> Proxy y"- ,"Actual type: Proxy y -> Proxy y"- ]--testFail10Errors =- ["Couldn't match type ‘'False’ with ‘'True’"]--testFail11Errors =- ["Couldn't match type ‘CLog 2 4 <=? CLog 4 4’ with ‘'True’"]--testFail12Errors =- ["Expected type: Proxy (Div 4 0) -> Proxy 4"- ,"Actual type: Proxy 4 -> Proxy 4"- ]--testFail13Errors =- ["Expected type: Proxy (Mod 4 0) -> Proxy 4"- ,"Actual type: Proxy 4 -> Proxy 4"- ]--testFail14Errors =- ["Expected type: Proxy (FLog 0 4) -> Proxy 100"- ,"Actual type: Proxy 100 -> Proxy 100"- ]--testFail15Errors =- ["Expected type: Proxy (FLog 1 4) -> Proxy 100"- ,"Actual type: Proxy 100 -> Proxy 100"- ]--testFail16Errors =- ["Expected type: Proxy (FLog 4 0) -> Proxy 0"- ,"Actual type: Proxy 0 -> Proxy 0"- ]--testFail17Errors =- ["Expected type: Proxy (LCM 6 8) -> Proxy 48"- ,"Actual type: Proxy 48 -> Proxy 48"- ]--testFail18Errors =- ["Expected type: Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"- ,"Actual type: Proxy (x + LCM 6 9) -> Proxy (x + LCM 6 9)"- ]--testFail19Errors =- ["Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"]--testFail20Errors =- ["Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"]--testFail21Errors =- ["Expected type: Proxy (Min a (a * b)) -> Proxy a"- ,"Actual type: Proxy a -> Proxy a"- ]--testFail22Errors =- ["Expected type: Proxy (Max a (a * b)) -> Proxy (a * b)"- ,"Actual type: Proxy (a * b) -> Proxy (a * b)"]--testFail23Errors =-#if __GLASGOW_HASKELL__ >= 804- ["Couldn't match type ‘'True’ with ‘'False’"]-#else- ["Couldn't match type ‘1 <=? Div 18 3’ with ‘'False’"]-#endif--testFail24Errors =- ["Couldn't match type ‘z <=? Max x y’ with ‘'True’"]--testFail25Errors =- ["Couldn't match type ‘(x + 1) <=? Max x y’ with ‘'True’"]--testFail26Errors =- ["Could not deduce: Max x y ~ n"- ,"from the context: (x <=? n) ~ 'True"- ]
tests/Main.hs view
@@ -2,22 +2,32 @@ #if __GLASGOW_HASKELL__ >= 805 {-# LANGUAGE NoStarIsType #-} #endif++#if __GLASGOW_HASKELL__ >= 904+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}+#endif {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}+#if __GLASGOW_HASKELL__ < 904 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}+#endif -import Data.List (isInfixOf)+-- Even though binders are not used, they're compiled and that's what we're after.+{-# OPTIONS_GHC -Wno-unused-top-binds #-}++-- Only applies to old GHCs.+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}+ import Data.Proxy-import Data.Type.Bool-import Control.Exception+import Data.Type.Equality import Test.Tasty import Test.Tasty.HUnit -import ErrorTests- import GHC.TypeLits import GHC.TypeLits.Extra +import qualified ShouldError+ test1 :: Proxy (GCD 6 8) -> Proxy 2 test1 = id @@ -132,7 +142,7 @@ test38 :: Proxy (Min (0-1) 0) -> Proxy (0-1) test38 = id -test39 :: Proxy (Max (0-1) 0) -> Proxy 0+test39 :: Proxy (Max (0-1) 0) -> Proxy (0-1) test39 = id test40 :: Proxy x -> Proxy y -> Proxy (Max x y) -> Proxy (Max y x)@@ -183,6 +193,97 @@ -> Proxy (2+((2^n)*2)) test51 _ = id +type family BitPack a :: Nat++test52+ :: Proxy a+ -> Proxy (1 + BitPack a)+ -> Proxy (Max 0 (BitPack a) + CLog 2 2)+test52 _ = id++test53+ :: Proxy n+ -> Proxy (1 <=? Max (n + 1) 1)+ -> Proxy True+test53 _ = id++test54+ :: Proxy n+ -> Proxy (n <=? Max (n + 1) 1)+ -> Proxy True+test54 _ = id++test55+ :: Proxy n+ -> Proxy (n + 1 <=? Max (n + 1) 1)+ -> Proxy True+test55 _ = id++test56+ :: Proxy n+ -> Proxy p+ -> Proxy (n <=? Max (n + p) p)+ -> Proxy True+test56 _ _ = id++test57+ :: Proxy n+ -> Proxy p+ -> Proxy (n + 1 <=? Max (n + p + 1) p)+ -> Proxy True+test57 _ _ = id++test58a+ :: 1 <= n+ => Proxy n+ -> Proxy n+test58a = id++test58b+ :: Proxy n+ -> Proxy (Max (n+2) 1)+ -> Proxy (Max (n+2) 1)+test58b _ = test58a++test59 :: Proxy (CLogWZ 3 10 9) -> Proxy 3+test59 = id++test60 :: Proxy ((CLogWZ 3 10 3) + x) -> Proxy (x + (CLogWZ 2 7 8))+test60 = id++test61 :: Proxy (CLogWZ x (x^y) 8) -> Proxy y+test61 = id++test62 :: Integer+test62 = natVal (Proxy :: Proxy (CLogWZ 6 8 3))++test63 :: Integer+test63 = natVal (Proxy :: Proxy (CLogWZ 3 10 9))++test64 :: Integer+test64 = natVal (Proxy :: Proxy ((CLogWZ 2 4 11) * (3 ^ (CLogWZ 2 4 8))))++test65 :: Integer+test65 = natVal (Proxy :: Proxy (Max (CLogWZ 2 4 8) (CLogWZ 4 20 5)))++test66 :: Proxy (CLogWZ 3 0 8) -> Proxy 8+test66 = id++test67 :: Proxy (CLogWZ 2 0 x) -> Proxy x+test67 = id++test68 :: Proxy (CLogWZ 5 0 0) -> Proxy 0+test68 = id++test69 :: 1 <= n => Proxy n -> Proxy (CLogWZ 2 n 0) -> Proxy (CLog 2 n)+test69 _ = id++-- Regression test for: https://github.com/clash-lang/ghc-typelits-extra/issues/73+test70 :: (CLog 2 n ~ CLogWZ 2 n 0) => Proxy n -> Proxy n+test70 _ =+ case (Refl :: Max (n + 1) 1 :~: (1 + n)) of+ Refl -> Proxy+ main :: IO () main = defaultMain tests @@ -303,7 +404,7 @@ , testCase "Min (0-1) 0 ~ (0-1)" $ show (test38 Proxy) @?= "Proxy"- , testCase "Max (0-1) 0 ~ 0" $+ , testCase "Max (0-1) 0 ~ (0-1)" $ show (test39 Proxy) @?= "Proxy" , testCase "forall x y . Max x y ~ Max y x" $@@ -342,52 +443,60 @@ , testCase "forall n . Max (((2 ^ n) + 1) + ((2 ^ n) + 1)) 1 ~ 2 + ((2 ^ n) * 2)" $ show (test51 Proxy Proxy) @?= "Proxy"- ]- , testGroup "errors"- [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors- , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail2 `throws` testFail2Errors- , testCase "CLog 3 10 /~ 2" $ testFail3 `throws` testFail3Errors- , testCase "CLog 3 10 + x /~ x + CLog 2 9" $ testFail4 `throws` testFail4Errors- , testCase "CLog 0 4 /~ 100" $ testFail5 `throws` testFail5Errors- , testCase "CLog 1 4 /~ 100" $ testFail5 `throws` testFail5Errors- , testCase "CLog 4 0 /~ 0" $ testFail7 `throws` testFail7Errors- , testCase "CLog 1 (1^y) /~ y" $ testFail8 `throws` testFail8Errors- , testCase "CLog 0 (0^y) /~ y" $ testFail9 `throws` testFail9Errors- , testCase "No instance (KnownNat (CLog 1 4))" $ testFail10 `throws` testFail10Errors- , testCase "No instance (KnownNat (CLog 4 4 - CLog 2 4))" $ testFail11 `throws` testFail11Errors- , testCase "Div 4 0 /~ 4" $ testFail12 `throws` testFail12Errors- , testCase "Mod 4 0 /~ 4" $ testFail13 `throws` testFail13Errors- , testCase "FLog 0 4 /~ 100" $ testFail14 `throws` testFail14Errors- , testCase "FLog 1 4 /~ 100" $ testFail15 `throws` testFail15Errors- , testCase "FLog 4 0 /~ 0" $ testFail16 `throws` testFail16Errors- , testCase "GCD 6 8 /~ 4" $ testFail17 `throws` testFail17Errors- , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail18 `throws` testFail18Errors- , testCase "No instance (KnownNat (Log 3 0))" $ testFail19 `throws` testFail19Errors- , testCase "No instance (KnownNat (Log 3 10))" $ testFail20 `throws` testFail20Errors- , testCase "Min a (a*b) /~ a" $ testFail21 `throws` testFail21Errors- , testCase "Max a (a*b) /~ (a*b)" $ testFail22 `throws` testFail22Errors- , testCase "(1 <=? Div 18 6) ~ False" $ testFail23 `throws` testFail23Errors- , testCase "(z <=? Max x y) /~ True" $ testFail24 `throws` testFail24Errors- , testCase "(x+1 <=? Max x y) /~ True" $ testFail25 `throws` testFail25Errors- , testCase "(x <= n) /=> (Max x y) ~ n" $ testFail26 `throws` testFail26Errors+ , testCase "forall a . (1 + BitPack a) ~ (Max 0 (BitPack a) + CLog 2 2" $+ show (test52 Proxy Proxy) @?=+ "Proxy"+ , testCase "forall n . 1 <= Max (n + 1) 1" $+ show (test53 Proxy Proxy) @?=+ "Proxy"+ , testCase "forall n . n <= Max (n + 1) 1" $+ show (test54 Proxy Proxy) @?=+ "Proxy"+ , testCase "forall n . n + 1 <= Max (n + 1) 1" $+ show (test55 Proxy Proxy) @?=+ "Proxy"+ , testCase "forall n p . n <= Max (n + p) p" $+ show (test56 Proxy Proxy Proxy) @?=+ "Proxy"+ , testCase "forall n p . n + 1 <= Max (n + p + 1) p" $+ show (test57 Proxy Proxy Proxy) @?=+ "Proxy"+ , testCase "CLogWZ 3 10 9 ~ 3" $+ show (test59 Proxy) @?=+ "Proxy"+ , testCase "forall x . CLogWZ 3 10 3 + x ~ x + CLogWZ 2 7 8" $+ show (test60 Proxy) @?=+ "Proxy"+ , testCase "forall x>1 . CLogWZ x (x^y) 8 ~ y" $+ show (test61 Proxy) @?=+ "Proxy"+ , testCase "KnownNat (CLogWZ 6 8 3) ~ 2" $+ show test62 @?=+ "2"+ , testCase "KnownNat (CLogWZ 3 10 9) ~ 3" $+ show test63 @?=+ "3"+ , testCase "KnownNat ((CLogWZ 2 4 11) * (3 ^ (CLogWZ 2 4 8)))) ~ 18" $+ show test64 @?=+ "18"+ , testCase "KnownNat (Max (CLogWZ 2 4 8) (CLogWZ 4 20 5)) ~ 3" $+ show test65 @?=+ "3"+ , testCase "CLogWZ 3 0 8 ~ 8" $+ show (test66 Proxy) @?=+ "Proxy"+ , testCase "forall x. CLogWZ 2 0 x ~ x" $+ show (test67 Proxy) @?=+ "Proxy"+ , testCase "CLogWZ 5 0 0 ~ 0" $+ show (test68 Proxy) @?=+ "Proxy"+ , testCase "1 <= n => CLogWZ 2 n 0 ~ CLog 2 n" $+ show (test69 (Proxy :: Proxy 3) Proxy) @?=+ "Proxy"+ , testCase "CLogWZ ~ CLog given does not loop" $+ show (test70 (Proxy :: Proxy 1)) @?=+ "Proxy" ]+ , ShouldError.tests ]---- | Assert that evaluation of the first argument (to WHNF) will throw--- an exception whose string representation contains the given--- substrings.-throws :: a -> [String] -> Assertion-throws v xs = do- result <- try (evaluate v)- case result of- Right _ -> assertFailure "No exception!"- Left (TypeError msg) ->- if all (`isInfixOf` (removeProblemChars msg)) $ map removeProblemChars xs- then return ()- else assertFailure msg---- The kind and amount of quotes in GHC error messages changes depending on--- whether or not our locale supports unicode.--- Remove the problematic characters to enable comparison of errors.-removeProblemChars = filter (`notElem` problemChars)- where problemChars = "‘’`'"
+ tests/ShouldError.hs view
@@ -0,0 +1,574 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TemplateHaskell #-}++module ShouldError (tests) where++import Data.String.Interpolate (i)+import ShouldError.Tasty (assertCompileError)+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.HUnit (testCase)++tests :: TestTree+tests = testGroup "ShouldError"+ [ test1+ , test2+ , test3+ , test4+ , test5+ , test6+ , test7+ , test8+ , test9+ , test10+ , test11+ , test12+ , test13+ , test14+ , test15+ , test16+ , test17+ , test18+ , test19+ , test20+ , test21+ , test22+ , test23+ , test24+ , test25+ , test26+ , test27+ , test28+ ]++preamble :: String+preamble = [i|+import Data.Proxy+import GHC.TypeLits+import GHC.TypeLits.Extra+|] <> "\n"++source1 :: String+source1 = preamble <> [i|+test :: Proxy (GCD 6 8) -> Proxy 4+test = id+|]++expected1 :: [String]+expected1 =+ ["Proxy (GCD 6 8) -> Proxy 4"+ ,"Proxy 4 -> Proxy 4"+ ]++test1 :: TestTree+test1 = testCase "GCD 6 8 /~ 4" $ assertCompileError source1 expected1++source2 :: String+source2 = preamble <> [i|+test :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9))+test = id+|]++expected2 :: [String]+expected2 =+#if __GLASGOW_HASKELL__ >= 904+ ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"+ ,"Proxy (2 + x) -> Proxy (2 + x)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"+ ,"Proxy (GCD 6 8 + x) -> Proxy (GCD 6 8 + x)"+ ]+#else+ ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"+ ,"Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)"+ ]+#endif++test2 :: TestTree+test2 = testCase "GCD 6 8 + x /~ x + GCD 9 6" $ assertCompileError source2 expected2++source3 :: String+source3 = preamble <> [i|+test :: Proxy (CLog 3 10) -> Proxy 2+test = id+|]++expected3 :: [String]+expected3 =+ ["Proxy (CLog 3 10) -> Proxy 2"+ ,"Proxy 2 -> Proxy 2"+ ]++test3 :: TestTree+test3 = testCase "CLog 3 10 /~ 2" $ assertCompileError source3 expected3++source4 :: String+source4 = preamble <> [i|+test :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9))+test = id+|]++expected4 :: [String]+expected4 =+#if __GLASGOW_HASKELL__ >= 904+ ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"+ ,"Proxy (3 + x) -> Proxy (3 + x)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"+ ,"Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)"+ ]+#else+ ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"+ ,"Proxy (x + CLog 2 9) -> Proxy (x + CLog 2 9)"+ ]+#endif++test4 :: TestTree+test4 = testCase "CLog 3 10 + x /~ x + CLog 2 10" $ assertCompileError source4 expected4++source5 :: String+source5 = preamble <> [i|+test :: Proxy (CLog 0 4) -> Proxy 100+test = id+|]++expected5 :: [String]+expected5 =+ ["Proxy (CLog 0 4) -> Proxy 100"+ ,"Proxy 100 -> Proxy 100"+ ]++test5 :: TestTree+test5 = testCase "CLog 0 4 /~ 100" $ assertCompileError source5 expected5++source6 :: String+source6 = preamble <> [i|+test :: Proxy (CLog 1 4) -> Proxy 100+test = id+|]++expected6 :: [String]+expected6 =+ ["Proxy (CLog 1 4) -> Proxy 100"+ ,"Proxy 100 -> Proxy 100"+ ]++test6 :: TestTree+test6 = testCase "CLog 1 4 /~ 100" $ assertCompileError source6 expected6++source7 :: String+source7 = preamble <> [i|+test :: Proxy (CLog 4 0) -> Proxy 0+test = id+|]++expected7 :: [String]+expected7 =+ ["Proxy (CLog 4 0) -> Proxy 0"+ ,"Proxy 0 -> Proxy 0"+ ]++test7 :: TestTree+test7 = testCase "CLog 4 0 /~ 0" $ assertCompileError source7 expected7++source8 :: String+source8 = preamble <> [i|+test :: Proxy (CLog 1 (1^y)) -> Proxy y+test = id+|]++expected8 :: [String]+expected8 =+ ["Proxy (CLog 1 (1 ^ y)) -> Proxy y"+ ,"Proxy y -> Proxy y"+ ]++test8 :: TestTree+test8 = testCase "CLog 1 (1^y) /~ y" $ assertCompileError source8 expected8++source9 :: String+source9 = preamble <> [i|+test :: Proxy (CLog 0 (0^y)) -> Proxy y+test = id+|]++expected9 :: [String]+expected9 =+ ["Proxy (CLog 0 (0 ^ y)) -> Proxy y"+ ,"Proxy y -> Proxy y"+ ]++test9 :: TestTree+test9 = testCase "CLog 0 (0^y) /~ y" $ assertCompileError source9 expected9++source10 :: String+source10 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test :: Integer+test = natVal (Proxy :: Proxy (CLog 1 4))+|]++expected10 :: [String]+expected10 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 2 <= 1"]+#else+ ["Couldn't match type ''False' with ''True'"]+#endif++test10 :: TestTree+test10 = testCase "No instance (KnownNat (CLog 1 4))" $ assertCompileError source10 expected10++source11 :: String+source11 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test :: Integer+test = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4)))+|]++expected11 :: [String]+expected11 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 2 <= 1"]+#else+ ["Couldn't match type ''False` with ''True'"]+#endif++test11 :: TestTree+test11 = testCase "No instance (KnownNat (CLog 4 4 - CLog 2 4))" $ assertCompileError source11 expected11++source12 :: String+source12 = preamble <> [i|+test :: Proxy (Div 4 0) -> Proxy 4+test = id+|]++expected12 :: [String]+expected12 =+ ["Proxy (Div 4 0) -> Proxy 4"+ ,"Proxy 4 -> Proxy 4"+ ]++test12 :: TestTree+test12 = testCase "Div 4 0 /~ 4" $ assertCompileError source12 expected12++source13 :: String+source13 = preamble <> [i|+test :: Proxy (Mod 4 0) -> Proxy 4+test = id+|]++expected13 :: [String]+expected13 =+ ["Proxy (Mod 4 0) -> Proxy 4"+ ,"Proxy 4 -> Proxy 4"+ ]++test13 :: TestTree+test13 = testCase "Mod 4 0 /~ 4" $ assertCompileError source13 expected13++source14 :: String+source14 = preamble <> [i|+test :: Proxy (FLog 0 4) -> Proxy 100+test = id+|]++expected14 :: [String]+expected14 =+ ["Proxy (FLog 0 4) -> Proxy 100"+ ,"Proxy 100 -> Proxy 100"+ ]++test14 :: TestTree+test14 = testCase "FLog 0 4 /~ 100" $ assertCompileError source14 expected14++source15 :: String+source15 = preamble <> [i|+test :: Proxy (FLog 1 4) -> Proxy 100+test = id+|]++expected15 :: [String]+expected15 =+ ["Proxy (FLog 1 4) -> Proxy 100"+ ,"Proxy 100 -> Proxy 100"+ ]++test15 :: TestTree+test15 = testCase "FLog 1 4 /~ 100" $ assertCompileError source15 expected15++source16 :: String+source16 = preamble <> [i|+test :: Proxy (FLog 4 0) -> Proxy 0+test = id+|]++expected16 :: [String]+expected16 =+ ["Proxy (FLog 4 0) -> Proxy 0"+ ,"Proxy 0 -> Proxy 0"+ ]++test16 :: TestTree+test16 = testCase "FLog 4 0 /~ 0" $ assertCompileError source16 expected16++source17 :: String+source17 = preamble <> [i|+test :: Proxy (LCM 6 8) -> Proxy 48+test = id+|]++expected17 :: [String]+expected17 =+ ["Proxy (LCM 6 8) -> Proxy 48"+ ,"Proxy 48 -> Proxy 48"+ ]++test17 :: TestTree+test17 = testCase "LCM 6 8 /~ 48" $ assertCompileError source17 expected17++source18 :: String+source18 = preamble <> [i|+test :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9))+test = id+|]++expected18 :: [String]+expected18 =+#if __GLASGOW_HASKELL__ >= 904+ ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"+ ,"Proxy (24 + x) -> Proxy (24 + x)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"+ ,"Proxy (LCM 6 8 + x) -> Proxy (LCM 6 8 + x)"+ ]+#else+ ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"+ ,"Proxy (x + LCM 6 9) -> Proxy (x + LCM 6 9)"+ ]+#endif++test18 :: TestTree+test18 = testCase "LCM 6 8 + x /~ x + LCM 6 9" $ assertCompileError source18 expected18++source19 :: String+source19 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test :: Integer+test = natVal (Proxy :: Proxy (Log 3 0))+|]++expected19 :: [String]+expected19 =+#if __GLASGOW_HASKELL__ >= 900+ ["Couldn't match type: FLog 3 0"+ ," with: CLog 3 0"]+#else+ ["Couldn't match type 'FLog 3 0' with 'CLog 3 0'"]+#endif++test19 :: TestTree+test19 = testCase "No instance (KnownNat (Log 3 0))" $ assertCompileError source19 expected19++source20 :: String+source20 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test :: Integer+test = natVal (Proxy :: Proxy (Log 3 10))+|]++expected20 :: [String]+expected20 =+#if __GLASGOW_HASKELL__ >= 904+ ["Couldn't match type '2' with '3'"]+#elif __GLASGOW_HASKELL__ >= 900+ ["Couldn't match type: FLog 3 10"+ ," with: CLog 3 10"]+#else+ ["Couldn't match type 'FLog 3 10' with 'CLog 3 10'"]+#endif++test20 :: TestTree+test20 = testCase "No instance (KnownNat (Log 3 10))" $ assertCompileError source20 expected20++source21 :: String+source21 = preamble <> [i|+test :: Proxy a -> Proxy b -> Proxy (Min a (a * b)) -> Proxy a+test _ _ = id+|]++expected21 :: [String]+expected21 =+ ["Proxy (Min a (a * b)) -> Proxy a"+ ,"Proxy a -> Proxy a"+ ]++test21 :: TestTree+test21 = testCase "Min a (a*b) /~ a" $ assertCompileError source21 expected21++source22 :: String+source22 = preamble <> [i|+test :: Proxy a -> Proxy b -> Proxy (Max a (a * b)) -> Proxy (a * b)+test _ _ = id+|]++expected22 :: [String]+expected22 =+#if __GLASGOW_HASKELL__ >= 900+ ["Proxy (Max a (a * b)) -> Proxy (a * b)"+ ,"Proxy (Max a (a * b)) -> Proxy (Max a (a * b))"]+#else+ ["Proxy (Max a (a * b)) -> Proxy (a * b)"+ ,"Proxy (a * b) -> Proxy (a * b)"]+#endif++test22 :: TestTree+test22 = testCase "Max a (a*b) /~ (a*b)" $ assertCompileError source22 expected22++source23 :: String+source23 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> ()+test' _ _ = ()++test :: ()+test = test' (Proxy @18) (Proxy @3)+|]++expected23 :: [String]+expected23 =+#if __GLASGOW_HASKELL__ >= 804+ ["Couldn't match type ''True' with ''False'"]+#else+ ["Couldn't match type '1 <=? Div 18 3' with ''False'"]+#endif++test23 :: TestTree+test23 = testCase "(1 <=? Div 18 3) ~ False" $ assertCompileError source23 expected23++source24 :: String+source24 = [i|+{-# LANGUAGE CPP #-}+|] <> preamble <> [i|+#if __GLASGOW_HASKELL__ >= 901+import qualified Data.Type.Ord+#endif++test :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True+test _ _ _ = id+|]++expected24 :: [String]+expected24 =+#if __GLASGOW_HASKELL__ >= 902+ ["Couldn't match type 'Data.Type.Ord.OrdCond"+ ,"(CmpNat z (Max x y)) 'True 'True 'False'"+ ,"with ''True'"]+#else+ ["Couldn't match type 'z <=? Max x y' with ''True'"]+#endif++test24 :: TestTree+test24 = testCase "(z <=? Max x y) /~ True" $ assertCompileError source24 expected24++source25 :: String+source25 = [i|+{-# LANGUAGE CPP #-}+|] <> preamble <> [i|+#if __GLASGOW_HASKELL__ >= 901+import qualified Data.Type.Ord+#endif++test :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True+test _ _ = id+|]++expected25 :: [String]+expected25 =+#if __GLASGOW_HASKELL__ >= 902+ ["Couldn't match type 'Data.Type.Ord.OrdCond"+ ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False'"+ ,"with ''True'"]+#else+ ["Couldn't match type '(x + 1) <=? Max x y' with ''True'"]+#endif++test25 :: TestTree+test25 = testCase "(x+1 <=? Max x y) /~ True" $ assertCompileError source25 expected25++source26 :: String+source26 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|++-- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true.+test' :: ((x <=? n) ~ True) => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n+test' _ _ _ = id++test = test' (Proxy @4) (Proxy @6) (Proxy @6)+|]++expected26 :: [String]+expected26 =+#if __GLASGOW_HASKELL__ >= 906+ ["Could not deduce 'Max x y ~ n'"+ ,"from the context: (x <=? n) ~ True"+ ]+#elif __GLASGOW_HASKELL__ <= 902+ ["Could not deduce: Max x y ~ n"+ ,"from the context: (x <=? n) ~ 'True"+ ]+#else+ ["Could not deduce (Max x y ~ n)"+ ,"from the context: (x <=? n) ~ 'True"+ ]+#endif++test26 :: TestTree+test26 = testCase "(x <= n) /=> (Max x y) ~ n" $ assertCompileError source26 expected26++source27 :: String+source27 = preamble <> [i|+test :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True+test _ = id+|]++expected27 :: [String]+expected27 =+ ["Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True"+ ,"Proxy 'True -> Proxy 'True"+ ]++test27 :: TestTree+test27 = testCase "n + 2 <=? Max (n + 1) 1 /~ True" $ assertCompileError source27 expected27++source28 :: String+source28 = [i|+{-# LANGUAGE KindSignatures #-}+|] <> preamble <> [i|+type Size (n :: Nat) = Max 0 (CLogWZ 2 n 0)++pack :: Proxy n -> Proxy (Size n)+pack _ = Proxy++repro :: Proxy (Size 1)+repro = pack (undefined :: Proxy (n :: Nat))+|]++expected28 :: [String]+expected28 =+ ["CLogWZ 2 n"+ ,"ambiguous"+ ]++test28 :: TestTree+test28 = testCase "CLogWZ reify with Max 0 (type synonym) doesn't panic" $+ assertCompileError source28 expected28
+ tests/ShouldError/Tasty.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE CPP #-}++module ShouldError.Tasty where++import Data.List (isInfixOf)+import Data.Maybe (fromMaybe)+import System.Environment (lookupEnv)+import System.Exit+import System.IO+import System.IO.Temp+import System.Process+import Test.Tasty.HUnit++-- | Assert that a Haskell code snippet fails to compile with expected error messages+assertCompileError :: String -> [String] -> Assertion+assertCompileError source expectedErrors = do+ -- XXX: This will pick the wrong GHC if the HC environment variable (as seen on CI)+ -- isn't set and the test suite is compiled with a GHC compiler other than the+ -- system's default.+ hc <- fromMaybe "ghc" <$> lookupEnv "HC"+ withSystemTempFile "ShouldError.hs" $ \tempFile tempHandle -> do+ hPutStr tempHandle source+ hClose tempHandle+ (exitCode, _, stderrOutput) <- readProcessWithExitCode hc+ [ "-XCPP"+ , "-XDataKinds"+ , "-XTypeOperators"+ , "-XTypeApplications"+ , "-XTypeFamilies"+ , "-XNoStarIsType"+ , "-fno-code"+ , "-fplugin", "GHC.TypeLits.Normalise"+ , "-fplugin", "GHC.TypeLits.KnownNat.Solver"+ , "-fplugin", "GHC.TypeLits.Extra.Solver"+ , tempFile+ ] ""+ case exitCode of+ ExitSuccess -> assertFailure "Expected compilation to fail but it succeeded"+ ExitFailure _ ->+ let cleanedStderr = removeProblemChars stderrOutput+ cleanedExpected = map removeProblemChars expectedErrors+ in if all (`isInfixOf` cleanedStderr) cleanedExpected+ then return ()+ else assertFailure $ "Error message mismatch:\n" +++ "Expected substrings: " ++ show expectedErrors ++ "\n" +++ "Actual output:\n" ++ stderrOutput++-- | Remove problematic characters that vary depending on locale+-- The kind and amount of quotes in GHC error messages changes depending on+-- whether or not our locale supports unicode.+removeProblemChars :: String -> String+removeProblemChars = filter (`notElem` problemChars)+ where problemChars = "‘’`'"