ghc-typelits-extra 0.4.8 → 0.5.0
raw patch · 13 files changed
+834/−1823 lines, 13 filesdep +ghc-tcplugin-apidep −ghc-tcplugins-extradep ~containersdep ~ghcdep ~ghc-bignumPVP ok
version bump matches the API change (PVP)
Dependencies added: ghc-tcplugin-api
Dependencies removed: ghc-tcplugins-extra
Dependency ranges changed: containers, ghc, ghc-bignum, ghc-typelits-knownnat, ghc-typelits-natnormalise, template-haskell
API changes (from Hackage documentation)
- GHC.TypeLits.Extra: type DivMod n d = '(Div n d, Mod n d)
+ GHC.TypeLits.Extra: type DivMod (n :: Natural) (d :: Natural) = '(Div n d, Mod n d)
- GHC.TypeLits.Extra: type DivRU n d = Div (n + (d - 1)) d
+ GHC.TypeLits.Extra: type DivRU (n :: Natural) (d :: Natural) = Div n + d - 1 d
Files
- CHANGELOG.md +5/−0
- ghc-typelits-extra.cabal +52/−43
- src-ghc-9.12/GHC/TypeLits/Extra/Solver.hs +0/−349
- src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs +0/−348
- src-pre-ghc-9.4/GHC/TypeLits/Extra/Solver.hs +0/−347
- src/GHC/TypeLits/Extra/Solver.hs +256/−0
- src/GHC/TypeLits/Extra/Solver/Compat.hs +99/−0
- src/GHC/TypeLits/Extra/Solver/Operations.hs +39/−64
- src/GHC/TypeLits/Extra/Solver/Unify.hs +70/−70
- tests-ghc-9.4/ErrorTests.hs +0/−253
- tests-pre-ghc-9.4/ErrorTests.hs +0/−347
- tests/ErrorTests.hs +303/−0
- tests/Main.hs +10/−2
CHANGELOG.md view
@@ -1,5 +1,10 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package +# 0.5.0 *October 17th 2025*+* Add support for GHC 9.14+* Uses https://hackage.haskell.org/package/ghc-tcplugin-api to make supporting new GHC versions easier+* Support for GHC versions older than 8.8 is dropped+ # 0.4.8 *March 4th 2025* * Add support for GHC 9.12.1
ghc-typelits-extra.cabal view
@@ -1,42 +1,43 @@+cabal-version: 3.0 name: ghc-typelits-extra-version: 0.4.8+version: 0.5.0 synopsis: Additional type-level operations on GHC.TypeLits.Nat description: Additional type-level operations on @GHC.TypeLits.Nat@:- .+ * @Max@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:max max>- .+ * @Min@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:min min>- .+ * @Div@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:div div>- .+ * @Mod@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:mod mod>- .+ * @FLog@: type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> i.e. the exact integer equivalent to @floor (logBase x y)@- .+ * @CLog@: type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> i.e. the exact integer equivalent to @ceiling (logBase x y)@- .+ * @Log@: type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> where the operation only reduces when @floor (logBase b x) ~ ceiling (logBase b x)@- .+ * @GCD@: a type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd gcd>- .+ * @LCM@: a type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:lcm lcm>- .+ And a custom solver for the above operations defined in @GHC.TypeLits.Extra.Solver@ as a GHC type-checker plugin. To use the plugin, add the- .+ @ OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver @- .+ pragma to the header of your file. homepage: http://www.clash-lang.org/ bug-reports: http://github.com/clash-lang/ghc-typelits-extra/issues-license: BSD2+license: BSD-2-Clause license-file: LICENSE author: Christiaan Baaij maintainer: christiaan.baaij@gmail.com@@ -46,11 +47,9 @@ build-type: Simple extra-source-files: README.md CHANGELOG.md-cabal-version: >=1.10-tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,- GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,- GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1,- GHC == 9.12.1+tested-with: GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,+ GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.3,+ GHC == 9.12.2 source-repository head@@ -66,29 +65,43 @@ library exposed-modules: GHC.TypeLits.Extra, GHC.TypeLits.Extra.Solver- other-modules: GHC.TypeLits.Extra.Solver.Unify+ other-modules: GHC.TypeLits.Extra.Solver.Compat+ GHC.TypeLits.Extra.Solver.Unify GHC.TypeLits.Extra.Solver.Operations- build-depends: base >= 4.8 && <5,- containers >= 0.5.7.1 && <0.8,- ghc >= 7.10 && <9.13,- ghc-prim >= 0.5 && <1.0,- ghc-tcplugins-extra >= 0.3.1,- ghc-typelits-knownnat >= 0.7.2 && <0.8,- ghc-typelits-natnormalise >= 0.7.1 && <0.8,- transformers >= 0.4.2.0 && <0.7+ build-depends: base >= 4.8 && <5,+ containers >= 0.5.7.1 && <0.9,+ ghc >= 8.8 && <9.17,+ ghc-prim >= 0.5 && <1.0,+ ghc-tcplugin-api >= 0.18.1.0 && <0.19,+ ghc-typelits-knownnat >= 0.7.2 && <0.9,+ ghc-typelits-natnormalise >= 0.9 && <0.10,+ transformers >= 0.4.2.0 && <0.7,+ template-haskell >= 2.15 && <2.25 if impl(ghc >= 9.0.0)- build-depends: ghc-bignum >=1.0 && <1.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+ , DataCon as GHC.Core.DataCon+ , TyCoRep as GHC.Core.TyCo.Rep+ , Type as GHC.Core.Type+ , Plugins as GHC.Driver.Plugins+ )++ if impl(ghc >= 8.9)+ mixins:+ ghc+ ( Constraint as GHC.Tc.Types.Constraint+ )+ else+ mixins:+ ghc+ ( TcRnTypes as GHC.Tc.Types.Constraint+ )+ hs-source-dirs: src- 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: DataKinds FlexibleInstances@@ -113,15 +126,11 @@ Other-Modules: ErrorTests build-depends: base >= 4.8 && <5, ghc-typelits-extra,- ghc-typelits-knownnat >= 0.7.2,- ghc-typelits-natnormalise >= 0.7.1,+ ghc-typelits-knownnat >= 0.8.2,+ ghc-typelits-natnormalise >= 0.9.0, tasty >= 0.10, tasty-hunit >= 0.9 hs-source-dirs: tests- if impl(ghc >= 8.0) && impl(ghc < 9.4)- hs-source-dirs: tests-pre-ghc-9.4- if impl(ghc >= 9.4) && impl(ghc < 9.13)- hs-source-dirs: tests-ghc-9.4 default-language: Haskell2010 other-extensions: DataKinds TypeOperators
− src-ghc-9.12/GHC/TypeLits/Extra/Solver.hs
@@ -1,349 +0,0 @@-{-|-Copyright : (C) 2015-2016, University of Twente-License : BSD2 (see the file LICENSE)-Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>--To use the plugin, add the--@-{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}-@--pragma to the header of your file---}--{-# LANGUAGE TupleSections #-}-{-# LANGUAGE TemplateHaskellQuotes #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.Extra.Solver- ( plugin )-where---- external-import Control.Monad.Trans.Maybe (MaybeT (..))-import Data.Maybe (catMaybes)-import GHC.TcPluginM.Extra (evByFiatWithDependencies, tracePlugin, newWanted)-import qualified Data.Type.Ord-import qualified GHC.TypeError---- GHC API-import GHC.Builtin.Names (eqPrimTyConKey, hasKey, getUnique)-import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon)-import GHC.Builtin.Types (boolTy, naturalTy, cTupleDataCon, cTupleTyCon)-import GHC.Builtin.Types.Literals (typeNatDivTyCon, typeNatModTyCon, typeNatCmpTyCon)-import GHC.Core.Coercion (Coercion, mkUnivCo)-import GHC.Core.DataCon (dataConWrapId)-import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType)-import GHC.Core.Reduction (Reduction(..))-import GHC.Core.TyCon (TyCon)-import GHC.Core.TyCo.Rep (Type (..), TyLit (..), UnivCoProvenance (PluginProv))-import GHC.Core.Type (Kind, mkTyConApp, splitTyConApp_maybe, typeKind)-import GHC.Core.TyCo.Compare (eqType)-import GHC.Data.IOEnv (getEnv)-import GHC.Driver.Env (hsc_NC)-import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)-import GHC.Plugins (thNameToGhcNameIO)-import GHC.Tc.Plugin- (TcPluginM, tcLookupTyCon, tcPluginTrace, tcPluginIO, unsafeTcPluginTcM)-import GHC.Tc.Types- (TcPlugin(..), TcPluginSolveResult (..), TcPluginRewriter, TcPluginRewriteResult (..),- Env (env_top))-import GHC.Tc.Types.Constraint (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt)-import GHC.Tc.Types.Constraint- (Ct (..), DictCt(..), EqCt(..), IrredCt(..), ctEvCoercion, qci_ev)-import GHC.Tc.Types.Evidence (EvTerm, EvBindsVar, Role(..), evCast, evId)-import GHC.Types.Unique.FM (UniqFM, listToUFM)-import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)-import GHC (Name)---- template-haskell-import qualified Language.Haskell.TH as TH---- internal-import GHC.TypeLits.Extra.Solver.Operations-import GHC.TypeLits.Extra.Solver.Unify-import GHC.TypeLits.Extra---- | A solver implement as a type-checker plugin for:------ * 'Div': type-level 'div'------ * 'Mod': type-level 'mod'------ * 'FLog': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"------ * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"------ * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"------ * 'GCD': a type-level 'gcd'------ * 'LCM': a type-level 'lcm'------ To use the plugin, add------ @--- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}--- @------ To the header of your file.-plugin :: Plugin-plugin- = defaultPlugin- { tcPlugin = const $ Just normalisePlugin- , pluginRecompile = purePlugin- }--normalisePlugin :: TcPlugin-normalisePlugin = tracePlugin "ghc-typelits-extra"- TcPlugin { tcPluginInit = lookupExtraDefs- , tcPluginSolve = decideEqualSOP- , tcPluginRewrite = extraRewrite- , tcPluginStop = const (return ())- }--extraRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter-extraRewrite defs = listToUFM- [ (gcdTyCon defs, gcdRewrite)- , (lcmTyCon defs, lcmRewrite)- ]- where- gcdRewrite _ _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $- TcPluginRewriteTo (reduce (gcdTyCon defs) args (LitTy (NumTyLit (i `gcd` j)))) []- gcdRewrite _ _ _ = pure TcPluginNoRewrite-- lcmRewrite _ _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $- TcPluginRewriteTo (reduce (lcmTyCon defs) args (LitTy (NumTyLit (i `lcm` j)))) []- lcmRewrite _ _ _ = pure TcPluginNoRewrite-- reduce tc args res = Reduction co res- where- co = mkUnivCo (PluginProv "ghc-typelits-extra") [] Nominal- (mkTyConApp tc args) res---decideEqualSOP :: ExtraDefs -> EvBindsVar -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult-decideEqualSOP _ _ _givens [] = return (TcPluginOk [] [])-decideEqualSOP defs _ givens wanteds = do- unit_wanteds <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) wanteds- case unit_wanteds of- [] -> return (TcPluginOk [] [])- _ -> do- unit_givens <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) givens- sr <- simplifyExtra defs (unit_givens ++ unit_wanteds)- tcPluginTrace "normalised" (ppr sr)- case sr of- Simplified evs new -> return (TcPluginOk (filter (isWantedCt . snd) evs) new)- Impossible eq -> return (TcPluginContradiction [fromSolverConstraint eq])--data SolverConstraint- = NatEquality Ct ExtraOp ExtraOp Normalised- | NatInequality Ct [Coercion] ExtraOp ExtraOp Bool Normalised--instance Outputable SolverConstraint where- ppr (NatEquality ct op1 op2 norm) =- text "NatEquality" $$ ppr ct $$ ppr op1 $$ ppr op2 $$ ppr norm- ppr (NatInequality _ _ op1 op2 b norm) =- text "NatInequality" $$ ppr op1 $$ ppr op2 $$ ppr b $$ ppr norm--data SimplifyResult- = Simplified [(EvTerm,Ct)] [Ct]- | Impossible SolverConstraint--instance Outputable SimplifyResult where- ppr (Simplified evs new) =- text "Simplified" $$ text "Solved:" $$ ppr evs $$ text "New:" $$ ppr new- ppr (Impossible sct) =- text "Impossible" <+> ppr sct--simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM SimplifyResult-simplifyExtra defs eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] eqs- where- simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult- simples evs news [] = return (Simplified (catMaybes evs) news)- simples evs news (eq@(NatEquality ct u v norm):eqs') = do- ur <- unifyExtra ct u v- tcPluginTrace "unifyExtra result" (ppr ur)- case ur of- Win -> simples (((,) <$> evMagic ct [] <*> pure ct):evs) news eqs'- Lose | null evs && null eqs' -> return (Impossible eq)- _ | norm == Normalised && isWantedCt ct -> do- newCt <- createWantedFromNormalised defs eq- simples (((,) <$> evMagic ct [] <*> pure ct):evs) (newCt:news) eqs'- Lose -> simples evs news eqs'- Draw -> simples evs news eqs'- simples evs news (eq@(NatInequality ct deps u v b norm):eqs') = do- tcPluginTrace "unifyExtra leq result" (ppr (u,v,b))- case (u,v) of- (I i,I j)- | (i <= j) == b -> simples (((,) <$> evMagic ct deps <*> pure ct):evs) news eqs'- | otherwise -> return (Impossible eq)- (p, Max x y)- | b && (p == x || p == y)- -> simples (((,) <$> evMagic ct deps <*> pure ct):evs) news eqs'-- -- transform: q ~ Max x y => (p <=? q ~ True)- -- to: (p <=? Max x y) ~ True- -- and try to solve that along with the rest of the eqs'- (p, q@(V _))- | b -> case findMax q eqs of- Just (i,m) ->- simples evs news- (NatInequality ct (i:deps) p m b norm:eqs')- Nothing -> simples evs news eqs'- _ | norm == Normalised && isWantedCt ct -> do- newCt <- createWantedFromNormalised defs eq- simples (((,) <$> evMagic ct deps <*> pure ct):evs) (newCt:news) eqs'- _ -> simples evs news eqs'-- -- look for given constraint with the form: c ~ Max x y- findMax :: ExtraOp -> [SolverConstraint] -> Maybe (Coercion, ExtraOp)- findMax c = go- where- go [] = Nothing- go ((NatEquality ct a b@(Max _ _) _) :_)- | c == a && not (isWantedCt ct)- = Just (ctEvCoercion (ctEvidence ct), b)- go ((NatEquality ct a@(Max _ _) b _) :_)- | c == b && not (isWantedCt ct)- = Just (ctEvCoercion (ctEvidence ct), a)- go (_:rest) = go rest----- Extract the Nat equality constraints-toSolverConstraint :: ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint-toSolverConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2- | isNatKind (typeKind t1) || isNatKind (typeKind t2)- -> do- (t1', n1) <- normaliseNat defs t1- (t2', n2) <- normaliseNat defs t2- pure (NatEquality ct t1' t2' (mergeNormalised n1 n2))- | TyConApp tc [_,cmpNat,TyConApp tt1 [],TyConApp tt2 [],TyConApp ff1 []] <- t1- , tc == ordTyCon defs- , TyConApp cmpNatTc [x,y] <- cmpNat- , cmpNatTc == typeNatCmpTyCon- , tt1 == promotedTrueDataCon- , tt2 == promotedTrueDataCon- , ff1 == promotedFalseDataCon- , TyConApp tc' [] <- t2- -> do- (x', n1) <- normaliseNat defs x- (y', n2) <- normaliseNat defs y- let res | tc' == promotedTrueDataCon- = pure (NatInequality ct [] x' y' True- (mergeNormalised n1 n2))- | tc' == promotedFalseDataCon- = pure (NatInequality ct [] x' y' False- (mergeNormalised n1 n2))- | otherwise = fail "Nothing"- res- | TyConApp tc [TyConApp ordCondTc zs, _] <- t1- , tc == assertTC defs- , TyConApp tc' [] <- t2- , tc' == cTupleTyCon 0- , ordCondTc == ordTyCon defs- , [_,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- -> do- (x', n1) <- normaliseNat defs x- (y', n2) <- normaliseNat defs y- pure (NatInequality ct [] x' y' True (mergeNormalised n1 n2))- IrredPred (TyConApp tc [TyConApp ordCondTc zs, _])- | tc == assertTC defs- , ordCondTc == ordTyCon defs- , [_,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- -> do- (x', n1) <- normaliseNat defs x- (y', n2) <- normaliseNat defs y- pure (NatInequality ct [] x' y' True (mergeNormalised n1 n2))- _ -> fail "Nothing"- where- isNatKind :: Kind -> Bool- isNatKind = (`eqType` naturalTy)--createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM Ct-createWantedFromNormalised defs sct = do- let extractCtSides (NatEquality ct t1 t2 _) = (ct, reifyEOP defs t1, reifyEOP defs t2)- extractCtSides (NatInequality ct _ x y b _) =- let tc = if b then promotedTrueDataCon else promotedFalseDataCon- t1 = TyConApp (ordTyCon defs)- [ boolTy- , TyConApp typeNatCmpTyCon [reifyEOP defs x, reifyEOP defs y]- , TyConApp promotedTrueDataCon []- , TyConApp promotedTrueDataCon []- , TyConApp promotedFalseDataCon []- ]- t2 = TyConApp tc []- in (ct, t1, t2)- let (ct, t1, t2) = extractCtSides sct- newPredTy <- case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of- Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2])- Just (tc, [_, b]) | tc `hasKey` getUnique (assertTC defs) -> pure (mkTyConApp tc [t1,b])- _ -> error "Impossible: neither (<=?) nor Assert"- ev <- newWanted (ctLoc ct) newPredTy- let ctN = case ct of- CQuantCan qc -> CQuantCan (qc { qci_ev = ev})- CDictCan di -> CDictCan (di { di_ev = ev})- CIrredCan ir -> CIrredCan (ir { ir_ev = ev})- CEqCan eq -> CEqCan (eq { eq_ev = ev})- CNonCanonical _ -> CNonCanonical ev- return ctN--fromSolverConstraint :: SolverConstraint -> Ct-fromSolverConstraint (NatEquality ct _ _ _) = ct-fromSolverConstraint (NatInequality ct _ _ _ _ _) = ct--lookupExtraDefs :: TcPluginM ExtraDefs-lookupExtraDefs = do- ExtraDefs <$> look ''GHC.TypeLits.Extra.Max- <*> look ''GHC.TypeLits.Extra.Min- <*> pure typeNatDivTyCon- <*> pure typeNatModTyCon- <*> look ''GHC.TypeLits.Extra.FLog- <*> look ''GHC.TypeLits.Extra.CLog- <*> look ''GHC.TypeLits.Extra.Log- <*> look ''GHC.TypeLits.Extra.GCD- <*> look ''GHC.TypeLits.Extra.LCM- <*> look ''Data.Type.Ord.OrdCond- <*> look ''GHC.TypeError.Assert- where- look nm = tcLookupTyCon =<< lookupTHName nm--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---- Utils-evMagic :: Ct -> [Coercion] -> Maybe EvTerm-evMagic ct deps = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2 -> Just (evByFiatWithDependencies "ghc-typelits-extra" deps t1 t2)- IrredPred p ->- let t1 = mkTyConApp (cTupleTyCon 0) []- co = mkUnivCo (PluginProv "ghc-typelits-extra") deps Representational t1 p- dcApp = evId (dataConWrapId (cTupleDataCon 0))- in Just (evCast dcApp co)- _ -> Nothing
− src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs
@@ -1,348 +0,0 @@-{-|-Copyright : (C) 2015-2016, University of Twente-License : BSD2 (see the file LICENSE)-Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>--To use the plugin, add the--@-{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}-@--pragma to the header of your file---}--{-# LANGUAGE CPP #-}-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE TemplateHaskellQuotes #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.Extra.Solver- ( plugin )-where---- external-import Control.Monad.Trans.Maybe (MaybeT (..))-import Data.Maybe (catMaybes)-import GHC.TcPluginM.Extra (evByFiat, tracePlugin, newWanted)-import qualified Data.Type.Ord-import qualified GHC.TypeError---- GHC API-import GHC.Builtin.Names (eqPrimTyConKey, hasKey, getUnique)-import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon)-import GHC.Builtin.Types (boolTy, naturalTy, cTupleDataCon, cTupleTyCon)-import GHC.Builtin.Types.Literals (typeNatDivTyCon, typeNatModTyCon, typeNatCmpTyCon)-import GHC.Core.Coercion (mkUnivCo)-import GHC.Core.DataCon (dataConWrapId)-import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType)-import GHC.Core.Reduction (Reduction(..))-import GHC.Core.TyCon (TyCon)-import GHC.Core.TyCo.Rep (Type (..), TyLit (..), UnivCoProvenance (PluginProv))-import GHC.Core.Type (Kind, mkTyConApp, splitTyConApp_maybe, typeKind)-#if MIN_VERSION_ghc(9,6,0)-import GHC.Core.TyCo.Compare (eqType)-#else-import GHC.Core.Type (eqType)-#endif-import GHC.Data.IOEnv (getEnv)-import GHC.Driver.Env (hsc_NC)-import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)-import GHC.Plugins (thNameToGhcNameIO)-import GHC.Tc.Plugin (TcPluginM, tcLookupTyCon, tcPluginTrace, tcPluginIO, unsafeTcPluginTcM)-import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), TcPluginRewriter, TcPluginRewriteResult (..), Env (env_top))-import GHC.Tc.Types.Constraint- (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt)-#if MIN_VERSION_ghc(9,8,0)-import GHC.Tc.Types.Constraint (Ct (..), DictCt(..), EqCt(..), IrredCt(..), qci_ev)-#else-import GHC.Tc.Types.Constraint (Ct (CQuantCan), qci_ev, cc_ev)-#endif-import GHC.Tc.Types.Evidence (EvTerm, EvBindsVar, Role(..), evCast, evId)-import GHC.Types.Unique.FM (UniqFM, listToUFM)-import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)-import GHC (Name)---- template-haskell-import qualified Language.Haskell.TH as TH---- internal-import GHC.TypeLits.Extra.Solver.Operations-import GHC.TypeLits.Extra.Solver.Unify-import GHC.TypeLits.Extra---- | A solver implement as a type-checker plugin for:------ * 'Div': type-level 'div'------ * 'Mod': type-level 'mod'------ * 'FLog': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"------ * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"------ * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"------ * 'GCD': a type-level 'gcd'------ * 'LCM': a type-level 'lcm'------ To use the plugin, add------ @--- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}--- @------ To the header of your file.-plugin :: Plugin-plugin- = defaultPlugin- { tcPlugin = const $ Just normalisePlugin- , pluginRecompile = purePlugin- }--normalisePlugin :: TcPlugin-normalisePlugin = tracePlugin "ghc-typelits-extra"- TcPlugin { tcPluginInit = lookupExtraDefs- , tcPluginSolve = decideEqualSOP- , tcPluginRewrite = extraRewrite- , tcPluginStop = const (return ())- }--extraRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter-extraRewrite defs = listToUFM- [ (gcdTyCon defs, gcdRewrite)- , (lcmTyCon defs, lcmRewrite)- ]- where- gcdRewrite _ _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $- TcPluginRewriteTo (reduce (gcdTyCon defs) args (LitTy (NumTyLit (i `gcd` j)))) []- gcdRewrite _ _ _ = pure TcPluginNoRewrite-- lcmRewrite _ _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $- TcPluginRewriteTo (reduce (lcmTyCon defs) args (LitTy (NumTyLit (i `lcm` j)))) []- lcmRewrite _ _ _ = pure TcPluginNoRewrite-- reduce tc args res = Reduction co res- where- co = mkUnivCo (PluginProv "ghc-typelits-extra") Nominal- (mkTyConApp tc args) res---decideEqualSOP :: ExtraDefs -> EvBindsVar -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult-decideEqualSOP _ _ _givens [] = return (TcPluginOk [] [])-decideEqualSOP defs _ givens wanteds = do- unit_wanteds <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) wanteds- case unit_wanteds of- [] -> return (TcPluginOk [] [])- _ -> do- unit_givens <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) givens- sr <- simplifyExtra defs (unit_givens ++ unit_wanteds)- tcPluginTrace "normalised" (ppr sr)- case sr of- Simplified evs new -> return (TcPluginOk (filter (isWantedCt . snd) evs) new)- Impossible eq -> return (TcPluginContradiction [fromSolverConstraint eq])--data SolverConstraint- = NatEquality Ct ExtraOp ExtraOp Normalised- | NatInequality Ct ExtraOp ExtraOp Bool Normalised--instance Outputable SolverConstraint where- ppr (NatEquality ct op1 op2 norm) = text "NatEquality" $$ ppr ct $$ ppr op1 $$ ppr op2 $$ ppr norm- ppr (NatInequality _ op1 op2 b norm) = text "NatInequality" $$ ppr op1 $$ ppr op2 $$ ppr b $$ ppr norm--data SimplifyResult- = Simplified [(EvTerm,Ct)] [Ct]- | Impossible SolverConstraint--instance Outputable SimplifyResult where- ppr (Simplified evs new) = text "Simplified" $$ text "Solved:" $$ ppr evs $$ text "New:" $$ ppr new- ppr (Impossible sct) = text "Impossible" <+> ppr sct--simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM SimplifyResult-simplifyExtra defs eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] eqs- where- simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult- simples evs news [] = return (Simplified (catMaybes evs) news)- simples evs news (eq@(NatEquality ct u v norm):eqs') = do- ur <- unifyExtra ct u v- tcPluginTrace "unifyExtra result" (ppr ur)- case ur of- Win -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs'- Lose | null evs && null eqs' -> return (Impossible eq)- _ | norm == Normalised && isWantedCt ct -> do- newCt <- createWantedFromNormalised defs eq- simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs'- Lose -> simples evs news eqs'- Draw -> simples evs news eqs'- simples evs news (eq@(NatInequality ct u v b norm):eqs') = do- tcPluginTrace "unifyExtra leq result" (ppr (u,v,b))- case (u,v) of- (I i,I j)- | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs'- | otherwise -> return (Impossible eq)- (p, Max x y)- | b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs'-- -- transform: q ~ Max x y => (p <=? q ~ True)- -- to: (p <=? Max x y) ~ True- -- and try to solve that along with the rest of the eqs'- (p, q@(V _))- | b -> case findMax q eqs of- Just m -> simples evs news (NatInequality ct p m b norm:eqs')- Nothing -> simples evs news eqs'- _ | norm == Normalised && isWantedCt ct -> do- newCt <- createWantedFromNormalised defs eq- simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs'- _ -> simples evs news eqs'-- -- look for given constraint with the form: c ~ Max x y- findMax :: ExtraOp -> [SolverConstraint] -> Maybe ExtraOp- findMax c = go- where- go [] = Nothing- go ((NatEquality ct a b@(Max _ _) _) :_)- | c == a && not (isWantedCt ct)- = Just b- go ((NatEquality ct a@(Max _ _) b _) :_)- | c == b && not (isWantedCt ct)- = Just a- go (_:rest) = go rest----- Extract the Nat equality constraints-toSolverConstraint :: ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint-toSolverConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2- | isNatKind (typeKind t1) || isNatKind (typeKind t2)- -> do- (t1', n1) <- normaliseNat defs t1- (t2', n2) <- normaliseNat defs t2- pure (NatEquality ct t1' t2' (mergeNormalised n1 n2))- | TyConApp tc [_,cmpNat,TyConApp tt1 [],TyConApp tt2 [],TyConApp ff1 []] <- t1- , tc == ordTyCon defs- , TyConApp cmpNatTc [x,y] <- cmpNat- , cmpNatTc == typeNatCmpTyCon- , tt1 == promotedTrueDataCon- , tt2 == promotedTrueDataCon- , ff1 == promotedFalseDataCon- , TyConApp tc' [] <- t2- -> do- (x', n1) <- normaliseNat defs x- (y', n2) <- normaliseNat defs y- let res | tc' == promotedTrueDataCon = pure (NatInequality ct x' y' True (mergeNormalised n1 n2))- | tc' == promotedFalseDataCon = pure (NatInequality ct x' y' False (mergeNormalised n1 n2))- | otherwise = fail "Nothing"- res- | TyConApp tc [TyConApp ordCondTc zs, _] <- t1- , tc == assertTC defs- , TyConApp tc' [] <- t2- , tc' == cTupleTyCon 0- , ordCondTc == ordTyCon defs- , [_,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- -> do- (x', n1) <- normaliseNat defs x- (y', n2) <- normaliseNat defs y- pure (NatInequality ct x' y' True (mergeNormalised n1 n2))- IrredPred (TyConApp tc [TyConApp ordCondTc zs, _])- | tc == assertTC defs- , ordCondTc == ordTyCon defs- , [_,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- -> do- (x', n1) <- normaliseNat defs x- (y', n2) <- normaliseNat defs y- pure (NatInequality ct x' y' True (mergeNormalised n1 n2))- _ -> fail "Nothing"- where- isNatKind :: Kind -> Bool- isNatKind = (`eqType` naturalTy)--createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM Ct-createWantedFromNormalised defs sct = do- let extractCtSides (NatEquality ct t1 t2 _) = (ct, reifyEOP defs t1, reifyEOP defs t2)- extractCtSides (NatInequality ct x y b _) =- let tc = if b then promotedTrueDataCon else promotedFalseDataCon- t1 = TyConApp (ordTyCon defs)- [ boolTy- , TyConApp typeNatCmpTyCon [reifyEOP defs x, reifyEOP defs y]- , TyConApp promotedTrueDataCon []- , TyConApp promotedTrueDataCon []- , TyConApp promotedFalseDataCon []- ]- t2 = TyConApp tc []- in (ct, t1, t2)- let (ct, t1, t2) = extractCtSides sct- newPredTy <- case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of- Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2])- Just (tc, [_, b]) | tc `hasKey` getUnique (assertTC defs) -> pure (mkTyConApp tc [t1,b])- _ -> error "Impossible: neither (<=?) nor Assert"- ev <- newWanted (ctLoc ct) newPredTy- let ctN = case ct of- CQuantCan qc -> CQuantCan (qc { qci_ev = ev})-#if MIN_VERSION_ghc(9,8,0)- CDictCan di -> CDictCan (di { di_ev = ev})- CIrredCan ir -> CIrredCan (ir { ir_ev = ev})- CEqCan eq -> CEqCan (eq { eq_ev = ev})- CNonCanonical _ -> CNonCanonical ev-#else- ctX -> ctX { cc_ev = ev }-#endif- return ctN--fromSolverConstraint :: SolverConstraint -> Ct-fromSolverConstraint (NatEquality ct _ _ _) = ct-fromSolverConstraint (NatInequality ct _ _ _ _) = ct--lookupExtraDefs :: TcPluginM ExtraDefs-lookupExtraDefs = do- ExtraDefs <$> look ''GHC.TypeLits.Extra.Max- <*> look ''GHC.TypeLits.Extra.Min- <*> pure typeNatDivTyCon- <*> pure typeNatModTyCon- <*> look ''GHC.TypeLits.Extra.FLog- <*> look ''GHC.TypeLits.Extra.CLog- <*> look ''GHC.TypeLits.Extra.Log- <*> look ''GHC.TypeLits.Extra.GCD- <*> look ''GHC.TypeLits.Extra.LCM- <*> look ''Data.Type.Ord.OrdCond- <*> look ''GHC.TypeError.Assert- where- look nm = tcLookupTyCon =<< lookupTHName nm--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---- Utils-evMagic :: Ct -> Maybe EvTerm-evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-extra" t1 t2)- IrredPred p ->- let t1 = mkTyConApp (cTupleTyCon 0) []- co = mkUnivCo (PluginProv "ghc-typelits-extra") Representational t1 p- dcApp = evId (dataConWrapId (cTupleDataCon 0))- in Just (evCast dcApp co)- _ -> Nothing
− src-pre-ghc-9.4/GHC/TypeLits/Extra/Solver.hs
@@ -1,347 +0,0 @@-{-|-Copyright : (C) 2015-2016, University of Twente-License : BSD2 (see the file LICENSE)-Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>--To use the plugin, add the--@-{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}-@--pragma to the header of your file---}--{-# LANGUAGE CPP #-}-{-# LANGUAGE TupleSections #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.Extra.Solver- ( plugin )-where---- external-import Control.Monad.Trans.Maybe (MaybeT (..))-import Data.Maybe (catMaybes)-import GHC.TcPluginM.Extra (evByFiat, lookupModule, lookupName- ,tracePlugin, newWanted)-#if MIN_VERSION_ghc(8,4,0)-import GHC.TcPluginM.Extra (flattenGivens)-#else-import Control.Monad ((<=<))-#endif---- GHC API-#if MIN_VERSION_ghc(9,0,0)-import GHC.Builtin.Names (eqPrimTyConKey, hasKey)-import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon)-#if MIN_VERSION_ghc(9,2,0)-import GHC.Builtin.Types (boolTy, naturalTy)-#else-import GHC.Builtin.Types (typeNatKind)-#endif-import GHC.Builtin.Types.Literals (typeNatDivTyCon, typeNatModTyCon)-#if MIN_VERSION_ghc(9,2,0)-import GHC.Builtin.Types.Literals (typeNatCmpTyCon)-#else-import GHC.Builtin.Types.Literals (typeNatLeqTyCon)-#endif-import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType)-import GHC.Core.TyCo.Rep (Type (..))-import GHC.Core.Type (Kind, eqType, mkTyConApp, splitTyConApp_maybe, typeKind)-import GHC.Data.FastString (fsLit)-import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)-import GHC.Tc.Plugin (TcPluginM, tcLookupTyCon, tcPluginTrace)-import GHC.Tc.Types (TcPlugin(..), TcPluginResult (..))-import GHC.Tc.Types.Constraint- (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev)-#if MIN_VERSION_ghc(9,2,0)-import GHC.Tc.Types.Constraint (Ct (CQuantCan), qci_ev)-#endif-import GHC.Tc.Types.Evidence (EvTerm)-import GHC.Types.Name.Occurrence (mkTcOcc)-import GHC.Unit.Module (mkModuleName)-import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)-#else-import FastString (fsLit)-import Module (mkModuleName)-import OccName (mkTcOcc)-import Outputable (Outputable (..), (<+>), ($$), text)-import Plugins (Plugin (..), defaultPlugin)-#if MIN_VERSION_ghc(8,6,0)-import Plugins (purePlugin)-#endif-import PrelNames (eqPrimTyConKey, hasKey)-import TcEvidence (EvTerm)-import TcPluginM (TcPluginM, tcLookupTyCon, tcPluginTrace)-import TcRnTypes (TcPlugin(..), TcPluginResult (..))-import Type (Kind, eqType, mkTyConApp, splitTyConApp_maybe)-import TyCoRep (Type (..))-import TysWiredIn (typeNatKind, promotedTrueDataCon, promotedFalseDataCon)-import TcTypeNats (typeNatLeqTyCon)-#if MIN_VERSION_ghc(8,4,0)-import TcTypeNats (typeNatDivTyCon, typeNatModTyCon)-#else-import TcPluginM (zonkCt)-#endif--#if MIN_VERSION_ghc(8,10,0)-import Constraint (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev)-import Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType)-import Type (typeKind)-#else-import TcRnTypes (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev)-import TcType (typeKind)-import Type (EqRel (NomEq), PredTree (EqPred), classifyPredType)-#endif-#endif---- internal-import GHC.TypeLits.Extra.Solver.Operations-import GHC.TypeLits.Extra.Solver.Unify--#if MIN_VERSION_ghc(9,2,0)-typeNatKind :: Type-typeNatKind = naturalTy-#endif---- | A solver implement as a type-checker plugin for:------ * 'Div': type-level 'div'------ * 'Mod': type-level 'mod'------ * 'FLog': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"------ * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"------ * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"------ * 'GCD': a type-level 'gcd'------ * 'LCM': a type-level 'lcm'------ To use the plugin, add------ @--- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}--- @------ To the header of your file.-plugin :: Plugin-plugin- = defaultPlugin- { tcPlugin = const $ Just normalisePlugin-#if MIN_VERSION_ghc(8,6,0)- , pluginRecompile = purePlugin-#endif- }--normalisePlugin :: TcPlugin-normalisePlugin = tracePlugin "ghc-typelits-extra"- TcPlugin { tcPluginInit = lookupExtraDefs- , tcPluginSolve = decideEqualSOP- , tcPluginStop = const (return ())- }--decideEqualSOP :: ExtraDefs -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult-decideEqualSOP _ _givens _deriveds [] = return (TcPluginOk [] [])-decideEqualSOP defs givens _deriveds wanteds = do- -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out- let wanteds' = filter isWantedCt wanteds- unit_wanteds <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) wanteds'- case unit_wanteds of- [] -> return (TcPluginOk [] [])- _ -> do-#if MIN_VERSION_ghc(8,4,0)- unit_givens <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) (givens ++ flattenGivens givens)-#else- unit_givens <- catMaybes <$> mapM ((runMaybeT . toSolverConstraint defs) <=< zonkCt) givens-#endif- sr <- simplifyExtra defs (unit_givens ++ unit_wanteds)- tcPluginTrace "normalised" (ppr sr)- case sr of- Simplified evs new -> return (TcPluginOk (filter (isWantedCt . snd) evs) new)- Impossible eq -> return (TcPluginContradiction [fromSolverConstraint eq])--data SolverConstraint- = NatEquality Ct ExtraOp ExtraOp Normalised- | NatInequality Ct ExtraOp ExtraOp Bool Normalised--instance Outputable SolverConstraint where- ppr (NatEquality ct op1 op2 norm) = text "NatEquality" $$ ppr ct $$ ppr op1 $$ ppr op2 $$ ppr norm- ppr (NatInequality _ op1 op2 b norm) = text "NatInequality" $$ ppr op1 $$ ppr op2 $$ ppr b $$ ppr norm--data SimplifyResult- = Simplified [(EvTerm,Ct)] [Ct]- | Impossible SolverConstraint--instance Outputable SimplifyResult where- ppr (Simplified evs new) = text "Simplified" $$ text "Solved:" $$ ppr evs $$ text "New:" $$ ppr new- ppr (Impossible sct) = text "Impossible" <+> ppr sct--simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM SimplifyResult-simplifyExtra defs eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] eqs- where- simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult- simples evs news [] = return (Simplified (catMaybes evs) news)- simples evs news (eq@(NatEquality ct u v norm):eqs') = do- ur <- unifyExtra ct u v- tcPluginTrace "unifyExtra result" (ppr ur)- case ur of- Win -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs'- Lose | null evs && null eqs' -> return (Impossible eq)- _ | norm == Normalised && isWantedCt ct -> do- newCt <- createWantedFromNormalised defs eq- simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs'- Lose -> simples evs news eqs'- Draw -> simples evs news eqs'- simples evs news (eq@(NatInequality ct u v b norm):eqs') = do- tcPluginTrace "unifyExtra leq result" (ppr (u,v,b))- case (u,v) of- (I i,I j)- | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs'- | otherwise -> return (Impossible eq)- (p, Max x y)- | b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs'-- -- transform: q ~ Max x y => (p <=? q ~ True)- -- to: (p <=? Max x y) ~ True- -- and try to solve that along with the rest of the eqs'- (p, q@(V _))- | b -> case findMax q eqs of- Just m -> simples evs news (NatInequality ct p m b norm:eqs')- Nothing -> simples evs news eqs'- _ | norm == Normalised && isWantedCt ct -> do- newCt <- createWantedFromNormalised defs eq- simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs'- _ -> simples evs news eqs'-- -- look for given constraint with the form: c ~ Max x y- findMax :: ExtraOp -> [SolverConstraint] -> Maybe ExtraOp- findMax c = go- where- go [] = Nothing- go ((NatEquality ct a b@(Max _ _) _) :_)- | c == a && not (isWantedCt ct)- = Just b- go ((NatEquality ct a@(Max _ _) b _) :_)- | c == b && not (isWantedCt ct)- = Just a- go (_:rest) = go rest----- Extract the Nat equality constraints-toSolverConstraint :: ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint-toSolverConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2- | isNatKind (typeKind t1) || isNatKind (typeKind t2)- -> do- (t1', n1) <- normaliseNat defs t1- (t2', n2) <- normaliseNat defs t2- pure (NatEquality ct t1' t2' (mergeNormalised n1 n2))-#if MIN_VERSION_ghc(9,2,0)- | TyConApp tc [_,cmpNat,TyConApp tt1 [],TyConApp tt2 [],TyConApp ff1 []] <- t1- , tc == ordTyCon defs- , TyConApp cmpNatTc [x,y] <- cmpNat- , cmpNatTc == typeNatCmpTyCon- , tt1 == promotedTrueDataCon- , tt2 == promotedTrueDataCon- , ff1 == promotedFalseDataCon-#else- | TyConApp tc [x,y] <- t1- , tc == typeNatLeqTyCon-#endif- , TyConApp tc' [] <- t2- -> do- (x', n1) <- normaliseNat defs x- (y', n2) <- normaliseNat defs y- let res | tc' == promotedTrueDataCon = pure (NatInequality ct x' y' True (mergeNormalised n1 n2))- | tc' == promotedFalseDataCon = pure (NatInequality ct x' y' False (mergeNormalised n1 n2))- | otherwise = fail "Nothing"- res- _ -> fail "Nothing"- where- isNatKind :: Kind -> Bool- isNatKind = (`eqType` typeNatKind)--createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM Ct-createWantedFromNormalised defs sct = do- let extractCtSides (NatEquality ct t1 t2 _) = (ct, reifyEOP defs t1, reifyEOP defs t2)- extractCtSides (NatInequality ct x y b _) =- let tc = if b then promotedTrueDataCon else promotedFalseDataCon-#if MIN_VERSION_ghc(9,2,0)- t1 = TyConApp (ordTyCon defs)- [ boolTy- , TyConApp typeNatCmpTyCon [reifyEOP defs x, reifyEOP defs y]- , TyConApp promotedTrueDataCon []- , TyConApp promotedTrueDataCon []- , TyConApp promotedFalseDataCon []- ]-#else- t1 = TyConApp typeNatLeqTyCon [reifyEOP defs x, reifyEOP defs y]-#endif- t2 = TyConApp tc []- in (ct, t1, t2)- let (ct, t1, t2) = extractCtSides sct- newPredTy <- case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of- Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2])- _ -> fail "Nothing"- ev <- newWanted (ctLoc ct) newPredTy- let ctN = case ct of-#if MIN_VERSION_ghc(9,2,0)- CQuantCan qc -> CQuantCan (qc { qci_ev = ev})-#endif- ctX -> ctX { cc_ev = ev }- return ctN--fromSolverConstraint :: SolverConstraint -> Ct-fromSolverConstraint (NatEquality ct _ _ _) = ct-fromSolverConstraint (NatInequality ct _ _ _ _) = ct--lookupExtraDefs :: TcPluginM ExtraDefs-lookupExtraDefs = do- md <- lookupModule myModule myPackage-#if MIN_VERSION_ghc(9,2,0)- md2 <- lookupModule ordModule basePackage-#endif- ExtraDefs <$> look md "Max"- <*> look md "Min"-#if MIN_VERSION_ghc(8,4,0)- <*> pure typeNatDivTyCon- <*> pure typeNatModTyCon-#else- <*> look md "Div"- <*> look md "Mod"-#endif- <*> look md "FLog"- <*> look md "CLog"- <*> look md "Log"- <*> look md "GCD"- <*> look md "LCM"-#if MIN_VERSION_ghc(9,2,0)- <*> look md2 "OrdCond"- <*> look md2 "OrdCond"-#else- <*> pure typeNatLeqTyCon- <*> pure typeNatLeqTyCon-#endif- where- look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)- myModule = mkModuleName "GHC.TypeLits.Extra"- myPackage = fsLit "ghc-typelits-extra"-#if MIN_VERSION_ghc(9,2,0)- ordModule = mkModuleName "Data.Type.Ord"- basePackage = fsLit "base"-#endif---- Utils-evMagic :: Ct -> Maybe EvTerm-evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-extra" t1 t2)- _ -> Nothing
+ src/GHC/TypeLits/Extra/Solver.hs view
@@ -0,0 +1,256 @@+{-|+Copyright : (C) 2015-2016, University of Twente+License : BSD2 (see the file LICENSE)+Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>++To use the plugin, add the++@+{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}+@++pragma to the header of your file++-}++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TemplateHaskellQuotes #-}++{-# OPTIONS_HADDOCK show-extensions #-}++module GHC.TypeLits.Extra.Solver+ ( plugin )+where++-- external+import Control.Monad.Trans.Maybe (MaybeT (..))+import Data.Maybe (catMaybes)++-- ghc-tcplugin-api+import GHC.TcPlugin.API+import GHC.TcPlugin.API.TyConSubst++-- GHC API+import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon)+import GHC.Core.DataCon (dataConWrapId)+import GHC.Core.TyCo.Rep (Type (..), TyLit (..))+import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)+import GHC.Tc.Types.Constraint (isWantedCt)+import GHC.Utils.Outputable ((<+>), ($$), text, vcat)++-- ghc-typelits-natnormalise+import GHC.TypeLits.Normalise.Compat++-- internal+import GHC.TypeLits.Extra.Solver.Compat+import GHC.TypeLits.Extra.Solver.Operations+import GHC.TypeLits.Extra.Solver.Unify++-- | A solver implement as a type-checker plugin for:+--+-- * 'Div': type-level 'div'+--+-- * 'Mod': type-level 'mod'+--+-- * 'FLog': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"+--+-- * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"+--+-- * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"+--+-- * 'GCD': a type-level 'gcd'+--+-- * 'LCM': a type-level 'lcm'+--+-- To use the plugin, add+--+-- @+-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}+-- @+--+-- To the header of your file.+plugin :: Plugin+plugin+ = defaultPlugin+ { tcPlugin = const (pure (mkTcPlugin normalisePlugin))+ , pluginRecompile = purePlugin+ }++normalisePlugin :: TcPlugin+normalisePlugin =+ TcPlugin { tcPluginInit = lookupExtraDefs+ , tcPluginSolve = decideEqualSOP+ , tcPluginRewrite = extraRewrite+ , tcPluginStop = const (return ())+ }++extraRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter+extraRewrite defs = listToUFM+ [ (gcdTyCon defs, gcdRewrite)+ , (lcmTyCon defs, lcmRewrite)+ ]+ where+ gcdRewrite _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $+ TcPluginRewriteTo (reduce (gcdTyCon defs) args (LitTy (NumTyLit (i `gcd` j)))) []+ gcdRewrite _ _ = pure TcPluginNoRewrite++ lcmRewrite _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $+ TcPluginRewriteTo (reduce (lcmTyCon defs) args (LitTy (NumTyLit (i `lcm` j)))) []+ lcmRewrite _ _ = pure TcPluginNoRewrite++ reduce tc args res = Reduction co res+ where+ co = mkPluginUnivCo "ghc-typelits-extra" Nominal []+ (mkTyConApp tc args) res+++decideEqualSOP :: ExtraDefs -> [Ct] -> [Ct] -> TcPluginM 'Solve TcPluginSolveResult+decideEqualSOP _ _givens [] = return (TcPluginOk [] [])+decideEqualSOP defs givens wanteds = do+ let givensTyConSubst = mkTyConSubst givens+ unit_wanteds <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs givensTyConSubst) wanteds+ case unit_wanteds of+ [] -> return (TcPluginOk [] [])+ _ -> do+ unit_givens <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs givensTyConSubst) givens+ sr <- simplifyExtra defs (unit_givens ++ unit_wanteds)+ tcPluginTrace "ghc-typelits-extra Wanteds {" $+ vcat [ text "givens:" <+> ppr givens+ , text "unit_givens" <+> ppr unit_givens+ , text $ replicate 80 '-'+ , text "wanteds:" <+> ppr wanteds+ , text "unit_wanteds:" <+> ppr unit_wanteds+ ]+ tcPluginTrace "normalised" (ppr sr)+ case sr of+ Simplified evs new -> return (TcPluginOk (filter (isWantedCt . snd) evs) new)+ Impossible eq -> return (TcPluginContradiction [fromSolverConstraint eq])++data SolverConstraint+ = NatEquality Ct ExtraOp ExtraOp Normalised+ | NatInequality Ct [Coercion] ExtraOp ExtraOp Bool Normalised++instance Outputable SolverConstraint where+ ppr (NatEquality ct op1 op2 norm) =+ text "NatEquality" $$ ppr ct $$ ppr op1 $$ ppr op2 $$ ppr norm+ ppr (NatInequality _ _ op1 op2 b norm) =+ text "NatInequality" $$ ppr op1 $$ ppr op2 $$ ppr b $$ ppr norm++data SimplifyResult+ = Simplified [(EvTerm,Ct)] [Ct]+ | Impossible SolverConstraint++instance Outputable SimplifyResult where+ ppr (Simplified evs new) =+ text "Simplified" $$ text "Solved:" $$ ppr evs $$ text "New:" $$ ppr new+ ppr (Impossible sct) =+ text "Impossible" <+> ppr sct++simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult+simplifyExtra defs eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] eqs+ where+ simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult+ simples evs news [] = return (Simplified (catMaybes evs) news)+ simples evs news (eq@(NatEquality ct u v norm):eqs') = do+ ur <- unifyExtra ct u v+ tcPluginTrace "unifyExtra result" (ppr ur)+ let evM = evMagic (ordTyCons defs) ct (depsFromNormalised norm)+ case ur of+ Win -> simples (fmap (,ct) evM:evs) news eqs'+ Lose | null evs && null eqs' -> return (Impossible eq)+ _ | Normalised {} <- norm+ , isWantedCt ct -> do+ newCt <- createWantedFromNormalised defs eq+ simples (fmap (,ct) evM:evs) (newCt:news) eqs'+ Lose -> simples evs news eqs'+ Draw -> simples evs news eqs'+ simples evs news (eq@(NatInequality ct deps u v b norm):eqs') = do+ tcPluginTrace "unifyExtra leq result" (ppr (u,v,b))+ let evM = evMagic (ordTyCons defs) ct (deps <> depsFromNormalised norm)+ case (u,v) of+ (I i,I j)+ | (i <= j) == b+ -> simples (fmap (,ct) evM:evs) news eqs'+ | otherwise -> return (Impossible eq)+ (p, Max x y)+ | b && (p == x || p == y)+ -> simples (fmap (,ct) evM:evs) news eqs'++ -- transform: q ~ Max x y => (p <=? q ~ True)+ -- to: (p <=? Max x y) ~ True+ -- and try to solve that along with the rest of the eqs'+ (p, q@(V _))+ | b -> case findMax q eqs of+ Just (i,m) ->+ simples evs news+ (NatInequality ct (i:deps) p m b norm:eqs')+ Nothing -> simples evs news eqs'+ _ | Normalised {} <- norm+ , isWantedCt ct -> do+ newCt <- createWantedFromNormalised defs eq+ simples (fmap (,ct) evM:evs) (newCt:news) eqs'+ _ -> simples evs news eqs'++ -- look for given constraint with the form: c ~ Max x y+ findMax :: ExtraOp -> [SolverConstraint] -> Maybe (Coercion, ExtraOp)+ findMax c = go+ where+ go [] = Nothing+ go ((NatEquality ct a b@(Max _ _) _) :_)+ | c == a && not (isWantedCt ct)+ = Just (ctEvCoercion (ctEvidence ct), b)+ go ((NatEquality ct a@(Max _ _) b _) :_)+ | c == b && not (isWantedCt ct)+ = Just (ctEvCoercion (ctEvidence ct), a)+ go (_:rest) = go rest+++-- Extract the Nat equality constraints+toSolverConstraint :: ExtraDefs -> TyConSubst -> Ct -> MaybeT (TcPluginM 'Solve) SolverConstraint+toSolverConstraint defs givensTyConSubst ct =+ case isNatRel (ordTyCons defs) givensTyConSubst ty0 of+ Nothing -> fail "Nothing"+ Just (((t1,t2),leqM),deps) -> do+ (t1', n1) <- normaliseNat defs t1+ (t2', n2) <- normaliseNat defs t2+ case leqM of+ Nothing ->+ pure (NatEquality ct t1' t2' (mergeNormalised n1 n2))+ Just b ->+ pure (NatInequality ct deps t1' t2' b (mergeNormalised n1 n2))+ where+ ty0 = ctEvPred (ctEvidence ct)++createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM 'Solve Ct+createWantedFromNormalised defs sct = do+ let extractCtSides (NatEquality ct t1 t2 _) = (ct, reifyEOP defs t1, reifyEOP defs t2)+ extractCtSides (NatInequality ct _ x y b _) =+ let t1 = mkLeqQNat (ordTyCons defs) (reifyEOP defs x) (reifyEOP defs y)+ tb = if b then promotedTrueDataCon else promotedFalseDataCon+ t2 = TyConApp tb []+ in (ct, t1, t2)+ let (ct, t1, t2) = extractCtSides sct+ newPredTy <- toLeqPredType (ordTyCons defs) ct t1 t2+ ev <- newWanted (ctLoc ct) newPredTy+ return (setCtEv ct ev)++fromSolverConstraint :: SolverConstraint -> Ct+fromSolverConstraint (NatEquality ct _ _ _) = ct+fromSolverConstraint (NatInequality ct _ _ _ _ _) = ct++-- Utils+evMagic :: LookedUpTyCons -> Ct -> [Coercion] -> Maybe EvTerm+evMagic tcs ct deps = case classifyPredType $ ctEvPred $ ctEvidence ct of+ EqPred NomEq t1 t2 ->+ let ctEv = mkPluginUnivCo "ghc-typelits-extra" Nominal deps t1 t2+ in Just (EvExpr (Coercion ctEv))+ IrredPred p ->+ let t1 = mkTyConApp (c0TyCon tcs) []+ co = mkPluginUnivCo "ghc-typelits-extra" Representational deps t1 p+ dcApp = evId (dataConWrapId (c0DataCon tcs))+ in Just (EvExpr (evCast dcApp co))+ _ -> Nothing
+ src/GHC/TypeLits/Extra/Solver/Compat.hs view
@@ -0,0 +1,99 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskellQuotes #-}++{-# OPTIONS_GHC -Wno-unused-matches #-}++module GHC.TypeLits.Extra.Solver.Compat where++import qualified Language.Haskell.TH as TH++import GHC.TcPlugin.API++import GHC.TypeLits.Normalise.Compat++import GHC.Builtin.Names+ ( eqPrimTyConKey, hasKey+ )+#if MIN_VERSION_ghc(9,1,0)+import GHC.Builtin.Types+ ( boolTy, promotedFalseDataCon, promotedTrueDataCon+ )+#endif+import GHC.Builtin.Types.Literals+ ( typeNatDivTyCon, typeNatModTyCon+ )+#if MIN_VERSION_ghc(9,8,0)+import GHC.Tc.Types.Constraint+ ( DictCt(..), EqCt(..), IrredCt(..)+ )+#endif+import GHC.Tc.Types.Constraint+ ( Ct (..), qci_ev+ )++import qualified GHC.TypeLits.Extra++data ExtraDefs = ExtraDefs+ { maxTyCon :: TyCon+ , minTyCon :: TyCon+ , divTyCon :: TyCon+ , modTyCon :: TyCon+ , flogTyCon :: TyCon+ , clogTyCon :: TyCon+ , logTyCon :: TyCon+ , gcdTyCon :: TyCon+ , lcmTyCon :: TyCon+ , ordTyCons :: LookedUpTyCons+ }++-- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat"+lookupExtraDefs :: TcPluginM 'Init ExtraDefs+lookupExtraDefs = do+ ExtraDefs <$> look ''GHC.TypeLits.Extra.Max+ <*> look ''GHC.TypeLits.Extra.Min+ <*> pure typeNatDivTyCon+ <*> pure typeNatModTyCon+ <*> look ''GHC.TypeLits.Extra.FLog+ <*> look ''GHC.TypeLits.Extra.CLog+ <*> look ''GHC.TypeLits.Extra.Log+ <*> look ''GHC.TypeLits.Extra.GCD+ <*> look ''GHC.TypeLits.Extra.LCM+ <*> lookupTyCons+ where+ look :: TH.Name -> TcPluginM 'Init TyCon+ look nm = tcLookupTyCon =<< lookupTHName nm++setCtEv :: Ct -> CtEvidence -> Ct+setCtEv ct ev = case ct of+ CQuantCan qc -> CQuantCan (qc { qci_ev = ev})+#if MIN_VERSION_ghc(9,8,0)+ CDictCan di -> CDictCan (di { di_ev = ev})+ CIrredCan ir -> CIrredCan (ir { ir_ev = ev})+ CEqCan eq -> CEqCan (eq { eq_ev = ev})+ CNonCanonical _ -> CNonCanonical ev+#else+ ctX -> ctX { cc_ev = ev }+#endif++mkLeqQNat :: LookedUpTyCons -> Type -> Type -> Type+mkLeqQNat tcs x y =+#if MIN_VERSION_ghc(9,1,0)+ mkTyConApp (ordCondTyCon tcs)+ [ boolTy+ , mkTyConApp (cmpNatTyCon tcs) [x,y]+ , mkTyConApp promotedTrueDataCon []+ , mkTyConApp promotedTrueDataCon []+ , mkTyConApp promotedFalseDataCon []+ ]+#else+ mkTyConApp (leqQNatTyCon tcs) [x, y]+#endif++toLeqPredType :: Monad m => LookedUpTyCons -> Ct -> Type -> Type -> m PredType+toLeqPredType defs ct t1 t2 = case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of+ Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2])+#if MIN_VERSION_ghc(9,3,0)+ Just (tc, [_, b]) | tc == assertTyCon defs -> pure (mkTyConApp tc [t1,b])+#endif+ _ -> error "Impossible: neither (<=?) nor Assert"
src/GHC/TypeLits/Extra/Solver/Operations.hs view
@@ -10,10 +10,10 @@ module GHC.TypeLits.Extra.Solver.Operations ( ExtraOp (..)- , ExtraDefs (..) , Normalised (..) , NormaliseResult , mergeNormalised+ , depsFromNormalised , reifyEOP , mergeMax , mergeMin@@ -39,32 +39,33 @@ import GHC.Integer.Logarithms (integerLogBase#) import GHC.TypeLits.Normalise.Unify (CType (..), normaliseNat, isNatural) +-- ghc-tcplugin-api+import GHC.TcPlugin.API+ -- GHC API-#if MIN_VERSION_ghc(9,0,0) import GHC.Builtin.Types.Literals (typeNatExpTyCon, typeNatSubTyCon)-import GHC.Core.TyCon (TyCon)-import GHC.Core.Type (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy)-import GHC.Utils.Outputable (Outputable (..), (<+>), integer, text)-#else-import Outputable (Outputable (..), (<+>), integer, text)-import TcTypeNats (typeNatExpTyCon, typeNatSubTyCon)-import TyCon (TyCon)-import Type (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy)-#endif+import GHC.Utils.Outputable ((<+>), integer, text) +-- internal+import GHC.TypeLits.Extra.Solver.Compat+ -- | Indicates whether normalisation has occured-data Normalised = Normalised | Untouched- deriving Eq+data Normalised = Normalised [Coercion] | Untouched instance Outputable Normalised where- ppr Normalised = text "Normalised"- ppr Untouched = text "Untouched"+ ppr Normalised{} = text "Normalised"+ ppr Untouched = text "Untouched" mergeNormalised :: Normalised -> Normalised -> Normalised-mergeNormalised Normalised _ = Normalised-mergeNormalised _ Normalised = Normalised-mergeNormalised _ _ = Untouched+mergeNormalised (Normalised d1) (Normalised d2) = Normalised (d1 ++ d2)+mergeNormalised (Normalised d) _ = Normalised d+mergeNormalised _ (Normalised d) = Normalised d+mergeNormalised _ _ = Untouched +depsFromNormalised :: Normalised -> [Coercion]+depsFromNormalised (Normalised deps) = deps+depsFromNormalised Untouched = []+ -- | A normalise result contains the ExtraOp and a flag that indicates whether any expression -- | was normalised within the ExtraOp. type NormaliseResult = (ExtraOp, Normalised)@@ -100,20 +101,6 @@ ppr (LCM x y) = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")" ppr (Exp x y) = text "Exp (" <+> ppr x <+> text "," <+> ppr y <+> text ")" -data ExtraDefs = ExtraDefs- { maxTyCon :: TyCon- , minTyCon :: TyCon- , divTyCon :: TyCon- , modTyCon :: TyCon- , flogTyCon :: TyCon- , clogTyCon :: TyCon- , logTyCon :: TyCon- , gcdTyCon :: TyCon- , lcmTyCon :: TyCon- , ordTyCon :: TyCon- , assertTC :: TyCon- }- reifyEOP :: ExtraDefs -> ExtraOp -> Type reifyEOP _ (I i) = mkNumLitTy i reifyEOP _ (V v) = mkTyVarTy v@@ -140,78 +127,66 @@ ,reifyEOP defs y] mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult-mergeMax _ (I 0) y = (y, Normalised)-mergeMax _ x (I 0) = (x, Normalised)+mergeMax _ (I 0) y = (y, Normalised [])+mergeMax _ x (I 0) = (x, Normalised []) mergeMax defs x y = let x' = reifyEOP defs x y' = reifyEOP defs y- z = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))-#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)+ (z,deps) = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x']))) in case runWriterT (isNatural z) of- Just (True , cs) | Set.null cs -> (y, Normalised)- Just (False, cs) | Set.null cs -> (x, Normalised)-#else- in case isNatural z of- Just True -> (y, Normalised)- Just False -> (x, Normalised)-#endif+ Just (True , cs) | Set.null cs -> (y, Normalised deps)+ Just (False, cs) | Set.null cs -> (x, Normalised deps) _ -> (Max x y, Untouched) mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult mergeMin defs x y = let x' = reifyEOP defs x y' = reifyEOP defs y- z = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))-#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)+ (z,deps) = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x']))) in case runWriterT (isNatural z) of- Just (True, cs) | Set.null cs -> (x, Normalised)- Just (False,cs) | Set.null cs -> (y, Normalised)-#else- in case isNatural z of- Just True -> (x, Normalised)- Just False -> (y, Normalised)-#endif+ Just (True, cs) | Set.null cs -> (x, Normalised deps)+ Just (False,cs) | Set.null cs -> (y, Normalised deps) _ -> (Min x y, Untouched) mergeDiv :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeDiv _ (I 0) = Nothing-mergeDiv (I i) (I j) = Just (I (div i j), Normalised)+mergeDiv (I i) (I j) = Just (I (div i j), Normalised []) mergeDiv x y = Just (Div x y, Untouched) mergeMod :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeMod _ (I 0) = Nothing-mergeMod (I i) (I j) = Just (I (mod i j), Normalised)+mergeMod (I i) (I j) = Just (I (mod i j), Normalised []) mergeMod x y = Just (Mod x y, Untouched) mergeFLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeFLog (I i) _ | i < 2 = Nothing-mergeFLog i (Exp j k) | i == j = Just (k, Normalised)-mergeFLog (I i) (I j) = fmap (\r -> (I r, Normalised)) (flogBase i j)+mergeFLog i (Exp j k) | i == j = Just (k, Normalised [])+mergeFLog (I i) (I j) = fmap (\r -> (I r, Normalised [])) (flogBase i j) mergeFLog x y = Just (FLog x y, Untouched) mergeCLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeCLog (I i) _ | i < 2 = Nothing-mergeCLog i (Exp j k) | i == j = Just (k, Normalised)-mergeCLog (I i) (I j) = fmap (\r -> (I r, Normalised)) (clogBase i j)+mergeCLog i (Exp j k) | i == j = Just (k, Normalised [])+mergeCLog (I i) (I j) = fmap (\r -> (I r, Normalised [])) (clogBase i j) mergeCLog x y = Just (CLog x y, Untouched) mergeLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeLog (I i) _ | i < 2 = Nothing-mergeLog b (Exp b' y) | b == b' = Just (y, Normalised)-mergeLog (I i) (I j) = fmap (\r -> (I r, Normalised)) (exactLogBase i j)+mergeLog b (Exp b' y) | b == b' = Just (y, Normalised [])+mergeLog (I i) (I j) = fmap (\r -> (I r, Normalised [])) (exactLogBase i j) mergeLog x y = Just (Log x y, Untouched) mergeGCD :: ExtraOp -> ExtraOp -> NormaliseResult-mergeGCD (I i) (I j) = (I (gcd i j), Normalised)+mergeGCD (I i) (I j) = (I (gcd i j), Normalised []) mergeGCD x y = (GCD x y, Untouched) mergeLCM :: ExtraOp -> ExtraOp -> NormaliseResult-mergeLCM (I i) (I j) = (I (lcm i j), Normalised)+mergeLCM (I i) (I j) = (I (lcm i j), Normalised []) mergeLCM x y = (LCM x y, Untouched) mergeExp :: ExtraOp -> ExtraOp -> NormaliseResult-mergeExp (I i) (I j) = (I (i^j), Normalised)-mergeExp b (Log b' y) | b == b' = (y, Normalised)+mergeExp (I i) (I j) = (I (i^j), Normalised [])+mergeExp b (Log b' y) | b == b' = (y, Normalised []) mergeExp x y = (Exp x y, Untouched) -- | \x y -> logBase x y, x > 1 && y > 0
src/GHC/TypeLits/Extra/Solver/Unify.hs view
@@ -5,11 +5,10 @@ Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> -} -{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-} module GHC.TypeLits.Extra.Solver.Unify- ( ExtraDefs (..)- , UnifyResult (..)+ ( UnifyResult (..) , NormaliseResult , normaliseNat , unifyExtra@@ -23,37 +22,25 @@ import Data.Function (on) import GHC.TypeLits.Normalise.Unify (CType (..)) +-- ghc-tcplugin-api+import GHC.TcPlugin.API+ -- GHC API-#if MIN_VERSION_ghc(9,0,0) import GHC.Builtin.Types.Literals (typeNatExpTyCon) import GHC.Core.TyCo.Rep (Type (..), TyLit (..))-import GHC.Core.Type (TyVar, coreView)-import GHC.Tc.Plugin (TcPluginM, tcPluginTrace)-import GHC.Tc.Types.Constraint (Ct)+import GHC.Core.Type (coreView) import GHC.Types.Unique.Set (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)-import GHC.Utils.Outputable (Outputable (..), ($$), text)-#else-import Outputable (Outputable (..), ($$), text)-import TcPluginM (TcPluginM, tcPluginTrace)-import TcTypeNats (typeNatExpTyCon)-import Type (TyVar, coreView)-import TyCoRep (Type (..), TyLit (..))-import UniqSet (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)-#if MIN_VERSION_ghc(8,10,0)-import Constraint (Ct)-#else-import TcRnMonad (Ct)-#endif-#endif+import GHC.Utils.Outputable (($$), text) -- internal+import GHC.TypeLits.Extra.Solver.Compat import GHC.TypeLits.Extra.Solver.Operations mergeNormResWith- :: (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)- -> MaybeT TcPluginM NormaliseResult- -> MaybeT TcPluginM NormaliseResult- -> MaybeT TcPluginM NormaliseResult+ :: (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)+ -> MaybeT (TcPluginM 'Solve) NormaliseResult+ -> MaybeT (TcPluginM 'Solve) NormaliseResult+ -> MaybeT (TcPluginM 'Solve) NormaliseResult mergeNormResWith f x y = do (x', n1) <- x (y', n2) <- y@@ -61,53 +48,66 @@ pure (res, n1 `mergeNormalised` n2 `mergeNormalised` n3) -normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult-normaliseNat defs ty | Just ty1 <- coreView ty = normaliseNat defs ty1-normaliseNat _ (TyVarTy v) = pure (V v, Untouched)-normaliseNat _ (LitTy (NumTyLit i)) = pure (I i, Untouched)-normaliseNat defs (TyConApp tc [x,y])- | tc == maxTyCon defs = mergeNormResWith (\x' y' -> return (mergeMax defs x' y'))- (normaliseNat defs x)- (normaliseNat defs y)- | tc == minTyCon defs = mergeNormResWith (\x' y' -> return (mergeMin defs x' y'))- (normaliseNat defs x)- (normaliseNat defs y)- | tc == divTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeDiv x' y')))- (normaliseNat defs x)- (normaliseNat defs y)- | tc == modTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeMod x' y')))- (normaliseNat defs x)- (normaliseNat defs y)- | tc == flogTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeFLog x' y')))- (normaliseNat defs x)- (normaliseNat defs y)- | tc == clogTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeCLog x' y')))- (normaliseNat defs x)- (normaliseNat defs y)- | tc == logTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeLog x' y')))- (normaliseNat defs x)- (normaliseNat defs y)- | tc == gcdTyCon defs = mergeNormResWith (\x' y' -> return (mergeGCD x' y'))- (normaliseNat defs x)- (normaliseNat defs y)- | tc == lcmTyCon defs = mergeNormResWith (\x' y' -> return (mergeLCM x' y'))- (normaliseNat defs x)- (normaliseNat defs y)- | tc == typeNatExpTyCon = mergeNormResWith (\x' y' -> return (mergeExp x' y'))- (normaliseNat defs x)- (normaliseNat defs y)+normaliseNat :: ExtraDefs -> Type -> MaybeT (TcPluginM 'Solve) NormaliseResult+normaliseNat defs = go+ where+ go :: Type -> MaybeT (TcPluginM 'Solve) NormaliseResult+ go ty | Just ty1 <- coreView ty = go ty1+ go (TyVarTy v) = pure (V v, Untouched)+ go (LitTy (NumTyLit i)) = pure (I i, Untouched)+ go (TyConApp tc [x,y])+ | tc == maxTyCon defs+ = mergeNormResWith (\x' y' -> return (mergeMax defs x' y'))+ (go x)+ (go y)+ | tc == minTyCon defs+ = mergeNormResWith (\x' y' -> return (mergeMin defs x' y'))+ (go x)+ (go y)+ | tc == divTyCon defs+ = mergeNormResWith (\x' y' -> MaybeT (return (mergeDiv x' y')))+ (go x)+ (go y)+ | tc == modTyCon defs+ = mergeNormResWith (\x' y' -> MaybeT (return (mergeMod x' y')))+ (go x)+ (go y)+ | tc == flogTyCon defs+ = mergeNormResWith (\x' y' -> MaybeT (return (mergeFLog x' y')))+ (go x)+ (go y)+ | tc == clogTyCon defs+ = mergeNormResWith (\x' y' -> MaybeT (return (mergeCLog x' y')))+ (go x)+ (go y)+ | tc == logTyCon defs+ = mergeNormResWith (\x' y' -> MaybeT (return (mergeLog x' y')))+ (go x)+ (go y)+ | tc == gcdTyCon defs+ = mergeNormResWith (\x' y' -> return (mergeGCD x' y'))+ (go x)+ (go y)+ | tc == lcmTyCon defs+ = mergeNormResWith (\x' y' -> return (mergeLCM x' y'))+ (go x)+ (go y)+ | tc == typeNatExpTyCon+ = mergeNormResWith (\x' y' -> return (mergeExp x' y'))+ (go x)+ (go y) -normaliseNat defs (TyConApp tc tys) = do- let mergeExtraOp [] = []- mergeExtraOp ((Just (op, Normalised), _):xs) = reifyEOP defs op:mergeExtraOp xs- mergeExtraOp ((_, ty):xs) = ty:mergeExtraOp xs+ go (TyConApp tc tys) = do+ let mergeExtraOp [] = []+ mergeExtraOp ((Just (op, Normalised []), _):xs) = reifyEOP defs op:mergeExtraOp xs+ mergeExtraOp ((_, ty):xs) = ty:mergeExtraOp xs - normResults <- lift (sequence (runMaybeT . normaliseNat defs <$> tys))- let anyNormalised = foldr mergeNormalised Untouched (snd <$> catMaybes normResults)- let tys' = mergeExtraOp (zip normResults tys)- pure (C (CType (TyConApp tc tys')), anyNormalised)+ normResults <- lift (sequence (runMaybeT . go <$> tys))+ let anyNormalised = foldr mergeNormalised Untouched (snd <$> catMaybes normResults)+ let tys' = mergeExtraOp (zip normResults tys)+ pure (C (CType (TyConApp tc tys')), anyNormalised) -normaliseNat _ t = return (C (CType t), Untouched)+ go t = return (C (CType t), Untouched) -- | Result of comparing two 'SOP' terms, returning a potential substitution -- list under which the two terms are equal.@@ -121,7 +121,7 @@ ppr Lose = text "Lose" ppr Draw = text "Draw" -unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult+unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM 'Solve UnifyResult unifyExtra ct u v = do tcPluginTrace "unifyExtra" (ppr ct $$ ppr u $$ ppr v) return (unifyExtra' u v)
− tests-ghc-9.4/ErrorTests.hs
@@ -1,253 +0,0 @@-{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-}-#if __GLASGOW_HASKELL__ >= 805-{-# LANGUAGE NoStarIsType #-}-#endif-{-# OPTIONS_GHC -fdefer-type-errors #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}--module ErrorTests where--import Data.Proxy-import GHC.TypeLits-import GHC.TypeLits.Extra--testFail1 :: Proxy (GCD 6 8) -> Proxy 4-testFail1 = id--testFail2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9))-testFail2 = id--testFail3 :: Proxy (CLog 3 10) -> Proxy 2-testFail3 = id--testFail4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9))-testFail4 = id--testFail5 :: Proxy (CLog 0 4) -> Proxy 100-testFail5 = id--testFail6 :: Proxy (CLog 1 4) -> Proxy 100-testFail6 = id--testFail7 :: Proxy (CLog 4 0) -> Proxy 0-testFail7 = id--testFail8 :: Proxy (CLog 1 (1^y)) -> Proxy y-testFail8 = id--testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y-testFail9 = id--testFail10 :: Integer-testFail10 = natVal (Proxy :: Proxy (CLog 1 4))--testFail11 :: Integer-testFail11 = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4)))--testFail12 :: Proxy (Div 4 0) -> Proxy 4-testFail12 = id--testFail13 :: Proxy (Mod 4 0) -> Proxy 4-testFail13 = id--testFail14 :: Proxy (FLog 0 4) -> Proxy 100-testFail14 = id--testFail15 :: Proxy (FLog 1 4) -> Proxy 100-testFail15 = id--testFail16 :: Proxy (FLog 4 0) -> Proxy 0-testFail16 = id--testFail17 :: Proxy (LCM 6 8) -> Proxy 48-testFail17 = id--testFail18 :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9))-testFail18 = id--testFail19 :: Integer-testFail19 = natVal (Proxy :: Proxy (Log 3 0))--testFail20 :: Integer-testFail20 = natVal (Proxy :: Proxy (Log 3 10))--testFail21 :: Proxy a -> Proxy b -> Proxy (Min a (a*b)) -> Proxy a-testFail21 _ _ = id--testFail22 :: Proxy a -> Proxy b -> Proxy (Max a (a*b)) -> Proxy (a*b)-testFail22 _ _ = id--testFail23' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> ()-testFail23' _ _ = ()--testFail23 :: ()-testFail23 = testFail23' (Proxy @18) (Proxy @3)--testFail24 :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True-testFail24 _ _ _ = id--testFail25 :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True-testFail25 _ _ = id---- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true.-testFail26' :: ((x <=? n) ~ True) => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n-testFail26' _ _ _ = id--testFail26 = testFail26' (Proxy @4) (Proxy @6) (Proxy @6)--testFail27 :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True-testFail27 _ = id--testFail1Errors =- ["Expected: Proxy (GCD 6 8) -> Proxy 4"- ," Actual: Proxy 4 -> Proxy 4"- ]--testFail2Errors =- ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"- ," Actual: Proxy (2 + x) -> Proxy (2 + x)"- ]--testFail3Errors =- ["Expected: Proxy (CLog 3 10) -> Proxy 2"- ," Actual: Proxy 2 -> Proxy 2"- ]--testFail4Errors =- ["Expected: Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"- ," Actual: Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)"- ]--testFail5Errors =- ["Expected: Proxy (CLog 0 4) -> Proxy 100"- ," Actual: Proxy 100 -> Proxy 100"- ]--testFail6Errors =- ["Expected: Proxy (CLog 1 4) -> Proxy 100"- ," Actual: Proxy 100 -> Proxy 100"- ]--testFail7Errors =- ["Expected: Proxy (CLog 4 0) -> Proxy 0"- ," Actual: Proxy 0 -> Proxy 0"- ]--testFail8Errors =- ["Expected: Proxy (CLog 1 (1 ^ y)) -> Proxy y"- ," Actual: Proxy y -> Proxy y"- ]--testFail9Errors =- ["Expected: Proxy (CLog 0 (0 ^ y)) -> Proxy y"- ," Actual: Proxy y -> Proxy y"- ]--testFail12Errors =- ["Expected: Proxy (Div 4 0) -> Proxy 4"- ," Actual: Proxy 4 -> Proxy 4"- ]--testFail13Errors =- ["Expected: Proxy (Mod 4 0) -> Proxy 4"- ," Actual: Proxy 4 -> Proxy 4"- ]--testFail14Errors =- ["Expected: Proxy (FLog 0 4) -> Proxy 100"- ," Actual: Proxy 100 -> Proxy 100"- ]--testFail15Errors =- ["Expected: Proxy (FLog 1 4) -> Proxy 100"- ," Actual: Proxy 100 -> Proxy 100"- ]--testFail16Errors =- ["Expected: Proxy (FLog 4 0) -> Proxy 0"- ," Actual: Proxy 0 -> Proxy 0"- ]--testFail17Errors =- ["Expected: Proxy (LCM 6 8) -> Proxy 48"- ," Actual: Proxy 48 -> Proxy 48"- ]--testFail18Errors =- ["Expected: Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"- ," Actual: Proxy (24 + x) -> Proxy (24 + x)"- ]--testFail19Errors =- ["Couldn't match type: FLog 3 0"- ," with: CLog 3 0"]--testFail20Errors =- ["Couldn't match type: FLog 3 10"- ," with: CLog 3 10"]--testFail21Errors =- ["Expected: Proxy (Min a (a * b)) -> Proxy a"- ," Actual: Proxy a -> Proxy a"- ]--testFail22Errors =- ["Expected: Proxy (Max a (a * b)) -> Proxy (a * b)"- ," Actual: Proxy (Max a (a * b)) -> Proxy (Max a (a * b))"]--testFail27Errors =- ["Expected: Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True"- ," Actual: Proxy 'True -> Proxy 'True"- ]--testFail10Errors =- ["Cannot satisfy: 2 <= 1"]--testFail11Errors =- ["Cannot satisfy: CLog 2 4 <= CLog 4 4"]--testFail23Errors =- ["Couldn't match type ‘'True’ with ‘'False’"]--testFail24Errors =-#if __GLASGOW_HASKELL__ >= 912- ["Couldn't match type ‘ghc-internal-9.1201.0:GHC.Internal.Data.Type.Ord.OrdCond"- ,"(CmpNat z (Max x y)) 'True 'True 'False’"- ,"with ‘'True’"]-#elif __GLASGOW_HASKELL__ >= 910- ["Couldn't match type ‘ghc-internal-9.1001.0:GHC.Internal.Data.Type.Ord.OrdCond"- ,"(CmpNat z (Max x y)) 'True 'True 'False’"- ,"with ‘'True’"]-#else- ["Couldn't match type ‘Data.Type.Ord.OrdCond"- ,"(CmpNat z (Max x y)) 'True 'True 'False’"- ,"with ‘'True’"]-#endif--testFail25Errors =-#if __GLASGOW_HASKELL__ >= 912- ["Couldn't match type ‘ghc-internal-9.1201.0:GHC.Internal.Data.Type.Ord.OrdCond"- ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’"- ,"with ‘'True’"]-#elif __GLASGOW_HASKELL__ >= 910- ["Couldn't match type ‘ghc-internal-9.1001.0:GHC.Internal.Data.Type.Ord.OrdCond"- ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’"- ,"with ‘'True’"]-#else- ["Couldn't match type ‘Data.Type.Ord.OrdCond"- ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’"- ,"with ‘'True’"]-#endif--testFail26Errors =-#if __GLASGOW_HASKELL__ >= 906- ["Could not deduce ‘Max x y ~ n’"- ,"from the context: (x <=? n) ~ True"- ]-#else- ["Could not deduce (Max x y ~ n)"- ,"from the context: (x <=? n) ~ 'True"- ]-#endif
− tests-pre-ghc-9.4/ErrorTests.hs
@@ -1,347 +0,0 @@-{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-}-#if __GLASGOW_HASKELL__ >= 805-{-# LANGUAGE NoStarIsType #-}-#endif-{-# OPTIONS_GHC -fdefer-type-errors #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}--module ErrorTests where--import Data.Proxy-import GHC.TypeLits-import GHC.TypeLits.Extra--testFail1 :: Proxy (GCD 6 8) -> Proxy 4-testFail1 = id--testFail2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9))-testFail2 = id--testFail3 :: Proxy (CLog 3 10) -> Proxy 2-testFail3 = id--testFail4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9))-testFail4 = id--testFail5 :: Proxy (CLog 0 4) -> Proxy 100-testFail5 = id--testFail6 :: Proxy (CLog 1 4) -> Proxy 100-testFail6 = id--testFail7 :: Proxy (CLog 4 0) -> Proxy 0-testFail7 = id--testFail8 :: Proxy (CLog 1 (1^y)) -> Proxy y-testFail8 = id--testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y-testFail9 = id--testFail10 :: Integer-testFail10 = natVal (Proxy :: Proxy (CLog 1 4))--testFail11 :: Integer-testFail11 = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4)))--testFail12 :: Proxy (Div 4 0) -> Proxy 4-testFail12 = id--testFail13 :: Proxy (Mod 4 0) -> Proxy 4-testFail13 = id--testFail14 :: Proxy (FLog 0 4) -> Proxy 100-testFail14 = id--testFail15 :: Proxy (FLog 1 4) -> Proxy 100-testFail15 = id--testFail16 :: Proxy (FLog 4 0) -> Proxy 0-testFail16 = id--testFail17 :: Proxy (LCM 6 8) -> Proxy 48-testFail17 = id--testFail18 :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9))-testFail18 = id--testFail19 :: Integer-testFail19 = natVal (Proxy :: Proxy (Log 3 0))--testFail20 :: Integer-testFail20 = natVal (Proxy :: Proxy (Log 3 10))--testFail21 :: Proxy a -> Proxy b -> Proxy (Min a (a*b)) -> Proxy a-testFail21 _ _ = id--testFail22 :: Proxy a -> Proxy b -> Proxy (Max a (a*b)) -> Proxy (a*b)-testFail22 _ _ = id--testFail23' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> ()-testFail23' _ _ = ()--testFail23 :: ()-testFail23 = testFail23' (Proxy @18) (Proxy @3)--testFail24 :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True-testFail24 _ _ _ = id--testFail25 :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True-testFail25 _ _ = id---- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true.-testFail26' :: ((x <=? n) ~ True) => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n-testFail26' _ _ _ = id--testFail26 = testFail26' (Proxy @4) (Proxy @6) (Proxy @6)--testFail27 :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True-testFail27 _ = id--#if __GLASGOW_HASKELL__ >= 900-testFail1Errors =- ["Expected: Proxy (GCD 6 8) -> Proxy 4"- ," Actual: Proxy 4 -> Proxy 4"- ]--testFail2Errors =- ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"- ," Actual: Proxy (GCD 6 8 + x) -> Proxy (GCD 6 8 + x)"- ]--testFail3Errors =- ["Expected: Proxy (CLog 3 10) -> Proxy 2"- ," Actual: Proxy 2 -> Proxy 2"- ]--testFail4Errors =- ["Expected: Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"- ," Actual: Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)"- ]--testFail5Errors =- ["Expected: Proxy (CLog 0 4) -> Proxy 100"- ," Actual: Proxy 100 -> Proxy 100"- ]--testFail6Errors =- ["Expected: Proxy (CLog 1 4) -> Proxy 100"- ," Actual: Proxy 100 -> Proxy 100"- ]--testFail7Errors =- ["Expected: Proxy (CLog 4 0) -> Proxy 0"- ," Actual: Proxy 0 -> Proxy 0"- ]--testFail8Errors =- ["Expected: Proxy (CLog 1 (1 ^ y)) -> Proxy y"- ," Actual: Proxy y -> Proxy y"- ]--testFail9Errors =- ["Expected: Proxy (CLog 0 (0 ^ y)) -> Proxy y"- ," Actual: Proxy y -> Proxy y"- ]--testFail12Errors =- ["Expected: Proxy (Div 4 0) -> Proxy 4"- ," Actual: Proxy 4 -> Proxy 4"- ]--testFail13Errors =- ["Expected: Proxy (Mod 4 0) -> Proxy 4"- ," Actual: Proxy 4 -> Proxy 4"- ]--testFail14Errors =- ["Expected: Proxy (FLog 0 4) -> Proxy 100"- ," Actual: Proxy 100 -> Proxy 100"- ]--testFail15Errors =- ["Expected: Proxy (FLog 1 4) -> Proxy 100"- ," Actual: Proxy 100 -> Proxy 100"- ]--testFail16Errors =- ["Expected: Proxy (FLog 4 0) -> Proxy 0"- ," Actual: Proxy 0 -> Proxy 0"- ]--testFail17Errors =- ["Expected: Proxy (LCM 6 8) -> Proxy 48"- ," Actual: Proxy 48 -> Proxy 48"- ]--testFail18Errors =- ["Expected: Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"- ," Actual: Proxy (LCM 6 8 + x) -> Proxy (LCM 6 8 + x)"- ]--testFail19Errors =- ["Couldn't match type: FLog 3 0"- ," with: CLog 3 0"]--testFail20Errors =- ["Couldn't match type: FLog 3 10"- ," with: CLog 3 10"]--testFail21Errors =- ["Expected: Proxy (Min a (a * b)) -> Proxy a"- ," Actual: Proxy a -> Proxy a"- ]--testFail22Errors =- ["Expected: Proxy (Max a (a * b)) -> Proxy (a * b)"- ," Actual: Proxy (Max a (a * b)) -> Proxy (Max a (a * b))"]--testFail27Errors =- ["Expected: Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True"- ," Actual: Proxy 'True -> Proxy 'True"- ]-#else-testFail1Errors =- ["Expected type: Proxy (GCD 6 8) -> Proxy 4"- ,"Actual type: Proxy 4 -> Proxy 4"- ]--testFail2Errors =- ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"- ,"Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)"- ]--testFail3Errors =- ["Expected type: Proxy (CLog 3 10) -> Proxy 2"- ,"Actual type: Proxy 2 -> Proxy 2"- ]--testFail4Errors =- ["Expected type: Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"- ,"Actual type: Proxy (x + CLog 2 9) -> Proxy (x + CLog 2 9)"- ]--testFail5Errors =- ["Expected type: Proxy (CLog 0 4) -> Proxy 100"- ,"Actual type: Proxy 100 -> Proxy 100"- ]--testFail6Errors =- ["Expected type: Proxy (CLog 1 4) -> Proxy 100"- ,"Actual type: Proxy 100 -> Proxy 100"- ]--testFail7Errors =- ["Expected type: Proxy (CLog 4 0) -> Proxy 0"- ,"Actual type: Proxy 0 -> Proxy 0"- ]--testFail8Errors =- ["Expected type: Proxy (CLog 1 (1 ^ y)) -> Proxy y"- ,"Actual type: Proxy y -> Proxy y"- ]--testFail9Errors =- ["Expected type: Proxy (CLog 0 (0 ^ y)) -> Proxy y"- ,"Actual type: Proxy y -> Proxy y"- ]--testFail12Errors =- ["Expected type: Proxy (Div 4 0) -> Proxy 4"- ,"Actual type: Proxy 4 -> Proxy 4"- ]--testFail13Errors =- ["Expected type: Proxy (Mod 4 0) -> Proxy 4"- ,"Actual type: Proxy 4 -> Proxy 4"- ]--testFail14Errors =- ["Expected type: Proxy (FLog 0 4) -> Proxy 100"- ,"Actual type: Proxy 100 -> Proxy 100"- ]--testFail15Errors =- ["Expected type: Proxy (FLog 1 4) -> Proxy 100"- ,"Actual type: Proxy 100 -> Proxy 100"- ]--testFail16Errors =- ["Expected type: Proxy (FLog 4 0) -> Proxy 0"- ,"Actual type: Proxy 0 -> Proxy 0"- ]--testFail17Errors =- ["Expected type: Proxy (LCM 6 8) -> Proxy 48"- ,"Actual type: Proxy 48 -> Proxy 48"- ]--testFail18Errors =- ["Expected type: Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"- ,"Actual type: Proxy (x + LCM 6 9) -> Proxy (x + LCM 6 9)"- ]--testFail19Errors =- ["Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"]--testFail20Errors =- ["Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"]--testFail21Errors =- ["Expected type: Proxy (Min a (a * b)) -> Proxy a"- ,"Actual type: Proxy a -> Proxy a"- ]--testFail22Errors =- ["Expected type: Proxy (Max a (a * b)) -> Proxy (a * b)"- ,"Actual type: Proxy (a * b) -> Proxy (a * b)"]--testFail27Errors =- ["Expected type: Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True"- ,"Actual type: Proxy 'True -> Proxy 'True"- ]-#endif--testFail10Errors =- ["Couldn't match type ‘'False’ with ‘'True’"]--testFail11Errors =-#if __GLASGOW_HASKELL__ >= 902- ["Couldn't match type ‘Data.Type.Ord.OrdCond"- ,"(CmpNat (CLog 2 4) (CLog 4 4)) 'True 'True 'False’"- ,"with ‘'True’"]-#else- ["Couldn't match type ‘CLog 2 4 <=? CLog 4 4’ with ‘'True’"]-#endif--testFail23Errors =-#if __GLASGOW_HASKELL__ >= 804- ["Couldn't match type ‘'True’ with ‘'False’"]-#else- ["Couldn't match type ‘1 <=? Div 18 3’ with ‘'False’"]-#endif--testFail24Errors =-#if __GLASGOW_HASKELL__ >= 902- ["Couldn't match type ‘Data.Type.Ord.OrdCond"- ,"(CmpNat z (Max x y)) 'True 'True 'False’"- ,"with ‘'True’"]-#else- ["Couldn't match type ‘z <=? Max x y’ with ‘'True’"]-#endif--testFail25Errors =-#if __GLASGOW_HASKELL__ >= 902- ["Couldn't match type ‘Data.Type.Ord.OrdCond"- ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’"- ,"with ‘'True’"]-#else- ["Couldn't match type ‘(x + 1) <=? Max x y’ with ‘'True’"]-#endif--testFail26Errors =- ["Could not deduce: Max x y ~ n"- ,"from the context: (x <=? n) ~ 'True"- ]
+ tests/ErrorTests.hs view
@@ -0,0 +1,303 @@+{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-}+#if __GLASGOW_HASKELL__ >= 805+{-# LANGUAGE NoStarIsType #-}+#endif+{-# OPTIONS_GHC -fdefer-type-errors #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}++module ErrorTests where++import Data.Proxy+import GHC.TypeLits+import GHC.TypeLits.Extra+#if __GLASGOW_HASKELL__ >= 901+import qualified Data.Type.Ord+#endif++testFail1 :: Proxy (GCD 6 8) -> Proxy 4+testFail1 = id++testFail2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9))+testFail2 = id++testFail3 :: Proxy (CLog 3 10) -> Proxy 2+testFail3 = id++testFail4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9))+testFail4 = id++testFail5 :: Proxy (CLog 0 4) -> Proxy 100+testFail5 = id++testFail6 :: Proxy (CLog 1 4) -> Proxy 100+testFail6 = id++testFail7 :: Proxy (CLog 4 0) -> Proxy 0+testFail7 = id++testFail8 :: Proxy (CLog 1 (1^y)) -> Proxy y+testFail8 = id++testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y+testFail9 = id++testFail10 :: Integer+testFail10 = natVal (Proxy :: Proxy (CLog 1 4))++testFail11 :: Integer+testFail11 = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4)))++testFail12 :: Proxy (Div 4 0) -> Proxy 4+testFail12 = id++testFail13 :: Proxy (Mod 4 0) -> Proxy 4+testFail13 = id++testFail14 :: Proxy (FLog 0 4) -> Proxy 100+testFail14 = id++testFail15 :: Proxy (FLog 1 4) -> Proxy 100+testFail15 = id++testFail16 :: Proxy (FLog 4 0) -> Proxy 0+testFail16 = id++testFail17 :: Proxy (LCM 6 8) -> Proxy 48+testFail17 = id++testFail18 :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9))+testFail18 = id++testFail19 :: Integer+testFail19 = natVal (Proxy :: Proxy (Log 3 0))++testFail20 :: Integer+testFail20 = natVal (Proxy :: Proxy (Log 3 10))++testFail21 :: Proxy a -> Proxy b -> Proxy (Min a (a*b)) -> Proxy a+testFail21 _ _ = id++testFail22 :: Proxy a -> Proxy b -> Proxy (Max a (a*b)) -> Proxy (a*b)+testFail22 _ _ = id++testFail23' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> ()+testFail23' _ _ = ()++testFail23 :: ()+testFail23 = testFail23' (Proxy @18) (Proxy @3)++testFail24 :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True+testFail24 _ _ _ = id++testFail25 :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True+testFail25 _ _ = id++-- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true.+testFail26' :: ((x <=? n) ~ True) => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n+testFail26' _ _ _ = id++testFail26 = testFail26' (Proxy @4) (Proxy @6) (Proxy @6)++testFail27 :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True+testFail27 _ = id++testFail1Errors =+ ["Proxy (GCD 6 8) -> Proxy 4"+ ,"Proxy 4 -> Proxy 4"+ ]++testFail2Errors =+#if __GLASGOW_HASKELL__ >= 904+ ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"+ ,"Proxy (2 + x) -> Proxy (2 + x)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"+ ,"Proxy (GCD 6 8 + x) -> Proxy (GCD 6 8 + x)"+ ]+#else+ ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"+ ,"Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)"+ ]+#endif++testFail3Errors =+ ["Proxy (CLog 3 10) -> Proxy 2"+ ,"Proxy 2 -> Proxy 2"+ ]++testFail4Errors =+#if __GLASGOW_HASKELL__ >= 900+ ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"+ ,"Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)"+ ]+#else+ ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"+ ,"Proxy (x + CLog 2 9) -> Proxy (x + CLog 2 9)"+ ]+#endif++testFail5Errors =+ ["Proxy (CLog 0 4) -> Proxy 100"+ ,"Proxy 100 -> Proxy 100"+ ]++testFail6Errors =+ ["Proxy (CLog 1 4) -> Proxy 100"+ ,"Proxy 100 -> Proxy 100"+ ]++testFail7Errors =+ ["Proxy (CLog 4 0) -> Proxy 0"+ ,"Proxy 0 -> Proxy 0"+ ]++testFail8Errors =+ ["Proxy (CLog 1 (1 ^ y)) -> Proxy y"+ ,"Proxy y -> Proxy y"+ ]++testFail9Errors =+ ["Proxy (CLog 0 (0 ^ y)) -> Proxy y"+ ,"Proxy y -> Proxy y"+ ]++testFail10Errors =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 2 <= 1"]+#else+ ["Couldn't match type ‘'False’ with ‘'True’"]+#endif++testFail11Errors =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: CLog 2 4 <= CLog 4 4"]+#elif __GLASGOW_HASKELL__ >= 902+ ["Couldn't match type ‘Data.Type.Ord.OrdCond"+ ,"(CmpNat (CLog 2 4) (CLog 4 4)) 'True 'True 'False’"+ ,"with ‘'True’"]+#else+ ["Couldn't match type ‘CLog 2 4 <=? CLog 4 4’ with ‘'True’"]+#endif++testFail12Errors =+ ["Proxy (Div 4 0) -> Proxy 4"+ ,"Proxy 4 -> Proxy 4"+ ]++testFail13Errors =+ ["Proxy (Mod 4 0) -> Proxy 4"+ ,"Proxy 4 -> Proxy 4"+ ]++testFail14Errors =+ ["Proxy (FLog 0 4) -> Proxy 100"+ ,"Proxy 100 -> Proxy 100"+ ]++testFail15Errors =+ ["Proxy (FLog 1 4) -> Proxy 100"+ ,"Proxy 100 -> Proxy 100"+ ]++testFail16Errors =+ ["Proxy (FLog 4 0) -> Proxy 0"+ ,"Proxy 0 -> Proxy 0"+ ]++testFail17Errors =+ ["Proxy (LCM 6 8) -> Proxy 48"+ ,"Proxy 48 -> Proxy 48"+ ]++testFail18Errors =+#if __GLASGOW_HASKELL__ >= 904+ ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"+ ,"Proxy (24 + x) -> Proxy (24 + x)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"+ ,"Proxy (LCM 6 8 + x) -> Proxy (LCM 6 8 + x)"+ ]+#else+ ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"+ ,"Proxy (x + LCM 6 9) -> Proxy (x + LCM 6 9)"+ ]+#endif++testFail19Errors =+#if __GLASGOW_HASKELL__ >= 900+ ["Couldn't match type: FLog 3 0"+ ," with: CLog 3 0"]+#else+ ["Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"]+#endif++testFail20Errors =+#if __GLASGOW_HASKELL__ >= 900+ ["Couldn't match type: FLog 3 10"+ ," with: CLog 3 10"]+#else+ ["Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"]+#endif++testFail21Errors =+ ["Proxy (Min a (a * b)) -> Proxy a"+ ,"Proxy a -> Proxy a"+ ]++testFail22Errors =+#if __GLASGOW_HASKELL__ >= 900+ ["Proxy (Max a (a * b)) -> Proxy (a * b)"+ ,"Proxy (Max a (a * b)) -> Proxy (Max a (a * b))"]+#else+ ["Proxy (Max a (a * b)) -> Proxy (a * b)"+ ,"Proxy (a * b) -> Proxy (a * b)"]+#endif++testFail23Errors =+#if __GLASGOW_HASKELL__ >= 804+ ["Couldn't match type ‘'True’ with ‘'False’"]+#else+ ["Couldn't match type ‘1 <=? Div 18 3’ with ‘'False’"]+#endif++testFail24Errors =+#if __GLASGOW_HASKELL__ >= 902+ ["Couldn't match type ‘Data.Type.Ord.OrdCond"+ ,"(CmpNat z (Max x y)) 'True 'True 'False’"+ ,"with ‘'True’"]+#else+ ["Couldn't match type ‘z <=? Max x y’ with ‘'True’"]+#endif++testFail25Errors =+#if __GLASGOW_HASKELL__ >= 902+ ["Couldn't match type ‘Data.Type.Ord.OrdCond"+ ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’"+ ,"with ‘'True’"]+#else+ ["Couldn't match type ‘(x + 1) <=? Max x y’ with ‘'True’"]+#endif++testFail26Errors =+#if __GLASGOW_HASKELL__ >= 906+ ["Could not deduce ‘Max x y ~ n’"+ ,"from the context: (x <=? n) ~ True"+ ]+#elif __GLASGOW_HASKELL__ <= 902+ ["Could not deduce: Max x y ~ n"+ ,"from the context: (x <=? n) ~ 'True"+ ]+#else+ ["Could not deduce (Max x y ~ n)"+ ,"from the context: (x <=? n) ~ 'True"+ ]+#endif++testFail27Errors =+ ["Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True"+ ,"Proxy 'True -> Proxy 'True"+ ]
tests/Main.hs view
@@ -2,10 +2,17 @@ #if __GLASGOW_HASKELL__ >= 805 {-# LANGUAGE NoStarIsType #-} #endif++#if __GLASGOW_HASKELL__ >= 904+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}+#endif {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}+#if __GLASGOW_HASKELL__ < 904 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}+#endif + import Data.List (isInfixOf) import Data.Proxy import Data.Type.Bool@@ -230,9 +237,10 @@ test58a = id test58b- :: Proxy (Max (n+2) 1)+ :: Proxy n -> Proxy (Max (n+2) 1)-test58b = test58a+ -> Proxy (Max (n+2) 1)+test58b _ = test58a main :: IO () main = defaultMain tests