ghc-typelits-natnormalise 0.5.10 → 0.9.6
raw patch · 11 files changed
Files
- CHANGELOG.md +125/−0
- README.md +2/−2
- ghc-typelits-natnormalise.cabal +50/−28
- src/GHC/TypeLits/Normalise.hs +927/−250
- src/GHC/TypeLits/Normalise/Compat.hs +399/−0
- src/GHC/TypeLits/Normalise/SOP.hs +25/−15
- src/GHC/TypeLits/Normalise/Unify.hs +816/−158
- tests/ErrorTests.hs +0/−161
- tests/ShouldError.hs +597/−0
- tests/ShouldError/Tasty.hs +58/−0
- tests/Tests.hs +508/−61
CHANGELOG.md view
@@ -1,5 +1,130 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.9.6 *May 13th 2026*+* Bump ghc-tcplugin-api to prepare for inclusion into stackage++## 0.9.5 *March 19th 2026*+* Make the test suite not emit compile warnings++## 0.9.4 *March 19th 2026*+* Fixes [#116](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/113) Compile-time loop when processing Given constraints.+* Fixes [#119](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/119) solving constraints involving type families applied to normalised Nat expressions (e.g. `Foo (a + b)`).+* Fixes [#120](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/120) stop emitting Assert (a <=? b) msg ~ (() :: Constraint) constraints+* Fixed regression [#124](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/124) involving unification of summands.++## 0.9.3 *December 2nd 2025*+* Fixes [#114](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/113) Poor error message in plugin version 0.8 and higher+* Fixes [#113](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/113) Wanted contraints rewrites to itself, leading to infinite solver iterations++## 0.9.2 *December 2nd 2025*+* Fixes [#108](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/108) Type error after plugin update+* Fixes [#111](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/111) Exception for unifying under non-injective type families++## 0.9.1 *October 21st 2025*+* Fixes [#105](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/105) Unsound derived contradiction with 0.9.0+* Support for GHC 9.14++## 0.9.0 *October 17th 2025*+* Drop `TyConSubst` argument from `normaliseNat`, `normaliseNatEverywhere` and `normaliseSimplifyNat`.+* Expose `GHC.TypeLits.Normalise.Compat`+* Report contractions for equations such as `1 + k <= n; n ~ 0` in "solve givens" phase++## 0.8.1 *October 1st 2025*+* Fixes [#85](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/85) Deriving equalities from inequalities produces a misleading error message+* Fixes [#94](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94) Normalization fails when adding an equality constraint with substraction+* Fixes [#96](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/96) Unification fails when variables occur on both LHS and RHS+* Fixes [#99](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/99) ghc-typelits-natnormalise erroneously unifies under type families+* Fixes [100](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/100) stack space overflow with ghc-typelits-natnormalize 0.8++## 0.8 *September 8th 2025*+* 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+* Fixes [#70](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/70) The constraint 0 < d+1 does not seem to resolve?+* Fixes [#71](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/71) "Could not deduce ... from the context ...", but if the context removed, deduced outright+* Fixes [#47](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/47) Could not deduce `KnownNat (F ((2 * a) + a) b + (2 * F (a + (2 * a)) b))` from `KnownNat (F (a * 3) b * 3)`++## 0.7.12 *August 22nd 2025*+* Support for GHC 9.10.2++## 0.7.11 *March 4th 2025*+* Support for GHC 9.12.1++## 0.7.10 *May 22nd 2024*+* Support for GHC 9.10.1++## 0.7.9 *October 10th 2023*+* Support for GHC 9.8.1++## 0.7.8 *February 20th 2023*+* Try and outright solve substituted constraints, the same as is done with the unsubstituted constraint. Partially Fixes [#65](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/65).+* Support for GHC-9.6.0.20230210++## 0.7.7 *October 10th 2022*+* Solve unflattened wanteds instead of the wanteds passed to the plugin. Fixes [#1901]https://github.com/clash-lang/clash-compiler/issues/1901.+* Add support for GHC 9.4++## 0.7.6 *June 20th 2021*+* Do not vacuously solve `forall a b . 1 <=? a^b ~ True`+* Do not solve constraints within `KnownNat`, leave that to https://hackage.haskell.org/package/ghc-typelits-knonwnnat++## 0.7.5 *June 17th 2021*+* Fixes [#52](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/50) Plugin doesn't solve inside arbitrary class constraints+* Build on GHC 9.2.0.20210422++## 0.7.4 *February 12th 2021*+* Fixes [#50](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/50) `x ^ C ~ y` erroneously deemed hard insoluable, a contradiction, when `C` is some type family other than +,-,*,^++## 0.7.3 *January 1st 2021*+* Build on GHC 9.0.1-rc1++## 0.7.2 *March 9 2020*+* Fixes [#44](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/44) infinite loop due to boxed equality++## 0.7.1 *February 6th 2020*+* Add support for GHC 8.10.1-alpha2+* Fixes [#23](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/23): Can't figure out `+` commutes in some contexts on GHC 8.6.3+* Fixes [#28](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/28): Using the solver seems to break GHC+* Fixes [#34](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/34): inequality solver mishandles subtraction++## 0.7 *August 26th 2019*+* Require KnownNat constraints when solving with constants++## 0.6.2 *July 10th 2018*+* Add support for GHC 8.6.1-alpha1+* Solve larger inequalities from smaller inequalities, e.g.+ * `a <= n` implies `a <= n + 1`++## 0.6.1 *May 9th 2018*+* Stop solving `x + y ~ a + b` by asking GHC to solve `x ~ a` and `y ~ b` as+ this leads to a situation where we find a solution that is not the most+ general.+* Stop using the smallest solution to an inequality to solve an equality, as+ this leads to finding solutions that are not the most general.+* Solve smaller inequalities from larger inequalities, e.g.+ * `1 <= 2*x` implies `1 <= x`+ * `x + 2 <= y` implies `x <= y` and `2 <= y`++## 0.6 *April 23rd 2018*+* Solving constraints with `a-b` will emit `b <= a` constraints. e.g. solving+ `n-1+1 ~ n` will emit a `1 <= n` constraint.+ * If you need subtraction to be treated as addition with a negated operarand+ run with `-fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers`, and+ the `b <= a` constraint won't be emitted. Note that doing so can lead to+ unsound behaviour.+* Try to solve equalities using smallest solution of inequalities:+ * Solve `x + 1 ~ y` using `1 <= y` => `x + 1 ~ 1` => `x ~ 0`+* Solve inequalities using simple transitivity rules:+ * `2 <= x` implies `1 <= x`+ * `x <= 9` implies `x <= 10`+* Solve inequalities using _simple_ monotonicity of addition rules:+ * `2 <= x` implies `2 + 2*x <= 3*x`+* Solve inequalities using _simple_ monotonicity of multiplication rules:+ * `1 <= x` implies `1 <= 3*x`+* Solve inequalities using _simple_ monotonicity of exponentiation rules:+ * `1 <= x` implies `2 <= 2^x`+* Solve inequalities using powers of 2 and monotonicity of exponentiation:+ * `2 <= x` implies `2^(2 + 2*x) <= 2^(3*x)`+ ## 0.5.10 *April 15th 2018* * Add support for GHC 8.5.20180306
README.md view
@@ -1,10 +1,10 @@ # ghc-typelits-natnormalise -[](http://travis-ci.org/clash-lang/ghc-typelits-natnormalise)+[](https://github.com/clash-lang/ghc-typelits-natnormalise/actions) [](https://hackage.haskell.org/package/ghc-typelits-natnormalise) [](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-natnormalise) -A type checker plugin for GHC that can solve _equalities_ +A type checker plugin for GHC that can solve _equalities_ and _inequalities_ of types of kind `Nat`, where these types are either: * Type-level naturals
ghc-typelits-natnormalise.cabal view
@@ -1,43 +1,44 @@+cabal-version: 3.0 name: ghc-typelits-natnormalise-version: 0.5.10+version: 0.9.6 synopsis: GHC typechecker plugin for types of kind GHC.TypeLits.Nat description:- A type checker plugin for GHC that can solve /equalities/ of types of kind- @Nat@, where these types are either:- .+ A type checker plugin for GHC that can solve /equalities/ and /inequalities/+ of types of kind @Nat@, where these types are either:+ * Type-level naturals- .+ * Type variables- .+ * Applications of the arithmetic expressions @(+,-,*,^)@.- .+ It solves these equalities by normalising them to /sort-of/ @SOP@ (Sum-of-Products) form, and then perform a simple syntactic equality.- .+ For example, this solver can prove the equality between:- .+ @ (x + 2)^(y + 2) @- .+ and- .+ @ 4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2 @- .+ Because the latter is actually the @SOP@ normal form of the former.- .+ To use the plugin, add the- .+ @ OPTIONS_GHC -fplugin GHC.TypeLits.Normalise @- .+ Pragma to the header of your file. homepage: http://www.clash-lang.org/ bug-reports: http://github.com/clash-lang/ghc-typelits-natnormalise/issues-license: BSD2+license: BSD-2-Clause license-file: LICENSE author: Christiaan Baaij maintainer: christiaan.baaij@gmail.com@@ -45,11 +46,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.1, GHC == 8.4.2,- GHC == 8.5.0+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.7, GHC == 9.8.4, GHC == 9.10.2,+ GHC == 9.12.2 source-repository head type: git@@ -63,12 +64,28 @@ library exposed-modules: GHC.TypeLits.Normalise,+ GHC.TypeLits.Normalise.Compat, GHC.TypeLits.Normalise.SOP, GHC.TypeLits.Normalise.Unify build-depends: base >=4.9 && <5,- ghc >=8.0.1 && <8.6,- ghc-tcplugins-extra >=0.2.5,- integer-gmp >=1.0 && <1.1+ containers >=0.5.7.1 && <0.9,+ ghc >=8.8.1 && <9.15,+ ghc-tcplugin-api >=0.19 && <0.20,+ transformers >=0.5.2 && < 0.7+ 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+ , TyCon as GHC.Core.TyCon+ , TysWiredIn as GHC.Builtin.Types+ , Unique as GHC.Types.Unique+ , Util as GHC.Utils.Misc+ )+ hs-source-dirs: src default-language: Haskell2010 other-extensions: CPP@@ -80,24 +97,29 @@ else ghc-options: -Wall -test-suite test-ghc-typelits-natnormalise+test-suite unit-tests type: exitcode-stdio-1.0 main-is: Tests.hs- Other-Modules: ErrorTests+ Other-Modules: ShouldError+ ShouldError.Tasty build-depends: base >=4.8 && <5, ghc-typelits-natnormalise,+ interpolate,+ process, tasty >= 0.10, tasty-hunit >= 0.9,- template-haskell >= 2.11.0.0+ temporary+ if impl(ghc >= 9.4)+ build-depends: ghc-prim >= 0.9 hs-source-dirs: tests+ ghc-options: -Wall default-language: Haskell2010 other-extensions: DataKinds GADTs KindSignatures NoImplicitPrelude- TemplateHaskell TypeFamilies TypeOperators ScopedTypeVariables if flag(deverror)- ghc-options: -O0 -dcore-lint+ ghc-options: -Werror -dcore-lint
src/GHC/TypeLits/Normalise.hs view
@@ -37,253 +37,930 @@ @ To the header of your file.--}--{-# LANGUAGE CPP #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE TupleSections #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.Normalise- ( plugin )-where---- external-import Control.Arrow (second)-import Control.Monad (replicateM)-import Data.Either (rights)-import Data.List (intersect)-import Data.Maybe (mapMaybe)-import GHC.TcPluginM.Extra (tracePlugin)-#if MIN_VERSION_ghc(8,4,0)-import GHC.TcPluginM.Extra (flattenGivens)-#endif---- GHC API-#if MIN_VERSION_ghc(8,5,0)-import CoreSyn (Expr (..))-#endif-import Outputable (Outputable (..), (<+>), ($$), text)-import Plugins (Plugin (..), defaultPlugin)-import TcEvidence (EvTerm (..))-#if !MIN_VERSION_ghc(8,4,0)-import TcPluginM (zonkCt)-#endif-import TcPluginM (TcPluginM, tcPluginTrace)-import TcRnTypes (Ct, TcPlugin (..), TcPluginResult(..), ctEvidence, ctEvPred,- isWanted, mkNonCanonical)-import Type (EqRel (NomEq), Kind, PredTree (EqPred), PredType,- classifyPredType, eqType, getEqPredTys, mkTyVarTy)-import TysWiredIn (typeNatKind)--import Coercion (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo,- mkNomReflCo, mkUnivCo)-import TcPluginM (newCoercionHole, newFlexiTyVar)-import TcRnTypes (CtEvidence (..), CtLoc, TcEvDest (..), ctLoc)-#if MIN_VERSION_ghc(8,2,0)-import TcRnTypes (ShadowInfo (WDeriv))-#endif-import TyCoRep (UnivCoProvenance (..))-import Type (mkPrimEqPred)-import TcType (typeKind)-import TyCoRep (Type (..))-import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,- typeNatSubTyCon)--import TcTypeNats (typeNatLeqTyCon)-import Type (mkNumLitTy,mkTyConApp)-import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon)---- internal-import GHC.TypeLits.Normalise.Unify---- | To use the plugin, add------ @--- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}--- @------ To the header of your file.-plugin :: Plugin-plugin = defaultPlugin { tcPlugin = const $ Just normalisePlugin }--normalisePlugin :: TcPlugin-normalisePlugin = tracePlugin "ghc-typelits-natnormalise"- TcPlugin { tcPluginInit = return ()- , tcPluginSolve = const decideEqualSOP- , tcPluginStop = const (return ())- }--decideEqualSOP :: [Ct] -> [Ct] -> [Ct]- -> TcPluginM TcPluginResult-decideEqualSOP _givens _deriveds [] = return (TcPluginOk [] [])-decideEqualSOP givens _deriveds wanteds = do- -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out- let wanteds' = filter (isWanted . ctEvidence) wanteds- let unit_wanteds = mapMaybe toNatEquality wanteds'- case unit_wanteds of- [] -> return (TcPluginOk [] [])- _ -> do-#if MIN_VERSION_ghc(8,4,0)- let unit_givens = mapMaybe toNatEquality (givens ++ flattenGivens givens)-#else- unit_givens <- mapMaybe toNatEquality <$> mapM zonkCt givens-#endif- sr <- simplifyNats unit_givens unit_wanteds- tcPluginTrace "normalised" (ppr sr)- case sr of- Simplified evs -> do- let solved = filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs- (solved',newWanteds) = second concat (unzip solved)- return (TcPluginOk solved' newWanteds)- Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])--type NatEquality = (Ct,CoreSOP,CoreSOP)-type NatInEquality = (Ct,CoreSOP)--fromNatEquality :: Either NatEquality NatInEquality -> Ct-fromNatEquality (Left (ct, _, _)) = ct-fromNatEquality (Right (ct, _)) = ct--data SimplifyResult- = Simplified [((EvTerm,Ct),[Ct])]- | Impossible (Either NatEquality NatInEquality)--instance Outputable SimplifyResult where- ppr (Simplified evs) = text "Simplified" $$ ppr evs- ppr (Impossible eq) = text "Impossible" <+> ppr eq--simplifyNats- :: [Either NatEquality NatInEquality]- -- ^ Given constraints- -> [Either NatEquality NatInEquality]- -- ^ Wanted constraints- -> TcPluginM SimplifyResult-simplifyNats eqsG eqsW =- let eqs = eqsG ++ eqsW- in tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs- where- simples :: [CoreUnify]- -> [((EvTerm, Ct), [Ct])]- -> [Either NatEquality NatInEquality]- -> [Either NatEquality NatInEquality]- -> TcPluginM SimplifyResult- simples _subst evs _xs [] = return (Simplified evs)- simples subst evs xs (eq@(Left (ct,u,v)):eqs') = do- ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v)- tcPluginTrace "unifyNats result" (ppr ur)- case ur of- Win -> do- evs' <- maybe evs (:evs) <$> evMagic ct []- simples subst evs' [] (xs ++ eqs')- Lose -> return (Impossible eq)- Draw [] -> simples subst evs (eq:xs) eqs'- Draw subst' -> do- evM <- evMagic ct (map unifyItemToPredType subst')- case evM of- Nothing -> simples subst evs xs eqs'- Just ev ->- simples (substsSubst subst' subst ++ subst')- (ev:evs) [] (xs ++ eqs')- simples subst evs xs (eq@(Right (ct,u)):eqs') = do- let u' = substsSOP subst u- tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u'))- case isNatural u' of- Just True -> do- evs' <- maybe evs (:evs) <$> evMagic ct []- simples subst evs' xs eqs'- Just False -> return (Impossible eq)- Nothing ->- -- This inequality is either a given constraint, or it is a wanted- -- constraint, which in normal form is equal to another given- -- constraint, hence it can be solved.- if u `elem` (map snd (rights eqsG))- then do- evs' <- maybe evs (:evs) <$> evMagic ct []- simples subst evs' xs eqs'- else simples subst evs (eq:xs) eqs'---- Extract the Nat equality constraints-toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality)-toNatEquality ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2- -> go t1 t2- _ -> Nothing- where- go (TyConApp tc xs) (TyConApp tc' ys)- | tc == tc'- , null ([tc,tc'] `intersect` [typeNatAddTyCon,typeNatSubTyCon- ,typeNatMulTyCon,typeNatExpTyCon])- = case filter (not . uncurry eqType) (zip xs ys) of- [(x,y)] | isNatKind (typeKind x) && isNatKind (typeKind y)- -> Just (Left (ct, normaliseNat x, normaliseNat y))- _ -> Nothing- | tc == typeNatLeqTyCon- , [x,y] <- xs- = if tc' == promotedTrueDataCon- then Just (Right (ct,normaliseNat (mkTyConApp typeNatSubTyCon [y,x])))- else if tc' == promotedFalseDataCon- then Just (Right (ct,normaliseNat (mkTyConApp typeNatSubTyCon [x,mkTyConApp typeNatAddTyCon [y,mkNumLitTy 1]])))- else Nothing-- go x y- | isNatKind (typeKind x) && isNatKind (typeKind y)- = Just (Left (ct,normaliseNat x,normaliseNat y))- | otherwise- = Nothing-- isNatKind :: Kind -> Bool- isNatKind = (`eqType` typeNatKind)--unifyItemToPredType :: CoreUnify -> PredType-unifyItemToPredType ui =- mkPrimEqPred ty1 ty2- where- ty1 = case ui of- SubstItem {..} -> mkTyVarTy siVar- UnifyItem {..} -> reifySOP siLHS- ty2 = case ui of- SubstItem {..} -> reifySOP siSOP- UnifyItem {..} -> reifySOP siRHS--evMagic :: Ct -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))-evMagic ct preds = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2 -> do-#if MIN_VERSION_ghc(8,4,1)- holes <- mapM (newCoercionHole . uncurry mkPrimEqPred . getEqPredTys) preds-#else- holes <- replicateM (length preds) newCoercionHole-#endif- let newWanted = zipWith (unifyItemToCt (ctLoc ct)) preds holes- ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2-#if MIN_VERSION_ghc(8,4,1)- holeEvs = map mkHoleCo holes-#else- holeEvs = zipWith (\h p -> uncurry (mkHoleCo h Nominal) (getEqPredTys p)) holes preds-#endif- natReflCo = mkNomReflCo typeNatKind- natCoBndr = (,natReflCo) <$> (newFlexiTyVar typeNatKind)- forallEv <- mkForAllCos <$> (replicateM (length preds) natCoBndr) <*> pure ctEv- let finalEv = foldl mkInstCo forallEv holeEvs-#if MIN_VERSION_ghc(8,5,0)- return (Just ((EvExpr (Coercion finalEv), ct),newWanted))-#else- return (Just ((EvCoercion finalEv, ct),newWanted))-#endif- _ -> return Nothing--unifyItemToCt :: CtLoc- -> PredType- -> CoercionHole- -> Ct-unifyItemToCt loc pred_type hole =- mkNonCanonical- (CtWanted- pred_type- (HoleDest hole)-#if MIN_VERSION_ghc(8,2,0)- WDeriv-#endif- loc)++== Treating subtraction as addition with a negated number++If you are absolutely sure that your subtractions can /never/ lead to (a locally)+negative number, you can ask the plugin to treat subtraction as addition with+a negated operand by additionally adding:++@+{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}+@++to the header of your file, thereby allowing to use associativity and+commutativity rules when proving constraints involving subtractions. Note that+this option can lead to unsound behaviour and should be handled with extreme+care.++=== When it leads to unsound behaviour++For example, enabling the /allow-negated-numbers/ feature would allow+you to prove:++@+(n - 1) + 1 ~ n+@++/without/ a @(1 <= n)@ constraint, even though when /n/ is set to /0/ the+subtraction @n-1@ would be locally negative and hence not be a natural number.++This would allow the following erroneous definition:++@+data Fin (n :: Nat) where+ FZ :: Fin (n + 1)+ FS :: Fin n -> Fin (n + 1)++f :: forall n . Natural -> Fin n+f n = case of+ 0 -> FZ+ x -> FS (f \@(n-1) (x - 1))++fs :: [Fin 0]+fs = f \<$\> [0..]+@++=== When it might be Okay++This example is taken from the <http://hackage.haskell.org/package/mezzo mezzo>+library.++When you have:++@+-- | Singleton type for the number of repetitions of an element.+data Times (n :: Nat) where+ T :: Times n++-- | An element of a "run-length encoded" vector, containing the value and+-- the number of repetitions+data Elem :: Type -> Nat -> Type where+ (:*) :: t -> Times n -> Elem t n++-- | A length-indexed vector, optimised for repetitions.+data OptVector :: Type -> Nat -> Type where+ End :: OptVector t 0+ (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n+@++And you want to define:++@+-- | Append two optimised vectors.+type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where+ ys ++ End = ys+ End ++ ys = ys+ (x :- xs) ++ ys = x :- (xs ++ ys)+@++then the last line will give rise to the constraint:++@+(n-l)+m ~ (n+m)-l+@++because:++@+x :: Elem t l+xs :: OptVector t (n-l)+ys :: OptVector t m+@++In this case it's okay to add++@+{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}+@++if you can convince yourself you will never be able to construct a:++@+xs :: OptVector t (n-l)+@++where /n-l/ is a negative number.+-}++{-# LANGUAGE CPP #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE TemplateHaskellQuotes #-}++{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}+{-# OPTIONS_HADDOCK show-extensions #-}++module GHC.TypeLits.Normalise+ ( plugin )+where++-- base+import Control.Arrow+ ( second )+import Control.Monad+ ( (<=<), unless )+import Control.Monad.Trans.Writer.Strict+ ( WriterT(runWriterT), runWriter )+import Data.Either+ ( rights, partitionEithers )+import Data.Foldable+import Data.List+ ( stripPrefix, partition )+import Data.Maybe+ ( mapMaybe, catMaybes, fromMaybe, isJust )+import Data.Traversable+ ( for )+import Text.Read+ ( readMaybe )++-- containers+import Data.Set+ ( Set )+import qualified Data.Set as Set+ ( elems, empty )+import Data.Map.Strict+ ( Map )+import qualified Data.Map.Strict as Map+ ( empty, insertWith, traverseWithKey )++-- ghc+import GHC.Builtin.Names+ ( knownNatClassName )+import GHC.Builtin.Types.Literals+ ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon )+import GHC.Core.TyCon+ ( Injectivity (..), tyConInjectivityInfo, tyConArity )+import GHC.Utils.Misc+ ( filterByList )++-- ghc-tcplugin-api+import GHC.TcPlugin.API+import GHC.TcPlugin.API.TyConSubst+ ( TyConSubst, mkTyConSubst )+import GHC.Plugins+ ( Plugin(..), defaultPlugin, purePlugin, allVarSet, isEmptyVarSet, tyCoVarsOfType )+import GHC.Utils.Outputable++-- ghc-typelits-natnormalise+import GHC.TypeLits.Normalise.Compat+import GHC.TypeLits.Normalise.SOP+ ( SOP(S), Product(P), Symbol(V) )+import GHC.TypeLits.Normalise.Unify++-- transformers+import Control.Monad.Trans.Class+ ( lift )+import Control.Monad.Trans.State.Strict+ ( StateT, evalStateT, get, modify )++--------------------------------------------------------------------------------++-- | To use the plugin, add+--+-- @+-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}+-- @+--+-- To the header of your file.+plugin :: Plugin+plugin+ = defaultPlugin+ { tcPlugin = \ p -> do opts <- foldr id defaultOpts <$> traverse parseArgument p+ return $ mkTcPlugin $ normalisePlugin opts+ , pluginRecompile = purePlugin+ }+ where+ parseArgument "allow-negated-numbers" = Just (\ opts -> opts { negNumbers = True })+ parseArgument (readMaybe <=< stripPrefix "depth=" -> Just depth) = Just (\ opts -> opts { depth })+ parseArgument _ = Nothing+ defaultOpts = Opts { negNumbers = False, depth = 5 }++data Opts = Opts { negNumbers :: Bool, depth :: Word }++normalisePlugin :: Opts -> TcPlugin+normalisePlugin opts =+ TcPlugin { tcPluginInit = lookupExtraDefs+ , tcPluginSolve = decideEqualSOP opts+ , tcPluginRewrite = const emptyUFM+ , tcPluginPostTc = const (return ())+ , tcPluginShutdown = const (return ())+ }++data ExtraDefs+ = ExtraDefs+ { tyCons :: LookedUpTyCons }++lookupExtraDefs :: TcPluginM Init ExtraDefs+lookupExtraDefs = do+ tcs <- lookupTyCons+ return $+ ExtraDefs+ { tyCons = tcs }++decideEqualSOP+ :: Opts+ -> ExtraDefs+ -- ^ 1. Givens that is already generated.+ -- We have to generate new givens at most once;+ -- otherwise GHC will loop indefinitely.+ --+ --+ -- 2. For GHc 9.2: TyCon of Data.Type.Ord.OrdCond+ -- For older: TyCon of GHC.TypeLits.<=?+ -> [Ct]+ -> [Ct]+ -> TcPluginM Solve TcPluginSolveResult+-- Simplification phase: Derives /simplified/ givens;+-- we can reduce given constraints like @Show (Foo (n + 2))@+-- to its normal form @Show (Foo (2 + n))@, which is eventually+-- useful in solving phase.+--+-- This helps us to solve /indirect/ constraints;+-- without this phase, we cannot derive, e.g.,+-- @IsVector UVector (Fin (n + 1))@ from+-- @Unbox (1 + n)@!+decideEqualSOP opts (ExtraDefs { tyCons = tcs }) givens [] =+ do+ let+ givensTyConSubst = mkTyConSubst givens+ (redGivens, _) <- reduceGivens False opts tcs givens++ tcPluginTrace "decideEqualSOP Givens {" $+ vcat [ text "givens:" <+> ppr givens ]++ -- Try to find contradictory Givens, to improve pattern match warnings.+ SimplifyResult { simplifiedWanteds, contradictions, newGivens } <-+ simplifyNats opts tcs [] $+ concatMap (toNatEquality opts tcs givensTyConSubst) redGivens++ -- Only add new Givens that are genuinely new, i.e. that GHC doesn't+ -- already know.+ --+ -- For example, in #116 we had: [G] m ~ n, [G] n ~ 0. Recalling that+ -- the inert set in GHC is a /not necessarily idempotent/ terminating+ -- generalised substitution (see Note [The KickOut Criteria] in GHC.Tc.Solver.InertSet),+ -- we don't want to emit a new Given [G] m ~ 0: GHC already knows this, and+ -- if we repeatedly emit this Given we will cause a typechecker loop (as in #116).+ let+ isSolvedGiven subst ct =+ case classifyPredType $ substTy subst (ctPred ct) of+ EqPred _rel t1 t2 -> t1 `eqType` t2+ _ -> False+ tyEqLit ct =+ case classifyPredType (ctPred ct) of+ EqPred NomEq t1 t2 -> isTyVarTy t1 && isJust (isNumLitTy t2)+ _ -> False+ givensSubst = ctsSubst givens -- Computes the idempotent substitution from the Givens+ actuallyNewGivens =+ filter+ (\ ct ->+ tyEqLit ct+ -- For now, only admit improved Givens in the form of `n ~ L`,+ -- where `n` is a type variable and `L` is a numeric literal.+ &&+ not (isSolvedGiven givensSubst ct)+ -- Ensure this Given is genuinely new information to GHC, to+ -- avoid repeatedly emitting facts that GHC already knows,+ -- which can cause the typechecker to loop (#116).+ )+ newGivens++ tcPluginTrace "decideEqualSOP Givens }" $+ vcat [ text "givens:" <+> ppr givens+ , text "simpls:" <+> ppr simplifiedWanteds+ , text "contra:" <+> ppr contradictions+ , text "new:" <+> ppr actuallyNewGivens+ ]+ return $+ mkTcPluginSolveResult+#if MIN_VERSION_ghc(9,14,0)+ ( map fromNatEquality contradictions )+#else+ []+#endif+ [] -- no solved Givens+ actuallyNewGivens++-- Solving phase.+-- Solves in/equalities on Nats and simplifiable constraints+-- containing naturals.+decideEqualSOP opts (ExtraDefs { tyCons = tcs }) givens wanteds0 = do+ deriveds <- askDeriveds+ let wanteds = if null wanteds0+ then []+ else wanteds0 ++ deriveds+ givensTyConSubst = mkTyConSubst givens+ unit_wanteds0 = concatMap (toNatEquality opts tcs givensTyConSubst) wanteds+ nonEqs = filter ( not+ . (\p -> isEqPred p || isEqClassPred p)+ . ctEvPred+ . ctEvidence )+ wanteds++ (redGivens, negWanteds) <- reduceGivens True opts tcs givens+ reducible_wanteds+ <- catMaybes <$> mapM (\ct -> fmap (ct,) <$>+ reduceNatConstr redGivens ct)+ nonEqs++ tcPluginTrace "decideEqualSOP Wanteds {" $+ vcat [ text "givens:" <+> ppr givens+ , text "new reduced givens:" <+> ppr redGivens+ , text $ replicate 80 '-'+ , text "wanteds:" <+> ppr wanteds+ , text "unit_wanteds:" <+> ppr unit_wanteds0+ , text "reducible_wanteds:" <+> ppr reducible_wanteds+ ]+ if null unit_wanteds0 && null reducible_wanteds+ then return $ TcPluginOk [] []+ else do+ -- Since reducible Wanteds also can have some negation/subtraction+ -- subterms, we have to make sure appropriate inequalities to hold.+ -- Here, we generate such additional inequalities for reduction+ -- that is to be added to new [W]anteds.+ let mkNegWanted ( CType wtdPred ) loc = mkNonCanonical <$> newWanted loc wtdPred+ ineqForRedWants <- Map.traverseWithKey mkNegWanted negWanteds+ let unit_givens = concatMap (toNatEquality opts tcs givensTyConSubst) redGivens+ unit_wanteds = unit_wanteds0 ++ concatMap (toNatEquality opts tcs givensTyConSubst) ineqForRedWants+ sr@SimplifyResult{simplifiedWanteds, contradictions} <-+ simplifyNats opts tcs unit_givens unit_wanteds+ tcPluginTrace "normalised" (ppr sr)+ reds <- for reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do+ wants <- evSubtPreds (ctLoc origCt) $ subToPred opts tcs ws+ return ((term, origCt), wDicts ++ wants)+ let -- Only solve a Derived when there are Wanteds in play+ simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) simplifiedWanteds ++ reds of+ [] -> []+ _ -> simplifiedWanteds+ (solved,newWanteds) = second concat (unzip $ simpld1 ++ reds)++ tcPluginTrace "decideEqualSOP Wanteds }" $+ vcat [ text "givens:" <+> ppr givens+ , text "new reduced givens:" <+> ppr redGivens+ , text "unit givens:" <+> ppr unit_givens+ , text $ replicate 80 '-'+ , text "wanteds:" <+> ppr wanteds+ , text "ineqForRedWants:" <+> ppr ineqForRedWants+ , text "unit_wanteds:" <+> ppr unit_wanteds+ , text "reducible_wanteds:" <+> ppr reducible_wanteds+ , text $ replicate 80 '='+ , text "solved:" <+> ppr solved+ , text "newWanteds:" <+> ppr newWanteds+ ]+ return $+ mkTcPluginSolveResult+ (map fromNatEquality contradictions)+ solved+ newWanteds++type NatEquality = (Ct,CoreSOP,CoreSOP)+type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))++reduceGivens :: Bool -- ^ allow generating new "non-negative" Wanteds+ -> Opts -> LookedUpTyCons+ -> [Ct]+ -> TcPluginM Solve ([Ct], Map CType CtLoc)+reduceGivens gen_wanteds opts tcs origGivens = go [] Map.empty origGivens+ where+ go rev_acc_gs acc_ws [] = return ( reverse rev_acc_gs, acc_ws )+ go rev_acc_gs acc_ws (g:gs) =+ case tryReduceGiven opts tcs origGivens g of+ Just ( pred', evExpr, ws )+ | gen_wanteds || null ws || negNumbers opts+ -> do+ let loc = ctLoc g+ g' <- mkNonCanonical <$> newGiven loc pred' evExpr+ let !acc' = foldl' (insertWanted loc) acc_ws ws+ go ( g' : rev_acc_gs ) acc' gs+ _ ->+ go ( g : rev_acc_gs ) acc_ws gs++ insertWanted :: CtLoc -> Map CType CtLoc -> Type -> Map CType CtLoc+ insertWanted loc acc w =+ Map.insertWith (\ _new old -> old) (CType w) loc acc++tryReduceGiven+ :: Opts -> LookedUpTyCons+ -> [Ct] -> Ct+ -> Maybe (PredType, EvTerm, [PredType])+tryReduceGiven opts tcs simplGivens ct = do+ let (mans, ws) =+ runWriter $ normaliseNatEverywhere $+ ctEvPred $ ctEvidence ct+ ws' = [ p+ | p <- subToPred opts tcs ws+ , all (not . (`eqType` p) . ctEvPred . ctEvidence) simplGivens+ ]+ -- deps = unitDVarSet (ctEvId ct)+ (pred', deps) <- mans+ case classifyPredType pred' of+ EqPred _ l r+ | l `eqType` r+ -> Nothing+ _ -> return (pred', toReducedDict (ctEvidence ct) pred' deps, ws')++fromNatEquality :: Either NatEquality NatInEquality -> Ct+fromNatEquality (Left (ct, _, _)) = ct+fromNatEquality (Right (ct, _)) = ct++reduceNatConstr :: [Ct] -> Ct -> TcPluginM Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))+reduceNatConstr givens ct = do+ let pred0 = ctEvPred $ ctEvidence ct+ (mans, tests) = runWriter $ normaliseNatEverywhere pred0++ -- Even if we didn't rewrite the Wanted,+ -- we may still be able to solve it from a (rewritten) Given.+ (pred', deps') = fromMaybe (pred0, []) mans+ case find ((`eqType` pred') . ctEvPred . ctEvidence) givens of+ -- No existing evidence found+ Nothing+ | ClassPred cls _ <- classifyPredType pred'+ , className cls /= knownNatClassName++ -- We actually did do some rewriting/normalisation.+ , Just {} <- mans+ -> do+ -- Create new evidence binding for normalized class constraint+ wtdDictCt <- mkNonCanonical <$> newWanted (ctLoc ct) pred'+ -- Evidence for current wanted is simply the coerced binding for+ -- the new binding+ let evCo = mkPluginUnivCo "ghc-typelits-natnormalise"+ Representational+ deps'+ pred' pred0+ ev = evCast (evId $ ctEvId wtdDictCt) evCo+ -- Use newly created coerced wanted as evidence, and emit the+ -- normalized wanted as a new constraint to solve.+ return (Just (EvExpr ev, tests, [wtdDictCt]))+ | otherwise+ -> return Nothing+ -- Use existing evidence+ Just c -> return (Just (toReducedDict (ctEvidence c) pred0 deps', tests, []))++toReducedDict :: CtEvidence -> PredType -> [Coercion] -> EvTerm+toReducedDict ct pred' deps' =+ let pred0 = ctEvPred ct+ evCo = mkPluginUnivCo "ghc-typelits-natnormalise"+ Representational+ deps'+ pred0 pred'+ ev = evCast (ctEvExpr ct) evCo+ in EvExpr ev++data SimplifyResult+ = SimplifyResult+ { simplifiedWanteds :: [((EvTerm,Ct),[Ct])]+ -- ^ List of:+ -- * Tuple of:+ -- * Evidence for:+ -- * The solved Wanted+ -- * Preconditions (in the for of new Wanteds)+ , contradictions :: [Either NatEquality NatInEquality]+ -- ^ List of contradictions+ , newGivens :: [Ct]+ -- ^ Givens derived in the improve givens stage+ }++instance Outputable SimplifyResult where+ ppr (SimplifyResult { simplifiedWanteds, contradictions, newGivens }) =+ text "SimplifyResult { simplified =" <+> ppr simplifiedWanteds+ <+> text ", impossible =" <+> ppr contradictions+ <+> text ", new_givens =" <+> ppr newGivens <+> text "}"++data NatCt+ = NatCt+ { predicate :: Either NatEquality NatInEquality+ -- ^ Predicate: either an equality or inequality+ , preconds :: [PredType]+ -- ^ Preconditions (in the form of inequalities encoded as PredTypes)+ , ctDeps :: [Coercion]+ -- ^ Coercion(s) from which the predicate is derived, needed so that evidence+ -- doesn't float above the coercions from which it is derived.+ }++instance Outputable NatCt where+ ppr (NatCt {predicate, preconds, ctDeps}) =+ text "NatCt { predicate = " <+> ppr predicate+ <+> text ", preconditions = " <+> ppr preconds+ <+> text ", dependencies = " <+> ppr ctDeps <+> text "}"++data SimplifyState+ = SimplifyState+ { stDeps :: [Coercion]+ -- ^ Coercions on which the simplified evidence depends, this needs to be+ -- kept around because sometimes we solving one constraint (which has a+ -- depedency) is used to solve another constraint+ , subst :: [CoreUnify]+ -- ^ Derived simplifications (i.e. b ~ c derived from (a + b) ~ (a + c)),+ -- and substitutions (i.e. n := 0 derived from y ^ n ~ 1)+ , evs :: [((EvTerm,Ct),[Ct])]+ -- ^ Collected evidence+ , leqsG :: [(CoreSOP,CoreSOP,Bool)]+ -- ^ Given inequalities+ , unsolved :: [NatCt]+ -- ^ Tried, but unsolved predicates. We keep them around in case we solve a+ -- new predicate which could lead to a substitution that enables a solve.+ , derivedGivens :: [Ct]+ -- ^ Unifiers derived from Givens. E.g. when we have /[G] x ^ n ~ 1/, this+ -- field will hold a derived /[G] n ~ 0/.+ }++emptySimplifyState :: SimplifyState+emptySimplifyState+ = SimplifyState+ { stDeps = []+ , subst = []+ , evs = []+ , leqsG = []+ , unsolved = []+ , derivedGivens = []+ }++simplifyNats+ :: Opts+ -- ^ Allow negated numbers (potentially unsound!)+ -> LookedUpTyCons+ -> [NatCt]+ -- ^ Given constraints+ -> [NatCt]+ -- ^ Wanted constraints+ -> TcPluginM Solve SimplifyResult+simplifyNats Opts{depth} tcs eqsG eqsW = do+ let eqsG1 = map (\nCt -> nCt{preconds = []}) eqsG+ (varEqs, otherEqs) = partition (isVarEqs . predicate) eqsG1+ fancyGivens = concatMap (makeGivensSet otherEqs) varEqs+ case varEqs of+ [] -> do+ let eqs = otherEqs ++ eqsW+ tcPluginTrace "simplifyNats" (ppr eqs)+ evalStateT (simples eqs) emptySimplifyState+ _ -> do+ tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")")+ (ppr varEqs)++ allSimplified <- for fancyGivens $ \v -> do+ let eqs = v ++ eqsW+ tcPluginTrace "simplifyNats" (ppr eqs)+ evalStateT (simples eqs) emptySimplifyState++ pure (foldr findFirstSimpliedWanted (SimplifyResult [] [] []) allSimplified)+ where+ simples ::+ [NatCt] ->+ StateT SimplifyState (TcPluginM Solve) SimplifyResult+ simples [] = do+ SimplifyState{evs, derivedGivens} <- get+ return SimplifyResult { simplifiedWanteds = evs+ , contradictions = []+ , newGivens = derivedGivens+ }+ simples (eq@NatCt{predicate=(Left (ct,u,v)), preconds, ctDeps}:eqs) = do+ SimplifyState{stDeps, subst, evs, leqsG, unsolved, derivedGivens} <- get+ let allDeps = stDeps ++ ctDeps++ let u' = substsSOP subst u+ v' = substsSOP subst v+ ur <- lift (unifyNats ct u' v')+ lift (tcPluginTrace "unifyNats result" (ppr ur))+ case ur of+ Win -> do+ -- Do note record "new" evidence for given constraints.+ unless (isGiven (ctEvidence ct)) $ do+ -- Only recorde evidence for wanted contstraints+ evM <- lift (evMagic tcs ct allDeps mempty preconds)+ lift $ tcPluginTrace "unifyNats Win" $+ vcat [ text "evM:" <+> ppr evM+ , text "ct:" <+> ppr ct+ ]+ modify (\s -> s {evs = maybe evs (:evs) evM})+ simples eqs+ Lose ->+ addContra (predicate eq) <$> simples eqs+ Draw [] -> do+ -- No progress made, add it to the "unsolved" list, in the hope we+ -- can make progress when we later find a new substitution+ modify (\s -> s {unsolved = eq:unsolved})+ simples eqs+ Draw unifications -> do -- We made some progress in the form of a unifier++ -- As the derived unifiers we record here can lead to solving another+ -- equation, we add it and its dependencies to the list of global+ -- dependencies which we use when creating new evidence+ let stDeps1 = ctEvCoercion (ctEvidence ct):allDeps+ -- We add apply the derived unification in the existing set of+ -- unification, and also add the derived unificaiton to the global+ -- state; to be used in solving later equations.+ let subst1 = substsSubst unifications subst ++ unifications+ if isGiven (ctEvidence ct) then do+ if null preconds then do+ -- We only record the unification derived from a given constraint+ -- when it has no preconditions in order for this unification to+ -- hold. The reason for that is that we can currently not record+ -- new Wanteds to be emitted at the end of the solve.+ givensU <- lift (mapM (unifyItemToGiven (ctLoc ct) allDeps) unifications)+ modify (\s -> s { stDeps = stDeps1+ , subst = subst1+ , leqsG = eqToLeq u' v' ++ leqsG+ , unsolved = []+ , derivedGivens = givensU ++ derivedGivens+ })+ simples (unsolved ++ eqs)+ else+ simples eqs+ else do+ let allPreconds = map unifyItemToPredType unifications ++ preconds+ evM <- lift (evMagic tcs ct allDeps Set.empty allPreconds)+ case evM of+ Nothing ->+ simples eqs+ Just ev -> do+ -- We only record the unification derived from a wanted constraint+ -- when we can actually record evidence for a succesful solve.+ modify (\s -> s { stDeps = stDeps1+ , subst = subst1+ , evs = ev:evs+ , unsolved = []+ })+ simples (unsolved ++ eqs)++ simples (eq@NatCt{predicate=Right (ct,u@(x,y,b)), preconds, ctDeps}:eqs) = do+ SimplifyState{stDeps, subst, evs, leqsG, unsolved} <- get+ let u' = substsSOP subst (subtractIneq u)+ x' = substsSOP subst x+ y' = substsSOP subst y+ uS = (x',y',b)+ leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG+ | otherwise = leqsG+ ineqs = concat [ leqsG+ , map (substLeq subst) leqsG+ , map snd (rights (map predicate eqsG))+ ]+ allDeps = stDeps ++ ctDeps+ lift (tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs)))+ case runWriterT (isNatural u') of+ Just (True,knW) -> do+ evs' <- maybe evs (:evs) <$> lift (evMagic tcs ct allDeps knW preconds)+ modify (\s -> s {evs = evs', leqsG = leqsG'})+ simples eqs++ Just (False,_) | null preconds ->+ addContra (predicate eq) <$> simples eqs+ _ -> do+ let solvedIneq = mapMaybe runWriterT+ -- it is an inequality that can be instantly solved, such as+ -- `1 <= x^y`+ -- OR+ (instantSolveIneq depth u:+ instantSolveIneq depth uS:+ -- This inequality is either a given constraint, or it is a wanted+ -- constraint, which in normal form is equal to another given+ -- constraint, hence it can be solved.+ -- OR+ map (solveIneq depth u) ineqs +++ -- The above, but with valid substitutions applied to the wanted.+ map (solveIneq depth uS) ineqs)+ smallest = solvedInEqSmallestConstraint solvedIneq+ case smallest of+ (True,kW) -> do+ evs' <- maybe evs (:evs) <$> lift (evMagic tcs ct allDeps kW preconds)+ modify (\s -> s { stDeps = allDeps+ , evs = evs'+ , leqsG = leqsG'+ })+ simples eqs+ _ -> do+ modify (\s -> s {unsolved = eq:unsolved})+ simples eqs++ eqToLeq x y = [(x,y,True),(y,x,True)]+ substLeq s (x,y,b) = (substsSOP s x, substsSOP s y, b)++ isVarEqs (Left (_,S [P [V _]], S [P [V _]])) = True+ isVarEqs _ = False++ makeGivensSet :: [NatCt] -> NatCt -> [[NatCt]]+ makeGivensSet otherEqs varEq+ = let (noMentionsV,mentionsV) = partitionEithers+ (map (matchesVarEq varEq) otherEqs)+ (mentionsLHS,mentionsRHS) = partitionEithers mentionsV+ vS = varEq {predicate = swapVar (predicate varEq)}+ givensLHS = case mentionsLHS of+ [] -> []+ _ -> [mentionsLHS ++ ((varEq:mentionsRHS) ++ noMentionsV)]+ givensRHS = case mentionsRHS of+ [] -> []+ _ -> [mentionsRHS ++ (vS:mentionsLHS ++ noMentionsV)]+ in case mentionsV of+ [] -> [noMentionsV]+ _ -> givensLHS ++ givensRHS++ matchesVarEq :: NatCt+ -> NatCt+ -> Either NatCt (Either NatCt NatCt)+ matchesVarEq NatCt{predicate = Left (_, S [P [V v1]], S [P [V v2]])} r@(NatCt e _ _) =+ case e of+ Left (_,S [P [V v3]],_)+ | v1 == v3 -> Right (Left r)+ | v2 == v3 -> Right (Right r)+ Left (_,_,S [P [V v3]])+ | v1 == v3 -> Right (Left r)+ | v2 == v3 -> Right (Right r)+ Right (_,(S [P [V v3]],_,_))+ | v1 == v3 -> Right (Left r)+ | v2 == v3 -> Right (Right r)+ Right (_,(_,S [P [V v3]],_))+ | v1 == v3 -> Right (Left r)+ | v2 == v3 -> Right (Right r)+ _ -> Left r+ matchesVarEq _ _ = error "internal error"++ swapVar (Left (ct,S [P [V v1]], S [P [V v2]])) =+ Left (ct,S [P [V v2]], S [P [V v1]])+ swapVar _ = error "internal error"++ findFirstSimpliedWanted s1@(SimplifyResult {simplifiedWanteds, contradictions}) s2+ | not (null contradictions)+ || any (isWanted . ctEvidence . snd . fst) simplifiedWanteds+ = s1+ | otherwise+ = s2++addContra :: Either NatEquality NatInEquality -> SimplifyResult -> SimplifyResult+addContra contra sr = sr { contradictions = contra : contradictions sr }++-- If we allow negated numbers we simply do not emit the inequalities+-- derived from the subtractions that are converted to additions with a+-- negated operand+subToPred :: Opts -> LookedUpTyCons -> [(Type, Type)] -> [PredType]+subToPred Opts{..} tcs+ | negNumbers = const []+ | otherwise =+ -- Given 'a - b', require 'b <= a'.+ map (\ (a, b) -> mkLEqNat tcs b a)++-- | Extract all Nat equality and inequality constraints from another constraint.+toNatEquality :: Opts -> LookedUpTyCons -> TyConSubst -> Ct -> [NatCt]+toNatEquality opts tcs givensTyConSubst ct0+ | Just (((x,y), mbLTE), cos0) <- isNatRel tcs givensTyConSubst pred0+ , let+ ((x', cos1),k1) = runWriter (normaliseNat x)+ ((y', cos2),k2) = runWriter (normaliseNat y)+ preds = subToPred opts tcs (k1 ++ k2)+ = case mbLTE of+ Nothing ->+ -- Equality constraint: x ~ y+ [NatCt (Left (ct0, x', y')) preds (cos0 ++ cos1 ++ cos2)]+ Just b ->+ -- Inequality constraint: (x <=? y) ~ b+ [NatCt (Right (ct0, (x', y', b))) preds (cos0 ++ cos1 ++ cos2)]+ | otherwise+ = case classifyPredType pred0 of+ EqPred NomEq t1 t2+ -> goNomEq t1 t2+ ClassPred kn [x]+ -- From [G] KnownNat blah, also produce [G] 0 <= blah+ -- See https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94.+ | isGiven (ctEvidence ct0)+ , className kn == knownNatClassName+ , let ((x', cos0), ks) = runWriter (normaliseNat x)+ , let preds = subToPred opts tcs ks+ -> [NatCt (Right (ct0, (S [], x', True))) preds cos0]+ _ -> []+ where+ pred0 = ctPred ct0+ -- x ~ y+ goNomEq :: Type -> Type -> [NatCt]+ goNomEq lhs rhs+ -- Recur into a TyCon application for TyCons that we **do not** rewrite,+ -- e.g. peek inside the Maybe in 'Maybe (x + y) ~ Maybe (y + x)'.+ | Just (tc , xs) <- splitTyConApp_maybe lhs+ , Just (tc', ys) <- splitTyConApp_maybe rhs+ , tc == tc'+ , not $ tc `elem` [typeNatAddTyCon, typeNatSubTyCon, typeNatMulTyCon, typeNatExpTyCon]+ , let xys = zip xs ys+ -- Make sure not to recur into non-injective positions of type families,+ -- e.g. if we know 'F n ~ F m' that doesn't mean 'n ~ m'.+ subs =+ filter (not . uncurry eqType) $+ case tyConInjectivityInfo tc of+ Injective inj ->+ filterByList (inj ++ repeat True) xys+ _ ->+ -- However, it is okay to recur in the following specific+ -- exception:+ let (tcArgs,rest) = splitAt (tyConArity tc) xys+ diffs = filter (not . uncurry eqType) tcArgs+ in case diffs of+ -- 1. The types only differ in one argument position+ [(x,y)]+ | let xFVs = tyCoVarsOfType x+ , let yFVs = tyCoVarsOfType y+ -- 2. The argument must have variables, and they must+ -- all be skolem variables.+ , not (isEmptyVarSet xFVs)+ , allVarSet isSkolemTyVar xFVs+ -- 3. The variables in both argument postions must+ -- be the same.+ , xFVs == yFVs+ -> (x,y):rest+ _ -> rest+ = case concatMap (uncurry rewrite) subs of+ [] -> []+ [rw] -> [rw]+ rws ->+ -- For Given Cts, it's fine to extract multiple (in)equalities. However,+ -- for Wanted Cts we should not claim to solve the entire Ct when we+ -- only solve a part of the Ct. So when we can extra two or more inequalities+ -- from a Wanted Ct, we conservatively choose not to solve any of them.+ if isGiven (ctEvidence ct0) then+ rws+ else+ []+ | otherwise+ = rewrite lhs rhs++ rewrite :: Type -> Type -> [NatCt]+ rewrite x y+ | isNatKind (typeKind x)+ , isNatKind (typeKind y)+ , let ((x', cos1),k1) = runWriter (normaliseNat x)+ , let ((y', cos2),k2) = runWriter (normaliseNat y)+ , let preds = subToPred opts tcs (k1 ++ k2)+ = [NatCt (Left (ct0,x',y')) preds (cos1 ++ cos2)]+ | otherwise+ = []++ isNatKind :: Kind -> Bool+ isNatKind = (`eqType` natKind)++unifyItemToPredType :: CoreUnify -> PredType+unifyItemToPredType ui = mkEqPredRole Nominal ty1 ty2+ where+ ty1 = case ui of+ SubstItem {..} -> mkTyVarTy siVar+ UnifyItem {..} -> reifySOP siLHS+ ty2 = case ui of+ SubstItem {..} -> reifySOP siSOP+ UnifyItem {..} -> reifySOP siRHS+++unifyItemToGiven :: CtLoc -> [Coercion] -> CoreUnify -> TcPluginM Solve Ct+unifyItemToGiven loc deps ui = mkNonCanonical <$> newGiven loc pty (EvExpr (Coercion co))+ where+ ty1 = case ui of+ SubstItem {..} -> mkTyVarTy siVar+ UnifyItem {..} -> reifySOP siLHS+ ty2 = case ui of+ SubstItem {..} -> reifySOP siSOP+ UnifyItem {..} -> reifySOP siRHS++ pty = mkEqPredRole Nominal ty1 ty2+ co = mkPluginUnivCo "ghc-typelits-natnormalise" Nominal deps ty1 ty2++evSubtPreds :: CtLoc -> [PredType] -> TcPluginM Solve [Ct]+evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc)++evMagic ::+ -- | Known TyCon environment+ LookedUpTyCons ->+ -- | Constraint for which we are creating evidence+ Ct ->+ -- | Coercions in which the evidence depends+ [Coercion] ->+ -- | Types that we should be known to be a Natural+ Set CType ->+ -- | Inequalities that should hold+ [PredType] ->+ TcPluginM Solve (Maybe ((EvTerm, Ct), [Ct]))+evMagic tcs ct deps knW preds = do+ holeWanteds <- evSubtPreds (ctLoc ct) preds+ knWanted <- mapM (mkKnWanted (ctLoc ct)) (Set.elems knW)+ let newWant = knWanted ++ holeWanteds+ case classifyPredType $ ctEvPred $ ctEvidence ct of+ EqPred NomEq t1 t2 ->+ let ctEv = mkPluginUnivCo "ghc-typelits-natnormalise" Nominal deps t1 t2+ in return (Just ((EvExpr (Coercion ctEv), ct),newWant))+ IrredPred p ->+ let t1 = mkTyConApp (c0TyCon tcs) []+ co = mkPluginUnivCo "ghc-typelits-natnormalise" Representational deps t1 p+ dcApp = evDataConApp (c0DataCon tcs) [] []+ in return (Just ((EvExpr $ evCast dcApp co, ct),newWant))+ _ -> return Nothing++mkKnWanted+ :: CtLoc+ -> CType+ -> TcPluginM Solve Ct+mkKnWanted loc (CType ty) = do+ kc_clas <- tcLookupClass knownNatClassName+ let kn_pred = mkClassPred kc_clas [ty]+ wantedCtEv <- newWanted loc kn_pred+ return $ mkNonCanonical wantedCtEv
+ src/GHC/TypeLits/Normalise/Compat.hs view
@@ -0,0 +1,399 @@++{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE TemplateHaskellQuotes #-}++{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}++module GHC.TypeLits.Normalise.Compat+ ( LookedUpTyCons(..), lookupTyCons+ , upToGivens+ , mkLEqNat+ , Relation, isNatRel++ , UniqMap, intersectUniqMap_C, listToUniqMap, nonDetUniqMapToList++ , mkTcPluginSolveResult++ ) where++-- base+import Control.Arrow+ ( second )+import qualified Data.List.NonEmpty as NE+ ( toList )+import Data.Foldable+ ( asum )+import GHC.TypeNats+ ( CmpNat )+#if MIN_VERSION_ghc(9,3,0)+import qualified GHC.TypeError+ ( Assert )+#endif+#if MIN_VERSION_ghc(9,1,0)+import qualified Data.Type.Ord+ ( OrdCond, type (<=) )++#else+import GHC.TypeNats+ ( type (<=), type (<=?) )+#endif++-- ghc+import GHC.Builtin.Types+ ( isCTupleTyConName+ , promotedFalseDataCon, promotedTrueDataCon+ , promotedLTDataCon, promotedEQDataCon, promotedGTDataCon+ )+#if MIN_VERSION_ghc(9,1,0)+import GHC.Builtin.Types+ ( cTupleTyCon, cTupleDataCon )+#else+import GHC.Builtin.Types+ ( cTupleTyConName )+#endif+#if MIN_VERSION_ghc(9,7,0)+import GHC.Types.Unique.Map+ ( UniqMap, intersectUniqMap_C, listToUniqMap, nonDetUniqMapToList )+#else+import GHC.Types.Unique+ ( Uniquable )+import GHC.Types.Unique.FM+ ( intersectUFM_C, nonDetEltsUFM )+#endif++-- ghc-tcplugin-api+import GHC.TcPlugin.API+import GHC.TcPlugin.API.TyConSubst+ ( TyConSubst, splitTyConApp_upTo )++--------------------------------------------------------------------------------++data LookedUpTyCons+ = LookedUpTyCons+ {+#if MIN_VERSION_ghc(9,3,0)+ assertTyCon :: TyCon,+#endif+#if MIN_VERSION_ghc(9,1,0)+ -- | @<= :: k -> k -> Constraint@+ ordCondTyCon :: TyCon,+ leqTyCon :: TyCon,+#else+ -- | @<= :: Nat -> Nat -> Constraint@+ leqNatTyCon :: TyCon,+ -- | @<=? :: Nat -> Nat -> Constraint@+ leqQNatTyCon :: TyCon,+#endif+ cmpNatTyCon :: TyCon,+ c0TyCon :: TyCon,+ c0DataCon :: DataCon+ }++lookupTyCons :: TcPluginM Init LookedUpTyCons+lookupTyCons = do+ cmpNatT <- lookupTHName ''GHC.TypeNats.CmpNat >>= tcLookupTyCon+#if MIN_VERSION_ghc(9,3,0)+ assertT <- lookupTHName ''GHC.TypeError.Assert >>= tcLookupTyCon+#endif+#if MIN_VERSION_ghc(9,1,0)+ leqT <- lookupTHName ''(Data.Type.Ord.<=) >>= tcLookupTyCon+ ordCond <- lookupTHName ''Data.Type.Ord.OrdCond >>= tcLookupTyCon+ return $+ LookedUpTyCons+ { leqTyCon = leqT+ , ordCondTyCon = ordCond+# if MIN_VERSION_ghc(9,3,0)+ , assertTyCon = assertT+# endif+ , cmpNatTyCon = cmpNatT+ , c0TyCon = cTupleTyCon 0+ , c0DataCon = cTupleDataCon 0+ }+#else+ leqT <- lookupTHName ''(GHC.TypeNats.<=) >>= tcLookupTyCon+ leqQT <- lookupTHName ''(GHC.TypeNats.<=?) >>= tcLookupTyCon+ c0T <- tcLookupTyCon (cTupleTyConName 0)+ let c0D = tyConSingleDataCon c0T+ -- somehow looking up the 0-tuple data constructor fails+ -- with interface file errors, so use tyConSingleDataCon+ return $+ LookedUpTyCons+ { leqNatTyCon = leqT+ , leqQNatTyCon = leqQT+ , c0TyCon = c0T+ , c0DataCon = c0D+ , cmpNatTyCon = cmpNatT+ }+#endif++-- | The constraint @(a <= b)@.+mkLEqNat :: LookedUpTyCons -> Type -> Type -> PredType+mkLEqNat tcs a b =+#if MIN_VERSION_ghc(9,1,0)+ mkTyConApp (leqTyCon tcs) [natKind, a, b]+#else+ mkTyConApp (leqNatTyCon tcs) [a, b]+#endif++-- | Is this type 'True' or 'False'?+boolean_maybe :: TyConSubst -> Type -> Maybe (Bool, [Coercion])+boolean_maybe givensTyConSubst =+ upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys )+ where+ go tc []+ | tc == promotedTrueDataCon+ = Just True+ | tc == promotedFalseDataCon+ = Just False+ go _ _ = Nothing++-- | Is this type 'LT', 'EQ' or 'GT'?+ordering_maybe :: TyConSubst -> Type -> Maybe (Ordering, [Coercion])+ordering_maybe givensTyConSubst =+ upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys )+ where+ go tc []+ | tc == promotedLTDataCon+ = Just LT+ | tc == promotedEQDataCon+ = Just EQ+ | tc == promotedGTDataCon+ = Just GT+ go _ _ = Nothing++#if MIN_VERSION_ghc(9,1,0)+cmpNat_maybe :: LookedUpTyCons -> TyConSubst -> Type -> Maybe ((Type, Type), [Coercion])+cmpNat_maybe tcs givensTyConSubst =+ upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys )+ where+ go tc [x,y]+ | tc == cmpNatTyCon tcs+ = Just (x,y)+ go _ _ = Nothing+#endif++-- | Is this type @() :: Constraint@?+unitCTuple_maybe :: TyConSubst -> PredType -> Maybe ((), [Coercion])+unitCTuple_maybe givensTyConSubst =+ upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys )+ where+ go tc []+ | isCTupleTyConName (tyConName tc)+ = Just ()+ go _ _ = Nothing++-- | A relation between two natural numbers, @((x,y), mbRel)@.+--+-- The @mbRel@ value indicates the kind of relation:+--+-- - @Nothing@ <=> @x ~ y@,+-- - @Just b@ <=> @(x <=? y) ~ b@.+type Relation = ((Type, Type), Maybe Bool)++{- Note [Recognising Nat inequalities]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Recognising whether a type is an inequality between two natural numbers is+not as straightforward as one might initially think. The problem is that there+are many different built-in types that can be used to represent an equality of+natural numbers:++ 1. GHC.TypeNats.CmpNat, returning Ordering.+ This type family is primitive (on all GHC versions).+ 2. GHC.TypeNats.<=?, returning a Boolean.+ This type family is primitive prior to GHC 9.1, but is defined in+ terms of the 'OrdCond' type family starting in GHC 9.1.++ (NB: it also becomes poly-kinded starting in GHC 9.1.)+ 3. GHC.TypeNats.<=, which is defined:+ (a) as @x <= y@ <=> @(x <=? y) ~ True@ in GHC prior to 9.3.+ (b) as @Assert (x <=? y) ...@ in GHC 9.3 and above.++To catch all of these, we must thus handle all of the following type families:++ Case 1. CmpNat.+ Case 2. (<=?) in GHC 9.1 and prior.+ Case 3. OrdCond in GHC 9.1 and later.+ Case 4. Assert, in GHC 9.3 and later.++These are all the built-in type families defined in GHC used to express+inequalities between natural numbers.+-}++-- | Is this an equality or inequality between two natural numbers?+--+-- See Note [Recognising Nat inequalities].+isNatRel :: LookedUpTyCons -> TyConSubst -> PredType -> Maybe (Relation, [Coercion])+isNatRel tcs givensTyConSubst ty0+ | EqPred NomEq x y <- classifyPredType ty0+ = if+ -- (expr1 :: Nat) ~ (expr2 :: Nat)+ | all ( ( `eqType` natKind ) . typeKind ) [ x, y ]+ -> Just $ ( ( ( x, y ), Nothing ), [] )+ -- (b :: Bool) ~ y+ | Just ( b, cos1 ) <- boolean_maybe givensTyConSubst x+ -> second ( ++ cos1 ) <$> booleanRel b y+ -- x ~ (b :: Bool)+ | Just ( b, cos1 ) <- boolean_maybe givensTyConSubst y+ -> second ( ++ cos1 ) <$> booleanRel b x+ | Just ( o, cos1 ) <- ordering_maybe givensTyConSubst x+ -- (o :: Ordering) ~ y+ -> second ( ++ cos1 ) <$> orderingRel o y+ | Just ( o, cos1 ) <- ordering_maybe givensTyConSubst y+ -- x ~ (o :: Ordering)+ -> second ( ++ cos1 ) <$> orderingRel o x+ -- (() :: Constraint) ~ y+ | Just ( (), cos1 ) <- unitCTuple_maybe givensTyConSubst x+ -> second ( ++ cos1 ) <$> goTy y+ -- x ~ (() :: Constraint)+ | Just ( (), cos1 ) <- unitCTuple_maybe givensTyConSubst y+ -> second ( ++ cos1 ) <$> goTy x+ | otherwise+ -> Nothing+ | otherwise+ = goTy ty0+ where+ goTy :: PredType -> Maybe (Relation, [Coercion])+ goTy = upToGivens givensTyConSubst goTc++ goTc :: TyCon -> [Type] -> Maybe (Relation, [Coercion])+ goTc _tc _tys+#if MIN_VERSION_ghc(9,3,0)+ -- Look through 'Assert'.+ -- Case 4 in Note [Recognising Nat inequalities]+ | _tc == assertTyCon tcs+ , [ty, _] <- _tys+ = booleanRel True ty+#endif+ | otherwise+ = Nothing++ -- Recognise whether @(b :: Bool) ~ ty@ is an equality/inequality+ booleanRel :: Bool -> Type -> Maybe (Relation, [Coercion])+ booleanRel b = upToGivens givensTyConSubst (goBoolean b)++ goBoolean :: Bool -> TyCon -> [Type] -> Maybe (Relation, [Coercion])+ goBoolean b tc tys+#if MIN_VERSION_ghc(9,1,0)+ -- OrdCond (CmpNat x y) lt eq gt ~ b+ -- Case 3 in Note [Recognising Nat inequalities]+ | tc == ordCondTyCon tcs+ , [_,cmp,ltTy,eqTy,gtTy] <- tys+ , Just (lt, cos1) <- boolean_maybe givensTyConSubst ltTy+ , Just (eq, cos2) <- boolean_maybe givensTyConSubst eqTy+ , Just (gt, cos3) <- boolean_maybe givensTyConSubst gtTy+ , Just ((x,y), cos4) <- cmpNat_maybe tcs givensTyConSubst cmp+ = ( , cos1 ++ cos2 ++ cos3 ++ cos4 ) <$>+ if -- (x <= y) ~ b+ | lt && eq && not gt+ -> Just ((x,y), Just b)+ -- (x < y) ~ b+ -- <=>+ -- (y <= x) ~ not b+ | lt && not eq && not gt+ -> Just ((y,x), Just $ not b)+ -- (x >= y) ~ b+ -- <=>+ -- (y <= x) ~ b+ | not lt && eq && gt+ -> Just ((y,x), Just b)+ -- (x > y) ~ b+ -- <=>+ -- (x <= y) ~ not b+ | not lt && not eq && gt+ -> Just ((x,y), Just $ not b)+ -- x ~ y+ | ( b && not lt && eq && not gt )+ || ( not b && lt && not eq && gt )+ -> Just ((x,y), Nothing)+ | otherwise+ -> Nothing+#else+ -- (x <=? y) ~ b+ -- Case 2 in Note [Recognising Nat inequalities]+ | tc == leqQNatTyCon tcs+ , [x,y] <- tys+ = Just (((x,y), Just b), [])+#endif+ | otherwise+ = Nothing++ -- Recognise whether @(o :: Ordering) ~ ty@ is an equality/inequality+ orderingRel :: Ordering -> Type -> Maybe (Relation, [Coercion])+ orderingRel o = upToGivens givensTyConSubst (goOrdering o)++ goOrdering :: Ordering -> TyCon -> [Type] -> Maybe (Relation, [Coercion])+ goOrdering o tc tys+ -- CmpNat x y ~ o+ -- Case 1 in Note [Recognising Nat inequalities]+ | tc == cmpNatTyCon tcs+ , [x,y] <- tys+ = ( , [] ) <$>+ case o of+ EQ ->+ -- x ~ y+ Just ((x,y), Nothing)+ LT ->+ -- x < y <=> (y <= x) ~ False+ Just ((y,x), Just False)+ GT ->+ -- x > y <=> (x <= y) ~ False+ Just ((x,y), Just False)+ | otherwise+ = Nothing++upToGivens :: TyConSubst -> (TyCon -> [Type] -> Maybe (a, [Coercion])) -> Type -> Maybe (a, [Coercion])+upToGivens givensTyConSubst f ty =+ asum $ map ( \ (tc, tys, deps) -> second ( deps ++ ) <$> f tc tys ) $+ maybe [] NE.toList $ splitTyConApp_upTo givensTyConSubst ty++--------------------------------------------------------------------------------++#if !MIN_VERSION_ghc(9,7,0)++newtype UniqMap k a = UniqMap ( UniqFM k (k, a) )+ deriving (Eq, Functor)+type role UniqMap nominal representational++intersectUniqMap_C :: (a -> b -> c) -> UniqMap k a -> UniqMap k b -> UniqMap k c+intersectUniqMap_C f (UniqMap m1) (UniqMap m2) = UniqMap $ intersectUFM_C (\(k, a) (_, b) -> (k, f a b)) m1 m2+{-# INLINE intersectUniqMap_C #-}++listToUniqMap :: Uniquable k => [(k,a)] -> UniqMap k a+listToUniqMap kvs = UniqMap (listToUFM [ (k,(k,v)) | (k,v) <- kvs])+{-# INLINE listToUniqMap #-}++nonDetUniqMapToList :: UniqMap k a -> [(k, a)]+nonDetUniqMapToList (UniqMap m) = nonDetEltsUFM m+{-# INLINE nonDetUniqMapToList #-}++#endif++--------------------------------------------------------------------------------++mkTcPluginSolveResult :: [Ct] -> [(EvTerm, Ct)] -> [Ct]+ -> TcPluginSolveResult+#if MIN_VERSION_ghc(9,3,0)+mkTcPluginSolveResult = TcPluginSolveResult+#else+mkTcPluginSolveResult contras solved new =+ -- On GHC 9.2 and below, it's not possible to return+ -- both contradictions and solved/new constraints.+ --+ -- In general, we prefer returning solved constraints over contradictions.+ if null solved && not (null contras)+ then TcPluginContradiction contras+ else TcPluginOk solved new+#endif++--------------------------------------------------------------------------------
src/GHC/TypeLits/Normalise/SOP.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE LambdaCase #-} {-| Copyright : (C) 2015-2016, University of Twente, 2017 , QBayLogic B.V.@@ -73,6 +74,7 @@ x^(y*z) @ -}+ module GHC.TypeLits.Normalise.SOP ( -- * SOP types Symbol (..)@@ -85,16 +87,22 @@ , mergeSOPAdd , mergeSOPMul , normaliseExp+ , simplifySOP ) where --- External-import Data.Either (partitionEithers)-import Data.List (sort)+-- base+import Data.Either+ ( partitionEithers )+import Data.List+ ( sort ) --- GHC API-import Outputable (Outputable (..), (<+>), text, hcat, integer, punctuate)+-- ghc-tcplugin-api+import GHC.Utils.Outputable+ ( Outputable (..), (<+>), text, hcat, integer, punctuate ) +--------------------------------------------------------------------------------+ data Symbol v c = I Integer -- ^ Integer constant | C c -- ^ Non-integer constant@@ -120,7 +128,8 @@ (S ps1) == (S ps2) = ps1 == ps2 instance (Outputable v, Outputable c) => Outputable (SOP v c) where- ppr = hcat . punctuate (text " + ") . map ppr . unS+ ppr (S []) = integer 0+ ppr (S s) = hcat . punctuate (text " + ") . map ppr $ s instance (Outputable v, Outputable c) => Outputable (Product v c) where ppr = hcat . punctuate (text " * ") . map ppr . unP@@ -152,7 +161,7 @@ -- 2^3 ==> 8 -- (k ^ i) ^ j ==> k ^ (i * j) -- @-reduceExp :: (Ord v, Ord c) => Symbol v c -> Symbol v c+reduceExp :: (Outputable v, Outputable c, Ord v, Ord c) => Symbol v c -> Symbol v c reduceExp (E _ (P [(I 0)])) = I 1 -- x^0 ==> 1 reduceExp (E (S [P [I 0]]) _ ) = I 0 -- 0^x ==> 0 reduceExp (E (S [P [(I i)]]) (P [(I j)]))@@ -181,7 +190,7 @@ -- x^4 * x ==> x^5 -- y*y ==> y^2 -- @-mergeS :: (Ord v, Ord c) => Symbol v c -> Symbol v c+mergeS :: (Outputable v, Outputable c, Ord v, Ord c) => Symbol v c -> Symbol v c -> Either (Symbol v c) (Symbol v c) mergeS (I i) (I j) = Left (I (i * j)) -- 8 * 7 ==> 56 mergeS (I 1) r = Left r -- 1 * x ==> x@@ -237,7 +246,8 @@ -- xy + 2xy ==> 3xy -- xy + xy ==> 2xy -- @-mergeP :: (Eq v, Eq c) => Product v c -> Product v c+mergeP :: (Eq v, Eq c, Outputable v, Outputable c)+ => Product v c -> Product v c -> Either (Product v c) (Product v c) -- 2xy + 3xy ==> 5xy mergeP (P ((I i):is)) (P ((I j):js))@@ -264,7 +274,7 @@ -- (x + 2)^(2x) ==> (x^2 + 4xy + 4)^x -- (x + 2)^(y + 2) ==> 4x(2 + x)^y + 4(2 + x)^y + (2 + x)^yx^2 -- @-normaliseExp :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c+normaliseExp :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c -- b^1 ==> b normaliseExp b (S [P [I 1]]) = b @@ -275,7 +285,7 @@ normaliseExp b@(S [P [_]]) (S [e@(P [_])]) = S [P [reduceExp (E b e)]] -- (x + 2)^2 ==> x^2 + 4xy + 4-normaliseExp b (S [P [(I i)]]) =+normaliseExp b (S [P [(I i)]]) | i > 0 = foldr1 mergeSOPMul (replicate (fromInteger i) b) -- (x + 2)^(2x) ==> (x^2 + 4xy + 4)^x@@ -288,7 +298,7 @@ normaliseExp b (S [e]) = S [P [reduceExp (E b e)]] -- (x + 2)^(y + 2) ==> 4x(2 + x)^y + 4(2 + x)^y + (2 + x)^yx^2-normaliseExp b (S e) = foldr1 mergeSOPMul (map (normaliseExp b . S . (:[])) e)+normaliseExp b (S es) = foldr1 mergeSOPMul (map (normaliseExp b . S . (:[])) es) zeroP :: Product v c -> Bool zeroP (P ((I 0):_)) = True@@ -303,7 +313,7 @@ -- * 'mergeS' -- * 'mergeP' -- * 'reduceExp'-simplifySOP :: (Ord v, Ord c) => SOP v c -> SOP v c+simplifySOP :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c simplifySOP = repeatF go where go = mkNonEmpty@@ -321,12 +331,12 @@ {-# INLINEABLE simplifySOP #-} -- | Merge two SOP terms by additions-mergeSOPAdd :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c+mergeSOPAdd :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c mergeSOPAdd (S sop1) (S sop2) = simplifySOP $ S (sop1 ++ sop2) {-# INLINEABLE mergeSOPAdd #-} -- | Merge two SOP terms by multiplication-mergeSOPMul :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c+mergeSOPMul :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c mergeSOPMul (S sop1) (S sop2) = simplifySOP . S
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -5,21 +5,22 @@ Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> -} -{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE TupleSections #-} -{-# OPTIONS_GHC -fno-warn-unused-imports #-}-#if __GLASGOW_HASKELL__ < 801-#define nonDetCmpType cmpType-#endif+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-} module GHC.TypeLits.Normalise.Unify ( -- * 'Nat' expressions \<-\> 'SOP' terms CType (..) , CoreSOP , normaliseNat+ , normaliseNatEverywhere+ , normaliseSimplifyNat , reifySOP -- * Substitution on 'SOP' terms , UnifyItem (..)@@ -32,39 +33,65 @@ , unifiers -- * Free variables in 'SOP' terms , fvSOP+ -- * Inequalities+ , subtractIneq+ , solveIneq+ , ineqToSubst+ , instantSolveIneq+ , solvedInEqSmallestConstraint+ , negateProd -- * Properties , isNatural ) where --- External-import Data.Function (on)-import Data.List ((\\), intersect, mapAccumL, nub)+-- base+import Control.Arrow+ ( first, second )+import Control.Monad+ ( guard, zipWithM )+import Data.Either+ ( partitionEithers )+import Data.List+ ( (\\), intersect, nub, sort )+import Data.Maybe+ ( fromMaybe, mapMaybe, isJust )+import GHC.Base+ ( (==#), isTrue# )+import GHC.Integer+ ( smallInteger )+import GHC.Integer.Logarithms+ ( integerLogBase# ) -import GHC.Base (isTrue#,(==#))-import GHC.Integer (smallInteger)-import GHC.Integer.Logarithms (integerLogBase#)+-- containers+import Data.Set+ ( Set )+import qualified Data.Set as Set --- GHC API-import Outputable (Outputable (..), (<+>), ($$), text)-import TcPluginM (TcPluginM, tcPluginTrace)-import TcRnMonad (Ct, ctEvidence, isGiven)-import TcRnTypes (ctEvPred)-import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,- typeNatSubTyCon)-import Type (EqRel (NomEq), PredTree (EqPred), TyVar, classifyPredType,- coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy,- nonDetCmpType)-import TyCoRep (Type (..), TyLit (..))-import UniqSet (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets,- unitUniqSet)+-- ghc+import GHC.Builtin.Types.Literals+ ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon+ )+import GHC.Types.Unique.Set+ ( UniqSet+ , emptyUniqSet, unionManyUniqSets, unionUniqSets, unitUniqSet+ , nonDetEltsUniqSet, elementOfUniqSet+ ) --- Internal+-- ghc-tcplugin-api+import GHC.TcPlugin.API+import GHC.Utils.Outputable+++-- ghc-typelits-natnormalise import GHC.TypeLits.Normalise.SOP --- Used for haddock-import GHC.TypeLits (Nat)+-- transformers+import Control.Monad.Trans.Writer.Strict+ ( Writer, WriterT(..), runWriter, tell ) +--------------------------------------------------------------------------------+ newtype CType = CType { unCType :: Type } deriving Outputable @@ -79,25 +106,109 @@ type CoreProduct = Product TyVar CType type CoreSymbol = Symbol TyVar CType --- | Convert a type of /kind/ 'GHC.TypeLits.Nat' to an 'SOP' term, but--- only when the type is constructed out of:------ * literals--- * type variables--- * Applications of the arithmetic operators @(+,-,*,^)@-normaliseNat :: Type -> CoreSOP-normaliseNat ty | Just ty1 <- coreView ty = normaliseNat ty1-normaliseNat (TyVarTy v) = S [P [V v]]-normaliseNat (LitTy (NumTyLit i)) = S [P [I i]]-normaliseNat (TyConApp tc [x,y])- | tc == typeNatAddTyCon = mergeSOPAdd (normaliseNat x) (normaliseNat y)- | tc == typeNatSubTyCon = mergeSOPAdd (normaliseNat x)- (mergeSOPMul (S [P [I (-1)]])- (normaliseNat y))- | tc == typeNatMulTyCon = mergeSOPMul (normaliseNat x) (normaliseNat y)- | tc == typeNatExpTyCon = normaliseExp (normaliseNat x) (normaliseNat y)-normaliseNat t = S [P [C (CType t)]]+-- | Convert a type of /kind/ 'GHC.TypeLits.Nat' to an 'SOP' term+normaliseNat :: Type -> Writer [(Type,Type)] (CoreSOP, [Coercion])+normaliseNat ty+ | Just (tc, xs) <- splitTyConApp_maybe ty+ = goTyConApp tc xs+ | Just i <- isNumLitTy ty+ = return (S [P [I i]], [])+ | Just v <- getTyVar_maybe ty+ = return (S [P [V v]], [])+ | otherwise+ = return (S [P [C (CType ty)]], [])+ where+ goTyConApp :: TyCon -> [Type] -> Writer [(Type,Type)] (CoreSOP, [Coercion])+ goTyConApp tc [x,y]+ | tc == typeNatAddTyCon =+ do (x', cos1) <- normaliseNat x+ (y', cos2) <- normaliseNat y+ return (mergeSOPAdd x' y', cos1 ++ cos2)+ | tc == typeNatSubTyCon = do+ (x', cos1) <- normaliseNat x+ (y', cos2) <- normaliseNat y+ tell [(reifySOP $ simplifySOP x', reifySOP $ simplifySOP y')]+ return (mergeSOPAdd x' (mergeSOPMul (S [P [I (-1)]]) y'), cos1 ++ cos2)+ | tc == typeNatMulTyCon =+ do (x', cos1) <- normaliseNat x+ (y', cos2) <- normaliseNat y+ return (mergeSOPMul x' y', cos1 ++ cos2)+ | tc == typeNatExpTyCon =+ do (x', cos1) <- normaliseNat x+ (y', cos2) <- normaliseNat y+ return (normaliseExp x' y', cos1 ++ cos2)+ goTyConApp tc xs+ = do (xs', cos') <- fmap unzip (traverse normaliseSimplifyNat xs)+ return (S [P [C (CType (mkTyConApp tc xs'))]], concat cos') +knownTyCons :: [TyCon]+knownTyCons = [typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon, typeNatAddTyCon]+++-- | Runs writer action. If the result is /Nothing/, writer actions will be+-- discarded.+maybeRunWriter+ :: Monoid a+ => Writer a (Maybe b)+ -> Writer a (Maybe b)+maybeRunWriter w =+ case runWriter w of+ (Nothing, _) -> pure Nothing+ (b, a) -> tell a >> pure b++-- | Applies 'normaliseNat' and 'simplifySOP' to type or predicates to reduce+-- any occurrences of sub-terms of /kind/ 'GHC.TypeLits.Nat'. If the result is+-- the same as input, returns @'Nothing'@.+normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))+normaliseNatEverywhere ty0+ | Just (tc, fields) <- splitTyConApp_maybe ty0+ = if tc `elem` knownTyCons+ then do+ -- Normalize under current type constructor application. 'go' skips all+ -- known type constructors.+ ty1M <- maybeRunWriter (go tc fields)+ let (ty1, cos1) = fromMaybe (ty0, []) ty1M+ -- Normalize (subterm-normalized) type given to 'normaliseNatEverywhere'+ (ty2, cos2) <- normaliseSimplifyNat ty1+ -- TODO: 'normaliseNat' could keep track whether it changed anything. That's+ -- TODO: probably cheaper than checking for equality here.+ pure $+ if ty2 `eqType` ty1+ then second (cos1 ++) <$> ty1M+ else Just (ty2, cos1 ++ cos2)+ else+ go tc fields++ | otherwise+ = pure Nothing+ where++ -- Normalize given type, but ignore all top-level+ go :: TyCon -> [Type] -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))+ go tc_ fields0_ = do+ fields1_ <- mapM (maybeRunWriter . cont) fields0_+ if any isJust fields1_+ then do+ let cos' = concat $ mapMaybe (fmap snd) fields1_+ ty' = mkTyConApp tc_ (zipWith (\ f0 f1 -> maybe f0 fst f1) fields0_ fields1_)+ pure (Just (ty', cos'))+ else+ pure Nothing+ where+ cont ty'+ | tc_ `elem` knownTyCons+ , Just (tc', flds') <- splitTyConApp_maybe ty'+ = go tc' flds'+ | otherwise+ = normaliseNatEverywhere ty'++normaliseSimplifyNat :: Type -> Writer [(Type, Type)] (Type, [Coercion])+normaliseSimplifyNat ty+ | typeKind ty `eqType` natKind = do+ (ty', cos1) <- normaliseNat ty+ return $ (reifySOP $ simplifySOP ty', cos1)+ | otherwise = return (ty, [])+ -- | Convert a 'SOP' term back to a type of /kind/ 'GHC.TypeLits.Nat' reifySOP :: CoreSOP -> Type reifySOP = combineP . map negateP . unS@@ -140,17 +251,32 @@ reifyProduct :: CoreProduct -> Type reifyProduct (P ps) = let ps' = map reifySymbol (foldr mergeExp [] ps)- in foldr (\t1 t2 -> mkTyConApp typeNatMulTyCon [t1,t2]) (head ps') (tail ps')+ in foldr1 (\t1 t2 -> mkTyConApp typeNatMulTyCon [t1,t2]) ps' where -- "2 ^ -1 * 2 ^ a" must be merged into "2 ^ (a-1)", otherwise GHC barfs -- at the "2 ^ -1" because of the negative exponent. mergeExp :: CoreSymbol -> [Either CoreSymbol (CoreSOP,[CoreProduct])] -> [Either CoreSymbol (CoreSOP,[CoreProduct])]- mergeExp (E s p) [] = [Right (s,[p])]+ mergeExp (E (S [P [I 1]]) _) ys = ys+ mergeExp (E s p) [] = [Right (s,[p])]+ mergeExp (E (S [P [I s1]]) p1) (y:ys)+ | Right ((S [P [I s2]]), p2s) <- y+ , let s = gcd s1 s2+ t1 = s1 `quot` s+ t2 = s2 `quot` s+ , s > 1+ -- Deal with e.g. "2 ^ -1 * 6 ^ x", where the bases differ.+ --+ -- (s * t1) ^ p1 * (s * t2) ^ (p2 + ...) * rest+ -- ===>+ -- s ^ (p1 + p2 + ...) * t1 ^ p1 * t2 ^ (p2 + ..) * rest+ = Right (S [P [I s]], (p1:p2s)) :+ mergeExp (E (S [P [I t1]]) p1)+ (Right ((S [P [I t2]]), p2s):ys) mergeExp (E s1 p1) (y:ys)- | Right (s2,p2) <- y+ | Right (s2,p2s) <- y , s1 == s2- = Right (s1,(p1:p2)) : ys+ = Right (s1,(p1:p2s)) : ys | otherwise = Right (s1,[p1]) : y : ys mergeExp x ys = Left x : ys@@ -165,16 +291,87 @@ ,reifySOP (S s2) ] +-- | Simplify an inequality by first calling 'subtractIneq', producing a SOP+-- term, and then creating a new inequality by moving all the terms with+-- negative coefficients to one side.+--+-- Returns 'Nothing' if it is not able to simplify the original inequality.+simplifyIneq :: Ineq -> Maybe Ineq+simplifyIneq ineq@(x, y, isLE)+ = if x' == x && y' == y+ then Nothing+ else Just (x', y', isLE)+ where+ S ps = subtractIneq ineq+ -- We need to sort the products in order to retain our canonical form,+ -- not sorting would result in the following rewrite:+ --+ -- 2 * a + b ~ 5 ==>+ -- 5 + -1 * b + -2 * a ==>+ -- b + 2 * a ~ 5+ --+ -- Which lead to issue #113+ (sort -> neg, sort -> pos) = partitionEithers $ map classify ps+ (x', y') =+ if isLE+ then ( S neg, S pos )+ else ( S pos, S neg )+ classify :: CoreProduct -> Either CoreProduct CoreProduct+ classify p@(P (I i : _))+ | i < 0+ = Left $ negateProd p+ classify prod+ = Right prod++negateProd :: CoreProduct -> CoreProduct+negateProd (P (I i : r)) =+ -- preserve normal form+ if i == (-1)+ then+ if null r+ then P [I 1]+ else P r+ else P $ I (negate i) : r+negateProd (P r) = P $ I (-1) : r++-- | Subtract an inequality, in order to either:+--+-- * See if the smallest solution is a natural number+-- * Cancel sums, i.e. monotonicity of addition+--+-- @+-- subtractIneq (2*y <=? 3*x ~ True) = 3*x + (-2)*y+-- subtractIneq (2*y <=? 3*x ~ False) = -3*x + (-2)*y+-- @+subtractIneq+ :: (CoreSOP, CoreSOP, Bool)+ -> CoreSOP+subtractIneq (x,y,isLE)+ | isLE+ -- NB: keep orientations+ = mergeSOPAdd (mergeSOPMul (S [P [I (-1)]]) x) y+ | otherwise+ = mergeSOPAdd x (mergeSOPMul (S [P [I (-1)]]) (mergeSOPAdd y (S [P [I 1]])))++-- | Give the smallest solution for an inequality+ineqToSubst+ :: Ineq+ -> Maybe CoreUnify+ineqToSubst (x,S [P [V v]],True)+ = Just (SubstItem v x)+ineqToSubst _+ = Nothing+ -- | A substitution is essentially a list of (variable, 'SOP') pairs, -- but we keep the original 'Ct' that lead to the substitution being -- made, for use when turning the substitution back into constraints. type CoreUnify = UnifyItem TyVar CType -data UnifyItem v c = SubstItem { siVar :: v- , siSOP :: SOP v c+data UnifyItem v c = SubstItem { siVar :: v+ , siSOP :: SOP v c }- | UnifyItem { siLHS :: SOP v c- , siRHS :: SOP v c+ | UnifyItem { siLHS :: SOP v c+ , siRHS :: SOP v c } deriving Eq @@ -183,18 +380,18 @@ ppr (UnifyItem {..}) = ppr siLHS <+> text " :~ " <+> ppr siRHS -- | Apply a substitution to a single normalised 'SOP' term-substsSOP :: (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c+substsSOP :: (Outputable v, Outputable c, Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c substsSOP [] u = u substsSOP ((SubstItem {..}):s) u = substsSOP s (substSOP siVar siSOP u) substsSOP ((UnifyItem {}):s) u = substsSOP s u -substSOP :: (Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c-substSOP tv e = foldr1 mergeSOPAdd . map (substProduct tv e) . unS+substSOP :: (Outputable v, Outputable c, Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c+substSOP tv e = foldr mergeSOPAdd (S []) . map (substProduct tv e) . unS -substProduct :: (Ord v, Ord c) => v -> SOP v c -> Product v c -> SOP v c+substProduct :: (Outputable v, Outputable c, Ord v, Ord c) => v -> SOP v c -> Product v c -> SOP v c substProduct tv e = foldr1 mergeSOPMul . map (substSymbol tv e) . unP -substSymbol :: (Ord v, Ord c) => v -> SOP v c -> Symbol v c -> SOP v c+substSymbol :: (Outputable v, Outputable c, Ord v, Ord c) => v -> SOP v c -> Symbol v c -> SOP v c substSymbol _ _ s@(I _) = S [P [s]] substSymbol _ _ s@(C _) = S [P [s]] substSymbol tv e (V tv')@@ -203,7 +400,7 @@ substSymbol tv e (E s p) = normaliseExp (substSOP tv e s) (substProduct tv e p) -- | Apply a substitution to a substitution-substsSubst :: (Ord v, Ord c) => [UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c]+substsSubst :: (Outputable v, Outputable c, Ord v, Ord c) => [UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c] substsSubst s = map subt where subt si@(SubstItem {..}) = si {siSOP = substsSOP s siSOP}@@ -226,28 +423,33 @@ -- same, then we 'Win' if @u@ and @v@ are equal, and 'Lose' otherwise. -- -- If @u@ and @v@ do not have the same free variables, we result in a 'Draw',--- ware @u@ and @v@ are only equal when the returned 'CoreSubst' holds.-unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult+-- where @u@ and @v@ are only equal when the returned 'CoreSubst' holds.+unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM Solve UnifyResult unifyNats ct u v = do tcPluginTrace "unifyNats" (ppr ct $$ ppr u $$ ppr v) return (unifyNats' ct u v) unifyNats' :: Ct -> CoreSOP -> CoreSOP -> UnifyResult unifyNats' ct u v- = if eqFV u v- then if containsConstants u || containsConstants v- then if u == v- then Win- else Draw (filter diffFromConstraint (unifiers ct u v))- else if u == v- then Win- else Lose- else Draw (filter diffFromConstraint (unifiers ct u v))+ | u == v+ = Win+ | Just unifs <- unifiers ct u v+ , let newUnifs = if isGiven (ctEvidence ct)+ then unifs+ else filter diffFromConstraint unifs+ = Draw newUnifs+ | otherwise+ = Lose where- -- A unifier is only a unifier if differs from the original constraint++ -- A unifier is only a unifier if it differs from the original constraint diffFromConstraint (UnifyItem x y) = not (x == u && y == v)- diffFromConstraint _ = True + -- SubstItems can be in different orders+ diffFromConstraint (SubstItem x y) =+ not $ (S [P [V x]] == u && y == v)+ || (S [P [V x]] == v && y == u)+ -- | Find unifiers for two SOP terms -- -- Can find the following unifiers:@@ -281,39 +483,40 @@ -- @ -- [a := b] -- @-unifiers :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]+unifiers :: Ct -> CoreSOP -> CoreSOP -> Maybe [CoreUnify] unifiers ct u@(S [P [V x]]) v- = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 _- | CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct) -> [SubstItem x v]- _ -> []+ | EqPred NomEq t1 _ <- classifyPredType $ ctEvPred $ ctEvidence ct+ , CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct)+ = return [SubstItem x v] unifiers ct u v@(S [P [V x]])- = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq _ t2- | CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct) -> [SubstItem x u]- _ -> []+ | EqPred NomEq _ t2 <- classifyPredType $ ctEvPred $ ctEvidence ct+ , CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct)+ = return [SubstItem x u] unifiers ct u@(S [P [C _]]) v- = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2- | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 -> [UnifyItem u v]- _ -> []+ | EqPred NomEq t1 t2 <- classifyPredType $ ctEvPred $ ctEvidence ct+ , CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2+ = return [UnifyItem u v] unifiers ct u v@(S [P [C _]])- = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2- | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 -> [UnifyItem u v]- _ -> []+ | EqPred NomEq t1 t2 <- classifyPredType $ ctEvPred $ ctEvidence ct+ , CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2+ = return [UnifyItem u v] unifiers ct u v = unifiers' ct u v -unifiers' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]-unifiers' _ct (S [P [V x]]) (S []) = [SubstItem x (S [P [I 0]])]-unifiers' _ct (S []) (S [P [V x]]) = [SubstItem x (S [P [I 0]])]--unifiers' _ct (S [P [V x]]) s = [SubstItem x s]-unifiers' _ct s (S [P [V x]]) = [SubstItem x s]+unifiers' :: Ct -> CoreSOP -> CoreSOP -> Maybe [CoreUnify]+unifiers' _ct (S []) (S []) = return [] -unifiers' _ct s1@(S [P [C _]]) s2 = [UnifyItem s1 s2]-unifiers' _ct s1 s2@(S [P [C _]]) = [UnifyItem s1 s2]+unifiers' _ct (S [P [V x]]) (S []) = return [SubstItem x (S [P [I 0]])]+unifiers' _ct (S []) (S [P [V x]]) = return [SubstItem x (S [P [I 0]])] +unifiers' _ct (S [P [V x]]) s = do+ guard $ canBeNatural s+ return [SubstItem x s]+unifiers' _ct s (S [P [V x]]) = do+ guard $ canBeNatural s+ return [SubstItem x s]+unifiers' _ct s1@(S [P [C {}]]) s2@(S [P [C {}]])+ | s1 == s2+ = return [] -- (z ^ a) ~ (z ^ b) ==> [a := b] unifiers' ct (S [P [E s1 p1]]) (S [P [E s2 p2]])@@ -324,56 +527,54 @@ | all (`elem` p2) s1 = let base = intersect s1 p2 diff = p2 \\ s1- in unifiers ct (S [P diff]) (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]])+ in unifiers' ct (S [P diff]) (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) unifiers' ct (S [P p2]) (S [P [E (S [P s1]) p1]]) | all (`elem` p2) s1 = let base = intersect s1 p2 diff = p2 \\ s1- in unifiers ct (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) (S [P diff])+ in unifiers' ct (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) (S [P diff]) -- (i ^ a) ~ j ==> [a := round (logBase i j)], when `i` and `j` are integers, -- and `ceiling (logBase i j) == floor (logBase i j)` unifiers' ct (S [P [E (S [P [I i]]) p]]) (S [P [I j]])- = case integerLogBase i j of- Just k -> unifiers' ct (S [p]) (S [P [I k]])- Nothing -> []+ | Just k <- integerLogBase i j+ = unifiers' ct (S [p]) (S [P [I k]]) unifiers' ct (S [P [I j]]) (S [P [E (S [P [I i]]) p]])- = case integerLogBase i j of- Just k -> unifiers' ct (S [p]) (S [P [I k]])- Nothing -> []+ | Just k <- integerLogBase i j+ = unifiers' ct (S [p]) (S [P [I k]]) -- a^d * a^e ~ a^c ==> [c := d + e]-unifiers' ct (S [P [E s1 p1]]) (S [p2]) = case collectBases p2 of- Just (b:bs,ps) | all (== s1) (b:bs) ->- unifiers' ct (S [p1]) (S ps)- _ -> []+unifiers' ct (S [P [E s1 p1]]) (S [p2])+ | Just (b:bs,ps) <- collectBases p2+ , all (== s1) (b:bs)+ = unifiers' ct (S [p1]) (S ps) -unifiers' ct (S [p2]) (S [P [E s1 p1]]) = case collectBases p2 of- Just (b:bs,ps) | all (== s1) (b:bs) ->- unifiers' ct (S ps) (S [p1])- _ -> []+unifiers' ct (S [p2]) (S [P [E s1 p1]])+ | Just (b:bs,ps) <- collectBases p2+ , all (== s1) (b:bs)+ = unifiers' ct (S ps) (S [p1]) -- (i * a) ~ j ==> [a := div j i] -- Where 'a' is a variable, 'i' and 'j' are integer literals, and j `mod` i == 0-unifiers' ct (S [P ((I i):ps)]) (S [P [I j]]) =- case safeDiv j i of- Just k -> unifiers' ct (S [P ps]) (S [P [I k]])- _ -> []+unifiers' ct (S [P ((I i):ps)]) (S [P [I j]])+ | Just k <- safeDiv j i+ , not (null ps)+ = unifiers' ct (S [P ps]) (S [P [I k]]) -unifiers' ct (S [P [I j]]) (S [P ((I i):ps)]) =- case safeDiv j i of- Just k -> unifiers' ct (S [P ps]) (S [P [I k]])- _ -> []+unifiers' ct (S [P [I j]]) (S [P ((I i):ps)])+ | Just k <- safeDiv j i+ , not (null ps)+ = unifiers' ct (S [P ps]) (S [P [I k]]) -- (2*a) ~ (2*b) ==> [a := b] -- unifiers' ct (S [P (p:ps1)]) (S [P (p':ps2)]) -- | p == p' = unifiers' ct (S [P ps1]) (S [P ps2]) -- | otherwise = [] unifiers' ct (S [P ps1]) (S [P ps2])- | null psx = []- | otherwise = unifiers' ct (S [P ps1'']) (S [P ps2''])+ | not $ null psx+ = unifiers' ct (S [P ps1'']) (S [P ps2'']) where ps1' = ps1 \\ psx ps2' = ps2 \\ psx@@ -383,17 +584,24 @@ | otherwise = ps2' psx = intersect ps1 ps2 --- (2 + a) ~ 5 ==> [a := 3]-unifiers' ct (S ((P [I i]):ps1)) (S ((P [I j]):ps2))- | i < j = unifiers' ct (S ps1) (S ((P [I (j-i)]):ps2))- | i > j = unifiers' ct (S ((P [I (i-j)]):ps1)) (S ps2)- -- (a + c) ~ (b + c) ==> [a := b]-unifiers' ct (S ps1) (S ps2)- | null psx = case concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2) of- [] -> unifiers'' ct (S ps1) (S ps2)- ks -> nub ks- | otherwise = unifiers' ct (S ps1'') (S ps2'')+--+-- NB: this also handles situations such as (2 + x) ~ 5 ==> [x := 3].+unifiers' ct s1@(S ps1) s2@(S ps2)+ | not $ null psx+ = unifiers' ct (S ps1'') (S ps2'')+ | Just (s1',s2',_) <- simplifyIneq (s1, s2, True)+ = unifiers' ct s1' s2'+ | Just term_unifs <- termByTerm ct ps1 ps2+ = Just term_unifs+ -- If there are only two variables, try to collect them on either side.+ -- This makes 'termByTerm' more likely to succeed.+ | Just (S coll1, S coll2) <- partitionTerms ps1 ps2+ , Just term_unifs <- termByTerm ct coll1 coll2+ = Just term_unifs+ | null psx+ , isGiven (ctEvidence ct)+ = unifiers'' ct (S ps1) (S ps2) where ps1' = ps1 \\ psx ps2' = ps2 \\ psx@@ -403,12 +611,86 @@ | otherwise = ps2' psx = intersect ps1 ps2 -unifiers'' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]+-- Don't generate unify items where one of the sides is an empty sum (i.e.) zero+-- Doing so leads to poor error messages, see #114+unifiers' _ (S []) _ = return []+unifiers' _ _ (S []) = return []+unifiers' _ s1 s2 = return [UnifyItem s1 s2]++-- | Try to match the two expressions term-by-term.+-- If this produces a **single unifier**, then we succeed.+--+-- Example: x + 3^(x+2) ~ 2*y - 3^(2*(y+1))+--+-- We recur on each pair, (x, 2*y), (3^(x+2),3^(2*(y+1))).+-- This produces a single unifier "x ~ 2*y", so we proceed.+--+-- NB: this is somewhat fragile: if one moves the terms with negative+-- coefficients to the other side, due to the variable ordering x < y,+-- we would get:+--+-- x + 3^(2*(y+1)) ~ 3^(x+2) + 2*y+--+-- for which the same approach fails. So we use 'partitionTerms' as a heuristic+-- in the case there are only two free variables.+-- See https://github.com/clash-lang/ghc-typelits-natnormalise/issues/96.+termByTerm :: Ct -> [CoreProduct] -> [CoreProduct] -> Maybe [CoreUnify]+termByTerm ct ps1 ps2+ | length ps1 == length ps2+ , length ps1 > 1+ , Just u@[_] <- unifs+ = Just u+ | otherwise+ = Nothing+ where+ unifs = fmap (nub . concat) (zipWithM (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2)++-- | If an equality only contains two free variables, try to collect+-- terms with either FV on either side of the equality.+--+-- This makes 'termByTerm' more likely to succeed.+partitionTerms :: [CoreProduct] -> [CoreProduct] -> Maybe (CoreSOP, CoreSOP)+partitionTerms lhs rhs+ | [fv1, fv2] <- fvs+ , Just (lhs1, lhs2) <- mbPairs fv1 fv2 lhs+ , Just (rhs1, rhs2) <- mbPairs fv1 fv2 rhs+ = Just $+ let (lhs', rhs') =+ if length rhs1 + length lhs2 <= length lhs1 + length rhs2+ then (lhs1 ++ map negateProd rhs1, map negateProd lhs2 ++ rhs2)+ else (map negateProd lhs1 ++ rhs1, lhs2 ++ map negateProd rhs2)+ in (simplifySOP (S lhs'), simplifySOP (S rhs'))+ | otherwise+ = Nothing+ where+ fvs :: [TyVar]+ fvs = nonDetEltsUniqSet $ fvSOP (S $ lhs ++ rhs)++ mbPairs :: TyVar -> TyVar -> [CoreProduct] -> Maybe ([CoreProduct], [CoreProduct])+ mbPairs fv1 fv2 x = partitionEithers <$> traverse ( collect fv1 fv2 ) x++ collect :: TyVar -> TyVar -> CoreProduct -> Maybe (Either CoreProduct CoreProduct)+ collect fv1 fv2 tm =+ let tmFvs = fvProduct tm+ in case (fv1 `elementOfUniqSet` tmFvs, fv2 `elementOfUniqSet` tmFvs) of+ (True, False) -> Just $ Left tm+ (False, True) -> Just $ Right tm+ _ -> Nothing++unifiers'' :: Ct -> CoreSOP -> CoreSOP -> Maybe [CoreUnify] unifiers'' ct (S [P [I i],P [V v]]) s2- | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate i)]]))]+ | isGiven (ctEvidence ct)+ , let s' = mergeSOPAdd s2 (S [P [I (negate i)]])+ = if canBeNatural s'+ then Just [SubstItem v s']+ else Nothing unifiers'' ct s1 (S [P [I i],P [V v]])- | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate i)]]))]-unifiers'' _ _ _ = []+ | isGiven (ctEvidence ct)+ , let s' = mergeSOPAdd s1 (S [P [I (negate i)]])+ = if canBeNatural s'+ then Just [SubstItem v s']+ else Nothing+unifiers'' _ _ _ = Just [] collectBases :: CoreProduct -> Maybe ([CoreSOP],[CoreProduct]) collectBases = fmap unzip . traverse go . unP@@ -429,12 +711,6 @@ fvSymbol (V v) = unitUniqSet v fvSymbol (E s p) = fvSOP s `unionUniqSets` fvProduct p -eqFV :: CoreSOP -> CoreSOP -> Bool-eqFV = (==) `on` fvSOP--containsConstants :: CoreSOP -> Bool-containsConstants = any (any (\c -> case c of {(C _) -> True; _ -> False}) . unP) . unS- safeDiv :: Integer -> Integer -> Maybe Integer safeDiv i j | j == 0 = Just 0@@ -454,24 +730,49 @@ else Just (smallInteger z1) integerLogBase _ _ = Nothing -isNatural :: CoreSOP -> Maybe Bool-isNatural (S []) = return True-isNatural (S [P []]) = return True-isNatural (S [P (I i:ps)])- | i >= 0 = isNatural (S [P ps])- | otherwise = return False-isNatural (S [P (V _:ps)]) = isNatural (S [P ps])--- This is a quick hack, it determines that+-- | Might this be a natural number? ----- > a^b - 1+-- Equivalently: it is not the case that this is definitely not a natural number. ----- is a natural number as long as 'a' and 'b' are natural numbers.--- This used to assert that:+-- For example, @-1@ is definitely not a natural number, while @α@ or+-- @-2 * β@ could both be natural numbers (where @α, β@ are metavariables).+canBeNatural :: CoreSOP -> Bool+canBeNatural = maybe True fst . runWriterT . isNatural++-- | Is this a natural number? ----- > (1 <=? a^b) ~ True-isNatural (S [P [I (-1)],P [E s p]]) = (&&) <$> isNatural s <*> isNatural (S [p])+-- - @Just True@ <=> definitely a natural number+-- - @Just False@ <=> definitely not a natural number+-- - @Nothing@ <=> not sure+--+-- The 'Set CType' writer accumulator returns inner types that must also be+-- positive for the overall 'CoreSOP' to be positive.+isNatural :: CoreSOP -> WriterT (Set CType) Maybe Bool+isNatural (S []) = return True+isNatural (S [P []]) = return True+isNatural (S [P (I i:ps)]) =+ case compare i 0 of+ EQ -> return True+ GT ->+ -- NB: assumes the SOP term has been normalised, so no possibly of+ -- a second negative constant factor to cancel out this one.+ isNatural (S [P ps])+ LT ->+ -- '-1 * ty' can be a natural number if 'ty' ends up being zero+ if any canBeZero ps+ then WriterT Nothing+ else return False+isNatural (S [P (V _:ps)]) = isNatural (S [P ps])+isNatural (S [P (E s p:ps)]) = do+ sN <- isNatural s+ pN <- isNatural (S [p])+ if sN && pN+ then isNatural (S [P ps])+ else WriterT Nothing -- We give up for all other products for now-isNatural (S [P _]) = Nothing+isNatural (S [P (C c:ps)]) = do+ tell (Set.singleton c)+ isNatural (S [P ps]) -- Adding two natural numbers is also a natural number isNatural (S (p:ps)) = do pN <- isNatural (S [p])@@ -479,6 +780,363 @@ case (pN,pK) of (True,True) -> return True -- both are natural (False,False) -> return False -- both are non-natural- _ -> Nothing+ _ -> WriterT Nothing -- if one is natural and the other isn't, then their sum *might* be natural, -- but we simply cant be sure.++-- | Can this 'CoreSymbol' be zero?+--+-- Examples:+--+-- - the literal '0',+-- - a metavariable,+-- - a type family application.+canBeZero :: CoreSymbol -> Bool+canBeZero (I i) = i == 0+canBeZero (C {}) = True -- e.g. 'F 3' where 'F' is a type family+canBeZero (E (S es) _)+ | [P bs] <- es+ = any canBeZero bs+ | otherwise+ = True+canBeZero (V {}) = True -- e.g. 'tau' where 'tau' is an unfilled metavariable++-- | Try to solve inequalities+solveIneq+ :: Word+ -- ^ Solving depth+ -> Ineq+ -- ^ Inequality we want to solve+ -> Ineq+ -- ^ Given/proven inequality+ -> WriterT (Set CType) Maybe Bool+ -- ^ Solver result+ --+ -- * /Nothing/: exhausted solver steps+ --+ -- * /Just True/: inequality is solved+ --+ -- * /Just False/: solver is unable to solve inequality, note that this does+ -- __not__ mean the wanted inequality does not hold.+solveIneq 0 _ _ = noRewrite+solveIneq k want@(_,_,True) have@(_,_,True)+ | want == have+ = pure True+ | otherwise+ = do+ let -- Apply all the rules, and get all the successful ones+ new = mapMaybe (\f -> runWriterT (f want have)) ineqRules+ -- Recurse down with all the transformed equations+ solved = map (first (mapMaybe (runWriterT . uncurry (solveIneq (k-1))))) new+ -- For the results of every recursive call, find the one that yields+ -- 'True' and has the smallest set of constraints.+ solved1 = map (first solvedInEqSmallestConstraint) solved+ -- Union the constraints from the corresponding rewrites with the+ -- constraints from the recursive results+ solved2 = map (\((b,s1),s2) -> (b,Set.union s1 s2)) solved1+ -- From these results, again find the single result that yields 'True'+ -- and has the smallest set of constraints.+ solved3 = solvedInEqSmallestConstraint solved2+ if null solved then+ noRewrite+ else do+ WriterT (Just solved3)++solveIneq _ _ _ = pure False++-- Find the solved inequality with the fewest number of constraints+solvedInEqSmallestConstraint :: [(Bool,Set a)] -> (Bool, Set a)+solvedInEqSmallestConstraint = go (False, Set.empty)+ where+ go bs [] = bs+ go (b,s) ((b1,s1):solved)+ | not b && b1+ = go (b1,s1) solved+ | b && b1+ , Set.size s > Set.size s1+ = go (b1,s1) solved+ | otherwise+ = go (b,s) solved++-- | Try to instantly solve an inequality by using the inequality solver using+-- @1 <=? 1 ~ True@ as the given constraint.+instantSolveIneq+ :: Word+ -- ^ Solving depth+ -> Ineq+ -- ^ Inequality we want to solve+ -> WriterT (Set CType) Maybe Bool+instantSolveIneq k u = solveIneq k u (one,one,True)+ where+ one = S [P [I 1]]++type Ineq = (CoreSOP, CoreSOP, Bool)+type IneqRule = Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq,Ineq)]++noRewrite :: WriterT (Set CType) Maybe a+noRewrite = WriterT Nothing++ineqRules+ :: [IneqRule]+ineqRules =+ [ leTrans+ , plusMonotone+ , timesMonotone+ , powMonotone+ , pow2MonotoneSpecial+ , haveSmaller+ , haveBigger+ ]++-- | Transitivity of inequality+leTrans :: IneqRule+leTrans want@(a,b,le) (x,y,_)+ -- want: 1 <=? y ~ True+ -- have: 2 <=? y ~ True+ --+ -- new want: want+ -- new have: 1 <=? y ~ True+ | S [P [I a']] <- a+ , S [P [I x']] <- x+ , x' >= a'+ = pure [(want,(a,y,le))]+ -- want: y <=? 10 ~ True+ -- have: y <=? 9 ~ True+ --+ -- new want: want+ -- new have: y <=? 10 ~ True+ | S [P [I b']] <- b+ , S [P [I y']] <- y+ , y' < b'+ = pure [(want,(x,b,le))]+leTrans _ _ = noRewrite++-- | Monotonicity of addition+--+-- We use SOP normalization to apply this rule by e.g.:+--+-- * Given: (2*x+1) <= (3*x-1)+-- * Turn to: (3*x-1) - (2*x+1)+-- * SOP version: -2 + x+-- * Convert back to inequality: 2 <= x+plusMonotone :: IneqRule+plusMonotone want have =+ case (simplifyIneq want, simplifyIneq have) of+ (Just want', Just have') -> pure [(want', have')]+ (Just want', _ ) -> pure [(want', have )]+ (_ , Just have') -> pure [(want , have')]+ _ -> noRewrite++-- | Make the `a` of a given `a <= b` smaller+haveSmaller :: IneqRule+haveSmaller want have+ | (S (x:y:ys),us,True) <- have+ = pure [(want,(S (x:ys),us,True))+ ,(want,(S (y:ys),us,True))+ ]+ | (S [P [I 1]], S [P (I _:p@(_:_))],True) <- have+ = pure [(want,(S [P [I 1]],S [P p],True))]+haveSmaller _ _ = noRewrite++-- | Make the `b` of a given `a <= b` bigger+haveBigger :: IneqRule+haveBigger want have+ | (_ ,S vs,True) <- want+ , (as,S bs,True) <- have+ , let vs' = vs \\ bs+ , not (null vs')+ -- want : a <= x + 1+ -- have : y <= x+ --+ -- new want: want+ -- new have: y <= x + 1+ = do+ -- Ensure that we're actually making the RHS larger+ b <- isNatural (S vs')+ if b then+ pure [(want,(as,mergeSOPAdd (S bs) (S vs'),True))]+ else+ noRewrite+haveBigger _ _ = noRewrite++-- | Monotonicity of multiplication+timesMonotone :: IneqRule+timesMonotone want@(a,b,le) have@(x,y,_)+ -- want: C*a <=? b ~ True+ -- have: x <=? y ~ True+ --+ -- new want: want+ -- new have: C*a <=? C*y ~ True+ | S [P a'@(_:_:_)] <- a+ , S [P x'] <- x+ , S [P y'] <- y+ , let ax = a' \\ x'+ , let ay = a' \\ y'+ -- Ensure we don't repeat this rule over and over+ , not (null ax)+ , not (null ay)+ -- Pick the smallest product+ , let az = if length ax <= length ay then S [P ax] else S [P ay]+ = pure [(want,(mergeSOPMul az x, mergeSOPMul az y,le))]++ -- want: a <=? C*b ~ True+ -- have: x <=? y ~ True+ --+ -- new want: want+ -- new have: C*a <=? C*y ~ True+ | S [P b'@(_:_:_)] <- b+ , S [P x'] <- x+ , S [P y'] <- y+ , let bx = b' \\ x'+ , let by = b' \\ y'+ -- Ensure we don't repeat this rule over and over+ , not (null bx)+ , not (null by)+ -- Pick the smallest product+ , let bz = if length bx <= length by then S [P bx] else S [P by]+ = pure [(want,(mergeSOPMul bz x, mergeSOPMul bz y,le))]++ -- want: a <=? b ~ True+ -- have: C*x <=? y ~ True+ --+ -- new want: C*a <=? C*b ~ True+ -- new have: have+ | S [P x'@(_:_:_)] <- x+ , S [P a'] <- a+ , S [P b'] <- b+ , let xa = x' \\ a'+ , let xb = x' \\ b'+ -- Ensure we don't repeat this rule over and over+ , not (null xa)+ , not (null xb)+ -- Pick the smallest product+ , let xz = if length xa <= length xb then S [P xa] else S [P xb]+ = pure [((mergeSOPMul xz a, mergeSOPMul xz b,le),have)]++ -- want: a <=? b ~ True+ -- have: x <=? C*y ~ True+ --+ -- new want: C*a <=? C*b ~ True+ -- new have: have+ | S [P y'@(_:_:_)] <- y+ , S [P a'] <- a+ , S [P b'] <- b+ , let ya = y' \\ a'+ , let yb = y' \\ b'+ -- Ensure we don't repeat this rule over and over+ , not (null ya)+ , not (null yb)+ -- Pick the smallest product+ , let yz = if length ya <= length yb then S [P ya] else S [P yb]+ = pure [((mergeSOPMul yz a, mergeSOPMul yz b,le),have)]++timesMonotone _ _ = noRewrite++-- | Monotonicity of exponentiation+powMonotone :: IneqRule+powMonotone want (x, S [P [E yS yP]],le)+ = case x of+ S [P [E xS xP]]+ -- want: XXX+ -- have: 2^x <=? 2^y ~ True+ --+ -- new want: want+ -- new have: x <=? y ~ True+ | xS == yS+ -> pure [(want,(S [xP],S [yP],le))]+ -- want: XXX+ -- have: x^2 <=? y^2 ~ True+ --+ -- new want: want+ -- new have: x <=? y ~ True+ | xP == yP+ -> pure [(want,(xS,yS,le))]+ -- want: XXX+ -- have: 2 <=? 2 ^ x ~ True+ --+ -- new want: want+ -- new have: 1 <=? x ~ True+ _ | x == yS+ -> pure [(want,(S [P [I 1]],S [yP],le))]+ _ -> noRewrite++powMonotone (a,S [P [E bS bP]],le) have+ = case a of+ S [P [E aS aP]]+ -- want: 2^x <=? 2^y ~ True+ -- have: XXX+ --+ -- new want: x <=? y ~ True+ -- new have: have+ | aS == bS+ -> pure [((S [aP],S [bP],le),have)]+ -- want: x^2 <=? y^2 ~ True+ -- have: XXX+ --+ -- new want: x <=? y ~ True+ -- new have: have+ | aP == bP+ -> pure [((aS,bS,le),have)]+ -- want: 2 <=? 2 ^ x ~ True+ -- have: XXX+ --+ -- new want: 1 <=? x ~ True+ -- new have: XXX+ _ | a == bS+ -> pure [((S [P [I 1]],S [bP],le),have)]+ _ -> noRewrite++powMonotone _ _ = noRewrite++-- | Try to get the power-of-2 factors, and apply the monotonicity of+-- exponentiation rule.+--+-- TODO: I wish we could generalize to find arbitrary factors, but currently+-- I don't know how.+pow2MonotoneSpecial :: IneqRule+pow2MonotoneSpecial (a,b,le) have+ -- want: 4 * 4^x <=? 8^x ~ True+ -- have: XXX+ --+ -- want as pow 2 factors: 2^(2+2*x) <=? 2^(3*x) ~ True+ --+ -- new want: 2+2*x <=? 3*x ~ True+ -- new have: have+ | Just a' <- facSOP 2 a+ , Just b' <- facSOP 2 b+ = pure [((a',b',le),have)]+pow2MonotoneSpecial want (x,y,le)+ -- want: XXX+ -- have:4 * 4^x <=? 8^x ~ True+ --+ -- have as pow 2 factors: 2^(2+2*x) <=? 2^(3*x) ~ True+ --+ -- new want: want+ -- new have: 2+2*x <=? 3*x ~ True+ | Just x' <- facSOP 2 x+ , Just y' <- facSOP 2 y+ = pure [(want,(x',y',le))]+pow2MonotoneSpecial _ _ = noRewrite++-- | Get the power of /N/ factors of a SOP term+facSOP+ :: Integer+ -- ^ The power /N/+ -> CoreSOP+ -> Maybe CoreSOP+facSOP n (S [P ps]) = fmap (S . concat . map unS) (traverse (facSymbol n) ps)+facSOP _ _ = Nothing++-- | Get the power of /N/ factors of a Symbol+facSymbol+ :: Integer+ -- ^ The power+ -> CoreSymbol+ -> Maybe CoreSOP+facSymbol n (I i)+ | Just j <- integerLogBase n i+ = Just (S [P [I j]])+facSymbol n (E s p)+ | Just s' <- facSOP n s+ = Just (mergeSOPMul s' (S [p]))+facSymbol _ _ = Nothing
− tests/ErrorTests.hs
@@ -1,161 +0,0 @@-{-# LANGUAGE DataKinds, KindSignatures, TemplateHaskell, TypeFamilies, TypeOperators #-}--{-# OPTIONS_GHC -fdefer-type-errors #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}-module ErrorTests where--import Data.Proxy-import GHC.TypeLits--import GHC.IO.Encoding (getLocaleEncoding, textEncodingName, utf8)-import Language.Haskell.TH (litE, stringL)-import Language.Haskell.TH.Syntax (runIO)--testProxy1 :: Proxy (x + 1) -> Proxy (2 + x)-testProxy1 = id--testProxy1Errors =- ["Expected type: Proxy (x + 1) -> Proxy (2 + x)"- ,"Actual type: Proxy (2 + x) -> Proxy (2 + x)"- ]--type family GCD (x :: Nat) (y :: Nat) :: Nat-type instance GCD 6 8 = 2-type instance GCD 9 6 = 3--testProxy2 :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)-testProxy2 = id--testProxy2Errors =- ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"- ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)"- ]--proxyFun3 :: Proxy (x + x + x) -> ()-proxyFun3 = const ()--testProxy3 :: Proxy 8 -> ()-testProxy3 = proxyFun3--testProxy3Errors =- ["Expected type: Proxy 8 -> ()"- ,"Actual type: Proxy ((x0 + x0) + x0) -> ()"- ]--proxyFun4 :: Proxy ((2*y)+4) -> ()-proxyFun4 = const ()--testProxy4 :: Proxy 2 -> ()-testProxy4 = proxyFun4--testProxy4Errors =- ["Expected type: Proxy 2 -> ()"- ,"Actual type: Proxy ((2 * y0) + 4) -> ()"- ]--testProxy5 :: Proxy 7 -> ()-testProxy5 = proxyFun4--testProxy5Errors =- ["Expected type: Proxy 7 -> ()"- ,"Actual type: Proxy ((2 * y1) + 4) -> ()"- ]--proxyFun6 :: Proxy (2^k) -> Proxy (2^k)-proxyFun6 = const Proxy--testProxy6 :: Proxy 7-testProxy6 = proxyFun6 (Proxy :: Proxy 7)--testProxy6Errors =- ["Expected type: Proxy (2 ^ k0)"- ,"Actual type: Proxy 7"- ]--proxyFun7 :: Proxy (2^k) -> Proxy k-proxyFun7 = const Proxy--testProxy8 :: Proxy x -> Proxy (y + x)-testProxy8 = id--testProxy8Errors =- ["Expected type: Proxy x -> Proxy (y + x)"- ,"Actual type: Proxy x -> Proxy x"- ]--proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()-proxyInEq _ _ = ()--proxyInEq' :: ((a <=? b) ~ 'False) => Proxy a -> Proxy b -> ()-proxyInEq' _ _ = ()--testProxy9 :: Proxy (a + 1) -> Proxy a -> ()-testProxy9 = proxyInEq--testProxy9Errors =- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘(a + 1) <=? a’ with ‘'True’"- else litE $ stringL "Couldn't match type `(a + 1) <=? a' with 'True"- )]--testProxy10 :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()-testProxy10 = proxyInEq'--testProxy10Errors =- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘a <=? (a + 2)’ with ‘'False’"- else litE $ stringL "Couldn't match type `a <=? (a + 2)' with 'False"- )]--testProxy11 :: Proxy (a :: Nat) -> Proxy a -> ()-testProxy11 = proxyInEq'--testProxy11Errors =- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘'True’ with ‘'False’"- else litE $ stringL "Couldn't match type 'True with 'False"- )]--testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> ()-testProxy12 = proxyInEq--testProxy12Errors =- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘(a + b) <=? (a + c)’ with ‘'True’"- else litE $ stringL "Couldn't match type `(a + b) <=? (a + c)' with 'True"- )]--testProxy13 :: Proxy (4*a) -> Proxy (2*a) ->()-testProxy13 = proxyInEq--testProxy13Errors =- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘(4 * a) <=? (2 * a)’ with ‘'True’"- else litE $ stringL "Couldn't match type `(4 * a) <=? (2 * a)' with 'True"- )]--testProxy14 :: Proxy (2*a) -> Proxy (4*a) -> ()-testProxy14 = proxyInEq'--testProxy14Errors =- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘(2 * a) <=? (4 * a)’ with ‘'False’"- else litE $ stringL "Couldn't match type `(2 * a) <=? (4 * a)' with 'False"- )]--type family CLog (b :: Nat) (x :: Nat) :: Nat-type instance CLog 2 2 = 1--testProxy15 :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)-testProxy15 = id--testProxy15Errors =- ["Expected type: Proxy n -> Proxy (n + d)"- ,"Actual type: Proxy n -> Proxy n"- ]
+ tests/ShouldError.hs view
@@ -0,0 +1,597 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE QuasiQuotes #-}++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+ , testIssue126+ , inequalityTests+ ]++preamble :: String+preamble = [i|+import Data.Kind (Constraint)+import Data.Proxy+import GHC.TypeLits+|] <> "\n"++source1 :: String+source1 = preamble <> [i|+test :: Proxy (x + 1) -> Proxy (2 + x)+test = id+|]++expected1 :: [String]+expected1 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (2 + x)"+ ," Actual: Proxy (x + 1)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy (x + 1) -> Proxy (2 + x)"+ ," Actual: Proxy (x + 1) -> Proxy (x + 1)"+ ]+#else+ ["Expected type: Proxy (x + 1) -> Proxy (2 + x)"+ ,"Actual type: Proxy (2 + x) -> Proxy (2 + x)"+ ]+#endif++test1 :: TestTree+test1 = testCase "x + 1 /~ 2 + x" $ assertCompileError source1 expected1++source2 :: String+source2 = preamble <> [i|+type family GCD (x :: Nat) (y :: Nat) :: Nat+type instance GCD 6 8 = 2+type instance GCD 9 6 = 3++test :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)+test = id+|]++expected2 :: [String]+expected2 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (x + GCD 9 6)"+ ," Actual: Proxy (2 + x)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"+ ," Actual: Proxy (2 + x) -> Proxy (2 + x)"+ ]+#else+ ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"+ ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)"+ ]+#endif++test2 :: TestTree+test2 = testCase "GCD 6 8 + x /~ x + GCD 9 6" $ assertCompileError source2 expected2++source3 :: String+source3 = preamble <> [i|+proxyFun :: Proxy (x + x + x) -> ()+proxyFun = const ()++test :: Proxy 8 -> ()+test = proxyFun+|]++expected3 :: [String]+expected3 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy ((x0 + x0) + x0)"+ ," Actual: Proxy 8"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy 8 -> ()"+ ," Actual: Proxy ((x0 + x0) + x0) -> ()"+ ]+#else+ ["Expected type: Proxy 8 -> ()"+ ,"Actual type: Proxy ((x0 + x0) + x0) -> ()"+ ]+#endif++test3 :: TestTree+test3 = testCase "Unify \"x + x + x\" with \"8\"" $ assertCompileError source3 expected3++source4 :: String+source4 = preamble <> [i|+proxyFun :: Proxy ((2*y)+4) -> ()+proxyFun = const ()++test :: Proxy 2 -> ()+test = proxyFun+|]++expected4 :: [String]+expected4 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy ((2 * y0) + 4)"+ ," Actual: Proxy 2"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy 2 -> ()"+ ," Actual: Proxy ((2 * y0) + 4) -> ()"+ ]+#else+ ["Expected type: Proxy 2 -> ()"+ ,"Actual type: Proxy ((2 * y0) + 4) -> ()"+ ]+#endif++test4 :: TestTree+test4 = testCase "Unify \"(2*x)+4\" with \"2\"" $ assertCompileError source4 expected4++source5 :: String+source5 = preamble <> [i|+proxyFun :: Proxy ((2*y)+4) -> ()+proxyFun = const ()++test :: Proxy 7 -> ()+test = proxyFun+|]++expected5 :: [String]+expected5 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy ((2 * y"+ ,"Actual: Proxy 7"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy 7 -> ()"+ ,"Actual: Proxy ((2 * y"+ ]+#else+ ["Expected type: Proxy 7 -> ()"+ ,"Actual type: Proxy ((2 * y"+ ]+#endif++test5 :: TestTree+test5 = testCase "Unify \"(2*x)+4\" with \"7\"" $ assertCompileError source5 expected5++source6 :: String+source6 = preamble <> [i|+proxyFun :: Proxy (2^k) -> Proxy (2^k)+proxyFun = const Proxy++test :: Proxy 7+test = proxyFun (Proxy :: Proxy 7)+|]++expected6 :: [String]+expected6 =+#if __GLASGOW_HASKELL__ >= 902+ ["Expected: Proxy 7"+ ," Actual: Proxy (2 ^ k0)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy (2 ^ k0)"+ ," Actual: Proxy 7"+ ]+#else+ ["Expected type: Proxy (2 ^ k0)"+ ,"Actual type: Proxy 7"+ ]+#endif++test6 :: TestTree+test6 = testCase "Unify \"2^k\" with \"7\"" $ assertCompileError source6 expected6++source7 :: String+source7 = preamble <> [i|+test :: Proxy x -> Proxy (y + x)+test = id+|]++expected7 :: [String]+expected7 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (y + x)"+ ," Actual: Proxy x"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy x -> Proxy (y + x)"+ ," Actual: Proxy x -> Proxy x"+ ]+#else+ ["Expected type: Proxy x -> Proxy (y + x)"+ ,"Actual type: Proxy x -> Proxy x"+ ]+#endif++test7 :: TestTree+test7 = testCase "x /~ y + x" $ assertCompileError source7 expected7++source8 :: String+source8 = preamble <> [i|+type family CLog (b :: Nat) (x :: Nat) :: Nat+type instance CLog 2 2 = 1++test :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)+test = id+|]++expected8 :: [String]+expected8 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (n + d)"+ ," Actual: Proxy n"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy n -> Proxy (n + d)"+ ," Actual: Proxy n -> Proxy n"+ ]+#else+ ["Expected type: Proxy n -> Proxy (n + d)"+ ,"Actual type: Proxy n -> Proxy n"+ ]+#endif++test8 :: TestTree+test8 = testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n /~ n + d" $+ assertCompileError source8 expected8++source9 :: String+source9 = preamble <> [i|+data Fin (n :: Nat) where+ FZ :: Fin (n + 1)+ FS :: Fin n -> Fin (n + 1)++test :: forall n . Integer -> Fin n+test n = case n of+ 0 -> FZ+ x -> FS (test @(n-1) (x-1))+|]++expected9 :: [String]+expected9 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 1 <= n"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat 1 n) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type 1 <=? n with True" ]+#endif++test9 :: TestTree+test9 = testCase "(n - 1) + 1 ~ n implies (1 <= n)" $ assertCompileError source9 expected9++source10 :: String+source10 = preamble <> [i|+type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where+ Drop 0 xs = xs+ Drop n (x ': xs) = Drop (n-1) xs+ Drop n '[] = '[]++test :: Proxy ns -> Proxy (Drop 1 ns) -> Proxy (Drop 2 ns)+test _ px = px+|]++expected10 :: [String]+expected10 =+#if __GLASGOW_HASKELL__ >= 811+ [ "Couldn't match type: Drop 1 ns"+ , " with: Drop 2 ns"+ , "Expected: Proxy (Drop 2 ns)"+ , " Actual: Proxy (Drop 1 ns)"+ , "Drop is a non-injective type family"+ ]+#else+ [ "Couldn't match type Drop 1 ns with Drop 2 ns"+ , "Expected type: Proxy (Drop 2 ns)"+ , " Actual type: Proxy (Drop 1 ns)"+ , "Drop is a non-injective type family"+ ]+#endif++test10 :: TestTree+test10 = testCase "Do not unify in non-injective positions" $ assertCompileError source10 expected10++source11 :: String+source11 = preamble <> [i|+test :: Proxy a -> Proxy b -> Proxy ((2 * a) + b) -> Proxy 5+test _ _ = id+|]++expected11 :: [String]+expected11 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy 5"+ ," Actual: Proxy ((2 * a) + b)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy ((2 * a) + b) -> Proxy 5"+ ," Actual: Proxy 5 -> Proxy 5"+ ]+#else+ ["Expected type: Proxy ((2 * a) + b) -> Proxy 5"+ ,"Actual type: Proxy 5 -> Proxy 5"+ ]+#endif++test11 :: TestTree+test11 = testCase "Do not rewrite constraint to itself" $ assertCompileError source11 expected11++-- ((3 * (n - 1)) + 1) simplifies to (3 * n - 2), so+-- the equality would require b0 ~ -2, which is impossible at kind Nat.+sourceIssue126 :: String+sourceIssue126 = preamble <> [i|+data Index (n :: Nat) = Index++truncateB :: Index (a + b) -> Index a+truncateB = undefined++mul :: Index 4 -> Index n -> Index ((3 * (n - 1)) + 1)+mul _ _ = Index++zeroExtendTimesThree :: (1 <= n) => Index n -> Index (n * 3)+zeroExtendTimesThree = truncateB . (mul Index)+|]++expectedIssue126 :: [String]+expectedIssue126 =+#if __GLASGOW_HASKELL__ >= 906+ [ "Could not deduce ((n * 3) + b0) ~ ((3 * (n - 1)) + 1)"+#elif __GLASGOW_HASKELL__ >= 904+ [ "Could not deduce (((n * 3) + b0) ~ ((3 * (n - 1)) + 1))"+#elif __GLASGOW_HASKELL__ >= 902+ [ "Could not deduce: ((n * 3) + b0) ~ ((3 * (n - 1)) + 1)"+#else+ [ "Could not deduce: ((3 * (n - 1)) + 1) ~ ((n * 3) + b0)"+#endif+ , "from the context: 1 <= n"+ ]++++testIssue126 :: TestTree+testIssue126 =+ testCase "Issue 126 regression reproducer" $+ assertCompileError sourceIssue126 expectedIssue126++proxyInEqDef :: String+proxyInEqDef =+#if __GLASGOW_HASKELL__ >= 904+ [i|+proxyInEq :: ((a <= b) ~ (() :: Constraint)) => Proxy (a :: Nat) -> Proxy b -> ()+proxyInEq _ _ = ()+|]+#else+ [i|+proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> ()+proxyInEq _ _ = ()+|]+#endif++proxyInEq'Def :: String+proxyInEq'Def = [i|+proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> ()+proxyInEq' _ _ = ()+|]++source12 :: String+source12 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (a + 1) -> Proxy a -> ()+test = proxyInEq+|]++expected12 :: [String]+expected12 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: a + 1 <= a"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat (a + 1) a) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type (a + 1) <=? a with True" ]+#endif++test12 :: TestTree+test12 = testCase "a+1 <= a" $ assertCompileError source12 expected12++source13 :: String+source13 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()+test = proxyInEq'+|]++expected13 :: [String]+expected13 =+#if __GLASGOW_HASKELL__ >= 902+ [ "Data.Type.Ord.OrdCond"+ , "(CmpNat a (a + 2)) True True False"+ , "with False"+ ]+#else+ [ "Couldn't match type a <=? (a + 2) with False" ]+#endif++test13 :: TestTree+test13 = testCase "(a <=? a+1) ~ False" $ assertCompileError source13 expected13++source14 :: String+source14 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (a :: Nat) -> Proxy a -> ()+test = proxyInEq'+|]++expected14 :: [String]+expected14 = [ "Couldn't match type True with False" ]++test14 :: TestTree+test14 = testCase "(a <=? a) ~ False" $ assertCompileError source14 expected14++source15 :: String+source15 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (a + b) -> Proxy (a + c) -> ()+test = proxyInEq+|]++expected15 :: [String]+expected15 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: a + b <= a + c"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat (a + b) (a + c)) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type (a + b) <=? (a + c) with True" ]+#endif++test15 :: TestTree+test15 = testCase "() => (a+b <= a+c)" $ assertCompileError source15 expected15++source16 :: String+source16 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (4*a) -> Proxy (2*a) -> ()+test = proxyInEq+|]++expected16 :: [String]+expected16 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 4 * a <= 2 * a"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat (4 * a) (2 * a)) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type (4 * a) <=? (2 * a) with True" ]+#endif++test16 :: TestTree+test16 = testCase "4a <= 2a" $ assertCompileError source16 expected16++source17 :: String+source17 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (2*a) -> Proxy (4*a) -> ()+test = proxyInEq'+|]++expected17 :: [String]+expected17 =+#if __GLASGOW_HASKELL__ >= 902+ [ "Data.Type.Ord.OrdCond"+ , "(CmpNat (2 * a) (4 * a)) True True False"+ , "with False"+ ]+#else+ [ "Couldn't match type (2 * a) <=? (4 * a) with False" ]+#endif++test17 :: TestTree+test17 = testCase "2a <=? 4a ~ False" $ assertCompileError source17 expected17++source18 :: String+source18 = preamble <> [i|+data Boo (n :: Nat) = Boo++test :: Show (Boo n) => Proxy n -> Boo (n - 1 + 1) -> String+test = const show+|]++expected18 :: [String]+expected18 = expected9++test18 :: TestTree+test18 = testCase "Show (Boo n) => Show (Boo (n - 1 + 1))" $ assertCompileError source18 expected18++test19fDef :: String+test19fDef =+#if __GLASGOW_HASKELL__ >= 904+ [i|+test19f :: ((1 <= n) ~ (() :: Constraint)) => Proxy n -> Proxy n+test19f = id+|]+#else+ [i|+test19f :: (1 <= n) => Proxy n -> Proxy n+test19f = id+|]+#endif++source19 :: String+source19 = preamble <> test19fDef <> [i|+test :: (1 <= m, m <= rp) => Proxy m -> Proxy rp -> Proxy (rp - m) -> Proxy (rp - m)+test _ _ = test19f+|]++expected19 :: [String]+expected19 =+#if __GLASGOW_HASKELL__ >= 904+ [ "Cannot satisfy: 1 <= rp - m" ]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Could not deduce: Data.Type.Ord.OrdCond"+ , "(CmpNat 1 (rp - m)) True True False"+ , "~ True"+ ]+#else+ [ "Could not deduce: (1 <=? (rp - m)) ~ True" ]+#endif++test19 :: TestTree+test19 = testCase "1 <= m, m <= rp implies 1 <= rp - m" $ assertCompileError source19 expected19++source20 :: String+source20 = preamble <> proxyInEqDef <> [i|+test :: Proxy 1 -> Proxy (m ^ 2) -> ()+test = proxyInEq+|]++expected20 :: [String]+expected20 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 1 <= m ^ 2"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat 1 (m ^ 2)) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type 1 <=? (m ^ 2) with True" ]+#endif++test20 :: TestTree+test20 = testCase "Vacuously: 1 <= m ^ 2 ~ True" $ assertCompileError source20 expected20++inequalityTests :: TestTree+inequalityTests = testGroup "Inequality"+ [ test12+ , test13+ , test14+ , test15+ , test16+ , test17+ , test18+ , test19+ , test20+ ]
+ tests/ShouldError/Tasty.hs view
@@ -0,0 +1,58 @@+{-# 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"+ , "-XAllowAmbiguousTypes"+ , "-XConstraintKinds"+ , "-XDataKinds"+ , "-XFlexibleContexts"+ , "-XGADTs"+ , "-XScopedTypeVariables"+ , "-XStandaloneDeriving"+ , "-XTypeApplications"+ , "-XTypeFamilies"+ , "-XTypeOperators"+ , "-XUndecidableInstances"+ , "-XNoStarIsType"+ , "-fno-code"+ , "-fplugin", "GHC.TypeLits.Normalise"+ , 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 = "‘’`'"
tests/Tests.hs view
@@ -1,28 +1,52 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE NoImplicitPrelude #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} +#if __GLASGOW_HASKELL__ >= 805+{-# LANGUAGE NoStarIsType #-}+#endif+ {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}+{-# OPTIONS_GHC -dcore-lint #-}+{-# OPTIONS_GHC -Wno-unused-top-binds #-} import GHC.TypeLits+#if MIN_VERSION_base(4,18,0)+ hiding (type SNat)+#endif+ import Unsafe.Coerce import Prelude hiding (head,tail,init,(++),splitAt,concat,drop) import qualified Prelude as P -import Data.List (isInfixOf)+#if MIN_VERSION_base(4,16,0)+import Data.Type.Ord+#endif++import Data.Kind (Type, Constraint) import Data.Proxy-import Control.Exception+import Data.Type.Equality ((:~:)(..)) import Test.Tasty import Test.Tasty.HUnit -import ErrorTests+import qualified ShouldError -data Vec :: Nat -> * -> * where+data Vec :: Nat -> Type -> Type where Nil :: Vec 0 a (:>) :: a -> Vec n a -> Vec (n + 1) a @@ -55,7 +79,7 @@ snatToInteger :: SNat n -> Integer snatToInteger (SNat p) = natVal p -data UNat :: Nat -> * where+data UNat :: Nat -> Type where UZero :: UNat 0 USucc :: UNat n -> UNat (n + 1) @@ -98,22 +122,38 @@ -- 1 head :: Vec (n + 1) a -> a head (x :> _) = x+head Nil = error "head: impossible" +head'+ :: forall n a+ . (1 <= n)+ => Vec n a+ -> a+head' = head @(n-1)+ -- | Extract the elements after the head of a vector -- -- >>> tail (1:>2:>3:>Nil) -- <2,3> tail :: Vec (n + 1) a -> Vec n a tail (_ :> xs) = xs+tail Nil = error "tail: impossible" +tail' :: (1 <= m) => Vec m a -> Vec (m-1) a+tail' = tail+ -- | Extract all the elements of a vector except the last element -- -- >>> init (1:>2:>3:>Nil) -- <1,2> init :: Vec (n + 1) a -> Vec n a-init (_ :> Nil) = Nil+init (_ :> Nil) = Nil init (x :> y :> ys) = x :> init (y :> ys)+init Nil = error "init: impossible" +init' :: (1 <= m) => Vec m a -> Vec (m-1) a+init' = init+ infixr 5 ++ -- | Append two vectors --@@ -136,6 +176,7 @@ splitAtU UZero ys = (Nil,ys) splitAtU (USucc s) (y :> ys) = let (as,bs) = splitAtU s ys in (y :> as, bs)+splitAtU (USucc _) Nil = error "splitAtU: impossible" {-# INLINE splitAtI #-} -- | Split a vector into two vectors where the length of the two is determined@@ -211,6 +252,8 @@ merge :: Vec n a -> Vec n a -> Vec (n + n) a merge Nil Nil = Nil merge (x :> xs) (y :> ys) = x :> y :> merge xs ys+merge Nil (_ :> _) = error "merge: impossible"+merge (_ :> _) Nil = error "merge: impossible" -- | 'drop' @n xs@ returns the suffix of @xs@ after the first @n@ elements --@@ -223,6 +266,9 @@ drop :: SNat m -> Vec (m + n) a -> Vec n a drop n = snd . splitAt n +drop' :: (m <= k) => SNat m -> Vec k a -> Vec (k - m) a+drop' = drop+ -- | 'at' @n xs@ returns @n@'th element of @xs@ -- -- __NB__: vector elements have an __ASCENDING__ subscript starting from 0 and@@ -235,16 +281,71 @@ at :: SNat m -> Vec (m + (n + 1)) a -> a at n xs = head $ snd $ splitAt n xs +at'+ :: forall k m a+ . (1 <= k, m <= (k-1))+ => SNat m+ -> Vec k a+ -> a+at' = at @m @(k - 1 - m)+ leToPlus- :: forall (k :: Nat) (n :: Nat) f r+ :: forall (k :: Nat) (n :: Nat) (f :: Nat -> Type) (r :: Type) . (k <= n)- => f n+ => Proxy k+ -> f n -- ^ Argument with the @(k <= n)@ constraint- -> (forall m . f (m + k) -> r)+ -> (forall (m :: Nat) . f (m + k) -> r) -- ^ Function with the @(n + k)@ constraint -> r-leToPlus a f = f @ (n-k) a+leToPlus _ a f = f @(n-k) a +data BNat :: Nat -> Type where+ BT :: BNat 0+ B0 :: BNat n -> BNat (2*n)+ B1 :: BNat n -> BNat ((2*n) + 1)++instance KnownNat n => Show (BNat n) where+ show x = 'b':show (natVal x)++predBNat :: (1 <= n) => BNat n -> BNat (n-1)+predBNat (B1 a) = case a of+ BT -> BT+ a' -> B0 a'+predBNat (B0 x) = B1 (predBNat x)++proxyFun3 :: Proxy (x + x + x) -> ()+proxyFun3 = const ()++proxyFun4 :: Proxy ((2*y)+4) -> ()+proxyFun4 = const ()++proxyFun7 :: Proxy (2^k) -> Proxy k+proxyFun7 = const Proxy++-- issue 52 begin+type role Signal nominal representational+data Signal (dom :: Symbol) a = a :- Signal dom a++type role BitVector nominal+newtype BitVector (n :: Nat) = BV { unsafeToNatural :: Integer }++class Bundle (f :: Type -> Type) a res | f a -> res, f res -> a, a res -> f+bundle :: Bundle f a res => res -> f a+bundle = bundle++instance Bundle (Signal dom) (a,b) (Signal dom a, Signal dom b)++issue52 :: (1 <= n, KnownNat n) => (Signal dom (),Signal dom (BitVector (n-1+1))) -> Signal dom ((),BitVector n)+issue52 = bundle+-- issue 52 end++proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> ()+proxyInEq _ _ = ()++proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> ()+proxyInEq' _ _ = ()+ proxyInEq1 :: Proxy a -> Proxy (a+1) -> () proxyInEq1 = proxyInEq @@ -263,21 +364,49 @@ proxyInEq6 :: Proxy 1 -> Proxy (a + 3) -> () proxyInEq6 = proxyInEq -proxyEq1 :: Proxy ((2 ^ x) * (2 ^ (x + x))) -> Proxy (2 * (2 ^ ((x + (x + x)) - 1)))+proxyInEq7 :: Proxy 1 -> Proxy (2^(a + 3)) -> ()+proxyInEq7 = proxyInEq++proxyEq1+ :: (1 <= x)+ => Proxy ((2 ^ x) * (2 ^ (x + x)))+ -> Proxy (2 * (2 ^ ((x + (x + x)) - 1))) proxyEq1 = id -proxyEq2 :: Proxy (((2 ^ x) - 2) * (2 ^ (x + x))) -> Proxy ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1))))+proxyEq2+ :: (2 <= x)+ => Proxy (((2 ^ x) - 2) * (2 ^ (x + x)))+ -> Proxy ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1)))) proxyEq2 = id proxyEq3 :: forall x y- . ((x + 1) ~ (2 * y))+ . ((x + 1) ~ (2 * y), 1 <= y) => Proxy x -> Proxy y- -> Proxy (((2 * (y - 1)) + 1))+ -> Proxy ((2 * (y - 1)) + 1) -> Proxy x proxyEq3 _ _ x = x +-- Would yield (b <=? c) ~ 'True+proxyEq4+ :: forall a b c+ . (KnownNat a, c <= b, b <= a)+ => Proxy b+ -> Proxy c+ -> Proxy a+ -> Proxy (((a - b) + c) + (b - c))+proxyEq4 = theProxy+ where+ theProxy+ :: forall a' b' c'+ . (KnownNat (((a' - b') + c') + (b' - c')), c' <= b', b' <= a')+ => Proxy b'+ -> Proxy c'+ -> Proxy a'+ -> Proxy (((a' - b') + c') + (b' - c'))+ theProxy _ _ = id+ proxyInEqImplication :: (2 <= (2 ^ (n + d))) => Proxy d -> Proxy n@@ -290,6 +419,145 @@ -> Proxy n proxyInEqImplication' _ = id +proxyEqSubst+ :: ((n+1) ~ ((n1 + m) + 1), m ~ n1, n1 ~ ((n2 + m1) + 1))+ => Proxy n1+ -> Proxy n2+ -> Proxy m1+ -> Proxy n+ -> Proxy m+ -> Proxy (1 + (n2 + m1))+ -> Proxy n1+proxyEqSubst _ _ _ _ _ = id++proxyInEqImplication2+ :: forall n n1 n2+ . (n1 ~ (n2 + 1), (2^n) ~ (n1 + 1))+ => Proxy n1+ -> Proxy n2+ -> Proxy n+ -> Proxy ((n - 1) + 1)+ -> Proxy n+proxyInEqImplication2 _ _ _ x = x++type family F (n :: Nat) :: Nat+type instance F 3 = 8++proxyInEqImplication3 :: (KnownNat (F n))+ => Proxy (n :: Nat)+ -> Proxy (n :: Nat)+proxyInEqImplication3 = proxyInEqImplication3'++proxyInEqImplication3' :: (F n <= (3 * (F n)))+ => Proxy (n :: Nat)+ -> Proxy (n :: Nat)+proxyInEqImplication3' = id++type family G (n :: Nat) :: Nat+type instance G 2 = 3++proxyInEqImplication4 :: (1 <= (G n))+ => Proxy (n :: Nat)+ -> Proxy (n :: Nat)+proxyInEqImplication4 = proxyInEqImplication4'++proxyInEqImplication4' :: (F n <= ((G n) * (F n)))+ => Proxy (n :: Nat)+ -> Proxy (n :: Nat)+proxyInEqImplication4' = id++data AtMost n = forall a. (KnownNat a, a <= n) => AtMost (Proxy a)++instance Show (AtMost n) where+ show (AtMost (x :: Proxy a)) = "AtMost " P.++ show (natVal x)++succAtMost :: AtMost n -> AtMost (n + 1)+succAtMost (AtMost (Proxy :: Proxy a)) = AtMost (Proxy :: Proxy a)++data Dict c where+ Dict :: c => Dict c++instance Show (Dict c) where+ show Dict = "Dict"++data Boo (n :: Nat) = Boo++eqReduceForward+ :: Eq (Boo (n + 1))+ => Dict (Eq (Boo (n + 2 - 1)))+eqReduceForward = Dict++eqReduceForwardMinusPlus+ :: (Eq (Boo (0 + n + 1)), 1 <= n)+ => Dict (Eq (Boo (n - 1 + 2)))+eqReduceForwardMinusPlus = Dict++eqReduceBackward+ :: (Eq (Boo (m + 2 - 1)))+ => Dict (Eq (Boo (m + 1)))+eqReduceBackward = Dict++eqReduceBackward'+ :: (Eq (Boo (1 + m + 2)))+ => Dict (Eq (Boo (m + 3)))+eqReduceBackward' = Dict++type family CLog (b :: Nat) (x :: Nat) :: Nat+type instance CLog 2 2 = 1++proxyInEq8fun+ :: (1 <= (n + CLog 2 n))+ => Proxy n+ -> Proxy n+proxyInEq8fun = id++proxyInEq8+ :: (1 <= n, KnownNat (CLog 2 n))+ => Proxy n+ -> Proxy n+proxyInEq8 = proxyInEq8fun++data H2 = H2 { pNat :: Nat }++class Q (dom :: Symbol) where+ type G2 dom :: H2++type family P (c :: H2) :: Nat where+ P ('H2 pNat) = pNat++type F2 (dom :: Symbol) = P (G2 dom)++type Dom = "System"++instance Q Dom where+ type G2 Dom = 'H2 2++tyFamMonotonicityFun :: (1 <= F2 dom) => Proxy (dom :: Symbol) -> ()+tyFamMonotonicityFun _ = ()++tyFamMonotonicity :: (2 <= F2 dom) => Proxy (dom :: Symbol) -> ()+tyFamMonotonicity dom = tyFamMonotonicityFun dom++oneLtPowSubst :: forall a b. (b ~ (2^a)) => Proxy a -> Proxy a+oneLtPowSubst = go+ where+ go :: 1 <= b => Proxy a -> Proxy a+ go = id++type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where+ Drop 0 xs = xs+ Drop n (x ': xs) = Drop (n-1) xs+ Drop n '[] = '[]++isOkay ::+ forall x y sh .+ Proxy x ->+ Proxy y ->+ Proxy sh ->+ Proxy (Drop (x + y) sh) ->+ Proxy (Drop (y + x) sh)+isOkay _ _ _ px = px+ main :: IO () main = defaultMain tests @@ -297,25 +565,25 @@ tests = testGroup "ghc-typelits-natnormalise" [ testGroup "Basic functionality" [ testCase "show (head (1:>2:>3:>Nil))" $- show (head (1:>2:>3:>Nil)) @?=+ show (head ((1 :: Integer):>2:>3:>Nil)) @?= "1" , testCase "show (tail (1:>2:>3:>Nil))" $- show (tail (1:>2:>3:>Nil)) @?=+ show (tail ((1 :: Integer):>2:>3:>Nil)) @?= "<2,3>" , testCase "show (init (1:>2:>3:>Nil))" $- show (init (1:>2:>3:>Nil)) @?=+ show (init ((1 :: Integer):>2:>3:>Nil)) @?= "<1,2>" , testCase "show ((1:>2:>3:>Nil) ++ (7:>8:>Nil))" $- show ((1:>2:>3:>Nil) ++ (7:>8:>Nil)) @?=+ show (((1 :: Integer):>2:>3:>Nil) ++ (7:>8:>Nil)) @?= "<1,2,3,7,8>" , testCase "show (splitAt (snat :: SNat 3) (1:>2:>3:>7:>8:>Nil))" $- show (splitAt (snat :: SNat 3) (1:>2:>3:>7:>8:>Nil)) @?=+ show (splitAt (snat :: SNat 3) ((1 :: Integer):>2:>3:>7:>8:>Nil)) @?= "(<1,2,3>,<7,8>)" , testCase "show (concat ((1:>2:>3:>Nil) :> (4:>5:>6:>Nil) :> (7:>8:>9:>Nil) :> (10:>11:>12:>Nil) :> Nil))" $- show (concat ((1:>2:>3:>Nil) :> (4:>5:>6:>Nil) :> (7:>8:>9:>Nil) :> (10:>11:>12:>Nil) :> Nil)) @?=+ show (concat (((1 :: Integer):>2:>3:>Nil) :> (4:>5:>6:>Nil) :> (7:>8:>9:>Nil) :> (10:>11:>12:>Nil) :> Nil)) @?= "<1,2,3,4,5,6,7,8,9,10,11,12>" , testCase "show (unconcat (snat :: SNat 4) (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil))" $- show (unconcat (snat :: SNat 4) (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)) @?=+ show (unconcat (snat :: SNat 4) ((1 :: Integer):>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)) @?= "<<1,2,3,4>,<5,6,7,8>,<9,10,11,12>>" , testCase "show (proxyFun3 (Proxy :: Proxy 9))" $ show (proxyFun3 (Proxy :: Proxy 9)) @?=@@ -329,16 +597,23 @@ ] , testGroup "Equality" [ testCase "((2 ^ x) * (2 ^ (x + x))) ~ (2 * (2 ^ ((x + (x + x)) - 1)))" $- show (proxyEq1 Proxy) @?=+ show (proxyEq1 @1 Proxy) @?= "Proxy" , testCase "(((2 ^ x) - 2) * (2 ^ (x + x))) ~ ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1))))" $- show (proxyEq2 Proxy) @?=+ show (proxyEq2 @2 Proxy) @?= "Proxy"+ , testCase "Unify in non-injective positions under specific conditions" $+ show (isOkay @2 @3 @'[] Proxy Proxy Proxy Proxy) @?=+ "Proxy" ] , testGroup "Implications" [ testCase "(x + 1) ~ (2 * y)) implies (((2 * (y - 1)) + 1)) ~ x" $ show (proxyEq3 (Proxy :: Proxy 3) (Proxy :: Proxy 2) Proxy) @?= "Proxy"+ , testCase "(n+1) ~ ((n1 + m) + 1), m ~ n1, n1 ~ ((n2 + m1) + 1) implies n1 ~ 1 + (n2 + m1)" $+ show (proxyEqSubst (Proxy :: Proxy 6) (Proxy :: Proxy 2) (Proxy :: Proxy 3)+ (Proxy :: Proxy 12) (Proxy :: Proxy 6) (Proxy :: Proxy 6)) @?=+ "Proxy" ] , testGroup "Inequality" [ testCase "a <= a+1" $@@ -362,36 +637,208 @@ , testCase "1 <= a+3" $ show (proxyInEq6 (Proxy :: Proxy 1) (Proxy :: Proxy 8)) @?= "()"- ]- , testGroup "errors"- [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors- , testCase "GCD 6 8 + x ~ x + GCD 9 6" $ testProxy2 `throws` testProxy2Errors- , testCase "Unify \"x + x + x\" with \"8\"" $ testProxy3 `throws` testProxy3Errors- , testCase "Unify \"(2*x)+4\" with \"2\"" $ testProxy4 `throws` testProxy4Errors- , testCase "Unify \"(2*x)+4\" with \"7\"" $ testProxy5 `throws` testProxy5Errors- , testCase "Unify \"2^k\" with \"7\"" $ testProxy6 `throws` testProxy6Errors- , testCase "x ~ y + x" $ testProxy8 `throws` testProxy8Errors- , testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n ~ (n+d)" $ (testProxy15 (Proxy :: Proxy 1)) `throws` testProxy15Errors- , testGroup "Inequality"- [ testCase "a+1 <= a" $ testProxy9 `throws` testProxy9Errors- , testCase "(a <=? a+1) ~ False" $ testProxy10 `throws` testProxy10Errors- , testCase "(a <=? a) ~ False" $ testProxy11 `throws` testProxy11Errors- , testCase "() => (a+b <= a+c)" $ testProxy12 `throws` testProxy12Errors- , testCase "4a <= 2a" $ testProxy13 `throws` testProxy13Errors- , testCase "2a <=? 4a ~ False" $ testProxy14 `throws` testProxy14Errors- ]+ , testCase "`1 <= 2*x` implies `1 <= x`" $+ show (predBNat (B1 (B1 BT))) @?=+ "b2"+ , testCase "`x + 2 <= y` implies `x <= y` and `2 <= y`" $+ show (proxyInEqImplication2 (Proxy :: Proxy 3) (Proxy :: Proxy 2) (Proxy :: Proxy 2) Proxy) @?=+ "Proxy"+ , testCase "`a <= n` implies `a <= (n+1)`" $+ show (succAtMost (AtMost (Proxy :: Proxy 3) :: AtMost 5)) @?=+ "AtMost 3"+ , testCase "1 <= 2^(a+3)" $+ show (proxyInEq7 (Proxy :: Proxy 1) (Proxy :: Proxy 8)) @?=+ "()"+ , testCase "KnownNat (F a) implies F a <= 3 * F a" $+ show (proxyInEqImplication3 (Proxy :: Proxy 3)) @?=+ "Proxy"+ , testCase "1 <= G a implies F a <= G a * F a" $+ show (proxyInEqImplication4 (Proxy :: Proxy 2)) @?=+ "Proxy"+ , testCase "`(1 <= n)` only implies `(1 <= n + F n)` when `KnownNat (F n)`" $+ show (proxyInEq8 (Proxy :: Proxy 2)) @?=+ "Proxy"+ , testCase "2 <= P (G2 dom) implies 1 <= P (G2 dom)" $+ show (tyFamMonotonicity (Proxy :: Proxy Dom)) @?=+ "()"+ , testCase "b ~ (2^a) => 1 <= b" $+ show (oneLtPowSubst (Proxy :: Proxy 0)) @?=+ "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` msg) xs- then return ()- else assertFailure msg+showFin :: forall n. KnownNat n => Fin n -> String+showFin f = mconcat [+ show (finToInt f)+ , "/"+ , show (natVal (Proxy :: Proxy n))+ ]++finToInt :: Fin n -> Int+finToInt FZ = 0+finToInt (FS fn) = finToInt fn + 1++data Fin (n :: Nat) where+ FZ :: Fin (n + 1)+ FS :: Fin n -> Fin (n + 1)++predFin :: Fin (n + 2) -> Fin (n + 1)+predFin (FS fn) = fn+predFin FZ = FZ++showSucPred :: KnownNat (n + 2) => Fin (n + 2) -> String+showSucPred = showFin . FS . predFin++class Up env (n :: Nat) where+ up :: env -> Fin n -> Fin (n + 1)++class Down env (n :: Nat) where+ down :: env -> Fin n -> Fin (n - 1)++class ShowWith env (n :: Nat) where+ showWith :: env -> Fin n -> String++showDownUp+ :: (Up env n, Down env (n + 1), ShowWith env n)+ => env -> Fin n -> String+showDownUp env fn = showWith env $ down env $ up env fn++showDownUp'+ :: (Up env n, Down env (n + 1), KnownNat n)+ => env -> Fin n -> String+showDownUp' env fn = showFin $ down env $ up env fn++data family FakeUVector (n :: Nat) :: Type+data family FakeMUVector (n :: Nat) :: Type+type family Mutable (v :: Nat -> Type) :: Nat -> Type+type instance Mutable FakeUVector = FakeMUVector++class (IsMVector FakeMUVector n, IsVector FakeUVector n)+ => FakeUnbox n+class IsMVector (v :: Nat -> Type) a where+ touchMVector :: v a -> v a+class IsMVector (Mutable v) a => IsVector v a where+ touchVector :: v a -> v a++newtype WrapFakeVector n = WFV { unWrap :: FakeUVector (1 + n) }+newtype WrapFakeMVector n = MWFV { unWrapM :: FakeMUVector (1 + n) }+type instance Mutable WrapFakeVector = WrapFakeMVector++-- The following two instances cannot be derived without simplification phase!+instance FakeUnbox (n + 1) => IsVector WrapFakeVector n where+ touchVector = WFV . touchVector . unWrap+instance FakeUnbox (n + 1) => IsMVector WrapFakeMVector n where+ touchMVector = MWFV . touchMVector . unWrapM++#if MIN_VERSION_base(4,16,0)+-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/70+libFunc :: forall (i :: Nat) d. i < d => Proxy i -> Proxy d -> ()+libFunc _ _ = ()+useFunc :: forall (d :: Nat). Proxy d -> ()+useFunc _ = libFunc (Proxy @0) (Proxy @(d+1))+#endif++-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/71+t71_aux :: (((1 + m1) + n1) ~ (1 + (m2 + n2))) => Proxy '(m1, n1, m2, n2) -> ()+t71_aux _ = ()+t71 :: ((m1 + n1) ~ (m2 + n2)) => Proxy '(m1, n1, m2, n2) -> ()+t71 px = t71_aux px++-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94+t94 ::+ (KnownNat n, KnownNat m, KnownNat s, s ~ (m - n)) =>+ Proxy m -> Proxy n -> Proxy (s + 2) -> Proxy (s + 2)+t94 _ _ = t94_aux++t94_aux :: (1 <= n) => Proxy n -> Proxy n+t94_aux px = px++-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/96+t96+ :: ( 2 <= x, 2 <= y+ , ( 4 * x + 2 * 2^y ) ~ ( 4 * y + 2 * 2^x )+ )+ => Proxy x -> Proxy y+t96 x = x++type family TF (a :: Nat) (b :: Nat) :: Nat++proxyEq5+ :: forall a b+ . KnownNat (TF (a * 3) b * 3)+ => Proxy a+ -> Proxy b+ -> Proxy (3 * TF (3 * a) b)+proxyEq5 = theProxy+ where+ theProxy+ :: forall a' b'+ . KnownNat (TF (2 * a' + a') b' + (2 * TF (a' + 2 * a') b'))+ => Proxy a'+ -> Proxy b'+ -> Proxy (3 * TF (3 * a') b')+ theProxy _ _ = Proxy++type family Rank sh where+ Rank '[] = 0+ Rank (_ : sh) = Rank sh + 1+foo :: ( ( 1 + Rank sh ) ~ ( 1 + n ) )+ => Proxy sh -> Proxy n -> Proxy (Rank sh) -> Proxy n+foo _ _ px = px++noContra :: ((Rank sh + 2) <= 2) => Proxy sh -> ()+noContra _ = ()++-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/97+t97 :: ( (1 + n) ~ m, ( m - 1 ) ~ n ) => Proxy m -> Proxy n -> ()+t97 _ _ = ()++t97b+ :: ( n ~ (m - 2)+ , (n + 1) ~ (m - 1)+ , m ~ (n + 2)+ )+ => Proxy n -> Proxy m -> ()+t97b _ _ = ()++-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/116+t116 :: forall n m l. m :~: n -> n :~: 0 -> l :~: 1 -> Float+t116 a b c =+ case a of+ Refl ->+ case b of+ Refl ->+ case c of+ Refl ->+ 3.0++type family Foo (n :: Nat) :: Nat++t119a :: Proxy n -> Proxy (Foo (n + 2)) -> Proxy (Foo (2 + n))+t119a _ = id++--Only applicable for GHC >= 9.4 as prior InEq constraints are of the form `a <=? b ~ 'True`+#if __GLASGOW_HASKELL__ >= 904+t119b ::+ (1 <= a) =>+ (1 <= Foo (a + 1)) =>+ Proxy a ->+ Proxy a+t119b a = go a+ where+ go ::+ ((1 <= Foo (c + 1)) ~ (() :: Constraint)) =>+ Proxy c ->+ Proxy c+ go _ = Proxy+#endif++data NatPhantom (n :: Nat) = NatPhantom++-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/124+t124 :: 1 <= n => NatPhantom m -> NatPhantom (m + n - 1)+t124 x = go x+ where+ go :: NatPhantom a -> NatPhantom (b + a)+ go _ = NatPhantom