diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,10 +1,10 @@ # ghc-typelits-natnormalise -[![Build Status](https://secure.travis-ci.org/clash-lang/ghc-typelits-natnormalise.svg?branch=master)](http://travis-ci.org/clash-lang/ghc-typelits-natnormalise) +[![Build Status](https://github.com/clash-lang/ghc-typelits-natnormalise/actions/workflows/haskell-ci.yml/badge.svg?branch=master)](https://github.com/clash-lang/ghc-typelits-natnormalise/actions) [![Hackage](https://img.shields.io/hackage/v/ghc-typelits-natnormalise.svg)](https://hackage.haskell.org/package/ghc-typelits-natnormalise) [![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-natnormalise.svg?style=flat)](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 diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal --- a/ghc-typelits-natnormalise.cabal +++ b/ghc-typelits-natnormalise.cabal @@ -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 diff --git a/src/GHC/TypeLits/Normalise.hs b/src/GHC/TypeLits/Normalise.hs --- a/src/GHC/TypeLits/Normalise.hs +++ b/src/GHC/TypeLits/Normalise.hs @@ -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 +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 diff --git a/src/GHC/TypeLits/Normalise/Compat.hs b/src/GHC/TypeLits/Normalise/Compat.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits/Normalise/Compat.hs @@ -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 + +-------------------------------------------------------------------------------- diff --git a/src/GHC/TypeLits/Normalise/SOP.hs b/src/GHC/TypeLits/Normalise/SOP.hs --- a/src/GHC/TypeLits/Normalise/SOP.hs +++ b/src/GHC/TypeLits/Normalise/SOP.hs @@ -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 diff --git a/src/GHC/TypeLits/Normalise/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs --- a/src/GHC/TypeLits/Normalise/Unify.hs +++ b/src/GHC/TypeLits/Normalise/Unify.hs @@ -5,21 +5,22 @@ Maintainer : Christiaan Baaij -} -{-# 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 diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs deleted file mode 100644 --- a/tests/ErrorTests.hs +++ /dev/null @@ -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" - ] diff --git a/tests/ShouldError.hs b/tests/ShouldError.hs new file mode 100644 --- /dev/null +++ b/tests/ShouldError.hs @@ -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 + ] diff --git a/tests/ShouldError/Tasty.hs b/tests/ShouldError/Tasty.hs new file mode 100644 --- /dev/null +++ b/tests/ShouldError/Tasty.hs @@ -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 = "‘’`'" diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -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