ghc-typelits-extra 0.4.8 → 0.5.4
raw patch · 15 files changed
Files
- CHANGELOG.md +20/−0
- ghc-typelits-extra.cabal +66/−48
- 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.hs +22/−8
- src/GHC/TypeLits/Extra/Solver.hs +327/−0
- src/GHC/TypeLits/Extra/Solver/Compat.hs +101/−0
- src/GHC/TypeLits/Extra/Solver/Operations.hs +95/−100
- src/GHC/TypeLits/Extra/Solver/Unify.hs +109/−96
- tests-ghc-9.4/ErrorTests.hs +0/−253
- tests-pre-ghc-9.4/ErrorTests.hs +0/−347
- tests/Main.hs +94/−55
- tests/ShouldError.hs +574/−0
- tests/ShouldError/Tasty.hs +53/−0
CHANGELOG.md view
@@ -1,5 +1,25 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package +# 0.5.4 *May 13th 2026*+* Bump ghc-tcplugin-api to prepare for inclusion into stackage++# 0.5.3 *March 19th 2026*+* Do not require equality to unit constraint for wanted InEqs for `CLog` and `CLogWZ`.+* Fix wrong reification from `CLogWZ` to `CLog` causing GHC panic. [#71](https://github.com/clash-lang/ghc-typelits-extra/issues/71)+* Do not emit new wanteds for given `CLogWZ ~ CLog` equalities. [#73](https://github.com/clash-lang/ghc-typelits-extra/issues/73)++# 0.5.2 *December 3rd 2025*+* Add `CLogWZ`, an extension of 'CLog', which returns the additional third argument in case the second argument is zero+* Add rewrite rules for `Min`, `Max`, `FLog`, `CLog`, and `Log`++# 0.5.1 *October 21st 2025*+* Compatibility with `ghc-typelits-natnormalise` 0.9.1 release++# 0.5.0 *October 17th 2025*+* Add support for GHC 9.14+* Uses https://hackage.haskell.org/package/ghc-tcplugin-api to make supporting new GHC versions easier+* Support for GHC versions older than 8.8 is dropped+ # 0.4.8 *March 4th 2025* * Add support for GHC 9.12.1
ghc-typelits-extra.cabal view
@@ -1,42 +1,45 @@+cabal-version: 3.0 name: ghc-typelits-extra-version: 0.4.8+version: 0.5.4 synopsis: Additional type-level operations on GHC.TypeLits.Nat description: Additional type-level operations on @GHC.TypeLits.Nat@:- .+ * @Max@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:max max>- .+ * @Min@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:min min>- .+ * @Div@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:div div>- .+ * @Mod@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:mod mod>- .+ * @FLog@: type-level equivalent of <https://hackage.haskell.org/package/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)@- .++ * @CLogWZ@: extension of @CLog@, which returns the additional third argument in case the second argument is zero+ * @Log@: type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> where the operation only reduces when @floor (logBase b x) ~ ceiling (logBase b x)@- .+ * @GCD@: a type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd gcd>- .+ * @LCM@: a type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:lcm lcm>- .+ And a custom solver for the above operations defined in @GHC.TypeLits.Extra.Solver@ as a GHC type-checker plugin. To use the plugin, add the- .+ @ OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver @- .+ pragma to the header of your file. homepage: http://www.clash-lang.org/ bug-reports: http://github.com/clash-lang/ghc-typelits-extra/issues-license: BSD2+license: BSD-2-Clause license-file: LICENSE author: Christiaan Baaij maintainer: christiaan.baaij@gmail.com@@ -44,13 +47,11 @@ 2017-2018, QBayLogic B.V. category: Type System build-type: Simple-extra-source-files: README.md+extra-doc-files: README.md CHANGELOG.md-cabal-version: >=1.10-tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,- GHC == 8.8.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 +67,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,+ ghc-tcplugin-api >= 0.19 && <0.20,+ ghc-typelits-knownnat >= 0.7.2 && <0.9,+ ghc-typelits-natnormalise >= 0.9.5 && <0.10,+ transformers >= 0.4.2.0 && <0.7,+ template-haskell >= 2.15 && <2.25 if impl(ghc >= 9.0.0)- build-depends: ghc-bignum >=1.0 && <1.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@@ -110,20 +125,23 @@ test-suite test-ghc-typelits-extra type: exitcode-stdio-1.0 main-is: Main.hs- Other-Modules: ErrorTests- build-depends: base >= 4.8 && <5,+ Other-Modules: ShouldError+ ShouldError.Tasty+ build-depends: base,+ directory,+ filepath, ghc-typelits-extra,- ghc-typelits-knownnat >= 0.7.2,- ghc-typelits-natnormalise >= 0.7.1,+ ghc-typelits-knownnat,+ ghc-typelits-natnormalise,+ process,+ interpolate, tasty >= 0.10,- tasty-hunit >= 0.9+ tasty-hunit >= 0.9,+ temporary hs-source-dirs: tests- 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+ ghc-options: -Wall default-language: Haskell2010 other-extensions: DataKinds TypeOperators if flag(deverror)- ghc-options: -dcore-lint+ ghc-options: -Werror -dcore-lint
− 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.hs view
@@ -20,6 +20,8 @@ * '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)@" + * 'CLogWZ': extension of 'CLog', which returns the additional third argument in case the second argument is zero+ * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" @@ -70,6 +72,7 @@ -- ** Logarithm , FLog , CLog+ , CLogWZ -- *** Exact logarithm , Log -- Numeric@@ -81,9 +84,6 @@ import Data.Proxy (Proxy (..)) import Data.Type.Bool (If) import GHC.Base (Int#,isTrue#,(==#),(+#))-#if MIN_VERSION_ghc(9,4,0)-import GHC.Base (Constraint)-#endif import GHC.Integer.Logarithms (integerLogBase#) #if MIN_VERSION_ghc(8,2,0) import GHC.Magic (noinline)@@ -101,7 +101,8 @@ #if MIN_VERSION_ghc(8,4,0) import GHC.TypeLits (Div, Mod) #endif-import GHC.TypeLits.KnownNat (KnownNat2 (..), SNatKn (..), nameToSymbol)+import GHC.TypeLits.KnownNat (KnownNat2 (..), KnownNat3 (..),+ SNatKn (..), nameToSymbol) #if MIN_VERSION_ghc(8,2,0) intToNumber :: Int# -> Natural@@ -181,16 +182,29 @@ type family CLog (base :: Nat) (value :: Nat) :: Nat where CLog 2 1 = 0 -- Additional equations are provided by the custom solver -#if MIN_VERSION_ghc(9,4,0)-instance (KnownNat x, KnownNat y, (2 <= x) ~ (() :: Constraint), 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where-#else instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where-#endif natSing2 = let x = natVal (Proxy @x) y = natVal (Proxy @y) z1 = integerLogBase# x y z2 = integerLogBase# x (y-1) in case y of+ 1 -> SNatKn 0+ _ | isTrue# (z1 ==# z2) -> SNatKn (intToNumber (z1 +# 1#))+ | otherwise -> SNatKn (intToNumber z1)++-- | Extended version of 'CLog', which is well-defined for the second, non-base argument being zero. The additional third argument argument is returned in this particular case.+type family CLogWZ (base :: Nat) (value :: Nat) (ifzero :: Nat) :: Nat where+ CLogWZ _ 0 z = z+ CLogWZ b v _ = CLog b v++instance (KnownNat x, KnownNat y, KnownNat z, 2 <= x) => KnownNat3 $(nameToSymbol ''CLogWZ) x y z where+ natSing3 = let x = natVal (Proxy @x)+ y = natVal (Proxy @y)+ z = natVal (Proxy @z)+ z1 = integerLogBase# x y+ z2 = integerLogBase# x (y-1)+ in case y of+ 0 -> SNatKn $ fromInteger z 1 -> SNatKn 0 _ | isTrue# (z1 ==# z2) -> SNatKn (intToNumber (z1 +# 1#)) | otherwise -> SNatKn (intToNumber z1)
+ src/GHC/TypeLits/Extra/Solver.hs view
@@ -0,0 +1,327 @@+{-|+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)@"+--+-- * 'CLogWZ': extension of @CLog@, which returns the additional third argument in case the second argument is zero+--+-- * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"+--+-- * 'GCD': a type-level 'gcd'+--+-- * '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+ , tcPluginPostTc = const (return ())+ , tcPluginShutdown = const (return ())+ }++extraRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter+extraRewrite defs = listToUFM+ [ (minTyCon defs, minRewrite)+ , (maxTyCon defs, maxRewrite)+ , (flogTyCon defs, flogRewrite)+ , (clogTyCon defs, clogRewrite)+ , (clogWZTyCon defs, clogWZRewrite)+ , (logTyCon defs, logRewrite)+ , (gcdTyCon defs, gcdRewrite)+ , (lcmTyCon defs, lcmRewrite)+ ]+ where+ minRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ = pure $ rewriteTo (minTyCon defs) args $ min i j+ minRewrite _ _ = pure TcPluginNoRewrite++ maxRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ = pure $ rewriteTo (maxTyCon defs) args $ max i j+ maxRewrite _ _ = pure TcPluginNoRewrite++ flogRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ , i > 1+ , Just r <- flogBase i j+ = pure $ rewriteTo (flogTyCon defs) args r+ flogRewrite _ _ = pure TcPluginNoRewrite++ clogRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ , i > 1+ , Just r <- clogBase i j+ = pure $ rewriteTo (clogTyCon defs) args r+ clogRewrite _ _ = pure TcPluginNoRewrite++ clogWZRewrite _ args+ | [_, LitTy (NumTyLit 0), z] <- args+ = pure $ TcPluginRewriteTo (reduce (clogWZTyCon defs) args z) []+ clogWZRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j), _] <- args+ , i > 1+ , Just r <- clogBase i j+ = pure $ rewriteTo (clogWZTyCon defs) args r+ clogWZRewrite _ _ = pure TcPluginNoRewrite++ logRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ , i > 1+ , Just r <- exactLogBase i j+ = pure $ rewriteTo (logTyCon defs) args r+ logRewrite _ _ = pure TcPluginNoRewrite++ gcdRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ = pure $ rewriteTo (gcdTyCon defs) args (i `gcd` j)+ gcdRewrite _ _ = pure TcPluginNoRewrite++ lcmRewrite _ args+ | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args+ = pure $ rewriteTo (lcmTyCon defs) args (i `lcm` j)+ lcmRewrite _ _ = pure TcPluginNoRewrite++ rewriteTo tyCon args x =+ TcPluginRewriteTo (reduce tyCon args (LitTy (NumTyLit x))) []++ reduce tc args res = Reduction co res+ where+ co = mkPluginUnivCo "ghc-typelits-extra" Nominal []+ (mkTyConApp tc args) res+++decideEqualSOP :: ExtraDefs -> [Ct] -> [Ct] -> TcPluginM 'Solve TcPluginSolveResult+decideEqualSOP _ _givens [] = return (TcPluginOk [] [])+decideEqualSOP defs givens wanteds = do+ let givensTyConSubst = mkTyConSubst givens+ unit_wanteds <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs givensTyConSubst) wanteds+ case unit_wanteds of+ [] -> return (TcPluginOk [] [])+ _ -> do+ 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+ let evM = evMagic (ordTyCons defs) ct (depsFromNormalised norm)+ -- transform: CLogWZ a b c ~ CLog a b+ -- to: 1 <= b+ -- which is equivalent by definition and try to solve that+ -- along with the rest of the eqs'+ wz = case (u, v) of+ (CLogWZ a b _, CLog a' b') | a == a' && b == b' -> Just b+ (CLog a' b', CLogWZ a b _) | a == a' && b == b' -> Just b+ _ -> Nothing+ case wz of+ Just x | isWantedCt ct -> do+ let x' = reifyEOP defs x+ one = reifyEOP defs (I 1)+ ev <- newWanted (ctLoc ct) $ mkLEqNat (ordTyCons defs) one x'+ let newCt = mkNonCanonical ev+ simples (fmap (,ct) evM:evs) (newCt:news) eqs'+ _ -> do+ ur <- unifyExtra ct u v+ tcPluginTrace "unifyExtra result" (ppr ur)+ case ur of+ Win -> simples (fmap (,ct) evM:evs) news eqs'+ Lose | null evs && null eqs' -> return (Impossible eq)+ _ | Normalised {} <- norm+ , isWantedCt ct -> do+ newCt <- createWantedFromNormalised defs eq+ simples (fmap (,ct) evM:evs) (newCt:news) eqs'+ Lose -> simples evs news eqs'+ Draw -> simples evs news eqs'+ simples evs news (eq@(NatInequality ct deps u v b norm):eqs') = do+ tcPluginTrace "unifyExtra leq result" (ppr (u,v,b))+ let evM = evMagic (ordTyCons defs) ct (deps <> depsFromNormalised norm)+ case (u,v) of+ (I i,I j)+ | (i <= j) == b+ -> simples (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,101 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskellQuotes #-}++{-# OPTIONS_GHC -Wno-unused-matches #-}++module GHC.TypeLits.Extra.Solver.Compat where++import qualified Language.Haskell.TH as TH++import GHC.TcPlugin.API++import GHC.TypeLits.Normalise.Compat++import GHC.Builtin.Names+ ( eqPrimTyConKey, hasKey+ )+#if MIN_VERSION_ghc(9,1,0)+import GHC.Builtin.Types+ ( boolTy, promotedFalseDataCon, promotedTrueDataCon+ )+#endif+import GHC.Builtin.Types.Literals+ ( typeNatDivTyCon, typeNatModTyCon+ )+#if MIN_VERSION_ghc(9,8,0)+import GHC.Tc.Types.Constraint+ ( DictCt(..), EqCt(..), IrredCt(..)+ )+#endif+import GHC.Tc.Types.Constraint+ ( Ct (..), qci_ev+ )++import qualified GHC.TypeLits.Extra++data ExtraDefs = ExtraDefs+ { maxTyCon :: TyCon+ , minTyCon :: TyCon+ , divTyCon :: TyCon+ , modTyCon :: TyCon+ , flogTyCon :: TyCon+ , clogTyCon :: TyCon+ , clogWZTyCon :: TyCon+ , logTyCon :: TyCon+ , gcdTyCon :: TyCon+ , lcmTyCon :: TyCon+ , ordTyCons :: LookedUpTyCons+ }++-- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat"+lookupExtraDefs :: TcPluginM 'Init ExtraDefs+lookupExtraDefs = do+ ExtraDefs <$> look ''GHC.TypeLits.Extra.Max+ <*> look ''GHC.TypeLits.Extra.Min+ <*> pure typeNatDivTyCon+ <*> pure typeNatModTyCon+ <*> look ''GHC.TypeLits.Extra.FLog+ <*> look ''GHC.TypeLits.Extra.CLog+ <*> look ''GHC.TypeLits.Extra.CLogWZ+ <*> look ''GHC.TypeLits.Extra.Log+ <*> look ''GHC.TypeLits.Extra.GCD+ <*> look ''GHC.TypeLits.Extra.LCM+ <*> lookupTyCons+ where+ look :: TH.Name -> TcPluginM 'Init TyCon+ look nm = tcLookupTyCon =<< lookupTHName nm++setCtEv :: Ct -> CtEvidence -> Ct+setCtEv ct ev = case ct of+ CQuantCan qc -> CQuantCan (qc { qci_ev = ev})+#if MIN_VERSION_ghc(9,8,0)+ CDictCan di -> CDictCan (di { di_ev = ev})+ CIrredCan ir -> CIrredCan (ir { ir_ev = ev})+ CEqCan eq -> CEqCan (eq { eq_ev = ev})+ CNonCanonical _ -> CNonCanonical ev+#else+ ctX -> ctX { cc_ev = ev }+#endif++mkLeqQNat :: LookedUpTyCons -> Type -> Type -> Type+mkLeqQNat tcs x y =+#if MIN_VERSION_ghc(9,1,0)+ mkTyConApp (ordCondTyCon tcs)+ [ boolTy+ , mkTyConApp (cmpNatTyCon tcs) [x,y]+ , mkTyConApp promotedTrueDataCon []+ , mkTyConApp promotedTrueDataCon []+ , mkTyConApp promotedFalseDataCon []+ ]+#else+ mkTyConApp (leqQNatTyCon tcs) [x, y]+#endif++toLeqPredType :: Monad m => LookedUpTyCons -> Ct -> Type -> Type -> m PredType+toLeqPredType defs ct t1 t2 = case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of+ Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2])+#if MIN_VERSION_ghc(9,3,0)+ Just (tc, [_, b]) | tc == assertTyCon defs -> pure (mkTyConApp tc [t1,b])+#endif+ _ -> error "Impossible: neither (<=?) nor Assert"
src/GHC/TypeLits/Extra/Solver/Operations.hs view
@@ -7,13 +7,14 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE MagicHash #-}+{-# LANGUAGE LambdaCase #-} module GHC.TypeLits.Extra.Solver.Operations ( ExtraOp (..)- , ExtraDefs (..) , Normalised (..) , NormaliseResult , mergeNormalised+ , depsFromNormalised , reifyEOP , mergeMax , mergeMin@@ -21,10 +22,14 @@ , mergeMod , mergeFLog , mergeCLog+ , mergeCLogWZ , mergeLog , mergeGCD , mergeLCM , mergeExp+ , flogBase+ , clogBase+ , exactLogBase ) where @@ -39,50 +44,52 @@ 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) data ExtraOp- = I Integer- | V TyVar- | C CType- | Max ExtraOp ExtraOp- | Min ExtraOp ExtraOp- | Div ExtraOp ExtraOp- | Mod ExtraOp ExtraOp- | FLog ExtraOp ExtraOp- | CLog ExtraOp ExtraOp- | Log ExtraOp ExtraOp- | GCD ExtraOp ExtraOp- | LCM ExtraOp ExtraOp- | Exp ExtraOp ExtraOp+ = I Integer+ | V TyVar+ | C CType+ | Max ExtraOp ExtraOp+ | Min ExtraOp ExtraOp+ | Div ExtraOp ExtraOp+ | Mod ExtraOp ExtraOp+ | FLog ExtraOp ExtraOp+ | CLog ExtraOp ExtraOp+ | CLogWZ ExtraOp ExtraOp ExtraOp+ | Log ExtraOp ExtraOp+ | GCD ExtraOp ExtraOp+ | LCM ExtraOp ExtraOp+ | Exp ExtraOp ExtraOp deriving Eq instance Outputable ExtraOp where@@ -99,119 +106,107 @@ ppr (GCD x y) = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")" ppr (LCM x y) = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")" ppr (Exp x y) = text "Exp (" <+> ppr x <+> text "," <+> ppr y <+> text ")"--data ExtraDefs = ExtraDefs- { maxTyCon :: TyCon- , minTyCon :: TyCon- , divTyCon :: TyCon- , modTyCon :: TyCon- , flogTyCon :: TyCon- , clogTyCon :: TyCon- , logTyCon :: TyCon- , gcdTyCon :: TyCon- , lcmTyCon :: TyCon- , ordTyCon :: TyCon- , assertTC :: TyCon- }+ ppr (CLogWZ x y z) = text "CLogWZ " <+> text "(" <+> ppr x <+> text ","+ <+> ppr y <+> text "," <+> ppr z <+> text ")" reifyEOP :: ExtraDefs -> ExtraOp -> Type-reifyEOP _ (I i) = mkNumLitTy i-reifyEOP _ (V v) = mkTyVarTy v-reifyEOP _ (C (CType c)) = c-reifyEOP defs (Max x y) = mkTyConApp (maxTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (Min x y) = mkTyConApp (minTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (Div x y) = mkTyConApp (divTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (Mod x y) = mkTyConApp (modTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (CLog x y) = mkTyConApp (clogTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (FLog x y) = mkTyConApp (flogTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (Log x y) = mkTyConApp (logTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (GCD x y) = mkTyConApp (gcdTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (LCM x y) = mkTyConApp (lcmTyCon defs) [reifyEOP defs x- ,reifyEOP defs y]-reifyEOP defs (Exp x y) = mkTyConApp typeNatExpTyCon [reifyEOP defs x- ,reifyEOP defs y]+reifyEOP defs = \case+ I i -> mkNumLitTy i+ V v -> mkTyVarTy v+ C (CType c) -> c+ Max x y -> mkTyConApp (maxTyCon defs) $ reifyEOP defs <$> [x, y]+ Min x y -> mkTyConApp (minTyCon defs) $ reifyEOP defs <$> [x, y]+ Div x y -> mkTyConApp (divTyCon defs) $ reifyEOP defs <$> [x, y]+ Mod x y -> mkTyConApp (modTyCon defs) $ reifyEOP defs <$> [x, y]+ CLog x y -> mkTyConApp (clogTyCon defs) $ reifyEOP defs <$> [x, y]+ CLogWZ x y z -> mkTyConApp (clogWZTyCon defs) $ reifyEOP defs <$> [x, y, z]+ FLog x y -> mkTyConApp (flogTyCon defs) $ reifyEOP defs <$> [x, y]+ Log x y -> mkTyConApp (logTyCon defs) $ reifyEOP defs <$> [x, y]+ GCD x y -> mkTyConApp (gcdTyCon defs) $ reifyEOP defs <$> [x, y]+ LCM x y -> mkTyConApp (lcmTyCon defs) $ reifyEOP defs <$> [x, y]+ Exp x y -> mkTyConApp typeNatExpTyCon $ reifyEOP defs <$> [x, y] mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> 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'])))+ (z',deps') = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [x',y']))) 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+ Nothing -> case runWriterT (isNatural z') of+ Just (True ,cs) | Set.null cs -> (x, Normalised deps') -- x >= y+ Just (False,cs) | Set.null cs -> (y, Normalised deps') -- x < y+ _ -> (Max x y, Untouched)+ Just (True , cs) | Set.null cs -> (y, Normalised deps) -- y >= x+ Just (False, cs) | Set.null cs -> (x, Normalised deps) -- y < x _ -> (Max x y, Untouched) mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult mergeMin defs x y = let x' = reifyEOP defs x y' = reifyEOP defs y- z = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))-#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)+ (z,deps) = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))+ (z',deps') = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [x',y']))) in case runWriterT (isNatural z) of- Just (True, cs) | Set.null cs -> (x, Normalised)- Just (False,cs) | Set.null cs -> (y, Normalised)-#else- in case isNatural z of- Just True -> (x, Normalised)- Just False -> (y, Normalised)-#endif+ Nothing -> case runWriterT (isNatural z') of+ Just (True ,cs) | Set.null cs -> (y, Normalised deps') -- x >= y+ Just (False,cs) | Set.null cs -> (x, Normalised deps') -- x < y+ _ -> (Min x y, Untouched)+ Just (True, cs) | Set.null cs -> (x, Normalised deps) -- y >= x+ Just (False,cs) | Set.null cs -> (y, Normalised deps) -- y < x _ -> (Min x y, Untouched) mergeDiv :: ExtraOp -> ExtraOp -> Maybe 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) +mergeCLogWZ :: ExtraOp -> ExtraOp -> ExtraOp -> Maybe NormaliseResult+mergeCLogWZ (I i) _ _ | i < 2 = Nothing+mergeCLogWZ _ (I 0) z = Just (z, Normalised [])+mergeCLogWZ i (Exp j k) _ | i == j = Just (k, Normalised [])+-- CLogWZ a b c = CLog a b for all b > 0 by definition, hence we can+-- elide one layer of constructor applications in this particular case+mergeCLogWZ x y@(I _) _ = do (res, _) <- mergeCLog x y+ pure (res, Normalised [])+mergeCLogWZ x y z = Just (CLogWZ x y z, Untouched)+ mergeLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeLog (I i) _ | i < 2 = Nothing-mergeLog b (Exp b' y) | b == b' = Just (y, 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,11 @@ Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> -} -{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-} module GHC.TypeLits.Extra.Solver.Unify- ( ExtraDefs (..)- , UnifyResult (..)+ ( UnifyResult (..) , NormaliseResult , normaliseNat , unifyExtra@@ -23,37 +23,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,54 +49,76 @@ 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) -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 [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) - 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)+ go (TyConApp tc [x,y,z])+ | tc == clogWZTyCon defs+ = do (x', n1) <- normaliseNat defs x+ (y', n2) <- normaliseNat defs y+ (z', n3) <- normaliseNat defs z+ (res, n4) <- MaybeT $ return $ mergeCLogWZ x' y' z'+ pure (res, foldl mergeNormalised Untouched [n1,n2,n3,n4]) -normaliseNat _ t = return (C (CType t), Untouched)+ go (TyConApp tc tys) = do+ let mergeExtraOp [] = []+ mergeExtraOp ((Just (op, Normalised []), _):xs) = reifyEOP defs op:mergeExtraOp xs+ mergeExtraOp ((_, ty):xs) = ty:mergeExtraOp xs + normResults <- lift (sequence (runMaybeT . go <$> tys))+ let anyNormalised = foldr mergeNormalised Untouched (snd <$> catMaybes normResults)+ let tys' = mergeExtraOp (zip normResults tys)+ pure (C (CType (TyConApp tc tys')), anyNormalised)++ go t = return (C (CType t), Untouched)+ -- | Result of comparing two 'SOP' terms, returning a potential substitution -- list under which the two terms are equal. data UnifyResult@@ -121,7 +131,7 @@ ppr Lose = text "Lose" ppr Draw = text "Draw" -unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult+unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM 'Solve UnifyResult unifyExtra ct u v = do tcPluginTrace "unifyExtra" (ppr ct $$ ppr u $$ ppr v) return (unifyExtra' u v)@@ -149,34 +159,37 @@ commuteResult _ _ = Draw fvOP :: ExtraOp -> UniqSet TyVar-fvOP (I _) = emptyUniqSet-fvOP (V v) = unitUniqSet v-fvOP (C _) = emptyUniqSet-fvOP (Max x y) = fvOP x `unionUniqSets` fvOP y-fvOP (Min x y) = fvOP x `unionUniqSets` fvOP y-fvOP (Div x y) = fvOP x `unionUniqSets` fvOP y-fvOP (Mod x y) = fvOP x `unionUniqSets` fvOP y-fvOP (FLog x y) = fvOP x `unionUniqSets` fvOP y-fvOP (CLog x y) = fvOP x `unionUniqSets` fvOP y-fvOP (Log x y) = fvOP x `unionUniqSets` fvOP y-fvOP (GCD x y) = fvOP x `unionUniqSets` fvOP y-fvOP (LCM x y) = fvOP x `unionUniqSets` fvOP y-fvOP (Exp x y) = fvOP x `unionUniqSets` fvOP y+fvOP (I _) = emptyUniqSet+fvOP (V v) = unitUniqSet v+fvOP (C _) = emptyUniqSet+fvOP (Max x y) = fvOP x `unionUniqSets` fvOP y+fvOP (Min x y) = fvOP x `unionUniqSets` fvOP y+fvOP (Div x y) = fvOP x `unionUniqSets` fvOP y+fvOP (Mod x y) = fvOP x `unionUniqSets` fvOP y+fvOP (FLog x y) = fvOP x `unionUniqSets` fvOP y+fvOP (CLog x y) = fvOP x `unionUniqSets` fvOP y+fvOP (CLogWZ x y z) = fvOP x `unionUniqSets` fvOP y `unionUniqSets` fvOP z+fvOP (Log x y) = fvOP x `unionUniqSets` fvOP y+fvOP (GCD x y) = fvOP x `unionUniqSets` fvOP y+fvOP (LCM x y) = fvOP x `unionUniqSets` fvOP y+fvOP (Exp x y) = fvOP x `unionUniqSets` fvOP y eqFV :: ExtraOp -> ExtraOp -> Bool eqFV = (==) `on` fvOP containsConstants :: ExtraOp -> Bool-containsConstants (I _) = False-containsConstants (V _) = False-containsConstants (C _) = True-containsConstants (Max x y) = containsConstants x || containsConstants y-containsConstants (Min x y) = containsConstants x || containsConstants y-containsConstants (Div x y) = containsConstants x || containsConstants y-containsConstants (Mod x y) = containsConstants x || containsConstants y-containsConstants (FLog x y) = containsConstants x || containsConstants y-containsConstants (CLog x y) = containsConstants x || containsConstants y-containsConstants (Log x y) = containsConstants x || containsConstants y-containsConstants (GCD x y) = containsConstants x || containsConstants y-containsConstants (LCM x y) = containsConstants x || containsConstants y-containsConstants (Exp x y) = containsConstants x || containsConstants y+containsConstants = \case+ I _ -> False+ V _ -> False+ C _ -> True+ Max x y -> or $ containsConstants <$> [x, y]+ Min x y -> or $ containsConstants <$> [x, y]+ Div x y -> or $ containsConstants <$> [x, y]+ Mod x y -> or $ containsConstants <$> [x, y]+ FLog x y -> or $ containsConstants <$> [x, y]+ CLog x y -> or $ containsConstants <$> [x, y]+ CLogWZ x y z -> or $ containsConstants <$> [x, y, z]+ Log x y -> or $ containsConstants <$> [x, y]+ GCD x y -> or $ containsConstants <$> [x, y]+ LCM x y -> or $ containsConstants <$> [x, y]+ Exp x y -> or $ containsConstants <$> [x, y]
− tests-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/Main.hs view
@@ -2,22 +2,32 @@ #if __GLASGOW_HASKELL__ >= 805 {-# LANGUAGE NoStarIsType #-} #endif++#if __GLASGOW_HASKELL__ >= 904+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}+#endif {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}+#if __GLASGOW_HASKELL__ < 904 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}+#endif -import Data.List (isInfixOf)+-- Even though binders are not used, they're compiled and that's what we're after.+{-# OPTIONS_GHC -Wno-unused-top-binds #-}++-- Only applies to old GHCs.+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}+ import Data.Proxy-import Data.Type.Bool-import Control.Exception+import Data.Type.Equality import Test.Tasty import Test.Tasty.HUnit -import ErrorTests- import GHC.TypeLits import GHC.TypeLits.Extra +import qualified ShouldError+ test1 :: Proxy (GCD 6 8) -> Proxy 2 test1 = id @@ -230,10 +240,50 @@ test58a = id test58b- :: Proxy (Max (n+2) 1)+ :: Proxy n -> Proxy (Max (n+2) 1)-test58b = test58a+ -> Proxy (Max (n+2) 1)+test58b _ = test58a +test59 :: Proxy (CLogWZ 3 10 9) -> Proxy 3+test59 = id++test60 :: Proxy ((CLogWZ 3 10 3) + x) -> Proxy (x + (CLogWZ 2 7 8))+test60 = id++test61 :: Proxy (CLogWZ x (x^y) 8) -> Proxy y+test61 = id++test62 :: Integer+test62 = natVal (Proxy :: Proxy (CLogWZ 6 8 3))++test63 :: Integer+test63 = natVal (Proxy :: Proxy (CLogWZ 3 10 9))++test64 :: Integer+test64 = natVal (Proxy :: Proxy ((CLogWZ 2 4 11) * (3 ^ (CLogWZ 2 4 8))))++test65 :: Integer+test65 = natVal (Proxy :: Proxy (Max (CLogWZ 2 4 8) (CLogWZ 4 20 5)))++test66 :: Proxy (CLogWZ 3 0 8) -> Proxy 8+test66 = id++test67 :: Proxy (CLogWZ 2 0 x) -> Proxy x+test67 = id++test68 :: Proxy (CLogWZ 5 0 0) -> Proxy 0+test68 = id++test69 :: 1 <= n => Proxy n -> Proxy (CLogWZ 2 n 0) -> Proxy (CLog 2 n)+test69 _ = id++-- Regression test for: https://github.com/clash-lang/ghc-typelits-extra/issues/73+test70 :: (CLog 2 n ~ CLogWZ 2 n 0) => Proxy n -> Proxy n+test70 _ =+ case (Refl :: Max (n + 1) 1 :~: (1 + n)) of+ Refl -> Proxy+ main :: IO () main = defaultMain tests @@ -411,53 +461,42 @@ , testCase "forall n p . n + 1 <= Max (n + p + 1) p" $ show (test57 Proxy Proxy Proxy) @?= "Proxy"- ]- , testGroup "errors"- [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors- , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail2 `throws` testFail2Errors- , testCase "CLog 3 10 /~ 2" $ testFail3 `throws` testFail3Errors- , testCase "CLog 3 10 + x /~ x + CLog 2 9" $ testFail4 `throws` testFail4Errors- , testCase "CLog 0 4 /~ 100" $ testFail5 `throws` testFail5Errors- , testCase "CLog 1 4 /~ 100" $ testFail5 `throws` testFail5Errors- , testCase "CLog 4 0 /~ 0" $ testFail7 `throws` testFail7Errors- , testCase "CLog 1 (1^y) /~ y" $ testFail8 `throws` testFail8Errors- , testCase "CLog 0 (0^y) /~ y" $ testFail9 `throws` testFail9Errors- , testCase "No instance (KnownNat (CLog 1 4))" $ testFail10 `throws` testFail10Errors- , testCase "No instance (KnownNat (CLog 4 4 - CLog 2 4))" $ testFail11 `throws` testFail11Errors- , testCase "Div 4 0 /~ 4" $ testFail12 `throws` testFail12Errors- , testCase "Mod 4 0 /~ 4" $ testFail13 `throws` testFail13Errors- , testCase "FLog 0 4 /~ 100" $ testFail14 `throws` testFail14Errors- , testCase "FLog 1 4 /~ 100" $ testFail15 `throws` testFail15Errors- , testCase "FLog 4 0 /~ 0" $ testFail16 `throws` testFail16Errors- , testCase "GCD 6 8 /~ 4" $ testFail17 `throws` testFail17Errors- , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail18 `throws` testFail18Errors- , testCase "No instance (KnownNat (Log 3 0))" $ testFail19 `throws` testFail19Errors- , testCase "No instance (KnownNat (Log 3 10))" $ testFail20 `throws` testFail20Errors- , testCase "Min a (a*b) /~ a" $ testFail21 `throws` testFail21Errors- , testCase "Max a (a*b) /~ (a*b)" $ testFail22 `throws` testFail22Errors- , testCase "(1 <=? Div 18 6) ~ False" $ testFail23 `throws` testFail23Errors- , testCase "(z <=? Max x y) /~ True" $ testFail24 `throws` testFail24Errors- , testCase "(x+1 <=? Max x y) /~ True" $ testFail25 `throws` testFail25Errors- , testCase "(x <= n) /=> (Max x y) ~ n" $ testFail26 `throws` testFail26Errors- , testCase "n + 2 <=? Max (n + 1) 1 /~ True" $ testFail27 `throws` testFail27Errors+ , testCase "CLogWZ 3 10 9 ~ 3" $+ show (test59 Proxy) @?=+ "Proxy"+ , testCase "forall x . CLogWZ 3 10 3 + x ~ x + CLogWZ 2 7 8" $+ show (test60 Proxy) @?=+ "Proxy"+ , testCase "forall x>1 . CLogWZ x (x^y) 8 ~ y" $+ show (test61 Proxy) @?=+ "Proxy"+ , testCase "KnownNat (CLogWZ 6 8 3) ~ 2" $+ show test62 @?=+ "2"+ , testCase "KnownNat (CLogWZ 3 10 9) ~ 3" $+ show test63 @?=+ "3"+ , testCase "KnownNat ((CLogWZ 2 4 11) * (3 ^ (CLogWZ 2 4 8)))) ~ 18" $+ show test64 @?=+ "18"+ , testCase "KnownNat (Max (CLogWZ 2 4 8) (CLogWZ 4 20 5)) ~ 3" $+ show test65 @?=+ "3"+ , testCase "CLogWZ 3 0 8 ~ 8" $+ show (test66 Proxy) @?=+ "Proxy"+ , testCase "forall x. CLogWZ 2 0 x ~ x" $+ show (test67 Proxy) @?=+ "Proxy"+ , testCase "CLogWZ 5 0 0 ~ 0" $+ show (test68 Proxy) @?=+ "Proxy"+ , testCase "1 <= n => CLogWZ 2 n 0 ~ CLog 2 n" $+ show (test69 (Proxy :: Proxy 3) Proxy) @?=+ "Proxy"+ , testCase "CLogWZ ~ CLog given does not loop" $+ show (test70 (Proxy :: Proxy 1)) @?=+ "Proxy" ]+ , ShouldError.tests ]---- | Assert that evaluation of the first argument (to WHNF) will throw--- an exception whose string representation contains the given--- substrings.-throws :: a -> [String] -> Assertion-throws v xs = do- result <- try (evaluate v)- case result of- Right _ -> assertFailure "No exception!"- Left (TypeError msg) ->- if all (`isInfixOf` (removeProblemChars msg)) $ map removeProblemChars xs- then return ()- else assertFailure msg---- The kind and amount of quotes in GHC error messages changes depending on--- whether or not our locale supports unicode.--- Remove the problematic characters to enable comparison of errors.-removeProblemChars = filter (`notElem` problemChars)- where problemChars = "‘’`'"
+ tests/ShouldError.hs view
@@ -0,0 +1,574 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TemplateHaskell #-}++module ShouldError (tests) where++import Data.String.Interpolate (i)+import ShouldError.Tasty (assertCompileError)+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.HUnit (testCase)++tests :: TestTree+tests = testGroup "ShouldError"+ [ test1+ , test2+ , test3+ , test4+ , test5+ , test6+ , test7+ , test8+ , test9+ , test10+ , test11+ , test12+ , test13+ , test14+ , test15+ , test16+ , test17+ , test18+ , test19+ , test20+ , test21+ , test22+ , test23+ , test24+ , test25+ , test26+ , test27+ , test28+ ]++preamble :: String+preamble = [i|+import Data.Proxy+import GHC.TypeLits+import GHC.TypeLits.Extra+|] <> "\n"++source1 :: String+source1 = preamble <> [i|+test :: Proxy (GCD 6 8) -> Proxy 4+test = id+|]++expected1 :: [String]+expected1 =+ ["Proxy (GCD 6 8) -> Proxy 4"+ ,"Proxy 4 -> Proxy 4"+ ]++test1 :: TestTree+test1 = testCase "GCD 6 8 /~ 4" $ assertCompileError source1 expected1++source2 :: String+source2 = preamble <> [i|+test :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9))+test = id+|]++expected2 :: [String]+expected2 =+#if __GLASGOW_HASKELL__ >= 904+ ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"+ ,"Proxy (2 + x) -> Proxy (2 + x)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"+ ,"Proxy (GCD 6 8 + x) -> Proxy (GCD 6 8 + x)"+ ]+#else+ ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"+ ,"Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)"+ ]+#endif++test2 :: TestTree+test2 = testCase "GCD 6 8 + x /~ x + GCD 9 6" $ assertCompileError source2 expected2++source3 :: String+source3 = preamble <> [i|+test :: Proxy (CLog 3 10) -> Proxy 2+test = id+|]++expected3 :: [String]+expected3 =+ ["Proxy (CLog 3 10) -> Proxy 2"+ ,"Proxy 2 -> Proxy 2"+ ]++test3 :: TestTree+test3 = testCase "CLog 3 10 /~ 2" $ assertCompileError source3 expected3++source4 :: String+source4 = preamble <> [i|+test :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9))+test = id+|]++expected4 :: [String]+expected4 =+#if __GLASGOW_HASKELL__ >= 904+ ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"+ ,"Proxy (3 + x) -> Proxy (3 + x)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"+ ,"Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)"+ ]+#else+ ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"+ ,"Proxy (x + CLog 2 9) -> Proxy (x + CLog 2 9)"+ ]+#endif++test4 :: TestTree+test4 = testCase "CLog 3 10 + x /~ x + CLog 2 10" $ assertCompileError source4 expected4++source5 :: String+source5 = preamble <> [i|+test :: Proxy (CLog 0 4) -> Proxy 100+test = id+|]++expected5 :: [String]+expected5 =+ ["Proxy (CLog 0 4) -> Proxy 100"+ ,"Proxy 100 -> Proxy 100"+ ]++test5 :: TestTree+test5 = testCase "CLog 0 4 /~ 100" $ assertCompileError source5 expected5++source6 :: String+source6 = preamble <> [i|+test :: Proxy (CLog 1 4) -> Proxy 100+test = id+|]++expected6 :: [String]+expected6 =+ ["Proxy (CLog 1 4) -> Proxy 100"+ ,"Proxy 100 -> Proxy 100"+ ]++test6 :: TestTree+test6 = testCase "CLog 1 4 /~ 100" $ assertCompileError source6 expected6++source7 :: String+source7 = preamble <> [i|+test :: Proxy (CLog 4 0) -> Proxy 0+test = id+|]++expected7 :: [String]+expected7 =+ ["Proxy (CLog 4 0) -> Proxy 0"+ ,"Proxy 0 -> Proxy 0"+ ]++test7 :: TestTree+test7 = testCase "CLog 4 0 /~ 0" $ assertCompileError source7 expected7++source8 :: String+source8 = preamble <> [i|+test :: Proxy (CLog 1 (1^y)) -> Proxy y+test = id+|]++expected8 :: [String]+expected8 =+ ["Proxy (CLog 1 (1 ^ y)) -> Proxy y"+ ,"Proxy y -> Proxy y"+ ]++test8 :: TestTree+test8 = testCase "CLog 1 (1^y) /~ y" $ assertCompileError source8 expected8++source9 :: String+source9 = preamble <> [i|+test :: Proxy (CLog 0 (0^y)) -> Proxy y+test = id+|]++expected9 :: [String]+expected9 =+ ["Proxy (CLog 0 (0 ^ y)) -> Proxy y"+ ,"Proxy y -> Proxy y"+ ]++test9 :: TestTree+test9 = testCase "CLog 0 (0^y) /~ y" $ assertCompileError source9 expected9++source10 :: String+source10 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test :: Integer+test = natVal (Proxy :: Proxy (CLog 1 4))+|]++expected10 :: [String]+expected10 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 2 <= 1"]+#else+ ["Couldn't match type ''False' with ''True'"]+#endif++test10 :: TestTree+test10 = testCase "No instance (KnownNat (CLog 1 4))" $ assertCompileError source10 expected10++source11 :: String+source11 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test :: Integer+test = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4)))+|]++expected11 :: [String]+expected11 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 2 <= 1"]+#else+ ["Couldn't match type ''False` with ''True'"]+#endif++test11 :: TestTree+test11 = testCase "No instance (KnownNat (CLog 4 4 - CLog 2 4))" $ assertCompileError source11 expected11++source12 :: String+source12 = preamble <> [i|+test :: Proxy (Div 4 0) -> Proxy 4+test = id+|]++expected12 :: [String]+expected12 =+ ["Proxy (Div 4 0) -> Proxy 4"+ ,"Proxy 4 -> Proxy 4"+ ]++test12 :: TestTree+test12 = testCase "Div 4 0 /~ 4" $ assertCompileError source12 expected12++source13 :: String+source13 = preamble <> [i|+test :: Proxy (Mod 4 0) -> Proxy 4+test = id+|]++expected13 :: [String]+expected13 =+ ["Proxy (Mod 4 0) -> Proxy 4"+ ,"Proxy 4 -> Proxy 4"+ ]++test13 :: TestTree+test13 = testCase "Mod 4 0 /~ 4" $ assertCompileError source13 expected13++source14 :: String+source14 = preamble <> [i|+test :: Proxy (FLog 0 4) -> Proxy 100+test = id+|]++expected14 :: [String]+expected14 =+ ["Proxy (FLog 0 4) -> Proxy 100"+ ,"Proxy 100 -> Proxy 100"+ ]++test14 :: TestTree+test14 = testCase "FLog 0 4 /~ 100" $ assertCompileError source14 expected14++source15 :: String+source15 = preamble <> [i|+test :: Proxy (FLog 1 4) -> Proxy 100+test = id+|]++expected15 :: [String]+expected15 =+ ["Proxy (FLog 1 4) -> Proxy 100"+ ,"Proxy 100 -> Proxy 100"+ ]++test15 :: TestTree+test15 = testCase "FLog 1 4 /~ 100" $ assertCompileError source15 expected15++source16 :: String+source16 = preamble <> [i|+test :: Proxy (FLog 4 0) -> Proxy 0+test = id+|]++expected16 :: [String]+expected16 =+ ["Proxy (FLog 4 0) -> Proxy 0"+ ,"Proxy 0 -> Proxy 0"+ ]++test16 :: TestTree+test16 = testCase "FLog 4 0 /~ 0" $ assertCompileError source16 expected16++source17 :: String+source17 = preamble <> [i|+test :: Proxy (LCM 6 8) -> Proxy 48+test = id+|]++expected17 :: [String]+expected17 =+ ["Proxy (LCM 6 8) -> Proxy 48"+ ,"Proxy 48 -> Proxy 48"+ ]++test17 :: TestTree+test17 = testCase "LCM 6 8 /~ 48" $ assertCompileError source17 expected17++source18 :: String+source18 = preamble <> [i|+test :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9))+test = id+|]++expected18 :: [String]+expected18 =+#if __GLASGOW_HASKELL__ >= 904+ ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"+ ,"Proxy (24 + x) -> Proxy (24 + x)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"+ ,"Proxy (LCM 6 8 + x) -> Proxy (LCM 6 8 + x)"+ ]+#else+ ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"+ ,"Proxy (x + LCM 6 9) -> Proxy (x + LCM 6 9)"+ ]+#endif++test18 :: TestTree+test18 = testCase "LCM 6 8 + x /~ x + LCM 6 9" $ assertCompileError source18 expected18++source19 :: String+source19 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test :: Integer+test = natVal (Proxy :: Proxy (Log 3 0))+|]++expected19 :: [String]+expected19 =+#if __GLASGOW_HASKELL__ >= 900+ ["Couldn't match type: FLog 3 0"+ ," with: CLog 3 0"]+#else+ ["Couldn't match type 'FLog 3 0' with 'CLog 3 0'"]+#endif++test19 :: TestTree+test19 = testCase "No instance (KnownNat (Log 3 0))" $ assertCompileError source19 expected19++source20 :: String+source20 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test :: Integer+test = natVal (Proxy :: Proxy (Log 3 10))+|]++expected20 :: [String]+expected20 =+#if __GLASGOW_HASKELL__ >= 904+ ["Couldn't match type '2' with '3'"]+#elif __GLASGOW_HASKELL__ >= 900+ ["Couldn't match type: FLog 3 10"+ ," with: CLog 3 10"]+#else+ ["Couldn't match type 'FLog 3 10' with 'CLog 3 10'"]+#endif++test20 :: TestTree+test20 = testCase "No instance (KnownNat (Log 3 10))" $ assertCompileError source20 expected20++source21 :: String+source21 = preamble <> [i|+test :: Proxy a -> Proxy b -> Proxy (Min a (a * b)) -> Proxy a+test _ _ = id+|]++expected21 :: [String]+expected21 =+ ["Proxy (Min a (a * b)) -> Proxy a"+ ,"Proxy a -> Proxy a"+ ]++test21 :: TestTree+test21 = testCase "Min a (a*b) /~ a" $ assertCompileError source21 expected21++source22 :: String+source22 = preamble <> [i|+test :: Proxy a -> Proxy b -> Proxy (Max a (a * b)) -> Proxy (a * b)+test _ _ = id+|]++expected22 :: [String]+expected22 =+#if __GLASGOW_HASKELL__ >= 900+ ["Proxy (Max a (a * b)) -> Proxy (a * b)"+ ,"Proxy (Max a (a * b)) -> Proxy (Max a (a * b))"]+#else+ ["Proxy (Max a (a * b)) -> Proxy (a * b)"+ ,"Proxy (a * b) -> Proxy (a * b)"]+#endif++test22 :: TestTree+test22 = testCase "Max a (a*b) /~ (a*b)" $ assertCompileError source22 expected22++source23 :: String+source23 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> ()+test' _ _ = ()++test :: ()+test = test' (Proxy @18) (Proxy @3)+|]++expected23 :: [String]+expected23 =+#if __GLASGOW_HASKELL__ >= 804+ ["Couldn't match type ''True' with ''False'"]+#else+ ["Couldn't match type '1 <=? Div 18 3' with ''False'"]+#endif++test23 :: TestTree+test23 = testCase "(1 <=? Div 18 3) ~ False" $ assertCompileError source23 expected23++source24 :: String+source24 = [i|+{-# LANGUAGE CPP #-}+|] <> preamble <> [i|+#if __GLASGOW_HASKELL__ >= 901+import qualified Data.Type.Ord+#endif++test :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True+test _ _ _ = id+|]++expected24 :: [String]+expected24 =+#if __GLASGOW_HASKELL__ >= 902+ ["Couldn't match type 'Data.Type.Ord.OrdCond"+ ,"(CmpNat z (Max x y)) 'True 'True 'False'"+ ,"with ''True'"]+#else+ ["Couldn't match type 'z <=? Max x y' with ''True'"]+#endif++test24 :: TestTree+test24 = testCase "(z <=? Max x y) /~ True" $ assertCompileError source24 expected24++source25 :: String+source25 = [i|+{-# LANGUAGE CPP #-}+|] <> preamble <> [i|+#if __GLASGOW_HASKELL__ >= 901+import qualified Data.Type.Ord+#endif++test :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True+test _ _ = id+|]++expected25 :: [String]+expected25 =+#if __GLASGOW_HASKELL__ >= 902+ ["Couldn't match type 'Data.Type.Ord.OrdCond"+ ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False'"+ ,"with ''True'"]+#else+ ["Couldn't match type '(x + 1) <=? Max x y' with ''True'"]+#endif++test25 :: TestTree+test25 = testCase "(x+1 <=? Max x y) /~ True" $ assertCompileError source25 expected25++source26 :: String+source26 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|++-- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true.+test' :: ((x <=? n) ~ True) => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n+test' _ _ _ = id++test = test' (Proxy @4) (Proxy @6) (Proxy @6)+|]++expected26 :: [String]+expected26 =+#if __GLASGOW_HASKELL__ >= 906+ ["Could not deduce 'Max x y ~ n'"+ ,"from the context: (x <=? n) ~ True"+ ]+#elif __GLASGOW_HASKELL__ <= 902+ ["Could not deduce: Max x y ~ n"+ ,"from the context: (x <=? n) ~ 'True"+ ]+#else+ ["Could not deduce (Max x y ~ n)"+ ,"from the context: (x <=? n) ~ 'True"+ ]+#endif++test26 :: TestTree+test26 = testCase "(x <= n) /=> (Max x y) ~ n" $ assertCompileError source26 expected26++source27 :: String+source27 = preamble <> [i|+test :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True+test _ = id+|]++expected27 :: [String]+expected27 =+ ["Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True"+ ,"Proxy 'True -> Proxy 'True"+ ]++test27 :: TestTree+test27 = testCase "n + 2 <=? Max (n + 1) 1 /~ True" $ assertCompileError source27 expected27++source28 :: String+source28 = [i|+{-# LANGUAGE KindSignatures #-}+|] <> preamble <> [i|+type Size (n :: Nat) = Max 0 (CLogWZ 2 n 0)++pack :: Proxy n -> Proxy (Size n)+pack _ = Proxy++repro :: Proxy (Size 1)+repro = pack (undefined :: Proxy (n :: Nat))+|]++expected28 :: [String]+expected28 =+ ["CLogWZ 2 n"+ ,"ambiguous"+ ]++test28 :: TestTree+test28 = testCase "CLogWZ reify with Max 0 (type synonym) doesn't panic" $+ assertCompileError source28 expected28
+ tests/ShouldError/Tasty.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE CPP #-}++module ShouldError.Tasty where++import Data.List (isInfixOf)+import Data.Maybe (fromMaybe)+import System.Environment (lookupEnv)+import System.Exit+import System.IO+import System.IO.Temp+import System.Process+import Test.Tasty.HUnit++-- | Assert that a Haskell code snippet fails to compile with expected error messages+assertCompileError :: String -> [String] -> Assertion+assertCompileError source expectedErrors = do+ -- XXX: This will pick the wrong GHC if the HC environment variable (as seen on CI)+ -- isn't set and the test suite is compiled with a GHC compiler other than the+ -- system's default.+ hc <- fromMaybe "ghc" <$> lookupEnv "HC"+ withSystemTempFile "ShouldError.hs" $ \tempFile tempHandle -> do+ hPutStr tempHandle source+ hClose tempHandle+ (exitCode, _, stderrOutput) <- readProcessWithExitCode hc+ [ "-XCPP"+ , "-XDataKinds"+ , "-XTypeOperators"+ , "-XTypeApplications"+ , "-XTypeFamilies"+ , "-XNoStarIsType"+ , "-fno-code"+ , "-fplugin", "GHC.TypeLits.Normalise"+ , "-fplugin", "GHC.TypeLits.KnownNat.Solver"+ , "-fplugin", "GHC.TypeLits.Extra.Solver"+ , tempFile+ ] ""+ case exitCode of+ ExitSuccess -> assertFailure "Expected compilation to fail but it succeeded"+ ExitFailure _ ->+ let cleanedStderr = removeProblemChars stderrOutput+ cleanedExpected = map removeProblemChars expectedErrors+ in if all (`isInfixOf` cleanedStderr) cleanedExpected+ then return ()+ else assertFailure $ "Error message mismatch:\n" +++ "Expected substrings: " ++ show expectedErrors ++ "\n" +++ "Actual output:\n" ++ stderrOutput++-- | Remove problematic characters that vary depending on locale+-- The kind and amount of quotes in GHC error messages changes depending on+-- whether or not our locale supports unicode.+removeProblemChars :: String -> String+removeProblemChars = filter (`notElem` problemChars)+ where problemChars = "‘’`'"