diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 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,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 - . + * @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)@ - . + + * @CLogWZ@: extension of @CLog@, which returns the additional third argument in case the second argument is zero + * @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 @@ -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 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.hs b/src/GHC/TypeLits/Extra.hs --- a/src/GHC/TypeLits/Extra.hs +++ b/src/GHC/TypeLits/Extra.hs @@ -20,6 +20,8 @@ * 'CLog': type-level equivalent of /the ceiling of/ .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 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) 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,327 @@ +{-| +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)@" +-- +-- * 'CLogWZ': extension of @CLog@, which returns the additional third argument in case the second argument is zero +-- +-- * '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 + , 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 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,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" 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 @@ -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 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,11 @@ Maintainer : Christiaan Baaij -} -{-# 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] 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/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -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 = "‘’`'" diff --git a/tests/ShouldError.hs b/tests/ShouldError.hs new file mode 100644 --- /dev/null +++ b/tests/ShouldError.hs @@ -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 diff --git a/tests/ShouldError/Tasty.hs b/tests/ShouldError/Tasty.hs new file mode 100644 --- /dev/null +++ b/tests/ShouldError/Tasty.hs @@ -0,0 +1,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 = "‘’`'"