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