ghc-typelits-natnormalise 0.7.12 → 0.9.6
raw patch · 13 files changed
Files
- CHANGELOG.md +43/−0
- ghc-typelits-natnormalise.cabal +42/−37
- src-ghc-9.12/GHC/TypeLits/Normalise.hs +0/−739
- src-ghc-9.4/GHC/TypeLits/Normalise.hs +0/−740
- src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs +0/−862
- src/GHC/TypeLits/Normalise.hs +966/−0
- src/GHC/TypeLits/Normalise/Compat.hs +399/−0
- src/GHC/TypeLits/Normalise/SOP.hs +22/−20
- src/GHC/TypeLits/Normalise/Unify.hs +405/−284
- tests/ErrorTests.hs +0/−523
- tests/ShouldError.hs +597/−0
- tests/ShouldError/Tasty.hs +58/−0
- tests/Tests.hs +191/−58
CHANGELOG.md view
@@ -1,5 +1,48 @@ # 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
ghc-typelits-natnormalise.cabal view
@@ -1,43 +1,44 @@+cabal-version: 3.0 name: ghc-typelits-natnormalise-version: 0.7.12+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/ 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,13 +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.4, GHC == 8.6.5,- GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,- GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1,- GHC == 9.10.2, GHC == 9.12.1+tested-with: GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,+ GHC == 9.4.8, GHC == 9.6.7, GHC == 9.8.4, GHC == 9.10.2,+ GHC == 9.12.2 source-repository head type: git@@ -65,26 +64,29 @@ library exposed-modules: GHC.TypeLits.Normalise,+ GHC.TypeLits.Normalise.Compat, GHC.TypeLits.Normalise.SOP, GHC.TypeLits.Normalise.Unify build-depends: base >=4.9 && <5,- containers >=0.5.7.1 && <0.8,- ghc >=8.0.1 && <9.13,- ghc-tcplugins-extra >=0.5,- transformers >=0.5.2.0 && < 0.7+ 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.4+ 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- if impl(ghc >= 8.0) && impl(ghc < 9.4)- hs-source-dirs: src-pre-ghc-9.4- if impl(ghc >= 9.4) && impl(ghc < 9.11)- hs-source-dirs: src-ghc-9.4- build-depends: template-haskell >=2.17 && <2.23- if impl(ghc >= 9.11) && impl(ghc < 9.13)- hs-source-dirs: src-ghc-9.12- build-depends: template-haskell >=2.17 && <2.24 default-language: Haskell2010 other-extensions: CPP LambdaCase@@ -98,23 +100,26 @@ 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: -dcore-lint+ ghc-options: -Werror -dcore-lint
− src-ghc-9.12/GHC/TypeLits/Normalise.hs
@@ -1,739 +0,0 @@-{-|-Copyright : (C) 2015-2016, University of Twente,- 2017 , QBayLogic B.V.-License : BSD2 (see the file LICENSE)-Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>--A type checker plugin for GHC that can solve /equalities/ of types of kind-'GHC.TypeLits.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/-'GHC.TypeLits.Normalise.SOP.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 'GHC.TypeLits.Normalise.SOP.SOP' normal form-of the former.--To use the plugin, add--@-{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}-@--To the header of your file.--== Treating subtraction as addition with a negated number--If you are absolutely sure that your subtractions can /never/ lead to (a locally)-negative number, you can ask the plugin to treat subtraction as addition with-a negated operand by additionally adding:--@-{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}-@--to the header of your file, thereby allowing to use associativity and-commutativity rules when proving constraints involving subtractions. Note that-this option can lead to unsound behaviour and should be handled with extreme-care.--=== When it leads to unsound behaviour--For example, enabling the /allow-negated-numbers/ feature would allow-you to prove:--@-(n - 1) + 1 ~ n-@--/without/ a @(1 <= n)@ constraint, even though when /n/ is set to /0/ the-subtraction @n-1@ would be locally negative and hence not be a natural number.--This would allow the following erroneous definition:--@-data Fin (n :: Nat) where- FZ :: Fin (n + 1)- FS :: Fin n -> Fin (n + 1)--f :: forall n . Natural -> Fin n-f n = case of- 0 -> FZ- x -> FS (f \@(n-1) (x - 1))--fs :: [Fin 0]-fs = f \<$\> [0..]-@--=== When it might be Okay--This example is taken from the <http://hackage.haskell.org/package/mezzo mezzo>-library.--When you have:--@--- | Singleton type for the number of repetitions of an element.-data Times (n :: Nat) where- T :: Times n---- | An element of a "run-length encoded" vector, containing the value and--- the number of repetitions-data Elem :: Type -> Nat -> Type where- (:*) :: t -> Times n -> Elem t n---- | A length-indexed vector, optimised for repetitions.-data OptVector :: Type -> Nat -> Type where- End :: OptVector t 0- (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n-@--And you want to define:--@--- | Append two optimised vectors.-type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where- ys ++ End = ys- End ++ ys = ys- (x :- xs) ++ ys = x :- (xs ++ ys)-@--then the last line will give rise to the constraint:--@-(n-l)+m ~ (n+m)-l-@--because:--@-x :: Elem t l-xs :: OptVector t (n-l)-ys :: OptVector t m-@--In this case it's okay to add--@-{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}-@--if you can convince yourself you will never be able to construct a:--@-xs :: OptVector t (n-l)-@--where /n-l/ is a negative number.--}--{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE TemplateHaskellQuotes #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.Normalise- ( plugin )-where---- external-import Control.Arrow (second)-import Control.Monad ((<=<), forM)-import Control.Monad.Trans.Writer.Strict-import Data.Either (partitionEithers, rights)-import Data.IORef-import Data.List (intersect, partition, stripPrefix, find)-import Data.Maybe (mapMaybe, catMaybes)-import Data.Set (Set, empty, toList, notMember, fromList, union)-import Text.Read (readMaybe)-import qualified Data.Type.Ord-import qualified GHC.TypeError--import GHC.TcPluginM.Extra (tracePlugin, newGiven, newWanted)---- GHC API-import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey)-import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)-import GHC.Builtin.Types.Literals- (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)-import GHC.Builtin.Types (naturalTy, cTupleDataCon, cTupleTyCon)-import GHC.Builtin.Types.Literals (typeNatCmpTyCon)-import GHC.Core (Expr (..))-import GHC.Core.Class (className)-import GHC.Core.Coercion (Coercion, Role (..), mkUnivCo)-import GHC.Core.DataCon (dataConWrapId)-import GHC.Core.Predicate- (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType, mkClassPred,- mkPrimEqPred, isEqPred, isEqPrimPred, getClassPredTys_maybe)-import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..))-import GHC.Core.TyCon (TyCon)-import GHC.Core.Type- (Kind, PredType, mkTyVarTy, tyConAppTyCon_maybe, typeKind, mkTyConApp)-import GHC.Core.TyCo.Compare- (eqType)-import GHC.Data.IOEnv (getEnv)-import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)-import GHC.Plugins (thNameToGhcNameIO, HscEnv (hsc_NC))-import GHC.Tc.Plugin- (TcPluginM, tcLookupClass, tcPluginTrace, tcPluginIO, newEvVar)-import GHC.Tc.Plugin (tcLookupTyCon, unsafeTcPluginTcM)-import GHC.Tc.Types (TcPlugin (..), TcPluginSolveResult(..), Env (env_top))-import GHC.Tc.Types.Constraint- (Ct, CtEvidence (..), TcEvDest (..), ctEvidence, ctEvCoercion, ctLoc, isGiven,- isWanted, mkNonCanonical, isWantedCt, ctEvLoc, ctEvPred, ctEvExpr,- emptyRewriterSet, setCtEvLoc)-import GHC.Tc.Types.CtLoc (CtLoc, ctLocSpan, setCtLocSpan)-import GHC.Tc.Types.Evidence (EvBindsVar, EvTerm (..), evCast, evId, mkEvCast)-import GHC.Types.Unique.FM (emptyUFM)-import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)-import GHC (Name)---- template-haskell-import qualified Language.Haskell.TH as TH---- internal-import GHC.TypeLits.Normalise.SOP-import GHC.TypeLits.Normalise.Unify hiding (subtractionToPred)--isEqPredClass :: PredType -> Bool-isEqPredClass ty = case tyConAppTyCon_maybe ty of- Just tc -> tc `hasKey` eqTyConKey || tc `hasKey` heqTyConKey- _ -> False---- | To use the plugin, add------ @--- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}--- @------ To the header of your file.-plugin :: Plugin-plugin- = defaultPlugin- { tcPlugin = fmap (normalisePlugin . foldr id defaultOpts) . traverse parseArgument- , 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 = tracePlugin "ghc-typelits-natnormalise"- TcPlugin { tcPluginInit = lookupExtraDefs- , tcPluginSolve = decideEqualSOP opts- , tcPluginRewrite = const emptyUFM- , tcPluginStop = const (return ())- }--type ExtraDefs = (IORef (Set CType), (TyCon,TyCon,TyCon))--lookupExtraDefs :: TcPluginM ExtraDefs-lookupExtraDefs = do- ref <- tcPluginIO (newIORef empty)- ordCond <- lookupTHName ''Data.Type.Ord.OrdCond >>= tcLookupTyCon- leqT <- lookupTHName ''(Data.Type.Ord.<=) >>= tcLookupTyCon- assertT <- lookupTHName ''GHC.TypeError.Assert >>= tcLookupTyCon- return (ref, (leqT,assertT,ordCond))--lookupTHName :: TH.Name -> TcPluginM Name-lookupTHName th = do- nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv)- res <- tcPluginIO $ thNameToGhcNameIO nc th- maybe (fail $ "Failed to lookup " ++ show th) return res--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.<=?- -> EvBindsVar- -> [Ct]- -> [Ct]- -> TcPluginM 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 (gen'd,(leqT,_,_)) ev givens [] = do- done <- tcPluginIO $ readIORef gen'd- let reds =- filter (\(_,(_,_,v)) -> null v || negNumbers opts) $- reduceGivens opts leqT done givens- newlyDone = map (\(_,(prd, _,_)) -> CType prd) reds- tcPluginIO $- modifyIORef' gen'd $ union (fromList newlyDone)- newGivens <- forM reds $ \(origCt, (pred', evTerm, _)) ->- mkNonCanonical' (ctLoc origCt) <$> newGiven ev (ctLoc origCt) pred' evTerm- return (TcPluginOk [] newGivens)---- Solving phase.--- Solves in/equalities on Nats and simplifiable constraints--- containing naturals.-decideEqualSOP opts (gen'd,tcs@(leqT,_,_)) ev givens wanteds = do- let unit_wanteds = mapMaybe (toNatEquality tcs) wanteds- nonEqs = filter ( not- . (\p -> isEqPred p || isEqPrimPred p)- . ctEvPred- . ctEvidence )- wanteds- done <- tcPluginIO $ readIORef gen'd- let redGs = reduceGivens opts leqT done givens- newlyDone = map (\(_,(prd, _,_)) -> CType prd) redGs- redGivens <- forM redGs $ \(origCt, (pred', evTerm, _)) ->- mkNonCanonical' (ctLoc origCt) <$> newGiven ev (ctLoc origCt) pred' evTerm- reducible_wanteds- <- catMaybes <$> mapM (\ct -> fmap (ct,) <$>- reduceNatConstr (givens ++ redGivens) ct)- nonEqs- if null unit_wanteds && 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.- ineqForRedWants <- fmap concat $ forM redGs $ \(ct, (_,_, ws)) -> forM ws $- fmap (mkNonCanonical' (ctLoc ct)) . newWanted (ctLoc ct)- tcPluginIO $- modifyIORef' gen'd $ union (fromList newlyDone)- let unit_givens = mapMaybe- (toNatEquality tcs)- givens- sr <- simplifyNats opts leqT unit_givens unit_wanteds- tcPluginTrace "normalised" (ppr sr)- reds <- forM reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do- wants <- evSubtPreds (ctLoc origCt) $ subToPred opts leqT ws- return ((term, origCt), wDicts ++ wants)- case sr of- Simplified evs -> do- let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs- -- Only solve derived when we solved a wanted- simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of- [] -> []- _ -> simpld- (solved',newWanteds) = second concat (unzip $ simpld1 ++ reds)- return (TcPluginOk solved' $ newWanteds ++ ineqForRedWants)- Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])--type NatEquality = (Ct,CoreSOP,CoreSOP)-type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))--reduceGivens :: Opts -> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))]-reduceGivens opts leqT done givens =- let nonEqs =- [ ct- | ct <- givens- , let ev = ctEvidence ct- prd = ctEvPred ev- , isGiven ev- , not $ (\p -> isEqPred p || isEqPrimPred p || isEqPredClass p) prd- ]- in filter- (\(_, (prd, _, _)) ->- notMember (CType prd) done- )- $ mapMaybe- (\ct -> (ct,) <$> tryReduceGiven opts leqT givens ct)- nonEqs--tryReduceGiven- :: Opts -> TyCon -> [Ct] -> Ct- -> Maybe (PredType, EvTerm, [PredType])-tryReduceGiven opts leqT simplGivens ct = do- let (mans, ws) =- runWriter $ normaliseNatEverywhere $- ctEvPred $ ctEvidence ct- ws' = [ p- | p <- subToPred opts leqT ws- , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens- ]- -- deps = unitDVarSet (ctEvId ct)- pred' <- mans- return (pred', toReducedDict (ctEvidence ct) pred', ws')--fromNatEquality :: Either NatEquality NatInEquality -> Ct-fromNatEquality (Left (ct, _, _)) = ct-fromNatEquality (Right (ct, _)) = ct--reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))-reduceNatConstr givens ct = do- let pred0 = ctEvPred $ ctEvidence ct- (mans, tests) = runWriter $ normaliseNatEverywhere pred0- case mans of- Nothing -> return Nothing- Just pred' -> do- case find ((`eqType` pred') .ctEvPred . ctEvidence) givens of- -- No existing evidence found- Nothing -> case getClassPredTys_maybe pred' of- -- Are we trying to solve a class instance?- Just (cls,_) | className cls /= knownNatClassName -> do- -- Create new evidence binding for normalized class constraint- evVar <- newEvVar pred'- -- Bind the evidence to a new wanted normalized class constraint- let wDict = mkNonCanonical- (CtWanted pred' (EvVarDest evVar) (ctLoc ct) emptyRewriterSet)- -- Evidence for current wanted is simply the coerced binding for- -- the new binding- evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise") []- Representational- pred' pred0- ev = mkEvCast (evId evVar) evCo- -- Use newly created coerced wanted as evidence, and emit the- -- normalized wanted as a new constraint to solve.- return (Just (ev, tests, [wDict]))- _ -> return Nothing- -- Use existing evidence- Just c -> return (Just (toReducedDict (ctEvidence c) pred0, tests, []))--toReducedDict :: CtEvidence -> PredType -> EvTerm-toReducedDict ct pred' =- let pred0 = ctEvPred ct- evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise") []- Representational- pred0 pred'- ev = mkEvCast (ctEvExpr ct) evCo- in ev--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- :: Opts- -- ^ Allow negated numbers (potentially unsound!)- -> TyCon- -- * TyCon of Data.Type.Ord.<=- -> [(Either NatEquality NatInEquality,[(Type,Type)])]- -- ^ Given constraints- -> [(Either NatEquality NatInEquality,[(Type,Type)])]- -- ^ Wanted constraints- -> TcPluginM SimplifyResult-simplifyNats opts@Opts {..} leqT eqsG eqsW = do- let eqsG1 = map (second (const ([] :: [(Type,Type)]))) eqsG- (varEqs,otherEqs) = partition isVarEqs eqsG1- fancyGivens = concatMap (makeGivensSet otherEqs) varEqs- case varEqs of- [] -> do- let eqs = otherEqs ++ eqsW- tcPluginTrace "simplifyNats" (ppr eqs)- simples [] [] [] [] [] eqs- _ -> do- tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")")- (ppr varEqs)-- allSimplified <- forM fancyGivens $ \v -> do- let eqs = v ++ eqsW- tcPluginTrace "simplifyNats" (ppr eqs)- simples [] [] [] [] [] eqs-- pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified)- where- simples :: [Coercion]- -> [CoreUnify]- -> [((EvTerm, Ct), [Ct])]- -> [(CoreSOP,CoreSOP,Bool)]- -> [(Either NatEquality NatInEquality,[(Type,Type)])]- -> [(Either NatEquality NatInEquality,[(Type,Type)])]- -> TcPluginM SimplifyResult- simples _ _subst evs _leqsG _xs [] = return (Simplified evs)- simples deps subst evs leqsG xs (eq@(Left (ct,u,v),k):eqs') = do- let u' = substsSOP subst u- v' = substsSOP subst v- ur <- unifyNats ct u' v'- tcPluginTrace "unifyNats result" (ppr ur)- case ur of- Win -> do- evs' <- maybe evs (:evs) <$> evMagic ct deps empty (subToPred opts leqT k)- simples deps subst evs' leqsG [] (xs ++ eqs')- Lose -> if null evs && null eqs'- then return (Impossible (fst eq))- else simples deps subst evs leqsG xs eqs'- Draw [] -> simples deps subst evs [] (eq:xs) eqs'- Draw subst' -> do- evM <- evMagic ct deps empty (map unifyItemToPredType subst' ++- subToPred opts leqT k)- let (leqsG1, deps1)- | isGiven (ctEvidence ct) = ( eqToLeq u' v' ++ leqsG- , ctEvCoercion (ctEvidence ct):deps)- | otherwise = (leqsG, deps)- case evM of- Nothing -> simples deps1 subst evs leqsG1 xs eqs'- Just ev ->- simples (ctEvCoercion (ctEvidence ct):deps)- (substsSubst subst' subst ++ subst')- (ev:evs) leqsG1 [] (xs ++ eqs')- simples deps subst evs leqsG xs (eq@(Right (ct,u@(x,y,b)),k):eqs') = do- 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 fst eqsG))- ]- tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs))- case runWriterT (isNatural u') of- Just (True,knW) -> do- evs' <- maybe evs (:evs) <$> evMagic ct deps knW (subToPred opts leqT k)- simples deps subst evs' leqsG' xs eqs'-- Just (False,_) | null k -> return (Impossible (fst eq))- _ -> 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) <$> evMagic ct deps kW (subToPred opts leqT k)- simples deps subst evs' leqsG' xs eqs'- _ -> simples deps subst evs leqsG (eq:xs) 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 otherEqs varEq- = let (noMentionsV,mentionsV) = partitionEithers- (map (matchesVarEq varEq) otherEqs)- (mentionsLHS,mentionsRHS) = partitionEithers mentionsV- vS = swapVar 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 (Left (_, S [P [V v1]], S [P [V v2]]),_) r = case r 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]]),ps) =- (Left (ct,S [P [V v2]], S [P [V v1]]),ps)- swapVar _ = error "internal error"-- findFirstSimpliedWanted (Impossible e) _ = Impossible e- findFirstSimpliedWanted (Simplified evs) s2- | any (isWantedCt . snd . fst) evs- = Simplified evs- | otherwise- = s2---- 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 -> TyCon -> [(Type, Type)] -> [PredType]-subToPred Opts{..} leqT- | negNumbers = const []- | otherwise = map leq- where- leq (a,b) =- let lhs = TyConApp leqT [naturalTy,b,a]- rhs = TyConApp (cTupleTyCon 0) []- in mkPrimEqPred lhs rhs---- Extract the Nat equality constraints-toNatEquality :: (TyCon,TyCon,TyCon) -> Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])-toNatEquality (_,assertT,ordCond) ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2- -> go t1 t2- IrredPred p- -> go2 p- _ -> 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)- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- -> Just (Left (ct, x', y'),k1 ++ k2)- _ -> Nothing- | tc == ordCond- , [_,cmp,lt,eq,gt] <- xs- , TyConApp tcCmpNat [x,y] <- cmp- , tcCmpNat == typeNatCmpTyCon- , TyConApp ltTc [] <- lt- , ltTc == promotedTrueDataCon- , TyConApp eqTc [] <- eq- , eqTc == promotedTrueDataCon- , TyConApp gtTc [] <- gt- , gtTc == promotedFalseDataCon- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- , let ks = k1 ++ k2- = case tc' of- _ | tc' == promotedTrueDataCon- -> Just (Right (ct, (x', y', True)), ks)- _ | tc' == promotedFalseDataCon- -> Just (Right (ct, (x', y', False)), ks)- _ -> Nothing- | tc == assertT- , tc' == (cTupleTyCon 0)- , [] <- ys- , [TyConApp ordCondTc zs, _] <- xs- , ordCondTc == ordCond- , [_,cmp,lt,eq,gt] <- zs- , TyConApp tcCmpNat [x,y] <- cmp- , tcCmpNat == typeNatCmpTyCon- , TyConApp ltTc [] <- lt- , ltTc == promotedTrueDataCon- , TyConApp eqTc [] <- eq- , eqTc == promotedTrueDataCon- , TyConApp gtTc [] <- gt- , gtTc == promotedFalseDataCon- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- , let ks = k1 ++ k2- = Just (Right (ct, (x', y', True)), ks)-- go x y- | isNatKind (typeKind x)- , isNatKind (typeKind y)- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- = Just (Left (ct,x',y'),k1 ++ k2)- | otherwise- = Nothing-- go2 (TyConApp tc ys)- | tc == assertT- , [TyConApp ordCondTc xs, _] <- ys- , ordCondTc == ordCond- , [_,cmp,lt,eq,gt] <- xs- , TyConApp tcCmpNat [x,y] <- cmp- , tcCmpNat == typeNatCmpTyCon- , TyConApp ltTc [] <- lt- , ltTc == promotedTrueDataCon- , TyConApp eqTc [] <- eq- , eqTc == promotedTrueDataCon- , TyConApp gtTc [] <- gt- , gtTc == promotedFalseDataCon- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- , let ks = k1 ++ k2- = Just (Right (ct, (x', y', True)), ks)-- go2 _ = Nothing-- isNatKind :: Kind -> Bool- isNatKind = (`eqType` naturalTy)--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--evSubtPreds :: CtLoc -> [PredType] -> TcPluginM [Ct]-evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc)--evMagic :: Ct -> [Coercion] -> Set CType -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))-evMagic ct deps knW preds = do- holeWanteds <- evSubtPreds (ctLoc ct) preds- knWanted <- mapM (mkKnWanted (ctLoc ct)) (toList knW)- let newWant = knWanted ++ holeWanteds- case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2 ->- let ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") deps Nominal t1 t2- in return (Just ((EvExpr (Coercion ctEv), ct),newWant))- IrredPred p ->- let t1 = mkTyConApp (cTupleTyCon 0) []- co = mkUnivCo (PluginProv "ghc-typelits-natnormalise") deps Representational t1 p- dcApp = evId (dataConWrapId (cTupleDataCon 0))- in return (Just ((evCast dcApp co, ct),newWant))- _ -> return Nothing--mkNonCanonical' :: CtLoc -> CtEvidence -> Ct-mkNonCanonical' origCtl ev =- let ct_ls = ctLocSpan origCtl- ctl = ctEvLoc ev- in mkNonCanonical (setCtEvLoc ev (setCtLocSpan ctl ct_ls))--mkKnWanted- :: CtLoc- -> CType- -> TcPluginM Ct-mkKnWanted loc (CType ty) = do- kc_clas <- tcLookupClass knownNatClassName- let kn_pred = mkClassPred kc_clas [ty]- wantedCtEv <- newWanted loc kn_pred- let wanted' = mkNonCanonical' loc wantedCtEv- return wanted'
− src-ghc-9.4/GHC/TypeLits/Normalise.hs
@@ -1,740 +0,0 @@-{-|-Copyright : (C) 2015-2016, University of Twente,- 2017 , QBayLogic B.V.-License : BSD2 (see the file LICENSE)-Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>--A type checker plugin for GHC that can solve /equalities/ of types of kind-'GHC.TypeLits.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/-'GHC.TypeLits.Normalise.SOP.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 'GHC.TypeLits.Normalise.SOP.SOP' normal form-of the former.--To use the plugin, add--@-{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}-@--To the header of your file.--== Treating subtraction as addition with a negated number--If you are absolutely sure that your subtractions can /never/ lead to (a locally)-negative number, you can ask the plugin to treat subtraction as addition with-a negated operand by additionally adding:--@-{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}-@--to the header of your file, thereby allowing to use associativity and-commutativity rules when proving constraints involving subtractions. Note that-this option can lead to unsound behaviour and should be handled with extreme-care.--=== When it leads to unsound behaviour--For example, enabling the /allow-negated-numbers/ feature would allow-you to prove:--@-(n - 1) + 1 ~ n-@--/without/ a @(1 <= n)@ constraint, even though when /n/ is set to /0/ the-subtraction @n-1@ would be locally negative and hence not be a natural number.--This would allow the following erroneous definition:--@-data Fin (n :: Nat) where- FZ :: Fin (n + 1)- FS :: Fin n -> Fin (n + 1)--f :: forall n . Natural -> Fin n-f n = case of- 0 -> FZ- x -> FS (f \@(n-1) (x - 1))--fs :: [Fin 0]-fs = f \<$\> [0..]-@--=== When it might be Okay--This example is taken from the <http://hackage.haskell.org/package/mezzo mezzo>-library.--When you have:--@--- | Singleton type for the number of repetitions of an element.-data Times (n :: Nat) where- T :: Times n---- | An element of a "run-length encoded" vector, containing the value and--- the number of repetitions-data Elem :: Type -> Nat -> Type where- (:*) :: t -> Times n -> Elem t n---- | A length-indexed vector, optimised for repetitions.-data OptVector :: Type -> Nat -> Type where- End :: OptVector t 0- (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n-@--And you want to define:--@--- | Append two optimised vectors.-type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where- ys ++ End = ys- End ++ ys = ys- (x :- xs) ++ ys = x :- (xs ++ ys)-@--then the last line will give rise to the constraint:--@-(n-l)+m ~ (n+m)-l-@--because:--@-x :: Elem t l-xs :: OptVector t (n-l)-ys :: OptVector t m-@--In this case it's okay to add--@-{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}-@--if you can convince yourself you will never be able to construct a:--@-xs :: OptVector t (n-l)-@--where /n-l/ is a negative number.--}--{-# LANGUAGE CPP #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE TemplateHaskellQuotes #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.Normalise- ( plugin )-where---- external-import Control.Arrow (second)-import Control.Monad ((<=<), forM)-import Control.Monad.Trans.Writer.Strict-import Data.Either (partitionEithers, rights)-import Data.IORef-import Data.List (intersect, partition, stripPrefix, find)-import Data.Maybe (mapMaybe, catMaybes)-import Data.Set (Set, empty, toList, notMember, fromList, union)-import Text.Read (readMaybe)-import qualified Data.Type.Ord-import qualified GHC.TypeError--import GHC.TcPluginM.Extra (tracePlugin, newGiven, newWanted)---- GHC API-import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey)-import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)-import GHC.Builtin.Types.Literals- (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)-import GHC.Builtin.Types (naturalTy, cTupleDataCon, cTupleTyCon)-import GHC.Builtin.Types.Literals (typeNatCmpTyCon)-import GHC.Core (Expr (..))-import GHC.Core.Class (className)-import GHC.Core.Coercion (Role (..), mkUnivCo)-import GHC.Core.DataCon (dataConWrapId)-import GHC.Core.Predicate- (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType, mkClassPred,- mkPrimEqPred, isEqPred, isEqPrimPred, getClassPredTys_maybe)-import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..))-import GHC.Core.TyCon (TyCon)-#if MIN_VERSION_ghc(9,6,0)-import GHC.Core.Type- (Kind, PredType, mkTyVarTy, tyConAppTyCon_maybe, typeKind, mkTyConApp)-import GHC.Core.TyCo.Compare- (eqType)-#else-import GHC.Core.Type- (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe, typeKind, mkTyConApp)-#endif-import GHC.Data.IOEnv (getEnv)-import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)-import GHC.Plugins (thNameToGhcNameIO, HscEnv (hsc_NC))-import GHC.Tc.Plugin- (TcPluginM, tcLookupClass, tcPluginTrace, tcPluginIO, newEvVar)-import GHC.Tc.Plugin (tcLookupTyCon, unsafeTcPluginTcM)-import GHC.Tc.Types (TcPlugin (..), TcPluginSolveResult(..), Env (env_top))-import GHC.Tc.Types.Constraint- (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence,- ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLocSpan,- isWantedCt, ctEvLoc, ctEvPred, ctEvExpr, emptyRewriterSet, setCtEvLoc)-import GHC.Tc.Types.Evidence (EvBindsVar, EvTerm (..), evCast, evId)-import GHC.Types.Unique.FM (emptyUFM)-import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)-import GHC (Name)---- template-haskell-import qualified Language.Haskell.TH as TH---- internal-import GHC.TypeLits.Normalise.SOP-import GHC.TypeLits.Normalise.Unify hiding (subtractionToPred)--isEqPredClass :: PredType -> Bool-isEqPredClass ty = case tyConAppTyCon_maybe ty of- Just tc -> tc `hasKey` eqTyConKey || tc `hasKey` heqTyConKey- _ -> False---- | To use the plugin, add------ @--- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}--- @------ To the header of your file.-plugin :: Plugin-plugin- = defaultPlugin- { tcPlugin = fmap (normalisePlugin . foldr id defaultOpts) . traverse parseArgument- , 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 = tracePlugin "ghc-typelits-natnormalise"- TcPlugin { tcPluginInit = lookupExtraDefs- , tcPluginSolve = decideEqualSOP opts- , tcPluginRewrite = const emptyUFM- , tcPluginStop = const (return ())- }--type ExtraDefs = (IORef (Set CType), (TyCon,TyCon,TyCon))--lookupExtraDefs :: TcPluginM ExtraDefs-lookupExtraDefs = do- ref <- tcPluginIO (newIORef empty)- ordCond <- lookupTHName ''Data.Type.Ord.OrdCond >>= tcLookupTyCon- leqT <- lookupTHName ''(Data.Type.Ord.<=) >>= tcLookupTyCon- assertT <- lookupTHName ''GHC.TypeError.Assert >>= tcLookupTyCon- return (ref, (leqT,assertT,ordCond))--lookupTHName :: TH.Name -> TcPluginM Name-lookupTHName th = do- nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv)- res <- tcPluginIO $ thNameToGhcNameIO nc th- maybe (fail $ "Failed to lookup " ++ show th) return res--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.<=?- -> EvBindsVar- -> [Ct]- -> [Ct]- -> TcPluginM 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 (gen'd,(leqT,_,_)) ev givens [] = do- done <- tcPluginIO $ readIORef gen'd- let reds =- filter (\(_,(_,_,v)) -> null v || negNumbers opts) $- reduceGivens opts leqT done givens- newlyDone = map (\(_,(prd, _,_)) -> CType prd) reds- tcPluginIO $- modifyIORef' gen'd $ union (fromList newlyDone)- newGivens <- forM reds $ \(origCt, (pred', evTerm, _)) ->- mkNonCanonical' (ctLoc origCt) <$> newGiven ev (ctLoc origCt) pred' evTerm- return (TcPluginOk [] newGivens)---- Solving phase.--- Solves in/equalities on Nats and simplifiable constraints--- containing naturals.-decideEqualSOP opts (gen'd,tcs@(leqT,_,_)) ev givens wanteds = do- let unit_wanteds = mapMaybe (toNatEquality tcs) wanteds- nonEqs = filter ( not- . (\p -> isEqPred p || isEqPrimPred p)- . ctEvPred- . ctEvidence )- wanteds- done <- tcPluginIO $ readIORef gen'd- let redGs = reduceGivens opts leqT done givens- newlyDone = map (\(_,(prd, _,_)) -> CType prd) redGs- redGivens <- forM redGs $ \(origCt, (pred', evTerm, _)) ->- mkNonCanonical' (ctLoc origCt) <$> newGiven ev (ctLoc origCt) pred' evTerm- reducible_wanteds- <- catMaybes <$> mapM (\ct -> fmap (ct,) <$>- reduceNatConstr (givens ++ redGivens) ct)- nonEqs- if null unit_wanteds && 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.- ineqForRedWants <- fmap concat $ forM redGs $ \(ct, (_,_, ws)) -> forM ws $- fmap (mkNonCanonical' (ctLoc ct)) . newWanted (ctLoc ct)- tcPluginIO $- modifyIORef' gen'd $ union (fromList newlyDone)- let unit_givens = mapMaybe- (toNatEquality tcs)- givens- sr <- simplifyNats opts leqT unit_givens unit_wanteds- tcPluginTrace "normalised" (ppr sr)- reds <- forM reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do- wants <- evSubtPreds (ctLoc origCt) $ subToPred opts leqT ws- return ((term, origCt), wDicts ++ wants)- case sr of- Simplified evs -> do- let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs- -- Only solve derived when we solved a wanted- simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of- [] -> []- _ -> simpld- (solved',newWanteds) = second concat (unzip $ simpld1 ++ reds)- return (TcPluginOk solved' $ newWanteds ++ ineqForRedWants)- Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])--type NatEquality = (Ct,CoreSOP,CoreSOP)-type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))--reduceGivens :: Opts -> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))]-reduceGivens opts leqT done givens =- let nonEqs =- [ ct- | ct <- givens- , let ev = ctEvidence ct- prd = ctEvPred ev- , isGiven ev- , not $ (\p -> isEqPred p || isEqPrimPred p || isEqPredClass p) prd- ]- in filter- (\(_, (prd, _, _)) ->- notMember (CType prd) done- )- $ mapMaybe- (\ct -> (ct,) <$> tryReduceGiven opts leqT givens ct)- nonEqs--tryReduceGiven- :: Opts -> TyCon -> [Ct] -> Ct- -> Maybe (PredType, EvTerm, [PredType])-tryReduceGiven opts leqT simplGivens ct = do- let (mans, ws) =- runWriter $ normaliseNatEverywhere $- ctEvPred $ ctEvidence ct- ws' = [ p- | p <- subToPred opts leqT ws- , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens- ]- pred' <- mans- return (pred', toReducedDict (ctEvidence ct) pred', ws')--fromNatEquality :: Either NatEquality NatInEquality -> Ct-fromNatEquality (Left (ct, _, _)) = ct-fromNatEquality (Right (ct, _)) = ct--reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))-reduceNatConstr givens ct = do- let pred0 = ctEvPred $ ctEvidence ct- (mans, tests) = runWriter $ normaliseNatEverywhere pred0- case mans of- Nothing -> return Nothing- Just pred' -> do- case find ((`eqType` pred') .ctEvPred . ctEvidence) givens of- -- No existing evidence found- Nothing -> case getClassPredTys_maybe pred' of- -- Are we trying to solve a class instance?- Just (cls,_) | className cls /= knownNatClassName -> do- -- Create new evidence binding for normalized class constraint- evVar <- newEvVar pred'- -- Bind the evidence to a new wanted normalized class constraint- let wDict = mkNonCanonical- (CtWanted pred' (EvVarDest evVar) (ctLoc ct) emptyRewriterSet)- -- Evidence for current wanted is simply the coerced binding for- -- the new binding- evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise")- Representational- pred' pred0- ev = evId evVar `evCast` evCo- -- Use newly created coerced wanted as evidence, and emit the- -- normalized wanted as a new constraint to solve.- return (Just (ev, tests, [wDict]))- _ -> return Nothing- -- Use existing evidence- Just c -> return (Just (toReducedDict (ctEvidence c) pred0, tests, []))--toReducedDict :: CtEvidence -> PredType -> EvTerm-toReducedDict ct pred' =- let pred0 = ctEvPred ct- evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise")- Representational- pred0 pred'- ev = ctEvExpr ct- `evCast` evCo- in ev--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- :: Opts- -- ^ Allow negated numbers (potentially unsound!)- -> TyCon- -- * TyCon of Data.Type.Ord.<=- -> [(Either NatEquality NatInEquality,[(Type,Type)])]- -- ^ Given constraints- -> [(Either NatEquality NatInEquality,[(Type,Type)])]- -- ^ Wanted constraints- -> TcPluginM SimplifyResult-simplifyNats opts@Opts {..} leqT eqsG eqsW = do- let eqsG1 = map (second (const ([] :: [(Type,Type)]))) eqsG- (varEqs,otherEqs) = partition isVarEqs eqsG1- fancyGivens = concatMap (makeGivensSet otherEqs) varEqs- case varEqs of- [] -> do- let eqs = otherEqs ++ eqsW- tcPluginTrace "simplifyNats" (ppr eqs)- simples [] [] [] [] eqs- _ -> do- tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")")- (ppr varEqs)-- allSimplified <- forM fancyGivens $ \v -> do- let eqs = v ++ eqsW- tcPluginTrace "simplifyNats" (ppr eqs)- simples [] [] [] [] eqs-- pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified)- where- simples :: [CoreUnify]- -> [((EvTerm, Ct), [Ct])]- -> [(CoreSOP,CoreSOP,Bool)]- -> [(Either NatEquality NatInEquality,[(Type,Type)])]- -> [(Either NatEquality NatInEquality,[(Type,Type)])]- -> TcPluginM SimplifyResult- simples _subst evs _leqsG _xs [] = return (Simplified evs)- simples subst evs leqsG xs (eq@(Left (ct,u,v),k):eqs') = do- let u' = substsSOP subst u- v' = substsSOP subst v- ur <- unifyNats ct u' v'- tcPluginTrace "unifyNats result" (ppr ur)- case ur of- Win -> do- evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred opts leqT k)- simples subst evs' leqsG [] (xs ++ eqs')- Lose -> if null evs && null eqs'- then return (Impossible (fst eq))- else simples subst evs leqsG xs eqs'- Draw [] -> simples subst evs [] (eq:xs) eqs'- Draw subst' -> do- evM <- evMagic ct empty (map unifyItemToPredType subst' ++- subToPred opts leqT k)- let leqsG' | isGiven (ctEvidence ct) = eqToLeq u' v' ++ leqsG- | otherwise = leqsG- case evM of- Nothing -> simples subst evs leqsG' xs eqs'- Just ev ->- simples (substsSubst subst' subst ++ subst')- (ev:evs) leqsG' [] (xs ++ eqs')- simples subst evs leqsG xs (eq@(Right (ct,u@(x,y,b)),k):eqs') = do- 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 fst eqsG))- ]- tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs))- case runWriterT (isNatural u') of- Just (True,knW) -> do- evs' <- maybe evs (:evs) <$> evMagic ct knW (subToPred opts leqT k)- simples subst evs' leqsG' xs eqs'-- Just (False,_) | null k -> return (Impossible (fst eq))- _ -> 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) <$> evMagic ct kW (subToPred opts leqT k)- simples subst evs' leqsG' xs eqs'- _ -> simples subst evs leqsG (eq:xs) 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 otherEqs varEq- = let (noMentionsV,mentionsV) = partitionEithers- (map (matchesVarEq varEq) otherEqs)- (mentionsLHS,mentionsRHS) = partitionEithers mentionsV- vS = swapVar 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 (Left (_, S [P [V v1]], S [P [V v2]]),_) r = case r 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]]),ps) =- (Left (ct,S [P [V v2]], S [P [V v1]]),ps)- swapVar _ = error "internal error"-- findFirstSimpliedWanted (Impossible e) _ = Impossible e- findFirstSimpliedWanted (Simplified evs) s2- | any (isWantedCt . snd . fst) evs- = Simplified evs- | otherwise- = s2---- 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 -> TyCon -> [(Type, Type)] -> [PredType]-subToPred Opts{..} leqT- | negNumbers = const []- | otherwise = map leq- where- leq (a,b) =- let lhs = TyConApp leqT [naturalTy,b,a]- rhs = TyConApp (cTupleTyCon 0) []- in mkPrimEqPred lhs rhs---- Extract the Nat equality constraints-toNatEquality :: (TyCon,TyCon,TyCon) -> Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])-toNatEquality (_,assertT,ordCond) ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2- -> go t1 t2- IrredPred p- -> go2 p- _ -> 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)- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- -> Just (Left (ct, x', y'),k1 ++ k2)- _ -> Nothing- | tc == ordCond- , [_,cmp,lt,eq,gt] <- xs- , TyConApp tcCmpNat [x,y] <- cmp- , tcCmpNat == typeNatCmpTyCon- , TyConApp ltTc [] <- lt- , ltTc == promotedTrueDataCon- , TyConApp eqTc [] <- eq- , eqTc == promotedTrueDataCon- , TyConApp gtTc [] <- gt- , gtTc == promotedFalseDataCon- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- , let ks = k1 ++ k2- = case tc' of- _ | tc' == promotedTrueDataCon- -> Just (Right (ct, (x', y', True)), ks)- _ | tc' == promotedFalseDataCon- -> Just (Right (ct, (x', y', False)), ks)- _ -> Nothing- | tc == assertT- , tc' == (cTupleTyCon 0)- , [] <- ys- , [TyConApp ordCondTc zs, _] <- xs- , ordCondTc == ordCond- , [_,cmp,lt,eq,gt] <- zs- , TyConApp tcCmpNat [x,y] <- cmp- , tcCmpNat == typeNatCmpTyCon- , TyConApp ltTc [] <- lt- , ltTc == promotedTrueDataCon- , TyConApp eqTc [] <- eq- , eqTc == promotedTrueDataCon- , TyConApp gtTc [] <- gt- , gtTc == promotedFalseDataCon- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- , let ks = k1 ++ k2- = Just (Right (ct, (x', y', True)), ks)-- go x y- | isNatKind (typeKind x)- , isNatKind (typeKind y)- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- = Just (Left (ct,x',y'),k1 ++ k2)- | otherwise- = Nothing-- go2 (TyConApp tc ys)- | tc == assertT- , [TyConApp ordCondTc xs, _] <- ys- , ordCondTc == ordCond- , [_,cmp,lt,eq,gt] <- xs- , TyConApp tcCmpNat [x,y] <- cmp- , tcCmpNat == typeNatCmpTyCon- , TyConApp ltTc [] <- lt- , ltTc == promotedTrueDataCon- , TyConApp eqTc [] <- eq- , eqTc == promotedTrueDataCon- , TyConApp gtTc [] <- gt- , gtTc == promotedFalseDataCon- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- , let ks = k1 ++ k2- = Just (Right (ct, (x', y', True)), ks)-- go2 _ = Nothing-- isNatKind :: Kind -> Bool- isNatKind = (`eqType` naturalTy)--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--evSubtPreds :: CtLoc -> [PredType] -> TcPluginM [Ct]-evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc)--evMagic :: Ct -> Set CType -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))-evMagic ct knW preds = do- holeWanteds <- evSubtPreds (ctLoc ct) preds- knWanted <- mapM (mkKnWanted (ctLoc ct)) (toList knW)- let newWant = knWanted ++ holeWanteds- case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2 ->- let ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2- in return (Just ((EvExpr (Coercion ctEv), ct),newWant))- IrredPred p ->- let t1 = mkTyConApp (cTupleTyCon 0) []- co = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Representational t1 p- dcApp = evId (dataConWrapId (cTupleDataCon 0))- in return (Just ((evCast dcApp co, ct),newWant))- _ -> return Nothing--mkNonCanonical' :: CtLoc -> CtEvidence -> Ct-mkNonCanonical' origCtl ev =- let ct_ls = ctLocSpan origCtl- ctl = ctEvLoc ev- in mkNonCanonical (setCtEvLoc ev (setCtLocSpan ctl ct_ls))--mkKnWanted- :: CtLoc- -> CType- -> TcPluginM Ct-mkKnWanted loc (CType ty) = do- kc_clas <- tcLookupClass knownNatClassName- let kn_pred = mkClassPred kc_clas [ty]- wantedCtEv <- newWanted loc kn_pred- let wanted' = mkNonCanonical' loc wantedCtEv- return wanted'
− src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs
@@ -1,862 +0,0 @@-{-|-Copyright : (C) 2015-2016, University of Twente,- 2017 , QBayLogic B.V.-License : BSD2 (see the file LICENSE)-Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>--A type checker plugin for GHC that can solve /equalities/ of types of kind-'GHC.TypeLits.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/-'GHC.TypeLits.Normalise.SOP.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 'GHC.TypeLits.Normalise.SOP.SOP' normal form-of the former.--To use the plugin, add--@-{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}-@--To the header of your file.--== Treating subtraction as addition with a negated number--If you are absolutely sure that your subtractions can /never/ lead to (a locally)-negative number, you can ask the plugin to treat subtraction as addition with-a negated operand by additionally adding:--@-{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}-@--to the header of your file, thereby allowing to use associativity and-commutativity rules when proving constraints involving subtractions. Note that-this option can lead to unsound behaviour and should be handled with extreme-care.--=== When it leads to unsound behaviour--For example, enabling the /allow-negated-numbers/ feature would allow-you to prove:--@-(n - 1) + 1 ~ n-@--/without/ a @(1 <= n)@ constraint, even though when /n/ is set to /0/ the-subtraction @n-1@ would be locally negative and hence not be a natural number.--This would allow the following erroneous definition:--@-data Fin (n :: Nat) where- FZ :: Fin (n + 1)- FS :: Fin n -> Fin (n + 1)--f :: forall n . Natural -> Fin n-f n = case of- 0 -> FZ- x -> FS (f \@(n-1) (x - 1))--fs :: [Fin 0]-fs = f \<$\> [0..]-@--=== When it might be Okay--This example is taken from the <http://hackage.haskell.org/package/mezzo mezzo>-library.--When you have:--@--- | Singleton type for the number of repetitions of an element.-data Times (n :: Nat) where- T :: Times n---- | An element of a "run-length encoded" vector, containing the value and--- the number of repetitions-data Elem :: Type -> Nat -> Type where- (:*) :: t -> Times n -> Elem t n---- | A length-indexed vector, optimised for repetitions.-data OptVector :: Type -> Nat -> Type where- End :: OptVector t 0- (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n-@--And you want to define:--@--- | Append two optimised vectors.-type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where- ys ++ End = ys- End ++ ys = ys- (x :- xs) ++ ys = x :- (xs ++ ys)-@--then the last line will give rise to the constraint:--@-(n-l)+m ~ (n+m)-l-@--because:--@-x :: Elem t l-xs :: OptVector t (n-l)-ys :: OptVector t m-@--In this case it's okay to add--@-{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}-@--if you can convince yourself you will never be able to construct a:--@-xs :: OptVector t (n-l)-@--where /n-l/ is a negative number.--}--{-# LANGUAGE CPP #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE ViewPatterns #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.Normalise- ( plugin )-where---- external-import Control.Arrow (second)-import Control.Monad ((<=<), forM)-#if !MIN_VERSION_ghc(8,4,1)-import Control.Monad (replicateM)-#endif-import Control.Monad.Trans.Writer.Strict-import Data.Either (partitionEithers, rights)-import Data.IORef-import Data.List (intersect, partition, stripPrefix, find)-import Data.Maybe (mapMaybe, catMaybes)-import Data.Set (Set, empty, toList, notMember, fromList, union)-import GHC.TcPluginM.Extra (tracePlugin, newGiven, newWanted)-#if MIN_VERSION_ghc(9,2,0)-import GHC.TcPluginM.Extra (lookupModule, lookupName)-#endif-import qualified GHC.TcPluginM.Extra as TcPluginM-#if MIN_VERSION_ghc(8,4,0)-import GHC.TcPluginM.Extra (flattenGivens)-#endif-import Text.Read (readMaybe)---- GHC API-#if MIN_VERSION_ghc(9,0,0)-import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey)-import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)-import GHC.Builtin.Types.Literals- (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)-#if MIN_VERSION_ghc(9,2,0)-import GHC.Builtin.Types (naturalTy)-import GHC.Builtin.Types.Literals (typeNatCmpTyCon)-#else-import GHC.Builtin.Types (typeNatKind)-import GHC.Builtin.Types.Literals (typeNatLeqTyCon)-#endif-import GHC.Core (Expr (..))-import GHC.Core.Class (className)-import GHC.Core.Coercion (CoercionHole, Role (..), mkUnivCo)-import GHC.Core.Predicate- (EqRel (NomEq), Pred (EqPred), classifyPredType, getEqPredTys, mkClassPred,- mkPrimEqPred, isEqPred, isEqPrimPred, getClassPredTys_maybe)-import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..))-import GHC.Core.TyCon (TyCon)-import GHC.Core.Type- (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe, typeKind)-import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)-import GHC.Tc.Plugin- (TcPluginM, newCoercionHole, tcLookupClass, tcPluginTrace, tcPluginIO,- newEvVar)-#if MIN_VERSION_ghc(9,2,0)-import GHC.Tc.Plugin (tcLookupTyCon)-#endif-import GHC.Tc.Types (TcPlugin (..), TcPluginResult (..))-import GHC.Tc.Types.Constraint- (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ShadowInfo (WDeriv), ctEvidence,- ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan,- isWantedCt, ctEvLoc, ctEvPred, ctEvExpr)-import GHC.Tc.Types.Evidence (EvTerm (..), evCast, evId)-#if MIN_VERSION_ghc(9,2,0)-import GHC.Data.FastString (fsLit)-import GHC.Types.Name.Occurrence (mkTcOcc)-import GHC.Unit.Module (mkModuleName)-#endif-import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)-#else-#if MIN_VERSION_ghc(8,5,0)-import CoreSyn (Expr (..))-#endif-import Outputable (Outputable (..), (<+>), ($$), text)-import Plugins (Plugin (..), defaultPlugin)-#if MIN_VERSION_ghc(8,6,0)-import Plugins (purePlugin)-#endif-import PrelNames (hasKey, knownNatClassName)-import PrelNames (eqTyConKey, heqTyConKey)-import TcEvidence (EvTerm (..))-#if MIN_VERSION_ghc(8,6,0)-import TcEvidence (evCast, evId)-#endif-#if !MIN_VERSION_ghc(8,4,0)-import TcPluginM (zonkCt)-#endif-import TcPluginM (TcPluginM, tcPluginTrace, tcPluginIO)-import Type- (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe)-import TysWiredIn (typeNatKind)--import Coercion (CoercionHole, Role (..), mkUnivCo)-import Class (className)-import TcPluginM (newCoercionHole, tcLookupClass, newEvVar)-import TcRnTypes (TcPlugin (..), TcPluginResult(..))-import TyCoRep (UnivCoProvenance (..))-import TcType (isEqPred)-import TyCon (TyCon)-import TyCoRep (Type (..))-import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,- typeNatSubTyCon)--import TcTypeNats (typeNatLeqTyCon)-import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon)--#if MIN_VERSION_ghc(8,10,0)-import Constraint- (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence, ctEvLoc, ctEvPred,- ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan,- isWantedCt)-import Predicate- (EqRel (NomEq), Pred (EqPred), classifyPredType, getEqPredTys, mkClassPred,- mkPrimEqPred, getClassPredTys_maybe)-import Type (typeKind)-#else-import TcRnTypes- (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence, ctEvLoc, ctEvPred,- ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan,- isWantedCt)-import TcType (typeKind)-import Type- (EqRel (NomEq), PredTree (EqPred), classifyPredType, mkClassPred, mkPrimEqPred,- getClassPredTys_maybe)-#if MIN_VERSION_ghc(8,4,0)-import Type (getEqPredTys)-#endif-#endif--#if MIN_VERSION_ghc(8,10,0)-import Constraint (ctEvExpr)-#elif MIN_VERSION_ghc(8,6,0)-import TcRnTypes (ctEvExpr)-#else-import TcRnTypes (ctEvTerm)-#endif--#if MIN_VERSION_ghc(8,2,0)-#if MIN_VERSION_ghc(8,10,0)-import Constraint (ShadowInfo (WDeriv))-#else-import TcRnTypes (ShadowInfo (WDeriv))-#endif-#endif--#if MIN_VERSION_ghc(8,10,0)-import TcType (isEqPrimPred)-#endif-#endif---- internal-import GHC.TypeLits.Normalise.SOP-import GHC.TypeLits.Normalise.Unify--#if MIN_VERSION_ghc(9,2,0)-typeNatKind :: Type-typeNatKind = naturalTy-#endif--#if !MIN_VERSION_ghc(8,10,0)-isEqPrimPred :: PredType -> Bool-isEqPrimPred = isEqPred-#endif--isEqPredClass :: PredType -> Bool-isEqPredClass ty = case tyConAppTyCon_maybe ty of- Just tc -> tc `hasKey` eqTyConKey || tc `hasKey` heqTyConKey- _ -> False---- | To use the plugin, add------ @--- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}--- @------ To the header of your file.-plugin :: Plugin-plugin- = defaultPlugin- { tcPlugin = fmap (normalisePlugin . foldr id defaultOpts) . traverse parseArgument-#if MIN_VERSION_ghc(8,6,0)- , pluginRecompile = purePlugin-#endif- }- 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 = tracePlugin "ghc-typelits-natnormalise"- TcPlugin { tcPluginInit = lookupExtraDefs- , tcPluginSolve = decideEqualSOP opts- , tcPluginStop = const (return ())- }-newtype OrigCt = OrigCt { runOrigCt :: Ct }--type ExtraDefs = (IORef (Set CType), TyCon)--lookupExtraDefs :: TcPluginM ExtraDefs-lookupExtraDefs = do- ref <- tcPluginIO (newIORef empty)-#if !MIN_VERSION_ghc(9,2,0)- return (ref, typeNatLeqTyCon)-#else- md <- lookupModule myModule myPackage- ordCond <- look md "OrdCond"- return (ref, ordCond)- where- look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)- myModule = mkModuleName "Data.Type.Ord"- myPackage = fsLit "base"-#endif--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]- -> [Ct]- -> TcPluginM TcPluginResult---- 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 (gen'd,ordCond) givens _deriveds [] = do- done <- tcPluginIO $ readIORef gen'd-#if MIN_VERSION_ghc(8,4,0)- let simplGivens = flattenGivens givens-#else- simplGivens <- mapM zonkCt givens-#endif- let reds =- filter (\(_,(_,_,v)) -> null v || negNumbers opts) $- reduceGivens opts ordCond done simplGivens- newlyDone = map (\(_,(prd, _,_)) -> CType prd) reds- tcPluginIO $- modifyIORef' gen'd $ union (fromList newlyDone)- newGivens <- forM reds $ \(origCt, (pred', evTerm, _)) ->- mkNonCanonical' (ctLoc origCt) <$> newGiven (ctLoc origCt) pred' evTerm- return (TcPluginOk [] newGivens)---- Solving phase.--- Solves in/equalities on Nats and simplifiable constraints--- containing naturals.-decideEqualSOP opts (gen'd,ordCond) givens deriveds wanteds = do- -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out- let flat_wanteds0 = map (\ct -> (OrigCt ct, ct)) wanteds-#if MIN_VERSION_ghc(8,4,0)- -- flattenGivens should actually be called unflattenGivens- let simplGivens = givens ++ flattenGivens givens- subst = fst $ unzip $ TcPluginM.mkSubst' givens- unflattenWanted (oCt, ct) = (oCt, TcPluginM.substCt subst ct)- unflat_wanteds0 = map unflattenWanted flat_wanteds0-#else- let unflat_wanteds0 = flat_wanteds0- simplGivens <- mapM zonkCt givens-#endif- let unflat_wanteds1 = filter (isWanted . ctEvidence . snd) unflat_wanteds0- -- only return solve deriveds when there are wanteds to solve- unflat_wanteds2 = case unflat_wanteds1 of- [] -> []- w -> w ++ (map (\a -> (OrigCt a,a)) deriveds)- unit_wanteds = mapMaybe (toNatEquality ordCond) unflat_wanteds2- nonEqs = filter (not . (\p -> isEqPred p || isEqPrimPred p) . ctEvPred . ctEvidence.snd)- $ filter (isWanted. ctEvidence.snd) unflat_wanteds0- done <- tcPluginIO $ readIORef gen'd- let redGs = reduceGivens opts ordCond done simplGivens- newlyDone = map (\(_,(prd, _,_)) -> CType prd) redGs- redGivens <- forM redGs $ \(origCt, (pred', evTerm, _)) ->- mkNonCanonical' (ctLoc origCt) <$> newGiven (ctLoc origCt) pred' evTerm- reducible_wanteds- <- catMaybes <$>- mapM- (\(origCt, ct) -> fmap (runOrigCt origCt,) <$>- reduceNatConstr (simplGivens ++ redGivens) ct- )- nonEqs- if null unit_wanteds && 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.- ineqForRedWants <- fmap concat $ forM redGs $ \(ct, (_,_, ws)) -> forM ws $- fmap (mkNonCanonical' (ctLoc ct)) . newWanted (ctLoc ct)- tcPluginIO $- modifyIORef' gen'd $ union (fromList newlyDone)- let unit_givens = mapMaybe- (toNatEquality ordCond)- (map (\a -> (OrigCt a, a)) simplGivens)- sr <- simplifyNats opts ordCond unit_givens unit_wanteds- tcPluginTrace "normalised" (ppr sr)- reds <- forM reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do- wants <- evSubtPreds origCt $ subToPred opts ordCond ws- return ((term, origCt), wDicts ++ wants)- case sr of- Simplified evs -> do- let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs- -- Only solve derived when we solved a wanted- simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of- [] -> []- _ -> simpld- (solved',newWanteds) = second concat (unzip $ simpld1 ++ reds)- return (TcPluginOk solved' $ newWanteds ++ ineqForRedWants)- Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])--type NatEquality = (Ct,CoreSOP,CoreSOP)-type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))--reduceGivens :: Opts -> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))]-reduceGivens opts ordCond done givens =- let nonEqs =- [ ct- | ct <- givens- , let ev = ctEvidence ct- prd = ctEvPred ev- , isGiven ev- , not $ (\p -> isEqPred p || isEqPrimPred p || isEqPredClass p) prd- ]- in filter- (\(_, (prd, _, _)) ->- notMember (CType prd) done- )- $ mapMaybe- (\ct -> (ct,) <$> tryReduceGiven opts ordCond givens ct)- nonEqs--tryReduceGiven- :: Opts -> TyCon -> [Ct] -> Ct- -> Maybe (PredType, EvTerm, [PredType])-tryReduceGiven opts ordCond simplGivens ct = do- let (mans, ws) =- runWriter $ normaliseNatEverywhere $- ctEvPred $ ctEvidence ct- ws' = [ p- | (p, _) <- subToPred opts ordCond ws- , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens- ]- pred' <- mans- return (pred', toReducedDict (ctEvidence ct) pred', ws')--fromNatEquality :: Either NatEquality NatInEquality -> Ct-fromNatEquality (Left (ct, _, _)) = ct-fromNatEquality (Right (ct, _)) = ct--reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))-reduceNatConstr givens ct = do- let pred0 = ctEvPred $ ctEvidence ct- (mans, tests) = runWriter $ normaliseNatEverywhere pred0- case mans of- Nothing -> return Nothing- Just pred' -> do- case find ((`eqType` pred') .ctEvPred . ctEvidence) givens of- -- No existing evidence found- Nothing -> case getClassPredTys_maybe pred' of- -- Are we trying to solve a class instance?- Just (cls,_) | className cls /= knownNatClassName -> do- -- Create new evidence binding for normalized class constraint- evVar <- newEvVar pred'- -- Bind the evidence to a new wanted normalized class constraint- let wDict = mkNonCanonical- (CtWanted pred' (EvVarDest evVar)-#if MIN_VERSION_ghc(8,2,0)- WDeriv-#endif- (ctLoc ct))- -- Evidence for current wanted is simply the coerced binding for- -- the new binding- evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise")- Representational- pred' pred0-#if MIN_VERSION_ghc(8,6,0)- ev = evId evVar `evCast` evCo-#else- ev = EvId evVar `EvCast` evCo-#endif- -- Use newly created coerced wanted as evidence, and emit the- -- normalized wanted as a new constraint to solve.- return (Just (ev, tests, [wDict]))- _ -> return Nothing- -- Use existing evidence- Just c -> return (Just (toReducedDict (ctEvidence c) pred0, tests, []))--toReducedDict :: CtEvidence -> PredType -> EvTerm-toReducedDict ct pred' =- let pred0 = ctEvPred ct- evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise")- Representational- pred0 pred'-#if MIN_VERSION_ghc(8,6,0)- ev = ctEvExpr ct- `evCast` evCo-#else- ev = ctEvTerm ct `EvCast` evCo-#endif- in ev--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- :: Opts- -- ^ Allow negated numbers (potentially unsound!)- -> TyCon- -- ^ For GHc 9.2: TyCon of Data.Type.Ord.OrdCond- -- For older: TyCon of GHC.TypeLits.<=?- -> [(Either NatEquality NatInEquality,[(Type,Type)])]- -- ^ Given constraints- -> [(Either NatEquality NatInEquality,[(Type,Type)])]- -- ^ Wanted constraints- -> TcPluginM SimplifyResult-simplifyNats opts@Opts {..} ordCond eqsG eqsW = do- let eqsG1 = map (second (const ([] :: [(Type,Type)]))) eqsG- (varEqs,otherEqs) = partition isVarEqs eqsG1- fancyGivens = concatMap (makeGivensSet otherEqs) varEqs- case varEqs of- [] -> do- let eqs = otherEqs ++ eqsW- tcPluginTrace "simplifyNats" (ppr eqs)- simples [] [] [] [] eqs- _ -> do- tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")")- (ppr varEqs)-- allSimplified <- forM fancyGivens $ \v -> do- let eqs = v ++ eqsW- tcPluginTrace "simplifyNats" (ppr eqs)- simples [] [] [] [] eqs-- pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified)- where- simples :: [CoreUnify]- -> [((EvTerm, Ct), [Ct])]- -> [(CoreSOP,CoreSOP,Bool)]- -> [(Either NatEquality NatInEquality,[(Type,Type)])]- -> [(Either NatEquality NatInEquality,[(Type,Type)])]- -> TcPluginM SimplifyResult- simples _subst evs _leqsG _xs [] = return (Simplified evs)- simples subst evs leqsG xs (eq@(Left (ct,u,v),k):eqs') = do- let u' = substsSOP subst u- v' = substsSOP subst v- ur <- unifyNats ct u' v'- tcPluginTrace "unifyNats result" (ppr ur)- case ur of- Win -> do- evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred opts ordCond k)- simples subst evs' leqsG [] (xs ++ eqs')- Lose -> if null evs && null eqs'- then return (Impossible (fst eq))- else simples subst evs leqsG xs eqs'- Draw [] -> simples subst evs [] (eq:xs) eqs'- Draw subst' -> do- evM <- evMagic ct empty (map unifyItemToPredType subst' ++- subToPred opts ordCond k)- let leqsG' | isGiven (ctEvidence ct) = eqToLeq u' v' ++ leqsG- | otherwise = leqsG- case evM of- Nothing -> simples subst evs leqsG' xs eqs'- Just ev ->- simples (substsSubst subst' subst ++ subst')- (ev:evs) leqsG' [] (xs ++ eqs')- simples subst evs leqsG xs (eq@(Right (ct,u@(x,y,b)),k):eqs') = do- 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 fst eqsG))- ]- tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs))- case runWriterT (isNatural u') of- Just (True,knW) -> do- evs' <- maybe evs (:evs) <$> evMagic ct knW (subToPred opts ordCond k)- simples subst evs' leqsG' xs eqs'-- Just (False,_) | null k -> return (Impossible (fst eq))- _ -> 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) <$> evMagic ct kW (subToPred opts ordCond k)- simples subst evs' leqsG' xs eqs'- _ -> simples subst evs leqsG (eq:xs) 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 otherEqs varEq- = let (noMentionsV,mentionsV) = partitionEithers- (map (matchesVarEq varEq) otherEqs)- (mentionsLHS,mentionsRHS) = partitionEithers mentionsV- vS = swapVar 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 (Left (_, S [P [V v1]], S [P [V v2]]),_) r = case r 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]]),ps) =- (Left (ct,S [P [V v2]], S [P [V v1]]),ps)- swapVar _ = error "internal error"-- findFirstSimpliedWanted (Impossible e) _ = Impossible e- findFirstSimpliedWanted (Simplified evs) s2- | any (isWantedCt . snd . fst) evs- = Simplified evs- | otherwise- = s2---- 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 -> TyCon -> [(Type, Type)] -> [(PredType, Kind)]-subToPred Opts{..} ordCond- | negNumbers = const []- | otherwise = map (subtractionToPred ordCond)---- Extract the Nat equality constraints-toNatEquality :: TyCon -> (OrigCt, Ct) -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])-toNatEquality ordCond (OrigCt oCt, 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)- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- -> Just (Left (oCt, x', y'),k1 ++ k2)- _ -> Nothing-#if MIN_VERSION_ghc(9,2,0)- | tc == ordCond- , [_,cmp,lt,eq,gt] <- xs- , TyConApp tcCmpNat [x,y] <- cmp- , tcCmpNat == typeNatCmpTyCon- , TyConApp ltTc [] <- lt- , ltTc == promotedTrueDataCon- , TyConApp eqTc [] <- eq- , eqTc == promotedTrueDataCon- , TyConApp gtTc [] <- gt- , gtTc == promotedFalseDataCon- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- , let ks = k1 ++ k2- = case tc' of- _ | tc' == promotedTrueDataCon- -> Just (Right (oCt, (x', y', True)), ks)- _ | tc' == promotedFalseDataCon- -> Just (Right (oCt, (x', y', False)), ks)- _ -> Nothing-#else- | tc == ordCond- , [x,y] <- xs- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- , let ks = k1 ++ k2- = case tc' of- _ | tc' == promotedTrueDataCon- -> Just (Right (oCt, (x', y', True)), ks)- _ | tc' == promotedFalseDataCon- -> Just (Right (oCt, (x', y', False)), ks)- _ -> Nothing-#endif-- go x y- | isNatKind (typeKind x)- , isNatKind (typeKind y)- , let (x',k1) = runWriter (normaliseNat x)- , let (y',k2) = runWriter (normaliseNat y)- = Just (Left (oCt,x',y'),k1 ++ k2)- | otherwise- = Nothing-- isNatKind :: Kind -> Bool- isNatKind = (`eqType` typeNatKind)--unifyItemToPredType :: CoreUnify -> (PredType,Kind)-unifyItemToPredType ui =- (mkPrimEqPred ty1 ty2,typeNatKind)- where- ty1 = case ui of- SubstItem {..} -> mkTyVarTy siVar- UnifyItem {..} -> reifySOP siLHS- ty2 = case ui of- SubstItem {..} -> reifySOP siSOP- UnifyItem {..} -> reifySOP siRHS--evSubtPreds :: Ct -> [(PredType,Kind)] -> TcPluginM [Ct]-evSubtPreds ct preds = do- let predTypes = map fst preds-#if MIN_VERSION_ghc(8,4,1)- holes <- mapM (newCoercionHole . uncurry mkPrimEqPred . getEqPredTys) predTypes-#else- holes <- replicateM (length preds) newCoercionHole-#endif- return (zipWith (unifyItemToCt (ctLoc ct)) predTypes holes)--evMagic :: Ct -> Set CType -> [(PredType,Kind)] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))-evMagic ct knW preds = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2 -> do- holeWanteds <- evSubtPreds ct preds- knWanted <- mapM (mkKnWanted ct) (toList knW)- let newWant = knWanted ++ holeWanteds- ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2-#if MIN_VERSION_ghc(8,5,0)- return (Just ((EvExpr (Coercion ctEv), ct),newWant))-#else- return (Just ((EvCoercion ctEv, ct),newWant))-#endif- _ -> return Nothing--mkNonCanonical' :: CtLoc -> CtEvidence -> Ct-mkNonCanonical' origCtl ev =- let ct_ls = ctLocSpan origCtl- ctl = ctEvLoc ev- in setCtLoc (mkNonCanonical ev) (setCtLocSpan ctl ct_ls)--mkKnWanted- :: Ct- -> CType- -> TcPluginM Ct-mkKnWanted ct (CType ty) = do- kc_clas <- tcLookupClass knownNatClassName- let kn_pred = mkClassPred kc_clas [ty]- wantedCtEv <- TcPluginM.newWanted (ctLoc ct) kn_pred- let wanted' = mkNonCanonical' (ctLoc ct) wantedCtEv- return wanted'--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)
+ src/GHC/TypeLits/Normalise.hs view
@@ -0,0 +1,966 @@+{-|+Copyright : (C) 2015-2016, University of Twente,+ 2017 , QBayLogic B.V.+License : BSD2 (see the file LICENSE)+Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>++A type checker plugin for GHC that can solve /equalities/ of types of kind+'GHC.TypeLits.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/+'GHC.TypeLits.Normalise.SOP.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 'GHC.TypeLits.Normalise.SOP.SOP' normal form+of the former.++To use the plugin, add++@+{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}+@++To the header of your file.++== Treating subtraction as addition with a negated number++If you are absolutely sure that your subtractions can /never/ lead to (a locally)+negative number, you can ask the plugin to treat subtraction as addition with+a negated operand by additionally adding:++@+{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}+@++to the header of your file, thereby allowing to use associativity and+commutativity rules when proving constraints involving subtractions. Note that+this option can lead to unsound behaviour and should be handled with extreme+care.++=== When it leads to unsound behaviour++For example, enabling the /allow-negated-numbers/ feature would allow+you to prove:++@+(n - 1) + 1 ~ n+@++/without/ a @(1 <= n)@ constraint, even though when /n/ is set to /0/ the+subtraction @n-1@ would be locally negative and hence not be a natural number.++This would allow the following erroneous definition:++@+data Fin (n :: Nat) where+ FZ :: Fin (n + 1)+ FS :: Fin n -> Fin (n + 1)++f :: forall n . Natural -> Fin n+f n = case of+ 0 -> FZ+ x -> FS (f \@(n-1) (x - 1))++fs :: [Fin 0]+fs = f \<$\> [0..]+@++=== When it might be Okay++This example is taken from the <http://hackage.haskell.org/package/mezzo mezzo>+library.++When you have:++@+-- | Singleton type for the number of repetitions of an element.+data Times (n :: Nat) where+ T :: Times n++-- | An element of a "run-length encoded" vector, containing the value and+-- the number of repetitions+data Elem :: Type -> Nat -> Type where+ (:*) :: t -> Times n -> Elem t n++-- | A length-indexed vector, optimised for repetitions.+data OptVector :: Type -> Nat -> Type where+ End :: OptVector t 0+ (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n+@++And you want to define:++@+-- | Append two optimised vectors.+type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where+ ys ++ End = ys+ End ++ ys = ys+ (x :- xs) ++ ys = x :- (xs ++ ys)+@++then the last line will give rise to the constraint:++@+(n-l)+m ~ (n+m)-l+@++because:++@+x :: Elem t l+xs :: OptVector t (n-l)+ys :: OptVector t m+@++In this case it's okay to add++@+{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}+@++if you can convince yourself you will never be able to construct a:++@+xs :: OptVector t (n-l)+@++where /n-l/ is a negative number.+-}++{-# LANGUAGE CPP #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE TemplateHaskellQuotes #-}++{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}+{-# OPTIONS_HADDOCK show-extensions #-}++module GHC.TypeLits.Normalise+ ( plugin )+where++-- base+import Control.Arrow+ ( second )+import Control.Monad+ ( (<=<), unless )+import Control.Monad.Trans.Writer.Strict+ ( WriterT(runWriterT), runWriter )+import Data.Either+ ( rights, partitionEithers )+import Data.Foldable+import Data.List+ ( stripPrefix, partition )+import Data.Maybe+ ( mapMaybe, catMaybes, fromMaybe, isJust )+import Data.Traversable+ ( for )+import Text.Read+ ( readMaybe )++-- containers+import Data.Set+ ( Set )+import qualified Data.Set as Set+ ( elems, empty )+import Data.Map.Strict+ ( Map )+import qualified Data.Map.Strict as Map+ ( empty, insertWith, traverseWithKey )++-- ghc+import GHC.Builtin.Names+ ( knownNatClassName )+import GHC.Builtin.Types.Literals+ ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon )+import GHC.Core.TyCon+ ( Injectivity (..), tyConInjectivityInfo, tyConArity )+import GHC.Utils.Misc+ ( filterByList )++-- ghc-tcplugin-api+import GHC.TcPlugin.API+import GHC.TcPlugin.API.TyConSubst+ ( TyConSubst, mkTyConSubst )+import GHC.Plugins+ ( Plugin(..), defaultPlugin, purePlugin, allVarSet, isEmptyVarSet, tyCoVarsOfType )+import GHC.Utils.Outputable++-- ghc-typelits-natnormalise+import GHC.TypeLits.Normalise.Compat+import GHC.TypeLits.Normalise.SOP+ ( SOP(S), Product(P), Symbol(V) )+import GHC.TypeLits.Normalise.Unify++-- transformers+import Control.Monad.Trans.Class+ ( lift )+import Control.Monad.Trans.State.Strict+ ( StateT, evalStateT, get, modify )++--------------------------------------------------------------------------------++-- | To use the plugin, add+--+-- @+-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}+-- @+--+-- To the header of your file.+plugin :: Plugin+plugin+ = defaultPlugin+ { tcPlugin = \ p -> do opts <- foldr id defaultOpts <$> traverse parseArgument p+ return $ mkTcPlugin $ normalisePlugin opts+ , pluginRecompile = purePlugin+ }+ where+ parseArgument "allow-negated-numbers" = Just (\ opts -> opts { negNumbers = True })+ parseArgument (readMaybe <=< stripPrefix "depth=" -> Just depth) = Just (\ opts -> opts { depth })+ parseArgument _ = Nothing+ defaultOpts = Opts { negNumbers = False, depth = 5 }++data Opts = Opts { negNumbers :: Bool, depth :: Word }++normalisePlugin :: Opts -> TcPlugin+normalisePlugin opts =+ TcPlugin { tcPluginInit = lookupExtraDefs+ , tcPluginSolve = decideEqualSOP opts+ , tcPluginRewrite = const emptyUFM+ , tcPluginPostTc = const (return ())+ , tcPluginShutdown = const (return ())+ }++data ExtraDefs+ = ExtraDefs+ { tyCons :: LookedUpTyCons }++lookupExtraDefs :: TcPluginM Init ExtraDefs+lookupExtraDefs = do+ tcs <- lookupTyCons+ return $+ ExtraDefs+ { tyCons = tcs }++decideEqualSOP+ :: Opts+ -> ExtraDefs+ -- ^ 1. Givens that is already generated.+ -- We have to generate new givens at most once;+ -- otherwise GHC will loop indefinitely.+ --+ --+ -- 2. For GHc 9.2: TyCon of Data.Type.Ord.OrdCond+ -- For older: TyCon of GHC.TypeLits.<=?+ -> [Ct]+ -> [Ct]+ -> TcPluginM Solve TcPluginSolveResult+-- Simplification phase: Derives /simplified/ givens;+-- we can reduce given constraints like @Show (Foo (n + 2))@+-- to its normal form @Show (Foo (2 + n))@, which is eventually+-- useful in solving phase.+--+-- This helps us to solve /indirect/ constraints;+-- without this phase, we cannot derive, e.g.,+-- @IsVector UVector (Fin (n + 1))@ from+-- @Unbox (1 + n)@!+decideEqualSOP opts (ExtraDefs { tyCons = tcs }) givens [] =+ do+ let+ givensTyConSubst = mkTyConSubst givens+ (redGivens, _) <- reduceGivens False opts tcs givens++ tcPluginTrace "decideEqualSOP Givens {" $+ vcat [ text "givens:" <+> ppr givens ]++ -- Try to find contradictory Givens, to improve pattern match warnings.+ SimplifyResult { simplifiedWanteds, contradictions, newGivens } <-+ simplifyNats opts tcs [] $+ concatMap (toNatEquality opts tcs givensTyConSubst) redGivens++ -- Only add new Givens that are genuinely new, i.e. that GHC doesn't+ -- already know.+ --+ -- For example, in #116 we had: [G] m ~ n, [G] n ~ 0. Recalling that+ -- the inert set in GHC is a /not necessarily idempotent/ terminating+ -- generalised substitution (see Note [The KickOut Criteria] in GHC.Tc.Solver.InertSet),+ -- we don't want to emit a new Given [G] m ~ 0: GHC already knows this, and+ -- if we repeatedly emit this Given we will cause a typechecker loop (as in #116).+ let+ isSolvedGiven subst ct =+ case classifyPredType $ substTy subst (ctPred ct) of+ EqPred _rel t1 t2 -> t1 `eqType` t2+ _ -> False+ tyEqLit ct =+ case classifyPredType (ctPred ct) of+ EqPred NomEq t1 t2 -> isTyVarTy t1 && isJust (isNumLitTy t2)+ _ -> False+ givensSubst = ctsSubst givens -- Computes the idempotent substitution from the Givens+ actuallyNewGivens =+ filter+ (\ ct ->+ tyEqLit ct+ -- For now, only admit improved Givens in the form of `n ~ L`,+ -- where `n` is a type variable and `L` is a numeric literal.+ &&+ not (isSolvedGiven givensSubst ct)+ -- Ensure this Given is genuinely new information to GHC, to+ -- avoid repeatedly emitting facts that GHC already knows,+ -- which can cause the typechecker to loop (#116).+ )+ newGivens++ tcPluginTrace "decideEqualSOP Givens }" $+ vcat [ text "givens:" <+> ppr givens+ , text "simpls:" <+> ppr simplifiedWanteds+ , text "contra:" <+> ppr contradictions+ , text "new:" <+> ppr actuallyNewGivens+ ]+ return $+ mkTcPluginSolveResult+#if MIN_VERSION_ghc(9,14,0)+ ( map fromNatEquality contradictions )+#else+ []+#endif+ [] -- no solved Givens+ actuallyNewGivens++-- Solving phase.+-- Solves in/equalities on Nats and simplifiable constraints+-- containing naturals.+decideEqualSOP opts (ExtraDefs { tyCons = tcs }) givens wanteds0 = do+ deriveds <- askDeriveds+ let wanteds = if null wanteds0+ then []+ else wanteds0 ++ deriveds+ givensTyConSubst = mkTyConSubst givens+ unit_wanteds0 = concatMap (toNatEquality opts tcs givensTyConSubst) wanteds+ nonEqs = filter ( not+ . (\p -> isEqPred p || isEqClassPred p)+ . ctEvPred+ . ctEvidence )+ wanteds++ (redGivens, negWanteds) <- reduceGivens True opts tcs givens+ reducible_wanteds+ <- catMaybes <$> mapM (\ct -> fmap (ct,) <$>+ reduceNatConstr redGivens ct)+ nonEqs++ tcPluginTrace "decideEqualSOP Wanteds {" $+ vcat [ text "givens:" <+> ppr givens+ , text "new reduced givens:" <+> ppr redGivens+ , text $ replicate 80 '-'+ , text "wanteds:" <+> ppr wanteds+ , text "unit_wanteds:" <+> ppr unit_wanteds0+ , text "reducible_wanteds:" <+> ppr reducible_wanteds+ ]+ if null unit_wanteds0 && null reducible_wanteds+ then return $ TcPluginOk [] []+ else do+ -- Since reducible Wanteds also can have some negation/subtraction+ -- subterms, we have to make sure appropriate inequalities to hold.+ -- Here, we generate such additional inequalities for reduction+ -- that is to be added to new [W]anteds.+ let mkNegWanted ( CType wtdPred ) loc = mkNonCanonical <$> newWanted loc wtdPred+ ineqForRedWants <- Map.traverseWithKey mkNegWanted negWanteds+ let unit_givens = concatMap (toNatEquality opts tcs givensTyConSubst) redGivens+ unit_wanteds = unit_wanteds0 ++ concatMap (toNatEquality opts tcs givensTyConSubst) ineqForRedWants+ sr@SimplifyResult{simplifiedWanteds, contradictions} <-+ simplifyNats opts tcs unit_givens unit_wanteds+ tcPluginTrace "normalised" (ppr sr)+ reds <- for reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do+ wants <- evSubtPreds (ctLoc origCt) $ subToPred opts tcs ws+ return ((term, origCt), wDicts ++ wants)+ let -- Only solve a Derived when there are Wanteds in play+ simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) simplifiedWanteds ++ reds of+ [] -> []+ _ -> simplifiedWanteds+ (solved,newWanteds) = second concat (unzip $ simpld1 ++ reds)++ tcPluginTrace "decideEqualSOP Wanteds }" $+ vcat [ text "givens:" <+> ppr givens+ , text "new reduced givens:" <+> ppr redGivens+ , text "unit givens:" <+> ppr unit_givens+ , text $ replicate 80 '-'+ , text "wanteds:" <+> ppr wanteds+ , text "ineqForRedWants:" <+> ppr ineqForRedWants+ , text "unit_wanteds:" <+> ppr unit_wanteds+ , text "reducible_wanteds:" <+> ppr reducible_wanteds+ , text $ replicate 80 '='+ , text "solved:" <+> ppr solved+ , text "newWanteds:" <+> ppr newWanteds+ ]+ return $+ mkTcPluginSolveResult+ (map fromNatEquality contradictions)+ solved+ newWanteds++type NatEquality = (Ct,CoreSOP,CoreSOP)+type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))++reduceGivens :: Bool -- ^ allow generating new "non-negative" Wanteds+ -> Opts -> LookedUpTyCons+ -> [Ct]+ -> TcPluginM Solve ([Ct], Map CType CtLoc)+reduceGivens gen_wanteds opts tcs origGivens = go [] Map.empty origGivens+ where+ go rev_acc_gs acc_ws [] = return ( reverse rev_acc_gs, acc_ws )+ go rev_acc_gs acc_ws (g:gs) =+ case tryReduceGiven opts tcs origGivens g of+ Just ( pred', evExpr, ws )+ | gen_wanteds || null ws || negNumbers opts+ -> do+ let loc = ctLoc g+ g' <- mkNonCanonical <$> newGiven loc pred' evExpr+ let !acc' = foldl' (insertWanted loc) acc_ws ws+ go ( g' : rev_acc_gs ) acc' gs+ _ ->+ go ( g : rev_acc_gs ) acc_ws gs++ insertWanted :: CtLoc -> Map CType CtLoc -> Type -> Map CType CtLoc+ insertWanted loc acc w =+ Map.insertWith (\ _new old -> old) (CType w) loc acc++tryReduceGiven+ :: Opts -> LookedUpTyCons+ -> [Ct] -> Ct+ -> Maybe (PredType, EvTerm, [PredType])+tryReduceGiven opts tcs simplGivens ct = do+ let (mans, ws) =+ runWriter $ normaliseNatEverywhere $+ ctEvPred $ ctEvidence ct+ ws' = [ p+ | p <- subToPred opts tcs ws+ , all (not . (`eqType` p) . ctEvPred . ctEvidence) simplGivens+ ]+ -- deps = unitDVarSet (ctEvId ct)+ (pred', deps) <- mans+ case classifyPredType pred' of+ EqPred _ l r+ | l `eqType` r+ -> Nothing+ _ -> return (pred', toReducedDict (ctEvidence ct) pred' deps, ws')++fromNatEquality :: Either NatEquality NatInEquality -> Ct+fromNatEquality (Left (ct, _, _)) = ct+fromNatEquality (Right (ct, _)) = ct++reduceNatConstr :: [Ct] -> Ct -> TcPluginM Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))+reduceNatConstr givens ct = do+ let pred0 = ctEvPred $ ctEvidence ct+ (mans, tests) = runWriter $ normaliseNatEverywhere pred0++ -- Even if we didn't rewrite the Wanted,+ -- we may still be able to solve it from a (rewritten) Given.+ (pred', deps') = fromMaybe (pred0, []) mans+ case find ((`eqType` pred') . ctEvPred . ctEvidence) givens of+ -- No existing evidence found+ Nothing+ | ClassPred cls _ <- classifyPredType pred'+ , className cls /= knownNatClassName++ -- We actually did do some rewriting/normalisation.+ , Just {} <- mans+ -> do+ -- Create new evidence binding for normalized class constraint+ wtdDictCt <- mkNonCanonical <$> newWanted (ctLoc ct) pred'+ -- Evidence for current wanted is simply the coerced binding for+ -- the new binding+ let evCo = mkPluginUnivCo "ghc-typelits-natnormalise"+ Representational+ deps'+ pred' pred0+ ev = evCast (evId $ ctEvId wtdDictCt) evCo+ -- Use newly created coerced wanted as evidence, and emit the+ -- normalized wanted as a new constraint to solve.+ return (Just (EvExpr ev, tests, [wtdDictCt]))+ | otherwise+ -> return Nothing+ -- Use existing evidence+ Just c -> return (Just (toReducedDict (ctEvidence c) pred0 deps', tests, []))++toReducedDict :: CtEvidence -> PredType -> [Coercion] -> EvTerm+toReducedDict ct pred' deps' =+ let pred0 = ctEvPred ct+ evCo = mkPluginUnivCo "ghc-typelits-natnormalise"+ Representational+ deps'+ pred0 pred'+ ev = evCast (ctEvExpr ct) evCo+ in EvExpr ev++data SimplifyResult+ = SimplifyResult+ { simplifiedWanteds :: [((EvTerm,Ct),[Ct])]+ -- ^ List of:+ -- * Tuple of:+ -- * Evidence for:+ -- * The solved Wanted+ -- * Preconditions (in the for of new Wanteds)+ , contradictions :: [Either NatEquality NatInEquality]+ -- ^ List of contradictions+ , newGivens :: [Ct]+ -- ^ Givens derived in the improve givens stage+ }++instance Outputable SimplifyResult where+ ppr (SimplifyResult { simplifiedWanteds, contradictions, newGivens }) =+ text "SimplifyResult { simplified =" <+> ppr simplifiedWanteds+ <+> text ", impossible =" <+> ppr contradictions+ <+> text ", new_givens =" <+> ppr newGivens <+> text "}"++data NatCt+ = NatCt+ { predicate :: Either NatEquality NatInEquality+ -- ^ Predicate: either an equality or inequality+ , preconds :: [PredType]+ -- ^ Preconditions (in the form of inequalities encoded as PredTypes)+ , ctDeps :: [Coercion]+ -- ^ Coercion(s) from which the predicate is derived, needed so that evidence+ -- doesn't float above the coercions from which it is derived.+ }++instance Outputable NatCt where+ ppr (NatCt {predicate, preconds, ctDeps}) =+ text "NatCt { predicate = " <+> ppr predicate+ <+> text ", preconditions = " <+> ppr preconds+ <+> text ", dependencies = " <+> ppr ctDeps <+> text "}"++data SimplifyState+ = SimplifyState+ { stDeps :: [Coercion]+ -- ^ Coercions on which the simplified evidence depends, this needs to be+ -- kept around because sometimes we solving one constraint (which has a+ -- depedency) is used to solve another constraint+ , subst :: [CoreUnify]+ -- ^ Derived simplifications (i.e. b ~ c derived from (a + b) ~ (a + c)),+ -- and substitutions (i.e. n := 0 derived from y ^ n ~ 1)+ , evs :: [((EvTerm,Ct),[Ct])]+ -- ^ Collected evidence+ , leqsG :: [(CoreSOP,CoreSOP,Bool)]+ -- ^ Given inequalities+ , unsolved :: [NatCt]+ -- ^ Tried, but unsolved predicates. We keep them around in case we solve a+ -- new predicate which could lead to a substitution that enables a solve.+ , derivedGivens :: [Ct]+ -- ^ Unifiers derived from Givens. E.g. when we have /[G] x ^ n ~ 1/, this+ -- field will hold a derived /[G] n ~ 0/.+ }++emptySimplifyState :: SimplifyState+emptySimplifyState+ = SimplifyState+ { stDeps = []+ , subst = []+ , evs = []+ , leqsG = []+ , unsolved = []+ , derivedGivens = []+ }++simplifyNats+ :: Opts+ -- ^ Allow negated numbers (potentially unsound!)+ -> LookedUpTyCons+ -> [NatCt]+ -- ^ Given constraints+ -> [NatCt]+ -- ^ Wanted constraints+ -> TcPluginM Solve SimplifyResult+simplifyNats Opts{depth} tcs eqsG eqsW = do+ let eqsG1 = map (\nCt -> nCt{preconds = []}) eqsG+ (varEqs, otherEqs) = partition (isVarEqs . predicate) eqsG1+ fancyGivens = concatMap (makeGivensSet otherEqs) varEqs+ case varEqs of+ [] -> do+ let eqs = otherEqs ++ eqsW+ tcPluginTrace "simplifyNats" (ppr eqs)+ evalStateT (simples eqs) emptySimplifyState+ _ -> do+ tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")")+ (ppr varEqs)++ allSimplified <- for fancyGivens $ \v -> do+ let eqs = v ++ eqsW+ tcPluginTrace "simplifyNats" (ppr eqs)+ evalStateT (simples eqs) emptySimplifyState++ pure (foldr findFirstSimpliedWanted (SimplifyResult [] [] []) allSimplified)+ where+ simples ::+ [NatCt] ->+ StateT SimplifyState (TcPluginM Solve) SimplifyResult+ simples [] = do+ SimplifyState{evs, derivedGivens} <- get+ return SimplifyResult { simplifiedWanteds = evs+ , contradictions = []+ , newGivens = derivedGivens+ }+ simples (eq@NatCt{predicate=(Left (ct,u,v)), preconds, ctDeps}:eqs) = do+ SimplifyState{stDeps, subst, evs, leqsG, unsolved, derivedGivens} <- get+ let allDeps = stDeps ++ ctDeps++ let u' = substsSOP subst u+ v' = substsSOP subst v+ ur <- lift (unifyNats ct u' v')+ lift (tcPluginTrace "unifyNats result" (ppr ur))+ case ur of+ Win -> do+ -- Do note record "new" evidence for given constraints.+ unless (isGiven (ctEvidence ct)) $ do+ -- Only recorde evidence for wanted contstraints+ evM <- lift (evMagic tcs ct allDeps mempty preconds)+ lift $ tcPluginTrace "unifyNats Win" $+ vcat [ text "evM:" <+> ppr evM+ , text "ct:" <+> ppr ct+ ]+ modify (\s -> s {evs = maybe evs (:evs) evM})+ simples eqs+ Lose ->+ addContra (predicate eq) <$> simples eqs+ Draw [] -> do+ -- No progress made, add it to the "unsolved" list, in the hope we+ -- can make progress when we later find a new substitution+ modify (\s -> s {unsolved = eq:unsolved})+ simples eqs+ Draw unifications -> do -- We made some progress in the form of a unifier++ -- As the derived unifiers we record here can lead to solving another+ -- equation, we add it and its dependencies to the list of global+ -- dependencies which we use when creating new evidence+ let stDeps1 = ctEvCoercion (ctEvidence ct):allDeps+ -- We add apply the derived unification in the existing set of+ -- unification, and also add the derived unificaiton to the global+ -- state; to be used in solving later equations.+ let subst1 = substsSubst unifications subst ++ unifications+ if isGiven (ctEvidence ct) then do+ if null preconds then do+ -- We only record the unification derived from a given constraint+ -- when it has no preconditions in order for this unification to+ -- hold. The reason for that is that we can currently not record+ -- new Wanteds to be emitted at the end of the solve.+ givensU <- lift (mapM (unifyItemToGiven (ctLoc ct) allDeps) unifications)+ modify (\s -> s { stDeps = stDeps1+ , subst = subst1+ , leqsG = eqToLeq u' v' ++ leqsG+ , unsolved = []+ , derivedGivens = givensU ++ derivedGivens+ })+ simples (unsolved ++ eqs)+ else+ simples eqs+ else do+ let allPreconds = map unifyItemToPredType unifications ++ preconds+ evM <- lift (evMagic tcs ct allDeps Set.empty allPreconds)+ case evM of+ Nothing ->+ simples eqs+ Just ev -> do+ -- We only record the unification derived from a wanted constraint+ -- when we can actually record evidence for a succesful solve.+ modify (\s -> s { stDeps = stDeps1+ , subst = subst1+ , evs = ev:evs+ , unsolved = []+ })+ simples (unsolved ++ eqs)++ simples (eq@NatCt{predicate=Right (ct,u@(x,y,b)), preconds, ctDeps}:eqs) = do+ SimplifyState{stDeps, subst, evs, leqsG, unsolved} <- get+ let u' = substsSOP subst (subtractIneq u)+ x' = substsSOP subst x+ y' = substsSOP subst y+ uS = (x',y',b)+ leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG+ | otherwise = leqsG+ ineqs = concat [ leqsG+ , map (substLeq subst) leqsG+ , map snd (rights (map predicate eqsG))+ ]+ allDeps = stDeps ++ ctDeps+ lift (tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs)))+ case runWriterT (isNatural u') of+ Just (True,knW) -> do+ evs' <- maybe evs (:evs) <$> lift (evMagic tcs ct allDeps knW preconds)+ modify (\s -> s {evs = evs', leqsG = leqsG'})+ simples eqs++ Just (False,_) | null preconds ->+ addContra (predicate eq) <$> simples eqs+ _ -> do+ let solvedIneq = mapMaybe runWriterT+ -- it is an inequality that can be instantly solved, such as+ -- `1 <= x^y`+ -- OR+ (instantSolveIneq depth u:+ instantSolveIneq depth uS:+ -- This inequality is either a given constraint, or it is a wanted+ -- constraint, which in normal form is equal to another given+ -- constraint, hence it can be solved.+ -- OR+ map (solveIneq depth u) ineqs +++ -- The above, but with valid substitutions applied to the wanted.+ map (solveIneq depth uS) ineqs)+ smallest = solvedInEqSmallestConstraint solvedIneq+ case smallest of+ (True,kW) -> do+ evs' <- maybe evs (:evs) <$> lift (evMagic tcs ct allDeps kW preconds)+ modify (\s -> s { stDeps = allDeps+ , evs = evs'+ , leqsG = leqsG'+ })+ simples eqs+ _ -> do+ modify (\s -> s {unsolved = eq:unsolved})+ simples eqs++ eqToLeq x y = [(x,y,True),(y,x,True)]+ substLeq s (x,y,b) = (substsSOP s x, substsSOP s y, b)++ isVarEqs (Left (_,S [P [V _]], S [P [V _]])) = True+ isVarEqs _ = False++ makeGivensSet :: [NatCt] -> NatCt -> [[NatCt]]+ makeGivensSet otherEqs varEq+ = let (noMentionsV,mentionsV) = partitionEithers+ (map (matchesVarEq varEq) otherEqs)+ (mentionsLHS,mentionsRHS) = partitionEithers mentionsV+ vS = varEq {predicate = swapVar (predicate varEq)}+ givensLHS = case mentionsLHS of+ [] -> []+ _ -> [mentionsLHS ++ ((varEq:mentionsRHS) ++ noMentionsV)]+ givensRHS = case mentionsRHS of+ [] -> []+ _ -> [mentionsRHS ++ (vS:mentionsLHS ++ noMentionsV)]+ in case mentionsV of+ [] -> [noMentionsV]+ _ -> givensLHS ++ givensRHS++ matchesVarEq :: NatCt+ -> NatCt+ -> Either NatCt (Either NatCt NatCt)+ matchesVarEq NatCt{predicate = Left (_, S [P [V v1]], S [P [V v2]])} r@(NatCt e _ _) =+ case e of+ Left (_,S [P [V v3]],_)+ | v1 == v3 -> Right (Left r)+ | v2 == v3 -> Right (Right r)+ Left (_,_,S [P [V v3]])+ | v1 == v3 -> Right (Left r)+ | v2 == v3 -> Right (Right r)+ Right (_,(S [P [V v3]],_,_))+ | v1 == v3 -> Right (Left r)+ | v2 == v3 -> Right (Right r)+ Right (_,(_,S [P [V v3]],_))+ | v1 == v3 -> Right (Left r)+ | v2 == v3 -> Right (Right r)+ _ -> Left r+ matchesVarEq _ _ = error "internal error"++ swapVar (Left (ct,S [P [V v1]], S [P [V v2]])) =+ Left (ct,S [P [V v2]], S [P [V v1]])+ swapVar _ = error "internal error"++ findFirstSimpliedWanted s1@(SimplifyResult {simplifiedWanteds, contradictions}) s2+ | not (null contradictions)+ || any (isWanted . ctEvidence . snd . fst) simplifiedWanteds+ = s1+ | otherwise+ = s2++addContra :: Either NatEquality NatInEquality -> SimplifyResult -> SimplifyResult+addContra contra sr = sr { contradictions = contra : contradictions sr }++-- If we allow negated numbers we simply do not emit the inequalities+-- derived from the subtractions that are converted to additions with a+-- negated operand+subToPred :: Opts -> LookedUpTyCons -> [(Type, Type)] -> [PredType]+subToPred Opts{..} tcs+ | negNumbers = const []+ | otherwise =+ -- Given 'a - b', require 'b <= a'.+ map (\ (a, b) -> mkLEqNat tcs b a)++-- | Extract all Nat equality and inequality constraints from another constraint.+toNatEquality :: Opts -> LookedUpTyCons -> TyConSubst -> Ct -> [NatCt]+toNatEquality opts tcs givensTyConSubst ct0+ | Just (((x,y), mbLTE), cos0) <- isNatRel tcs givensTyConSubst pred0+ , let+ ((x', cos1),k1) = runWriter (normaliseNat x)+ ((y', cos2),k2) = runWriter (normaliseNat y)+ preds = subToPred opts tcs (k1 ++ k2)+ = case mbLTE of+ Nothing ->+ -- Equality constraint: x ~ y+ [NatCt (Left (ct0, x', y')) preds (cos0 ++ cos1 ++ cos2)]+ Just b ->+ -- Inequality constraint: (x <=? y) ~ b+ [NatCt (Right (ct0, (x', y', b))) preds (cos0 ++ cos1 ++ cos2)]+ | otherwise+ = case classifyPredType pred0 of+ EqPred NomEq t1 t2+ -> goNomEq t1 t2+ ClassPred kn [x]+ -- From [G] KnownNat blah, also produce [G] 0 <= blah+ -- See https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94.+ | isGiven (ctEvidence ct0)+ , className kn == knownNatClassName+ , let ((x', cos0), ks) = runWriter (normaliseNat x)+ , let preds = subToPred opts tcs ks+ -> [NatCt (Right (ct0, (S [], x', True))) preds cos0]+ _ -> []+ where+ pred0 = ctPred ct0+ -- x ~ y+ goNomEq :: Type -> Type -> [NatCt]+ goNomEq lhs rhs+ -- Recur into a TyCon application for TyCons that we **do not** rewrite,+ -- e.g. peek inside the Maybe in 'Maybe (x + y) ~ Maybe (y + x)'.+ | Just (tc , xs) <- splitTyConApp_maybe lhs+ , Just (tc', ys) <- splitTyConApp_maybe rhs+ , tc == tc'+ , not $ tc `elem` [typeNatAddTyCon, typeNatSubTyCon, typeNatMulTyCon, typeNatExpTyCon]+ , let xys = zip xs ys+ -- Make sure not to recur into non-injective positions of type families,+ -- e.g. if we know 'F n ~ F m' that doesn't mean 'n ~ m'.+ subs =+ filter (not . uncurry eqType) $+ case tyConInjectivityInfo tc of+ Injective inj ->+ filterByList (inj ++ repeat True) xys+ _ ->+ -- However, it is okay to recur in the following specific+ -- exception:+ let (tcArgs,rest) = splitAt (tyConArity tc) xys+ diffs = filter (not . uncurry eqType) tcArgs+ in case diffs of+ -- 1. The types only differ in one argument position+ [(x,y)]+ | let xFVs = tyCoVarsOfType x+ , let yFVs = tyCoVarsOfType y+ -- 2. The argument must have variables, and they must+ -- all be skolem variables.+ , not (isEmptyVarSet xFVs)+ , allVarSet isSkolemTyVar xFVs+ -- 3. The variables in both argument postions must+ -- be the same.+ , xFVs == yFVs+ -> (x,y):rest+ _ -> rest+ = case concatMap (uncurry rewrite) subs of+ [] -> []+ [rw] -> [rw]+ rws ->+ -- For Given Cts, it's fine to extract multiple (in)equalities. However,+ -- for Wanted Cts we should not claim to solve the entire Ct when we+ -- only solve a part of the Ct. So when we can extra two or more inequalities+ -- from a Wanted Ct, we conservatively choose not to solve any of them.+ if isGiven (ctEvidence ct0) then+ rws+ else+ []+ | otherwise+ = rewrite lhs rhs++ rewrite :: Type -> Type -> [NatCt]+ rewrite x y+ | isNatKind (typeKind x)+ , isNatKind (typeKind y)+ , let ((x', cos1),k1) = runWriter (normaliseNat x)+ , let ((y', cos2),k2) = runWriter (normaliseNat y)+ , let preds = subToPred opts tcs (k1 ++ k2)+ = [NatCt (Left (ct0,x',y')) preds (cos1 ++ cos2)]+ | otherwise+ = []++ isNatKind :: Kind -> Bool+ isNatKind = (`eqType` natKind)++unifyItemToPredType :: CoreUnify -> PredType+unifyItemToPredType ui = mkEqPredRole Nominal ty1 ty2+ where+ ty1 = case ui of+ SubstItem {..} -> mkTyVarTy siVar+ UnifyItem {..} -> reifySOP siLHS+ ty2 = case ui of+ SubstItem {..} -> reifySOP siSOP+ UnifyItem {..} -> reifySOP siRHS+++unifyItemToGiven :: CtLoc -> [Coercion] -> CoreUnify -> TcPluginM Solve Ct+unifyItemToGiven loc deps ui = mkNonCanonical <$> newGiven loc pty (EvExpr (Coercion co))+ where+ ty1 = case ui of+ SubstItem {..} -> mkTyVarTy siVar+ UnifyItem {..} -> reifySOP siLHS+ ty2 = case ui of+ SubstItem {..} -> reifySOP siSOP+ UnifyItem {..} -> reifySOP siRHS++ pty = mkEqPredRole Nominal ty1 ty2+ co = mkPluginUnivCo "ghc-typelits-natnormalise" Nominal deps ty1 ty2++evSubtPreds :: CtLoc -> [PredType] -> TcPluginM Solve [Ct]+evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc)++evMagic ::+ -- | Known TyCon environment+ LookedUpTyCons ->+ -- | Constraint for which we are creating evidence+ Ct ->+ -- | Coercions in which the evidence depends+ [Coercion] ->+ -- | Types that we should be known to be a Natural+ Set CType ->+ -- | Inequalities that should hold+ [PredType] ->+ TcPluginM Solve (Maybe ((EvTerm, Ct), [Ct]))+evMagic tcs ct deps knW preds = do+ holeWanteds <- evSubtPreds (ctLoc ct) preds+ knWanted <- mapM (mkKnWanted (ctLoc ct)) (Set.elems knW)+ let newWant = knWanted ++ holeWanteds+ case classifyPredType $ ctEvPred $ ctEvidence ct of+ EqPred NomEq t1 t2 ->+ let ctEv = mkPluginUnivCo "ghc-typelits-natnormalise" Nominal deps t1 t2+ in return (Just ((EvExpr (Coercion ctEv), ct),newWant))+ IrredPred p ->+ let t1 = mkTyConApp (c0TyCon tcs) []+ co = mkPluginUnivCo "ghc-typelits-natnormalise" Representational deps t1 p+ dcApp = evDataConApp (c0DataCon tcs) [] []+ in return (Just ((EvExpr $ evCast dcApp co, ct),newWant))+ _ -> return Nothing++mkKnWanted+ :: CtLoc+ -> CType+ -> TcPluginM Solve Ct+mkKnWanted loc (CType ty) = do+ kc_clas <- tcLookupClass knownNatClassName+ let kn_pred = mkClassPred kc_clas [ty]+ wantedCtEv <- newWanted loc kn_pred+ return $ mkNonCanonical wantedCtEv
+ src/GHC/TypeLits/Normalise/Compat.hs view
@@ -0,0 +1,399 @@++{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE TemplateHaskellQuotes #-}++{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}++module GHC.TypeLits.Normalise.Compat+ ( LookedUpTyCons(..), lookupTyCons+ , upToGivens+ , mkLEqNat+ , Relation, isNatRel++ , UniqMap, intersectUniqMap_C, listToUniqMap, nonDetUniqMapToList++ , mkTcPluginSolveResult++ ) where++-- base+import Control.Arrow+ ( second )+import qualified Data.List.NonEmpty as NE+ ( toList )+import Data.Foldable+ ( asum )+import GHC.TypeNats+ ( CmpNat )+#if MIN_VERSION_ghc(9,3,0)+import qualified GHC.TypeError+ ( Assert )+#endif+#if MIN_VERSION_ghc(9,1,0)+import qualified Data.Type.Ord+ ( OrdCond, type (<=) )++#else+import GHC.TypeNats+ ( type (<=), type (<=?) )+#endif++-- ghc+import GHC.Builtin.Types+ ( isCTupleTyConName+ , promotedFalseDataCon, promotedTrueDataCon+ , promotedLTDataCon, promotedEQDataCon, promotedGTDataCon+ )+#if MIN_VERSION_ghc(9,1,0)+import GHC.Builtin.Types+ ( cTupleTyCon, cTupleDataCon )+#else+import GHC.Builtin.Types+ ( cTupleTyConName )+#endif+#if MIN_VERSION_ghc(9,7,0)+import GHC.Types.Unique.Map+ ( UniqMap, intersectUniqMap_C, listToUniqMap, nonDetUniqMapToList )+#else+import GHC.Types.Unique+ ( Uniquable )+import GHC.Types.Unique.FM+ ( intersectUFM_C, nonDetEltsUFM )+#endif++-- ghc-tcplugin-api+import GHC.TcPlugin.API+import GHC.TcPlugin.API.TyConSubst+ ( TyConSubst, splitTyConApp_upTo )++--------------------------------------------------------------------------------++data LookedUpTyCons+ = LookedUpTyCons+ {+#if MIN_VERSION_ghc(9,3,0)+ assertTyCon :: TyCon,+#endif+#if MIN_VERSION_ghc(9,1,0)+ -- | @<= :: k -> k -> Constraint@+ ordCondTyCon :: TyCon,+ leqTyCon :: TyCon,+#else+ -- | @<= :: Nat -> Nat -> Constraint@+ leqNatTyCon :: TyCon,+ -- | @<=? :: Nat -> Nat -> Constraint@+ leqQNatTyCon :: TyCon,+#endif+ cmpNatTyCon :: TyCon,+ c0TyCon :: TyCon,+ c0DataCon :: DataCon+ }++lookupTyCons :: TcPluginM Init LookedUpTyCons+lookupTyCons = do+ cmpNatT <- lookupTHName ''GHC.TypeNats.CmpNat >>= tcLookupTyCon+#if MIN_VERSION_ghc(9,3,0)+ assertT <- lookupTHName ''GHC.TypeError.Assert >>= tcLookupTyCon+#endif+#if MIN_VERSION_ghc(9,1,0)+ leqT <- lookupTHName ''(Data.Type.Ord.<=) >>= tcLookupTyCon+ ordCond <- lookupTHName ''Data.Type.Ord.OrdCond >>= tcLookupTyCon+ return $+ LookedUpTyCons+ { leqTyCon = leqT+ , ordCondTyCon = ordCond+# if MIN_VERSION_ghc(9,3,0)+ , assertTyCon = assertT+# endif+ , cmpNatTyCon = cmpNatT+ , c0TyCon = cTupleTyCon 0+ , c0DataCon = cTupleDataCon 0+ }+#else+ leqT <- lookupTHName ''(GHC.TypeNats.<=) >>= tcLookupTyCon+ leqQT <- lookupTHName ''(GHC.TypeNats.<=?) >>= tcLookupTyCon+ c0T <- tcLookupTyCon (cTupleTyConName 0)+ let c0D = tyConSingleDataCon c0T+ -- somehow looking up the 0-tuple data constructor fails+ -- with interface file errors, so use tyConSingleDataCon+ return $+ LookedUpTyCons+ { leqNatTyCon = leqT+ , leqQNatTyCon = leqQT+ , c0TyCon = c0T+ , c0DataCon = c0D+ , cmpNatTyCon = cmpNatT+ }+#endif++-- | The constraint @(a <= b)@.+mkLEqNat :: LookedUpTyCons -> Type -> Type -> PredType+mkLEqNat tcs a b =+#if MIN_VERSION_ghc(9,1,0)+ mkTyConApp (leqTyCon tcs) [natKind, a, b]+#else+ mkTyConApp (leqNatTyCon tcs) [a, b]+#endif++-- | Is this type 'True' or 'False'?+boolean_maybe :: TyConSubst -> Type -> Maybe (Bool, [Coercion])+boolean_maybe givensTyConSubst =+ upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys )+ where+ go tc []+ | tc == promotedTrueDataCon+ = Just True+ | tc == promotedFalseDataCon+ = Just False+ go _ _ = Nothing++-- | Is this type 'LT', 'EQ' or 'GT'?+ordering_maybe :: TyConSubst -> Type -> Maybe (Ordering, [Coercion])+ordering_maybe givensTyConSubst =+ upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys )+ where+ go tc []+ | tc == promotedLTDataCon+ = Just LT+ | tc == promotedEQDataCon+ = Just EQ+ | tc == promotedGTDataCon+ = Just GT+ go _ _ = Nothing++#if MIN_VERSION_ghc(9,1,0)+cmpNat_maybe :: LookedUpTyCons -> TyConSubst -> Type -> Maybe ((Type, Type), [Coercion])+cmpNat_maybe tcs givensTyConSubst =+ upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys )+ where+ go tc [x,y]+ | tc == cmpNatTyCon tcs+ = Just (x,y)+ go _ _ = Nothing+#endif++-- | Is this type @() :: Constraint@?+unitCTuple_maybe :: TyConSubst -> PredType -> Maybe ((), [Coercion])+unitCTuple_maybe givensTyConSubst =+ upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys )+ where+ go tc []+ | isCTupleTyConName (tyConName tc)+ = Just ()+ go _ _ = Nothing++-- | A relation between two natural numbers, @((x,y), mbRel)@.+--+-- The @mbRel@ value indicates the kind of relation:+--+-- - @Nothing@ <=> @x ~ y@,+-- - @Just b@ <=> @(x <=? y) ~ b@.+type Relation = ((Type, Type), Maybe Bool)++{- Note [Recognising Nat inequalities]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Recognising whether a type is an inequality between two natural numbers is+not as straightforward as one might initially think. The problem is that there+are many different built-in types that can be used to represent an equality of+natural numbers:++ 1. GHC.TypeNats.CmpNat, returning Ordering.+ This type family is primitive (on all GHC versions).+ 2. GHC.TypeNats.<=?, returning a Boolean.+ This type family is primitive prior to GHC 9.1, but is defined in+ terms of the 'OrdCond' type family starting in GHC 9.1.++ (NB: it also becomes poly-kinded starting in GHC 9.1.)+ 3. GHC.TypeNats.<=, which is defined:+ (a) as @x <= y@ <=> @(x <=? y) ~ True@ in GHC prior to 9.3.+ (b) as @Assert (x <=? y) ...@ in GHC 9.3 and above.++To catch all of these, we must thus handle all of the following type families:++ Case 1. CmpNat.+ Case 2. (<=?) in GHC 9.1 and prior.+ Case 3. OrdCond in GHC 9.1 and later.+ Case 4. Assert, in GHC 9.3 and later.++These are all the built-in type families defined in GHC used to express+inequalities between natural numbers.+-}++-- | Is this an equality or inequality between two natural numbers?+--+-- See Note [Recognising Nat inequalities].+isNatRel :: LookedUpTyCons -> TyConSubst -> PredType -> Maybe (Relation, [Coercion])+isNatRel tcs givensTyConSubst ty0+ | EqPred NomEq x y <- classifyPredType ty0+ = if+ -- (expr1 :: Nat) ~ (expr2 :: Nat)+ | all ( ( `eqType` natKind ) . typeKind ) [ x, y ]+ -> Just $ ( ( ( x, y ), Nothing ), [] )+ -- (b :: Bool) ~ y+ | Just ( b, cos1 ) <- boolean_maybe givensTyConSubst x+ -> second ( ++ cos1 ) <$> booleanRel b y+ -- x ~ (b :: Bool)+ | Just ( b, cos1 ) <- boolean_maybe givensTyConSubst y+ -> second ( ++ cos1 ) <$> booleanRel b x+ | Just ( o, cos1 ) <- ordering_maybe givensTyConSubst x+ -- (o :: Ordering) ~ y+ -> second ( ++ cos1 ) <$> orderingRel o y+ | Just ( o, cos1 ) <- ordering_maybe givensTyConSubst y+ -- x ~ (o :: Ordering)+ -> second ( ++ cos1 ) <$> orderingRel o x+ -- (() :: Constraint) ~ y+ | Just ( (), cos1 ) <- unitCTuple_maybe givensTyConSubst x+ -> second ( ++ cos1 ) <$> goTy y+ -- x ~ (() :: Constraint)+ | Just ( (), cos1 ) <- unitCTuple_maybe givensTyConSubst y+ -> second ( ++ cos1 ) <$> goTy x+ | otherwise+ -> Nothing+ | otherwise+ = goTy ty0+ where+ goTy :: PredType -> Maybe (Relation, [Coercion])+ goTy = upToGivens givensTyConSubst goTc++ goTc :: TyCon -> [Type] -> Maybe (Relation, [Coercion])+ goTc _tc _tys+#if MIN_VERSION_ghc(9,3,0)+ -- Look through 'Assert'.+ -- Case 4 in Note [Recognising Nat inequalities]+ | _tc == assertTyCon tcs+ , [ty, _] <- _tys+ = booleanRel True ty+#endif+ | otherwise+ = Nothing++ -- Recognise whether @(b :: Bool) ~ ty@ is an equality/inequality+ booleanRel :: Bool -> Type -> Maybe (Relation, [Coercion])+ booleanRel b = upToGivens givensTyConSubst (goBoolean b)++ goBoolean :: Bool -> TyCon -> [Type] -> Maybe (Relation, [Coercion])+ goBoolean b tc tys+#if MIN_VERSION_ghc(9,1,0)+ -- OrdCond (CmpNat x y) lt eq gt ~ b+ -- Case 3 in Note [Recognising Nat inequalities]+ | tc == ordCondTyCon tcs+ , [_,cmp,ltTy,eqTy,gtTy] <- tys+ , Just (lt, cos1) <- boolean_maybe givensTyConSubst ltTy+ , Just (eq, cos2) <- boolean_maybe givensTyConSubst eqTy+ , Just (gt, cos3) <- boolean_maybe givensTyConSubst gtTy+ , Just ((x,y), cos4) <- cmpNat_maybe tcs givensTyConSubst cmp+ = ( , cos1 ++ cos2 ++ cos3 ++ cos4 ) <$>+ if -- (x <= y) ~ b+ | lt && eq && not gt+ -> Just ((x,y), Just b)+ -- (x < y) ~ b+ -- <=>+ -- (y <= x) ~ not b+ | lt && not eq && not gt+ -> Just ((y,x), Just $ not b)+ -- (x >= y) ~ b+ -- <=>+ -- (y <= x) ~ b+ | not lt && eq && gt+ -> Just ((y,x), Just b)+ -- (x > y) ~ b+ -- <=>+ -- (x <= y) ~ not b+ | not lt && not eq && gt+ -> Just ((x,y), Just $ not b)+ -- x ~ y+ | ( b && not lt && eq && not gt )+ || ( not b && lt && not eq && gt )+ -> Just ((x,y), Nothing)+ | otherwise+ -> Nothing+#else+ -- (x <=? y) ~ b+ -- Case 2 in Note [Recognising Nat inequalities]+ | tc == leqQNatTyCon tcs+ , [x,y] <- tys+ = Just (((x,y), Just b), [])+#endif+ | otherwise+ = Nothing++ -- Recognise whether @(o :: Ordering) ~ ty@ is an equality/inequality+ orderingRel :: Ordering -> Type -> Maybe (Relation, [Coercion])+ orderingRel o = upToGivens givensTyConSubst (goOrdering o)++ goOrdering :: Ordering -> TyCon -> [Type] -> Maybe (Relation, [Coercion])+ goOrdering o tc tys+ -- CmpNat x y ~ o+ -- Case 1 in Note [Recognising Nat inequalities]+ | tc == cmpNatTyCon tcs+ , [x,y] <- tys+ = ( , [] ) <$>+ case o of+ EQ ->+ -- x ~ y+ Just ((x,y), Nothing)+ LT ->+ -- x < y <=> (y <= x) ~ False+ Just ((y,x), Just False)+ GT ->+ -- x > y <=> (x <= y) ~ False+ Just ((x,y), Just False)+ | otherwise+ = Nothing++upToGivens :: TyConSubst -> (TyCon -> [Type] -> Maybe (a, [Coercion])) -> Type -> Maybe (a, [Coercion])+upToGivens givensTyConSubst f ty =+ asum $ map ( \ (tc, tys, deps) -> second ( deps ++ ) <$> f tc tys ) $+ maybe [] NE.toList $ splitTyConApp_upTo givensTyConSubst ty++--------------------------------------------------------------------------------++#if !MIN_VERSION_ghc(9,7,0)++newtype UniqMap k a = UniqMap ( UniqFM k (k, a) )+ deriving (Eq, Functor)+type role UniqMap nominal representational++intersectUniqMap_C :: (a -> b -> c) -> UniqMap k a -> UniqMap k b -> UniqMap k c+intersectUniqMap_C f (UniqMap m1) (UniqMap m2) = UniqMap $ intersectUFM_C (\(k, a) (_, b) -> (k, f a b)) m1 m2+{-# INLINE intersectUniqMap_C #-}++listToUniqMap :: Uniquable k => [(k,a)] -> UniqMap k a+listToUniqMap kvs = UniqMap (listToUFM [ (k,(k,v)) | (k,v) <- kvs])+{-# INLINE listToUniqMap #-}++nonDetUniqMapToList :: UniqMap k a -> [(k, a)]+nonDetUniqMapToList (UniqMap m) = nonDetEltsUFM m+{-# INLINE nonDetUniqMapToList #-}++#endif++--------------------------------------------------------------------------------++mkTcPluginSolveResult :: [Ct] -> [(EvTerm, Ct)] -> [Ct]+ -> TcPluginSolveResult+#if MIN_VERSION_ghc(9,3,0)+mkTcPluginSolveResult = TcPluginSolveResult+#else+mkTcPluginSolveResult contras solved new =+ -- On GHC 9.2 and below, it's not possible to return+ -- both contradictions and solved/new constraints.+ --+ -- In general, we prefer returning solved constraints over contradictions.+ if null solved && not (null contras)+ then TcPluginContradiction contras+ else TcPluginOk solved new+#endif++--------------------------------------------------------------------------------
src/GHC/TypeLits/Normalise/SOP.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE LambdaCase #-} {-| Copyright : (C) 2015-2016, University of Twente, 2017 , QBayLogic B.V.@@ -74,8 +75,6 @@ @ -} -{-# LANGUAGE CPP #-}- module GHC.TypeLits.Normalise.SOP ( -- * SOP types Symbol (..)@@ -92,17 +91,18 @@ ) where --- External-import Data.Either (partitionEithers)-import Data.List (sort)+-- base+import Data.Either+ ( partitionEithers )+import Data.List+ ( sort ) --- GHC API-#if MIN_VERSION_ghc(9,0,0)-import GHC.Utils.Outputable (Outputable (..), (<+>), text, hcat, integer, punctuate)-#else-import Outputable (Outputable (..), (<+>), text, hcat, integer, punctuate)-#endif+-- 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@@ -128,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@@ -160,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)]))@@ -189,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@@ -245,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))@@ -272,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 @@ -296,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@@ -311,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@@ -329,12 +331,12 @@ {-# INLINEABLE simplifySOP #-} -- | Merge two SOP terms by additions-mergeSOPAdd :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c+mergeSOPAdd :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c mergeSOPAdd (S sop1) (S sop2) = simplifySOP $ S (sop1 ++ sop2) {-# INLINEABLE mergeSOPAdd #-} -- | Merge two SOP terms by multiplication-mergeSOPMul :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c+mergeSOPMul :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c mergeSOPMul (S sop1) (S sop2) = simplifySOP . S
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -5,15 +5,14 @@ Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> -} -{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE TupleSections #-} -{-# OPTIONS_GHC -fno-warn-unused-imports #-}-#if __GLASGOW_HASKELL__ < 801-#define nonDetCmpType cmpType-#endif+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-} module GHC.TypeLits.Normalise.Unify ( -- * 'Nat' expressions \<-\> 'SOP' terms@@ -38,90 +37,60 @@ , subtractIneq , solveIneq , ineqToSubst- , subtractionToPred , instantSolveIneq , solvedInEqSmallestConstraint+ , negateProd -- * Properties , isNatural ) where --- External-import Control.Arrow (first, second)-import Control.Monad.Trans.Writer.Strict-import Data.Function (on)-import Data.List ((\\), intersect, nub)-import Data.Maybe (fromMaybe, mapMaybe, isJust)-import Data.Set (Set)-import qualified Data.Set as Set+-- 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-#if MIN_VERSION_ghc(9,0,0)-import GHC.Builtin.Types (boolTy, promotedTrueDataCon)+-- ghc import GHC.Builtin.Types.Literals- (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)-#if MIN_VERSION_ghc(9,2,0)-import GHC.Builtin.Types (naturalTy, promotedFalseDataCon)-import GHC.Builtin.Types.Literals (typeNatCmpTyCon)-#else-import GHC.Builtin.Types (typeNatKind)-import GHC.Builtin.Types.Literals (typeNatLeqTyCon)-#endif-import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType, mkPrimEqPred)-import GHC.Core.TyCon (TyCon)-#if MIN_VERSION_ghc(9,6,0)-import GHC.Core.Type- (PredType, TyVar, coreView, mkNumLitTy, mkTyConApp, mkTyVarTy, typeKind)-import GHC.Core.TyCo.Compare- (eqType, nonDetCmpType)-#else-import GHC.Core.Type- (PredType, TyVar, coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy, nonDetCmpType, typeKind)-#endif-import GHC.Core.TyCo.Rep (Kind, Type (..), TyLit (..))-import GHC.Tc.Plugin (TcPluginM, tcPluginTrace)-import GHC.Tc.Types.Constraint (Ct, ctEvidence, ctEvId, ctEvPred, isGiven)+ ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon+ ) import GHC.Types.Unique.Set- (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets, unitUniqSet)-import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)-#else-import Outputable (Outputable (..), (<+>), ($$), text)-import TcPluginM (TcPluginM, tcPluginTrace)-import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,- typeNatSubTyCon, typeNatLeqTyCon)-import TyCon (TyCon)-import Type (TyVar,- coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy,- nonDetCmpType, PredType, typeKind)-import TyCoRep (Kind, Type (..), TyLit (..))-import TysWiredIn (boolTy, promotedTrueDataCon, typeNatKind)-import UniqSet (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets,- unitUniqSet)+ ( UniqSet+ , emptyUniqSet, unionManyUniqSets, unionUniqSets, unitUniqSet+ , nonDetEltsUniqSet, elementOfUniqSet+ ) -#if MIN_VERSION_ghc(8,10,0)-import Constraint (Ct, ctEvidence, ctEvId, ctEvPred, isGiven)-import Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType, mkPrimEqPred)-#else-import TcRnMonad (Ct, ctEvidence, isGiven)-import TcRnTypes (ctEvPred)-import Type (EqRel (NomEq), PredTree (EqPred), classifyPredType, mkPrimEqPred)-#endif-#endif+-- ghc-tcplugin-api+import GHC.TcPlugin.API+import GHC.Utils.Outputable --- Internal++-- 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 ) -#if MIN_VERSION_ghc(9,2,0)-typeNatKind :: Type-typeNatKind = naturalTy-#endif+-------------------------------------------------------------------------------- newtype CType = CType { unCType :: Type } deriving Outputable@@ -137,27 +106,46 @@ 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 -> Writer [(Type,Type)] CoreSOP-normaliseNat ty | Just ty1 <- coreView ty = normaliseNat ty1-normaliseNat (TyVarTy v) = return (S [P [V v]])-normaliseNat (LitTy (NumTyLit i)) = return (S [P [I i]])-normaliseNat (TyConApp tc [x,y])- | tc == typeNatAddTyCon = mergeSOPAdd <$> normaliseNat x <*> normaliseNat y- | tc == typeNatSubTyCon = do- tell [(x,y)]- 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 = return (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') --- | Runs writer action. If the result /Nothing/ writer actions will be+knownTyCons :: [TyCon]+knownTyCons = [typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon, typeNatAddTyCon]+++-- | Runs writer action. If the result is /Nothing/, writer actions will be -- discarded. maybeRunWriter :: Monoid a@@ -171,43 +159,55 @@ -- | 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)+normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion])) normaliseNatEverywhere ty0- | TyConApp tc _fields <- ty0- , tc `elem` knownTyCons = do- -- Normalize under current type constructor application. 'go' skips all- -- known type constructors.- ty1M <- maybeRunWriter (go ty0)- let ty1 = fromMaybe ty0 ty1M+ | 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 - -- Normalize (subterm-normalized) type given to 'normaliseNatEverywhere'- ty2 <- 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 ty1M else Just ty2)- | otherwise = go ty0+ | otherwise+ = pure Nothing where- knownTyCons :: [TyCon]- knownTyCons = [typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon, typeNatAddTyCon] -- Normalize given type, but ignore all top-level- go :: Type -> Writer [(Type, Type)] (Maybe Type)- go (TyConApp tc_ fields0_) = do+ go :: TyCon -> [Type] -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))+ go tc_ fields0_ = do fields1_ <- mapM (maybeRunWriter . cont) fields0_- if any isJust fields1_ then- pure (Just (TyConApp tc_ (zipWith fromMaybe fields0_ fields1_)))+ 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 = if tc_ `elem` knownTyCons then go else normaliseNatEverywhere- go _ = pure Nothing+ cont ty'+ | tc_ `elem` knownTyCons+ , Just (tc', flds') <- splitTyConApp_maybe ty'+ = go tc' flds'+ | otherwise+ = normaliseNatEverywhere ty' -normaliseSimplifyNat :: Type -> Writer [(Type, Type)] Type+normaliseSimplifyNat :: Type -> Writer [(Type, Type)] (Type, [Coercion]) normaliseSimplifyNat ty- | typeKind ty `eqType` typeNatKind = do- ty' <- normaliseNat ty- return $ reifySOP $ simplifySOP ty'- | otherwise = return 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@@ -257,11 +257,26 @@ -- 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@@ -276,43 +291,68 @@ ,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) = (-2*y + 3*x)--- subtractIneq (2*y <=? 3*x ~ False) = (-3*x + (-1) + 2*y)+-- 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- = mergeSOPAdd y (mergeSOPMul (S [P [I (-1)]]) x)+ -- 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]]))) --- | Try to reverse the process of 'subtractIneq'------ E.g.------ @--- subtractIneq (2*y <=? 3*x ~ True) = (-2*y + 3*x)--- sopToIneq (-2*y+3*x) = Just (2*x <=? 3*x ~ True)--- @-sopToIneq- :: CoreSOP- -> Maybe Ineq-sopToIneq (S [P ((I i):l),r])- | i < 0- = Just (mergeSOPMul (S [P [I (negate i)]]) (S [P l]),S [r],True)-sopToIneq (S [r,P ((I i:l))])- | i < 0- = Just (mergeSOPMul (S [P [I (negate i)]]) (S [P l]),S [r],True)-sopToIneq _ = Nothing- -- | Give the smallest solution for an inequality ineqToSubst :: Ineq@@ -322,25 +362,6 @@ ineqToSubst _ = Nothing -subtractionToPred- :: TyCon- -> (Type,Type)- -> (PredType, Kind)-subtractionToPred ordCond (x,y) =-#if MIN_VERSION_ghc(9,2,0)- let cmpNat = mkTyConApp typeNatCmpTyCon [y,x]- trueTc = mkTyConApp promotedTrueDataCon []- falseTc = mkTyConApp promotedFalseDataCon []- ordCmp = mkTyConApp ordCond- [boolTy,cmpNat,trueTc,trueTc,falseTc]- predTy = mkPrimEqPred ordCmp trueTc- in (predTy,boolTy)-#else- (mkPrimEqPred (mkTyConApp ordCond [y,x])- (mkTyConApp promotedTrueDataCon [])- ,boolTy)-#endif- -- | 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.@@ -359,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')@@ -379,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}@@ -402,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:@@ -457,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]])@@ -500,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@@ -559,32 +584,25 @@ | 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 s1@(S ps1) s2@(S ps2) = case sopToIneq k1 of- Just (s1',s2',_)- | s1' /= s1 || s2' /= s1- , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s1'))- , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s2'))- -> unifiers' ct s1' s2'- _ | null psx- , length ps1 == length ps2- -> case nub (concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2)) of- [] -> unifiers'' ct (S ps1) (S ps2)- [k] | length ps1 == length ps2 -> [k]- _ -> []- | null psx- , isGiven (ctEvidence ct)- -> unifiers'' ct (S ps1) (S ps2)- | null psx- -> []- _ -> 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- k1 = subtractIneq (s1,s2,True) ps1' = ps1 \\ psx ps2' = ps2 \\ psx ps1'' | null ps1' = [P [I 0]]@@ -593,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@@ -619,18 +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 symbolContainsConstant . unP) . unS- where- symbolContainsConstant c = case c of- C {} -> True- E s p -> containsConstants s || containsConstants (S [p])- _ -> False- safeDiv :: Integer -> Integer -> Maybe Integer safeDiv i j | j == 0 = Just 0@@ -650,12 +730,38 @@ else Just (smallInteger z1) integerLogBase _ _ = Nothing +-- | Might this be a natural number?+--+-- Equivalently: it is not the case that this is definitely not a natural number.+--+-- 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?+--+-- - @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)])- | i >= 0 = isNatural (S [P ps])- | otherwise = return False+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@@ -678,6 +784,23 @@ -- 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@@ -797,14 +920,12 @@ -- * SOP version: -2 + x -- * Convert back to inequality: 2 <= x plusMonotone :: IneqRule-plusMonotone want have- | Just want' <- sopToIneq (subtractIneq want)- , want' /= want- = pure [(want',have)]- | Just have' <- sopToIneq (subtractIneq have)- , have' /= have- = pure [(want,have')]-plusMonotone _ _ = noRewrite+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
− tests/ErrorTests.hs
@@ -1,523 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}--#if __GLASGOW_HASKELL__ >= 805-{-# LANGUAGE NoStarIsType #-}-#endif--{-# OPTIONS_GHC -fdefer-type-errors #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}-module ErrorTests where--import Data.Proxy-import GHC.TypeLits-#if __GLASGOW_HASKELL__ >= 904-import GHC.Types-#endif--import GHC.IO.Encoding (getLocaleEncoding, textEncodingName, utf8)-import Language.Haskell.TH (litE, stringL)-import Language.Haskell.TH.Syntax (runIO)--#if __GLASGOW_HASKELL__ >= 901-import qualified Data.Type.Ord-#endif--testProxy1 :: Proxy (x + 1) -> Proxy (2 + x)-testProxy1 = id--testProxy1Errors =-#if __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--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 =-#if __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--proxyFun3 :: Proxy (x + x + x) -> ()-proxyFun3 = const ()--testProxy3 :: Proxy 8 -> ()-testProxy3 = proxyFun3--testProxy3Errors =-#if __GLASGOW_HASKELL__ >= 900- ["Expected: Proxy 8 -> ()"- ," Actual: Proxy ((x0 + x0) + x0) -> ()"- ]-#else- ["Expected type: Proxy 8 -> ()"- ,"Actual type: Proxy ((x0 + x0) + x0) -> ()"- ]-#endif--proxyFun4 :: Proxy ((2*y)+4) -> ()-proxyFun4 = const ()--testProxy4 :: Proxy 2 -> ()-testProxy4 = proxyFun4--testProxy4Errors =-#if __GLASGOW_HASKELL__ >= 900- ["Expected: Proxy 2 -> ()"- ," Actual: Proxy ((2 * y0) + 4) -> ()"- ]-#else- ["Expected type: Proxy 2 -> ()"- ,"Actual type: Proxy ((2 * y0) + 4) -> ()"- ]-#endif--testProxy5 :: Proxy 7 -> ()-testProxy5 = proxyFun4--testProxy5Errors =-#if __GLASGOW_HASKELL__ >= 900- ["Expected: Proxy 7 -> ()"- ," Actual: Proxy ((2 * y1) + 4) -> ()"- ]-#else- ["Expected type: Proxy 7 -> ()"- ,"Actual type: Proxy ((2 * y1) + 4) -> ()"- ]-#endif--proxyFun6 :: Proxy (2^k) -> Proxy (2^k)-proxyFun6 = const Proxy--testProxy6 :: Proxy 7-testProxy6 = proxyFun6 (Proxy :: Proxy 7)--testProxy6Errors =-#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--proxyFun7 :: Proxy (2^k) -> Proxy k-proxyFun7 = const Proxy--testProxy8 :: Proxy x -> Proxy (y + x)-testProxy8 = id--testProxy8Errors =-#if __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--#if __GLASGOW_HASKELL__ >= 904-proxyInEq :: ((a <= b) ~ (() :: Constraint)) => Proxy (a :: Nat) -> Proxy b -> ()-#else-proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> ()-#endif-proxyInEq _ _ = ()--proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> ()-proxyInEq' _ _ = ()--testProxy9 :: Proxy (a + 1) -> Proxy a -> ()-testProxy9 = proxyInEq--testProxy9Errors =-#if __GLASGOW_HASKELL__ >= 904- ["Cannot satisfy: a + 1 <= a"]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat (a + 1) a) 'True 'True 'False’"- else litE $ stringL "(CmpNat (a + 1) a) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'True’"- else litE $ stringL "with 'True"- )- ]-#else- [$(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"- )]-#endif--testProxy10 :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()-testProxy10 = proxyInEq'--testProxy10Errors =-#if __GLASGOW_HASKELL__ >= 910- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat a (a + 2)) True True False’"- else litE $ stringL "(CmpNat a (a + 2)) True True False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘False"- else litE $ stringL "with `False"- )- ]-#elif __GLASGOW_HASKELL__ >= 906- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat a (a + 2)) True True False’"- else litE $ stringL "(CmpNat a (a + 2)) True True False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘False"- else litE $ stringL "with False"- )- ]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat a (a + 2)) 'True 'True 'False’"- else litE $ stringL "(CmpNat a (a + 2)) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'False"- else litE $ stringL "with 'False"- )- ]-#else- [$(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"- )]-#endif--testProxy11 :: Proxy (a :: Nat) -> Proxy a -> ()-testProxy11 = proxyInEq'--testProxy11Errors =- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8-#if __GLASGOW_HASKELL__ >= 910- then litE $ stringL "Couldn't match type ‘True’ with ‘False’"- else litE $ stringL "Couldn't match type `True' with `False'"-#elif __GLASGOW_HASKELL__ >= 906- then litE $ stringL "Couldn't match type ‘True’ with ‘False’"- else litE $ stringL "Couldn't match type True with False"-#else- then litE $ stringL "Couldn't match type ‘'True’ with ‘'False’"- else litE $ stringL "Couldn't match type 'True with 'False"-#endif- )]--testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> ()-testProxy12 = proxyInEq--testProxy12Errors =-#if __GLASGOW_HASKELL__ >= 904- ["Cannot satisfy: a + b <= a + c"]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat (a + b) (a + c)) 'True 'True 'False’"- else litE $ stringL "(CmpNat (a + b) (a + c)) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'True’"- else litE $ stringL "with 'True"- )- ]-#else- [$(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"- )]-#endif--testProxy13 :: Proxy (4*a) -> Proxy (2*a) ->()-testProxy13 = proxyInEq--testProxy13Errors =-#if __GLASGOW_HASKELL__ >= 904- ["Cannot satisfy: 4 * a <= 2 * a"]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat (4 * a) (2 * a)) 'True 'True 'False’"- else litE $ stringL "(CmpNat (4 * a) (2 * a)) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'True’"- else litE $ stringL "with 'True"- )- ]-#else- [$(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"- )]-#endif--testProxy14 :: Proxy (2*a) -> Proxy (4*a) -> ()-testProxy14 = proxyInEq'--testProxy14Errors =-#if __GLASGOW_HASKELL__ >= 910- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False’"- else litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘False"- else litE $ stringL "with `False"- )- ]-#elif __GLASGOW_HASKELL__ >= 906- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False’"- else litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘False"- else litE $ stringL "with False"- )- ]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat (2 * a) (4 * a)) 'True 'True 'False’"- else litE $ stringL "(CmpNat (2 * a) (4 * a)) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'False"- else litE $ stringL "with 'False"- )- ]-#else- [$(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"- )]-#endif--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 =-#if __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--data Fin (n :: Nat) where- FZ :: Fin (n + 1)- FS :: Fin n -> Fin (n + 1)--test16 :: forall n . Integer -> Fin n-test16 n = case n of- 0 -> FZ- x -> FS (test16 @(n-1) (x-1))--test16Errors =-#if __GLASGOW_HASKELL__ >= 904- ["Cannot satisfy: 1 <= n"]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat 1 n) 'True 'True 'False’"- else litE $ stringL "(CmpNat 1 n) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'True’"- else litE $ stringL "with 'True"- )- ]-#else- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘1 <=? n’ with ‘'True’"- else litE $ stringL "Couldn't match type `1 <=? n' with 'True"- )]-#endif--data Dict c where- Dict :: c => Dict c-deriving instance Show (Dict c)-data Boo (n :: Nat) = Boo--test17 :: Show (Boo n) => Proxy n -> Boo (n - 1 + 1) -> String-test17 = const show--testProxy17 :: String--testProxy17 = test17 (Proxy :: Proxy 17) Boo-test17Errors = test16Errors--#if __GLASGOW_HASKELL__ >= 904-test19f :: ((1 <= n) ~ (() :: Constraint))-#else-test19f :: (1 <= n)-#endif- => Proxy n -> Proxy n-test19f = id--testProxy19 :: (1 <= m, m <= rp)- => Proxy m- -> Proxy rp- -> Proxy (rp - m)- -> Proxy (rp - m)-testProxy19 _ _ = test19f--test19Errors =-#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--testProxy20 :: Proxy 1 -> Proxy (m ^ 2) -> ()-testProxy20 = proxyInEq--testProxy20Errors =-#if __GLASGOW_HASKELL__ >= 904- ["Cannot satisfy: 1 <= m ^ 2"]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat 1 (m ^ 2)) 'True 'True 'False’"- else litE $ stringL "(CmpNat 1 (m ^ 2)) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'True’"- else litE $ stringL "with 'True"- )- ]-#else- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘1 <=? (m ^ 2)’ with ‘'True’"- else litE $ stringL "Couldn't match type `1 <=? (m ^ 2)' with 'True"- )]-#endif
+ tests/ShouldError.hs view
@@ -0,0 +1,597 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE QuasiQuotes #-}++module ShouldError (tests) where++import Data.String.Interpolate (i)+import ShouldError.Tasty (assertCompileError)+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.HUnit (testCase)++tests :: TestTree+tests = testGroup "ShouldError"+ [ test1+ , test2+ , test3+ , test4+ , test5+ , test6+ , test7+ , test8+ , test9+ , test10+ , test11+ , testIssue126+ , inequalityTests+ ]++preamble :: String+preamble = [i|+import Data.Kind (Constraint)+import Data.Proxy+import GHC.TypeLits+|] <> "\n"++source1 :: String+source1 = preamble <> [i|+test :: Proxy (x + 1) -> Proxy (2 + x)+test = id+|]++expected1 :: [String]+expected1 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (2 + x)"+ ," Actual: Proxy (x + 1)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy (x + 1) -> Proxy (2 + x)"+ ," Actual: Proxy (x + 1) -> Proxy (x + 1)"+ ]+#else+ ["Expected type: Proxy (x + 1) -> Proxy (2 + x)"+ ,"Actual type: Proxy (2 + x) -> Proxy (2 + x)"+ ]+#endif++test1 :: TestTree+test1 = testCase "x + 1 /~ 2 + x" $ assertCompileError source1 expected1++source2 :: String+source2 = preamble <> [i|+type family GCD (x :: Nat) (y :: Nat) :: Nat+type instance GCD 6 8 = 2+type instance GCD 9 6 = 3++test :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)+test = id+|]++expected2 :: [String]+expected2 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (x + GCD 9 6)"+ ," Actual: Proxy (2 + x)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"+ ," Actual: Proxy (2 + x) -> Proxy (2 + x)"+ ]+#else+ ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"+ ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)"+ ]+#endif++test2 :: TestTree+test2 = testCase "GCD 6 8 + x /~ x + GCD 9 6" $ assertCompileError source2 expected2++source3 :: String+source3 = preamble <> [i|+proxyFun :: Proxy (x + x + x) -> ()+proxyFun = const ()++test :: Proxy 8 -> ()+test = proxyFun+|]++expected3 :: [String]+expected3 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy ((x0 + x0) + x0)"+ ," Actual: Proxy 8"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy 8 -> ()"+ ," Actual: Proxy ((x0 + x0) + x0) -> ()"+ ]+#else+ ["Expected type: Proxy 8 -> ()"+ ,"Actual type: Proxy ((x0 + x0) + x0) -> ()"+ ]+#endif++test3 :: TestTree+test3 = testCase "Unify \"x + x + x\" with \"8\"" $ assertCompileError source3 expected3++source4 :: String+source4 = preamble <> [i|+proxyFun :: Proxy ((2*y)+4) -> ()+proxyFun = const ()++test :: Proxy 2 -> ()+test = proxyFun+|]++expected4 :: [String]+expected4 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy ((2 * y0) + 4)"+ ," Actual: Proxy 2"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy 2 -> ()"+ ," Actual: Proxy ((2 * y0) + 4) -> ()"+ ]+#else+ ["Expected type: Proxy 2 -> ()"+ ,"Actual type: Proxy ((2 * y0) + 4) -> ()"+ ]+#endif++test4 :: TestTree+test4 = testCase "Unify \"(2*x)+4\" with \"2\"" $ assertCompileError source4 expected4++source5 :: String+source5 = preamble <> [i|+proxyFun :: Proxy ((2*y)+4) -> ()+proxyFun = const ()++test :: Proxy 7 -> ()+test = proxyFun+|]++expected5 :: [String]+expected5 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy ((2 * y"+ ,"Actual: Proxy 7"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy 7 -> ()"+ ,"Actual: Proxy ((2 * y"+ ]+#else+ ["Expected type: Proxy 7 -> ()"+ ,"Actual type: Proxy ((2 * y"+ ]+#endif++test5 :: TestTree+test5 = testCase "Unify \"(2*x)+4\" with \"7\"" $ assertCompileError source5 expected5++source6 :: String+source6 = preamble <> [i|+proxyFun :: Proxy (2^k) -> Proxy (2^k)+proxyFun = const Proxy++test :: Proxy 7+test = proxyFun (Proxy :: Proxy 7)+|]++expected6 :: [String]+expected6 =+#if __GLASGOW_HASKELL__ >= 902+ ["Expected: Proxy 7"+ ," Actual: Proxy (2 ^ k0)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy (2 ^ k0)"+ ," Actual: Proxy 7"+ ]+#else+ ["Expected type: Proxy (2 ^ k0)"+ ,"Actual type: Proxy 7"+ ]+#endif++test6 :: TestTree+test6 = testCase "Unify \"2^k\" with \"7\"" $ assertCompileError source6 expected6++source7 :: String+source7 = preamble <> [i|+test :: Proxy x -> Proxy (y + x)+test = id+|]++expected7 :: [String]+expected7 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (y + x)"+ ," Actual: Proxy x"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy x -> Proxy (y + x)"+ ," Actual: Proxy x -> Proxy x"+ ]+#else+ ["Expected type: Proxy x -> Proxy (y + x)"+ ,"Actual type: Proxy x -> Proxy x"+ ]+#endif++test7 :: TestTree+test7 = testCase "x /~ y + x" $ assertCompileError source7 expected7++source8 :: String+source8 = preamble <> [i|+type family CLog (b :: Nat) (x :: Nat) :: Nat+type instance CLog 2 2 = 1++test :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)+test = id+|]++expected8 :: [String]+expected8 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (n + d)"+ ," Actual: Proxy n"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy n -> Proxy (n + d)"+ ," Actual: Proxy n -> Proxy n"+ ]+#else+ ["Expected type: Proxy n -> Proxy (n + d)"+ ,"Actual type: Proxy n -> Proxy n"+ ]+#endif++test8 :: TestTree+test8 = testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n /~ n + d" $+ assertCompileError source8 expected8++source9 :: String+source9 = preamble <> [i|+data Fin (n :: Nat) where+ FZ :: Fin (n + 1)+ FS :: Fin n -> Fin (n + 1)++test :: forall n . Integer -> Fin n+test n = case n of+ 0 -> FZ+ x -> FS (test @(n-1) (x-1))+|]++expected9 :: [String]+expected9 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 1 <= n"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat 1 n) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type 1 <=? n with True" ]+#endif++test9 :: TestTree+test9 = testCase "(n - 1) + 1 ~ n implies (1 <= n)" $ assertCompileError source9 expected9++source10 :: String+source10 = preamble <> [i|+type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where+ Drop 0 xs = xs+ Drop n (x ': xs) = Drop (n-1) xs+ Drop n '[] = '[]++test :: Proxy ns -> Proxy (Drop 1 ns) -> Proxy (Drop 2 ns)+test _ px = px+|]++expected10 :: [String]+expected10 =+#if __GLASGOW_HASKELL__ >= 811+ [ "Couldn't match type: Drop 1 ns"+ , " with: Drop 2 ns"+ , "Expected: Proxy (Drop 2 ns)"+ , " Actual: Proxy (Drop 1 ns)"+ , "Drop is a non-injective type family"+ ]+#else+ [ "Couldn't match type Drop 1 ns with Drop 2 ns"+ , "Expected type: Proxy (Drop 2 ns)"+ , " Actual type: Proxy (Drop 1 ns)"+ , "Drop is a non-injective type family"+ ]+#endif++test10 :: TestTree+test10 = testCase "Do not unify in non-injective positions" $ assertCompileError source10 expected10++source11 :: String+source11 = preamble <> [i|+test :: Proxy a -> Proxy b -> Proxy ((2 * a) + b) -> Proxy 5+test _ _ = id+|]++expected11 :: [String]+expected11 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy 5"+ ," Actual: Proxy ((2 * a) + b)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy ((2 * a) + b) -> Proxy 5"+ ," Actual: Proxy 5 -> Proxy 5"+ ]+#else+ ["Expected type: Proxy ((2 * a) + b) -> Proxy 5"+ ,"Actual type: Proxy 5 -> Proxy 5"+ ]+#endif++test11 :: TestTree+test11 = testCase "Do not rewrite constraint to itself" $ assertCompileError source11 expected11++-- ((3 * (n - 1)) + 1) simplifies to (3 * n - 2), so+-- the equality would require b0 ~ -2, which is impossible at kind Nat.+sourceIssue126 :: String+sourceIssue126 = preamble <> [i|+data Index (n :: Nat) = Index++truncateB :: Index (a + b) -> Index a+truncateB = undefined++mul :: Index 4 -> Index n -> Index ((3 * (n - 1)) + 1)+mul _ _ = Index++zeroExtendTimesThree :: (1 <= n) => Index n -> Index (n * 3)+zeroExtendTimesThree = truncateB . (mul Index)+|]++expectedIssue126 :: [String]+expectedIssue126 =+#if __GLASGOW_HASKELL__ >= 906+ [ "Could not deduce ((n * 3) + b0) ~ ((3 * (n - 1)) + 1)"+#elif __GLASGOW_HASKELL__ >= 904+ [ "Could not deduce (((n * 3) + b0) ~ ((3 * (n - 1)) + 1))"+#elif __GLASGOW_HASKELL__ >= 902+ [ "Could not deduce: ((n * 3) + b0) ~ ((3 * (n - 1)) + 1)"+#else+ [ "Could not deduce: ((3 * (n - 1)) + 1) ~ ((n * 3) + b0)"+#endif+ , "from the context: 1 <= n"+ ]++++testIssue126 :: TestTree+testIssue126 =+ testCase "Issue 126 regression reproducer" $+ assertCompileError sourceIssue126 expectedIssue126++proxyInEqDef :: String+proxyInEqDef =+#if __GLASGOW_HASKELL__ >= 904+ [i|+proxyInEq :: ((a <= b) ~ (() :: Constraint)) => Proxy (a :: Nat) -> Proxy b -> ()+proxyInEq _ _ = ()+|]+#else+ [i|+proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> ()+proxyInEq _ _ = ()+|]+#endif++proxyInEq'Def :: String+proxyInEq'Def = [i|+proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> ()+proxyInEq' _ _ = ()+|]++source12 :: String+source12 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (a + 1) -> Proxy a -> ()+test = proxyInEq+|]++expected12 :: [String]+expected12 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: a + 1 <= a"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat (a + 1) a) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type (a + 1) <=? a with True" ]+#endif++test12 :: TestTree+test12 = testCase "a+1 <= a" $ assertCompileError source12 expected12++source13 :: String+source13 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()+test = proxyInEq'+|]++expected13 :: [String]+expected13 =+#if __GLASGOW_HASKELL__ >= 902+ [ "Data.Type.Ord.OrdCond"+ , "(CmpNat a (a + 2)) True True False"+ , "with False"+ ]+#else+ [ "Couldn't match type a <=? (a + 2) with False" ]+#endif++test13 :: TestTree+test13 = testCase "(a <=? a+1) ~ False" $ assertCompileError source13 expected13++source14 :: String+source14 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (a :: Nat) -> Proxy a -> ()+test = proxyInEq'+|]++expected14 :: [String]+expected14 = [ "Couldn't match type True with False" ]++test14 :: TestTree+test14 = testCase "(a <=? a) ~ False" $ assertCompileError source14 expected14++source15 :: String+source15 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (a + b) -> Proxy (a + c) -> ()+test = proxyInEq+|]++expected15 :: [String]+expected15 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: a + b <= a + c"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat (a + b) (a + c)) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type (a + b) <=? (a + c) with True" ]+#endif++test15 :: TestTree+test15 = testCase "() => (a+b <= a+c)" $ assertCompileError source15 expected15++source16 :: String+source16 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (4*a) -> Proxy (2*a) -> ()+test = proxyInEq+|]++expected16 :: [String]+expected16 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 4 * a <= 2 * a"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat (4 * a) (2 * a)) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type (4 * a) <=? (2 * a) with True" ]+#endif++test16 :: TestTree+test16 = testCase "4a <= 2a" $ assertCompileError source16 expected16++source17 :: String+source17 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (2*a) -> Proxy (4*a) -> ()+test = proxyInEq'+|]++expected17 :: [String]+expected17 =+#if __GLASGOW_HASKELL__ >= 902+ [ "Data.Type.Ord.OrdCond"+ , "(CmpNat (2 * a) (4 * a)) True True False"+ , "with False"+ ]+#else+ [ "Couldn't match type (2 * a) <=? (4 * a) with False" ]+#endif++test17 :: TestTree+test17 = testCase "2a <=? 4a ~ False" $ assertCompileError source17 expected17++source18 :: String+source18 = preamble <> [i|+data Boo (n :: Nat) = Boo++test :: Show (Boo n) => Proxy n -> Boo (n - 1 + 1) -> String+test = const show+|]++expected18 :: [String]+expected18 = expected9++test18 :: TestTree+test18 = testCase "Show (Boo n) => Show (Boo (n - 1 + 1))" $ assertCompileError source18 expected18++test19fDef :: String+test19fDef =+#if __GLASGOW_HASKELL__ >= 904+ [i|+test19f :: ((1 <= n) ~ (() :: Constraint)) => Proxy n -> Proxy n+test19f = id+|]+#else+ [i|+test19f :: (1 <= n) => Proxy n -> Proxy n+test19f = id+|]+#endif++source19 :: String+source19 = preamble <> test19fDef <> [i|+test :: (1 <= m, m <= rp) => Proxy m -> Proxy rp -> Proxy (rp - m) -> Proxy (rp - m)+test _ _ = test19f+|]++expected19 :: [String]+expected19 =+#if __GLASGOW_HASKELL__ >= 904+ [ "Cannot satisfy: 1 <= rp - m" ]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Could not deduce: Data.Type.Ord.OrdCond"+ , "(CmpNat 1 (rp - m)) True True False"+ , "~ True"+ ]+#else+ [ "Could not deduce: (1 <=? (rp - m)) ~ True" ]+#endif++test19 :: TestTree+test19 = testCase "1 <= m, m <= rp implies 1 <= rp - m" $ assertCompileError source19 expected19++source20 :: String+source20 = preamble <> proxyInEqDef <> [i|+test :: Proxy 1 -> Proxy (m ^ 2) -> ()+test = proxyInEq+|]++expected20 :: [String]+expected20 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 1 <= m ^ 2"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat 1 (m ^ 2)) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type 1 <=? (m ^ 2) with True" ]+#endif++test20 :: TestTree+test20 = testCase "Vacuously: 1 <= m ^ 2 ~ True" $ assertCompileError source20 expected20++inequalityTests :: TestTree+inequalityTests = testGroup "Inequality"+ [ test12+ , test13+ , test14+ , test15+ , test16+ , test17+ , test18+ , test19+ , test20+ ]
+ tests/ShouldError/Tasty.hs view
@@ -0,0 +1,58 @@+{-# LANGUAGE CPP #-}++module ShouldError.Tasty where++import Data.List (isInfixOf)+import Data.Maybe (fromMaybe)+import System.Environment (lookupEnv)+import System.Exit+import System.IO+import System.IO.Temp+import System.Process+import Test.Tasty.HUnit++-- | Assert that a Haskell code snippet fails to compile with expected error messages+assertCompileError :: String -> [String] -> Assertion+assertCompileError source expectedErrors = do+ -- XXX: This will pick the wrong GHC if the HC environment variable (as seen on CI)+ -- isn't set and the test suite is compiled with a GHC compiler other than the+ -- system's default.+ hc <- fromMaybe "ghc" <$> lookupEnv "HC"+ withSystemTempFile "ShouldError.hs" $ \tempFile tempHandle -> do+ hPutStr tempHandle source+ hClose tempHandle+ (exitCode, _, stderrOutput) <- readProcessWithExitCode hc+ [ "-XCPP"+ , "-XAllowAmbiguousTypes"+ , "-XConstraintKinds"+ , "-XDataKinds"+ , "-XFlexibleContexts"+ , "-XGADTs"+ , "-XScopedTypeVariables"+ , "-XStandaloneDeriving"+ , "-XTypeApplications"+ , "-XTypeFamilies"+ , "-XTypeOperators"+ , "-XUndecidableInstances"+ , "-XNoStarIsType"+ , "-fno-code"+ , "-fplugin", "GHC.TypeLits.Normalise"+ , tempFile+ ] ""+ case exitCode of+ ExitSuccess -> assertFailure "Expected compilation to fail but it succeeded"+ ExitFailure _ ->+ let cleanedStderr = removeProblemChars stderrOutput+ cleanedExpected = map removeProblemChars expectedErrors+ in if all (`isInfixOf` cleanedStderr) cleanedExpected+ then return ()+ else assertFailure $ "Error message mismatch:\n" +++ "Expected substrings: " ++ show expectedErrors ++ "\n" +++ "Actual output:\n" ++ stderrOutput++-- | Remove problematic characters that vary depending on locale+-- The kind and amount of quotes in GHC error messages changes depending on+-- whether or not our locale supports unicode.+removeProblemChars :: String -> String+removeProblemChars = filter (`notElem` problemChars)+ where problemChars = "‘’`'"
tests/Tests.hs view
@@ -23,6 +23,7 @@ {-# 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)@@ -33,14 +34,17 @@ import Prelude hiding (head,tail,init,(++),splitAt,concat,drop) import qualified Prelude as P -import Data.Kind (Type)-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 -> Type -> Type where Nil :: Vec 0 a@@ -118,6 +122,7 @@ -- 1 head :: Vec (n + 1) a -> a head (x :> _) = x+head Nil = error "head: impossible" head' :: forall n a@@ -132,6 +137,7 @@ -- <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@@ -143,6 +149,7 @@ init :: Vec (n + 1) a -> Vec n a 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@@ -169,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@@ -244,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 --@@ -304,6 +314,15 @@ 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@@ -321,6 +340,12 @@ 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 @@ -359,7 +384,7 @@ . ((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 @@ -374,12 +399,12 @@ 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))+ :: 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)))@@ -449,6 +474,14 @@ 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)))@@ -469,6 +502,9 @@ => 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@@ -481,13 +517,13 @@ -> Proxy n proxyInEq8 = proxyInEq8fun -data H2 = H2 { p :: Nat }+data H2 = H2 { pNat :: Nat } class Q (dom :: Symbol) where type G2 dom :: H2 type family P (c :: H2) :: Nat where- P ('H2 p) = p+ P ('H2 pNat) = pNat type F2 (dom :: Symbol) = P (G2 dom) @@ -506,8 +542,22 @@ oneLtPowSubst = go where go :: 1 <= b => Proxy a -> Proxy a- go = id + 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 @@ -515,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)) @?=@@ -552,6 +602,9 @@ , testCase "(((2 ^ x) - 2) * (2 ^ (x + x))) ~ ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1))))" $ 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" $@@ -612,45 +665,9 @@ show (oneLtPowSubst (Proxy :: Proxy 0)) @?= "Proxy" ]- , 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- , testCase "(n - 1) + 1 ~ n implies (1 <= n)" $ test16 `throws` test16Errors- , 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 "Show (Boo n) => Show (Boo (n - 1 + 1))" $- testProxy17 `throws` test17Errors- , testCase "1 <= m, m <= rp implies 1 <= rp - m" $ (testProxy19 (Proxy @1) (Proxy @1)) `throws` test19Errors- , testCase "Vacuously: 1 <= m ^ 2 ~ True" $ testProxy20 `throws` testProxy20Errors- ]- ]+ , 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)@@ -662,6 +679,10 @@ 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@@ -709,3 +730,115 @@ 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