diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,48 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.9.6 *May 13th 2026* +* Bump ghc-tcplugin-api to prepare for inclusion into stackage + +## 0.9.5 *March 19th 2026* +* Make the test suite not emit compile warnings + +## 0.9.4 *March 19th 2026* +* Fixes [#116](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/113) Compile-time loop when processing Given constraints. +* Fixes [#119](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/119) solving constraints involving type families applied to normalised Nat expressions (e.g. `Foo (a + b)`). +* Fixes [#120](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/120) stop emitting Assert (a <=? b) msg ~ (() :: Constraint) constraints +* Fixed regression [#124](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/124) involving unification of summands. + +## 0.9.3 *December 2nd 2025* +* Fixes [#114](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/113) Poor error message in plugin version 0.8 and higher +* Fixes [#113](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/113) Wanted contraints rewrites to itself, leading to infinite solver iterations + +## 0.9.2 *December 2nd 2025* +* Fixes [#108](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/108) Type error after plugin update +* Fixes [#111](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/111) Exception for unifying under non-injective type families + +## 0.9.1 *October 21st 2025* +* Fixes [#105](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/105) Unsound derived contradiction with 0.9.0 +* Support for GHC 9.14 + +## 0.9.0 *October 17th 2025* +* Drop `TyConSubst` argument from `normaliseNat`, `normaliseNatEverywhere` and `normaliseSimplifyNat`. +* Expose `GHC.TypeLits.Normalise.Compat` +* Report contractions for equations such as `1 + k <= n; n ~ 0` in "solve givens" phase + +## 0.8.1 *October 1st 2025* +* Fixes [#85](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/85) Deriving equalities from inequalities produces a misleading error message +* Fixes [#94](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94) Normalization fails when adding an equality constraint with substraction +* Fixes [#96](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/96) Unification fails when variables occur on both LHS and RHS +* Fixes [#99](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/99) ghc-typelits-natnormalise erroneously unifies under type families +* Fixes [100](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/100) stack space overflow with ghc-typelits-natnormalize 0.8 + +## 0.8 *September 8th 2025* +* Uses https://hackage.haskell.org/package/ghc-tcplugin-api to make supporting new GHC versions easier +* Support for GHC versions older than 8.8 is dropped +* Fixes [#70](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/70) The constraint 0 < d+1 does not seem to resolve? +* Fixes [#71](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/71) "Could not deduce ... from the context ...", but if the context removed, deduced outright +* Fixes [#47](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/47) Could not deduce `KnownNat (F ((2 * a) + a) b + (2 * F (a + (2 * a)) b))` from `KnownNat (F (a * 3) b * 3)` + ## 0.7.12 *August 22nd 2025* * Support for GHC 9.10.2 diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal --- a/ghc-typelits-natnormalise.cabal +++ b/ghc-typelits-natnormalise.cabal @@ -1,43 +1,44 @@ +cabal-version: 3.0 name: ghc-typelits-natnormalise -version: 0.7.12 +version: 0.9.6 synopsis: GHC typechecker plugin for types of kind GHC.TypeLits.Nat description: A type checker plugin for GHC that can solve /equalities/ and /inequalities/ of types of kind @Nat@, where these types are either: - . + * Type-level naturals - . + * Type variables - . + * Applications of the arithmetic expressions @(+,-,*,^)@. - . + It solves these equalities by normalising them to /sort-of/ @SOP@ (Sum-of-Products) form, and then perform a simple syntactic equality. - . + For example, this solver can prove the equality between: - . + @ (x + 2)^(y + 2) @ - . + and - . + @ 4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2 @ - . + Because the latter is actually the @SOP@ normal form of the former. - . + To use the plugin, add the - . + @ OPTIONS_GHC -fplugin GHC.TypeLits.Normalise @ - . + Pragma to the header of your file. homepage: http://www.clash-lang.org/ bug-reports: http://github.com/clash-lang/ghc-typelits-natnormalise/issues -license: BSD2 +license: BSD-2-Clause license-file: LICENSE author: Christiaan Baaij maintainer: christiaan.baaij@gmail.com @@ -45,13 +46,11 @@ 2017-2018, QBayLogic B.V. category: Type System build-type: Simple -extra-source-files: README.md +extra-doc-files: README.md CHANGELOG.md -cabal-version: >=1.10 -tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5, - GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8, - GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1, - GHC == 9.10.2, GHC == 9.12.1 +tested-with: GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8, + GHC == 9.4.8, GHC == 9.6.7, GHC == 9.8.4, GHC == 9.10.2, + GHC == 9.12.2 source-repository head type: git @@ -65,26 +64,29 @@ library exposed-modules: GHC.TypeLits.Normalise, + GHC.TypeLits.Normalise.Compat, GHC.TypeLits.Normalise.SOP, GHC.TypeLits.Normalise.Unify build-depends: base >=4.9 && <5, - containers >=0.5.7.1 && <0.8, - ghc >=8.0.1 && <9.13, - ghc-tcplugins-extra >=0.5, - transformers >=0.5.2.0 && < 0.7 + containers >=0.5.7.1 && <0.9, + ghc >=8.8.1 && <9.15, + ghc-tcplugin-api >=0.19 && <0.20, + transformers >=0.5.2 && < 0.7 if impl(ghc >= 9.0.0) - build-depends: ghc-bignum >=1.0 && <1.4 + build-depends: ghc-bignum >=1.0 && <1.5 else build-depends: integer-gmp >=1.0 && <1.1 + + mixins: + ghc + ( TcTypeNats as GHC.Builtin.Types.Literals + , TyCon as GHC.Core.TyCon + , TysWiredIn as GHC.Builtin.Types + , Unique as GHC.Types.Unique + , Util as GHC.Utils.Misc + ) + hs-source-dirs: src - if impl(ghc >= 8.0) && impl(ghc < 9.4) - hs-source-dirs: src-pre-ghc-9.4 - if impl(ghc >= 9.4) && impl(ghc < 9.11) - hs-source-dirs: src-ghc-9.4 - build-depends: template-haskell >=2.17 && <2.23 - if impl(ghc >= 9.11) && impl(ghc < 9.13) - hs-source-dirs: src-ghc-9.12 - build-depends: template-haskell >=2.17 && <2.24 default-language: Haskell2010 other-extensions: CPP LambdaCase @@ -98,23 +100,26 @@ test-suite unit-tests type: exitcode-stdio-1.0 main-is: Tests.hs - Other-Modules: ErrorTests + Other-Modules: ShouldError + ShouldError.Tasty build-depends: base >=4.8 && <5, ghc-typelits-natnormalise, + interpolate, + process, tasty >= 0.10, tasty-hunit >= 0.9, - template-haskell >= 2.11.0.0 + temporary if impl(ghc >= 9.4) build-depends: ghc-prim >= 0.9 hs-source-dirs: tests + ghc-options: -Wall default-language: Haskell2010 other-extensions: DataKinds GADTs KindSignatures NoImplicitPrelude - TemplateHaskell TypeFamilies TypeOperators ScopedTypeVariables if flag(deverror) - ghc-options: -dcore-lint + ghc-options: -Werror -dcore-lint diff --git a/src-ghc-9.12/GHC/TypeLits/Normalise.hs b/src-ghc-9.12/GHC/TypeLits/Normalise.hs deleted file mode 100644 --- a/src-ghc-9.12/GHC/TypeLits/Normalise.hs +++ /dev/null @@ -1,739 +0,0 @@ -{-| -Copyright : (C) 2015-2016, University of Twente, - 2017 , QBayLogic B.V. -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij - -A type checker plugin for GHC that can solve /equalities/ of types of kind -'GHC.TypeLits.Nat', where these types are either: - -* Type-level naturals -* Type variables -* Applications of the arithmetic expressions @(+,-,*,^)@. - -It solves these equalities by normalising them to /sort-of/ -'GHC.TypeLits.Normalise.SOP.SOP' (Sum-of-Products) form, and then perform a -simple syntactic equality. - -For example, this solver can prove the equality between: - -@ -(x + 2)^(y + 2) -@ - -and - -@ -4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2 -@ - -Because the latter is actually the 'GHC.TypeLits.Normalise.SOP.SOP' normal form -of the former. - -To use the plugin, add - -@ -{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\} -@ - -To the header of your file. - -== Treating subtraction as addition with a negated number - -If you are absolutely sure that your subtractions can /never/ lead to (a locally) -negative number, you can ask the plugin to treat subtraction as addition with -a negated operand by additionally adding: - -@ -{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\} -@ - -to the header of your file, thereby allowing to use associativity and -commutativity rules when proving constraints involving subtractions. Note that -this option can lead to unsound behaviour and should be handled with extreme -care. - -=== When it leads to unsound behaviour - -For example, enabling the /allow-negated-numbers/ feature would allow -you to prove: - -@ -(n - 1) + 1 ~ n -@ - -/without/ a @(1 <= n)@ constraint, even though when /n/ is set to /0/ the -subtraction @n-1@ would be locally negative and hence not be a natural number. - -This would allow the following erroneous definition: - -@ -data Fin (n :: Nat) where - FZ :: Fin (n + 1) - FS :: Fin n -> Fin (n + 1) - -f :: forall n . Natural -> Fin n -f n = case of - 0 -> FZ - x -> FS (f \@(n-1) (x - 1)) - -fs :: [Fin 0] -fs = f \<$\> [0..] -@ - -=== When it might be Okay - -This example is taken from the -library. - -When you have: - -@ --- | Singleton type for the number of repetitions of an element. -data Times (n :: Nat) where - T :: Times n - --- | An element of a "run-length encoded" vector, containing the value and --- the number of repetitions -data Elem :: Type -> Nat -> Type where - (:*) :: t -> Times n -> Elem t n - --- | A length-indexed vector, optimised for repetitions. -data OptVector :: Type -> Nat -> Type where - End :: OptVector t 0 - (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n -@ - -And you want to define: - -@ --- | Append two optimised vectors. -type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where - ys ++ End = ys - End ++ ys = ys - (x :- xs) ++ ys = x :- (xs ++ ys) -@ - -then the last line will give rise to the constraint: - -@ -(n-l)+m ~ (n+m)-l -@ - -because: - -@ -x :: Elem t l -xs :: OptVector t (n-l) -ys :: OptVector t m -@ - -In this case it's okay to add - -@ -{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\} -@ - -if you can convince yourself you will never be able to construct a: - -@ -xs :: OptVector t (n-l) -@ - -where /n-l/ is a negative number. --} - -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE TemplateHaskellQuotes #-} - -{-# OPTIONS_HADDOCK show-extensions #-} - -module GHC.TypeLits.Normalise - ( plugin ) -where - --- external -import Control.Arrow (second) -import Control.Monad ((<=<), forM) -import Control.Monad.Trans.Writer.Strict -import Data.Either (partitionEithers, rights) -import Data.IORef -import Data.List (intersect, partition, stripPrefix, find) -import Data.Maybe (mapMaybe, catMaybes) -import Data.Set (Set, empty, toList, notMember, fromList, union) -import Text.Read (readMaybe) -import qualified Data.Type.Ord -import qualified GHC.TypeError - -import GHC.TcPluginM.Extra (tracePlugin, newGiven, newWanted) - --- GHC API -import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey) -import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon) -import GHC.Builtin.Types.Literals - (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon) -import GHC.Builtin.Types (naturalTy, cTupleDataCon, cTupleTyCon) -import GHC.Builtin.Types.Literals (typeNatCmpTyCon) -import GHC.Core (Expr (..)) -import GHC.Core.Class (className) -import GHC.Core.Coercion (Coercion, Role (..), mkUnivCo) -import GHC.Core.DataCon (dataConWrapId) -import GHC.Core.Predicate - (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType, mkClassPred, - mkPrimEqPred, isEqPred, isEqPrimPred, getClassPredTys_maybe) -import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..)) -import GHC.Core.TyCon (TyCon) -import GHC.Core.Type - (Kind, PredType, mkTyVarTy, tyConAppTyCon_maybe, typeKind, mkTyConApp) -import GHC.Core.TyCo.Compare - (eqType) -import GHC.Data.IOEnv (getEnv) -import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin) -import GHC.Plugins (thNameToGhcNameIO, HscEnv (hsc_NC)) -import GHC.Tc.Plugin - (TcPluginM, tcLookupClass, tcPluginTrace, tcPluginIO, newEvVar) -import GHC.Tc.Plugin (tcLookupTyCon, unsafeTcPluginTcM) -import GHC.Tc.Types (TcPlugin (..), TcPluginSolveResult(..), Env (env_top)) -import GHC.Tc.Types.Constraint - (Ct, CtEvidence (..), TcEvDest (..), ctEvidence, ctEvCoercion, ctLoc, isGiven, - isWanted, mkNonCanonical, isWantedCt, ctEvLoc, ctEvPred, ctEvExpr, - emptyRewriterSet, setCtEvLoc) -import GHC.Tc.Types.CtLoc (CtLoc, ctLocSpan, setCtLocSpan) -import GHC.Tc.Types.Evidence (EvBindsVar, EvTerm (..), evCast, evId, mkEvCast) -import GHC.Types.Unique.FM (emptyUFM) -import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text) -import GHC (Name) - --- template-haskell -import qualified Language.Haskell.TH as TH - --- internal -import GHC.TypeLits.Normalise.SOP -import GHC.TypeLits.Normalise.Unify hiding (subtractionToPred) - -isEqPredClass :: PredType -> Bool -isEqPredClass ty = case tyConAppTyCon_maybe ty of - Just tc -> tc `hasKey` eqTyConKey || tc `hasKey` heqTyConKey - _ -> False - --- | To use the plugin, add --- --- @ --- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\} --- @ --- --- To the header of your file. -plugin :: Plugin -plugin - = defaultPlugin - { tcPlugin = fmap (normalisePlugin . foldr id defaultOpts) . traverse parseArgument - , pluginRecompile = purePlugin - } - where - parseArgument "allow-negated-numbers" = Just (\ opts -> opts { negNumbers = True }) - parseArgument (readMaybe <=< stripPrefix "depth=" -> Just depth) = Just (\ opts -> opts { depth }) - parseArgument _ = Nothing - defaultOpts = Opts { negNumbers = False, depth = 5 } - -data Opts = Opts { negNumbers :: Bool, depth :: Word } - -normalisePlugin :: Opts -> TcPlugin -normalisePlugin opts = tracePlugin "ghc-typelits-natnormalise" - TcPlugin { tcPluginInit = lookupExtraDefs - , tcPluginSolve = decideEqualSOP opts - , tcPluginRewrite = const emptyUFM - , tcPluginStop = const (return ()) - } - -type ExtraDefs = (IORef (Set CType), (TyCon,TyCon,TyCon)) - -lookupExtraDefs :: TcPluginM ExtraDefs -lookupExtraDefs = do - ref <- tcPluginIO (newIORef empty) - ordCond <- lookupTHName ''Data.Type.Ord.OrdCond >>= tcLookupTyCon - leqT <- lookupTHName ''(Data.Type.Ord.<=) >>= tcLookupTyCon - assertT <- lookupTHName ''GHC.TypeError.Assert >>= tcLookupTyCon - return (ref, (leqT,assertT,ordCond)) - -lookupTHName :: TH.Name -> TcPluginM Name -lookupTHName th = do - nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv) - res <- tcPluginIO $ thNameToGhcNameIO nc th - maybe (fail $ "Failed to lookup " ++ show th) return res - -decideEqualSOP - :: Opts - -> ExtraDefs - -- ^ 1. Givens that is already generated. - -- We have to generate new givens at most once; - -- otherwise GHC will loop indefinitely. - -- - -- - -- 2. For GHc 9.2: TyCon of Data.Type.Ord.OrdCond - -- For older: TyCon of GHC.TypeLits.<=? - -> EvBindsVar - -> [Ct] - -> [Ct] - -> TcPluginM TcPluginSolveResult - --- Simplification phase: Derives /simplified/ givens; --- we can reduce given constraints like @Show (Foo (n + 2))@ --- to its normal form @Show (Foo (2 + n))@, which is eventually --- useful in solving phase. --- --- This helps us to solve /indirect/ constraints; --- without this phase, we cannot derive, e.g., --- @IsVector UVector (Fin (n + 1))@ from --- @Unbox (1 + n)@! -decideEqualSOP opts (gen'd,(leqT,_,_)) ev givens [] = do - done <- tcPluginIO $ readIORef gen'd - let reds = - filter (\(_,(_,_,v)) -> null v || negNumbers opts) $ - reduceGivens opts leqT done givens - newlyDone = map (\(_,(prd, _,_)) -> CType prd) reds - tcPluginIO $ - modifyIORef' gen'd $ union (fromList newlyDone) - newGivens <- forM reds $ \(origCt, (pred', evTerm, _)) -> - mkNonCanonical' (ctLoc origCt) <$> newGiven ev (ctLoc origCt) pred' evTerm - return (TcPluginOk [] newGivens) - --- Solving phase. --- Solves in/equalities on Nats and simplifiable constraints --- containing naturals. -decideEqualSOP opts (gen'd,tcs@(leqT,_,_)) ev givens wanteds = do - let unit_wanteds = mapMaybe (toNatEquality tcs) wanteds - nonEqs = filter ( not - . (\p -> isEqPred p || isEqPrimPred p) - . ctEvPred - . ctEvidence ) - wanteds - done <- tcPluginIO $ readIORef gen'd - let redGs = reduceGivens opts leqT done givens - newlyDone = map (\(_,(prd, _,_)) -> CType prd) redGs - redGivens <- forM redGs $ \(origCt, (pred', evTerm, _)) -> - mkNonCanonical' (ctLoc origCt) <$> newGiven ev (ctLoc origCt) pred' evTerm - reducible_wanteds - <- catMaybes <$> mapM (\ct -> fmap (ct,) <$> - reduceNatConstr (givens ++ redGivens) ct) - nonEqs - if null unit_wanteds && null reducible_wanteds - then return $ TcPluginOk [] [] - else do - -- Since reducible wanteds also can have some negation/subtraction - -- subterms, we have to make sure appropriate inequalities to hold. - -- Here, we generate such additional inequalities for reduction - -- that is to be added to new [W]anteds. - ineqForRedWants <- fmap concat $ forM redGs $ \(ct, (_,_, ws)) -> forM ws $ - fmap (mkNonCanonical' (ctLoc ct)) . newWanted (ctLoc ct) - tcPluginIO $ - modifyIORef' gen'd $ union (fromList newlyDone) - let unit_givens = mapMaybe - (toNatEquality tcs) - givens - sr <- simplifyNats opts leqT unit_givens unit_wanteds - tcPluginTrace "normalised" (ppr sr) - reds <- forM reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do - wants <- evSubtPreds (ctLoc origCt) $ subToPred opts leqT ws - return ((term, origCt), wDicts ++ wants) - case sr of - Simplified evs -> do - let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs - -- Only solve derived when we solved a wanted - simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of - [] -> [] - _ -> simpld - (solved',newWanteds) = second concat (unzip $ simpld1 ++ reds) - return (TcPluginOk solved' $ newWanteds ++ ineqForRedWants) - Impossible eq -> return (TcPluginContradiction [fromNatEquality eq]) - -type NatEquality = (Ct,CoreSOP,CoreSOP) -type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool)) - -reduceGivens :: Opts -> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))] -reduceGivens opts leqT done givens = - let nonEqs = - [ ct - | ct <- givens - , let ev = ctEvidence ct - prd = ctEvPred ev - , isGiven ev - , not $ (\p -> isEqPred p || isEqPrimPred p || isEqPredClass p) prd - ] - in filter - (\(_, (prd, _, _)) -> - notMember (CType prd) done - ) - $ mapMaybe - (\ct -> (ct,) <$> tryReduceGiven opts leqT givens ct) - nonEqs - -tryReduceGiven - :: Opts -> TyCon -> [Ct] -> Ct - -> Maybe (PredType, EvTerm, [PredType]) -tryReduceGiven opts leqT simplGivens ct = do - let (mans, ws) = - runWriter $ normaliseNatEverywhere $ - ctEvPred $ ctEvidence ct - ws' = [ p - | p <- subToPred opts leqT ws - , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens - ] - -- deps = unitDVarSet (ctEvId ct) - pred' <- mans - return (pred', toReducedDict (ctEvidence ct) pred', ws') - -fromNatEquality :: Either NatEquality NatInEquality -> Ct -fromNatEquality (Left (ct, _, _)) = ct -fromNatEquality (Right (ct, _)) = ct - -reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct])) -reduceNatConstr givens ct = do - let pred0 = ctEvPred $ ctEvidence ct - (mans, tests) = runWriter $ normaliseNatEverywhere pred0 - case mans of - Nothing -> return Nothing - Just pred' -> do - case find ((`eqType` pred') .ctEvPred . ctEvidence) givens of - -- No existing evidence found - Nothing -> case getClassPredTys_maybe pred' of - -- Are we trying to solve a class instance? - Just (cls,_) | className cls /= knownNatClassName -> do - -- Create new evidence binding for normalized class constraint - evVar <- newEvVar pred' - -- Bind the evidence to a new wanted normalized class constraint - let wDict = mkNonCanonical - (CtWanted pred' (EvVarDest evVar) (ctLoc ct) emptyRewriterSet) - -- Evidence for current wanted is simply the coerced binding for - -- the new binding - evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise") [] - Representational - pred' pred0 - ev = mkEvCast (evId evVar) evCo - -- Use newly created coerced wanted as evidence, and emit the - -- normalized wanted as a new constraint to solve. - return (Just (ev, tests, [wDict])) - _ -> return Nothing - -- Use existing evidence - Just c -> return (Just (toReducedDict (ctEvidence c) pred0, tests, [])) - -toReducedDict :: CtEvidence -> PredType -> EvTerm -toReducedDict ct pred' = - let pred0 = ctEvPred ct - evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise") [] - Representational - pred0 pred' - ev = mkEvCast (ctEvExpr ct) evCo - in ev - -data SimplifyResult - = Simplified [((EvTerm,Ct),[Ct])] - | Impossible (Either NatEquality NatInEquality) - -instance Outputable SimplifyResult where - ppr (Simplified evs) = text "Simplified" $$ ppr evs - ppr (Impossible eq) = text "Impossible" <+> ppr eq - -simplifyNats - :: Opts - -- ^ Allow negated numbers (potentially unsound!) - -> TyCon - -- * TyCon of Data.Type.Ord.<= - -> [(Either NatEquality NatInEquality,[(Type,Type)])] - -- ^ Given constraints - -> [(Either NatEquality NatInEquality,[(Type,Type)])] - -- ^ Wanted constraints - -> TcPluginM SimplifyResult -simplifyNats opts@Opts {..} leqT eqsG eqsW = do - let eqsG1 = map (second (const ([] :: [(Type,Type)]))) eqsG - (varEqs,otherEqs) = partition isVarEqs eqsG1 - fancyGivens = concatMap (makeGivensSet otherEqs) varEqs - case varEqs of - [] -> do - let eqs = otherEqs ++ eqsW - tcPluginTrace "simplifyNats" (ppr eqs) - simples [] [] [] [] [] eqs - _ -> do - tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")") - (ppr varEqs) - - allSimplified <- forM fancyGivens $ \v -> do - let eqs = v ++ eqsW - tcPluginTrace "simplifyNats" (ppr eqs) - simples [] [] [] [] [] eqs - - pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified) - where - simples :: [Coercion] - -> [CoreUnify] - -> [((EvTerm, Ct), [Ct])] - -> [(CoreSOP,CoreSOP,Bool)] - -> [(Either NatEquality NatInEquality,[(Type,Type)])] - -> [(Either NatEquality NatInEquality,[(Type,Type)])] - -> TcPluginM SimplifyResult - simples _ _subst evs _leqsG _xs [] = return (Simplified evs) - simples deps subst evs leqsG xs (eq@(Left (ct,u,v),k):eqs') = do - let u' = substsSOP subst u - v' = substsSOP subst v - ur <- unifyNats ct u' v' - tcPluginTrace "unifyNats result" (ppr ur) - case ur of - Win -> do - evs' <- maybe evs (:evs) <$> evMagic ct deps empty (subToPred opts leqT k) - simples deps subst evs' leqsG [] (xs ++ eqs') - Lose -> if null evs && null eqs' - then return (Impossible (fst eq)) - else simples deps subst evs leqsG xs eqs' - Draw [] -> simples deps subst evs [] (eq:xs) eqs' - Draw subst' -> do - evM <- evMagic ct deps empty (map unifyItemToPredType subst' ++ - subToPred opts leqT k) - let (leqsG1, deps1) - | isGiven (ctEvidence ct) = ( eqToLeq u' v' ++ leqsG - , ctEvCoercion (ctEvidence ct):deps) - | otherwise = (leqsG, deps) - case evM of - Nothing -> simples deps1 subst evs leqsG1 xs eqs' - Just ev -> - simples (ctEvCoercion (ctEvidence ct):deps) - (substsSubst subst' subst ++ subst') - (ev:evs) leqsG1 [] (xs ++ eqs') - simples deps subst evs leqsG xs (eq@(Right (ct,u@(x,y,b)),k):eqs') = do - let u' = substsSOP subst (subtractIneq u) - x' = substsSOP subst x - y' = substsSOP subst y - uS = (x',y',b) - leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG - | otherwise = leqsG - ineqs = concat [ leqsG - , map (substLeq subst) leqsG - , map snd (rights (map fst eqsG)) - ] - tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs)) - case runWriterT (isNatural u') of - Just (True,knW) -> do - evs' <- maybe evs (:evs) <$> evMagic ct deps knW (subToPred opts leqT k) - simples deps subst evs' leqsG' xs eqs' - - Just (False,_) | null k -> return (Impossible (fst eq)) - _ -> do - let solvedIneq = mapMaybe runWriterT - -- it is an inequality that can be instantly solved, such as - -- `1 <= x^y` - -- OR - (instantSolveIneq depth u: - instantSolveIneq depth uS: - -- This inequality is either a given constraint, or it is a wanted - -- constraint, which in normal form is equal to another given - -- constraint, hence it can be solved. - -- OR - map (solveIneq depth u) ineqs ++ - -- The above, but with valid substitutions applied to the wanted. - map (solveIneq depth uS) ineqs) - smallest = solvedInEqSmallestConstraint solvedIneq - case smallest of - (True,kW) -> do - evs' <- maybe evs (:evs) <$> evMagic ct deps kW (subToPred opts leqT k) - simples deps subst evs' leqsG' xs eqs' - _ -> simples deps subst evs leqsG (eq:xs) eqs' - - eqToLeq x y = [(x,y,True),(y,x,True)] - substLeq s (x,y,b) = (substsSOP s x, substsSOP s y, b) - - isVarEqs (Left (_,S [P [V _]], S [P [V _]]), _) = True - isVarEqs _ = False - - makeGivensSet otherEqs varEq - = let (noMentionsV,mentionsV) = partitionEithers - (map (matchesVarEq varEq) otherEqs) - (mentionsLHS,mentionsRHS) = partitionEithers mentionsV - vS = swapVar varEq - givensLHS = case mentionsLHS of - [] -> [] - _ -> [mentionsLHS ++ ((varEq:mentionsRHS) ++ noMentionsV)] - givensRHS = case mentionsRHS of - [] -> [] - _ -> [mentionsRHS ++ (vS:mentionsLHS ++ noMentionsV)] - in case mentionsV of - [] -> [noMentionsV] - _ -> givensLHS ++ givensRHS - - matchesVarEq (Left (_, S [P [V v1]], S [P [V v2]]),_) r = case r of - (Left (_,S [P [V v3]],_),_) - | v1 == v3 -> Right (Left r) - | v2 == v3 -> Right (Right r) - (Left (_,_,S [P [V v3]]),_) - | v1 == v3 -> Right (Left r) - | v2 == v3 -> Right (Right r) - (Right (_,(S [P [V v3]],_,_)),_) - | v1 == v3 -> Right (Left r) - | v2 == v3 -> Right (Right r) - (Right (_,(_,S [P [V v3]],_)),_) - | v1 == v3 -> Right (Left r) - | v2 == v3 -> Right (Right r) - _ -> Left r - matchesVarEq _ _ = error "internal error" - - swapVar (Left (ct,S [P [V v1]], S [P [V v2]]),ps) = - (Left (ct,S [P [V v2]], S [P [V v1]]),ps) - swapVar _ = error "internal error" - - findFirstSimpliedWanted (Impossible e) _ = Impossible e - findFirstSimpliedWanted (Simplified evs) s2 - | any (isWantedCt . snd . fst) evs - = Simplified evs - | otherwise - = s2 - --- If we allow negated numbers we simply do not emit the inequalities --- derived from the subtractions that are converted to additions with a --- negated operand -subToPred :: Opts -> TyCon -> [(Type, Type)] -> [PredType] -subToPred Opts{..} leqT - | negNumbers = const [] - | otherwise = map leq - where - leq (a,b) = - let lhs = TyConApp leqT [naturalTy,b,a] - rhs = TyConApp (cTupleTyCon 0) [] - in mkPrimEqPred lhs rhs - --- Extract the Nat equality constraints -toNatEquality :: (TyCon,TyCon,TyCon) -> Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)]) -toNatEquality (_,assertT,ordCond) ct = case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 t2 - -> go t1 t2 - IrredPred p - -> go2 p - _ -> Nothing - where - go (TyConApp tc xs) (TyConApp tc' ys) - | tc == tc' - , null ([tc,tc'] `intersect` [typeNatAddTyCon,typeNatSubTyCon - ,typeNatMulTyCon,typeNatExpTyCon]) - = case filter (not . uncurry eqType) (zip xs ys) of - [(x,y)] - | isNatKind (typeKind x) - , isNatKind (typeKind y) - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - -> Just (Left (ct, x', y'),k1 ++ k2) - _ -> Nothing - | tc == ordCond - , [_,cmp,lt,eq,gt] <- xs - , TyConApp tcCmpNat [x,y] <- cmp - , tcCmpNat == typeNatCmpTyCon - , TyConApp ltTc [] <- lt - , ltTc == promotedTrueDataCon - , TyConApp eqTc [] <- eq - , eqTc == promotedTrueDataCon - , TyConApp gtTc [] <- gt - , gtTc == promotedFalseDataCon - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - , let ks = k1 ++ k2 - = case tc' of - _ | tc' == promotedTrueDataCon - -> Just (Right (ct, (x', y', True)), ks) - _ | tc' == promotedFalseDataCon - -> Just (Right (ct, (x', y', False)), ks) - _ -> Nothing - | tc == assertT - , tc' == (cTupleTyCon 0) - , [] <- ys - , [TyConApp ordCondTc zs, _] <- xs - , ordCondTc == ordCond - , [_,cmp,lt,eq,gt] <- zs - , TyConApp tcCmpNat [x,y] <- cmp - , tcCmpNat == typeNatCmpTyCon - , TyConApp ltTc [] <- lt - , ltTc == promotedTrueDataCon - , TyConApp eqTc [] <- eq - , eqTc == promotedTrueDataCon - , TyConApp gtTc [] <- gt - , gtTc == promotedFalseDataCon - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - , let ks = k1 ++ k2 - = Just (Right (ct, (x', y', True)), ks) - - go x y - | isNatKind (typeKind x) - , isNatKind (typeKind y) - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - = Just (Left (ct,x',y'),k1 ++ k2) - | otherwise - = Nothing - - go2 (TyConApp tc ys) - | tc == assertT - , [TyConApp ordCondTc xs, _] <- ys - , ordCondTc == ordCond - , [_,cmp,lt,eq,gt] <- xs - , TyConApp tcCmpNat [x,y] <- cmp - , tcCmpNat == typeNatCmpTyCon - , TyConApp ltTc [] <- lt - , ltTc == promotedTrueDataCon - , TyConApp eqTc [] <- eq - , eqTc == promotedTrueDataCon - , TyConApp gtTc [] <- gt - , gtTc == promotedFalseDataCon - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - , let ks = k1 ++ k2 - = Just (Right (ct, (x', y', True)), ks) - - go2 _ = Nothing - - isNatKind :: Kind -> Bool - isNatKind = (`eqType` naturalTy) - -unifyItemToPredType :: CoreUnify -> PredType -unifyItemToPredType ui = mkPrimEqPred ty1 ty2 - where - ty1 = case ui of - SubstItem {..} -> mkTyVarTy siVar - UnifyItem {..} -> reifySOP siLHS - ty2 = case ui of - SubstItem {..} -> reifySOP siSOP - UnifyItem {..} -> reifySOP siRHS - -evSubtPreds :: CtLoc -> [PredType] -> TcPluginM [Ct] -evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc) - -evMagic :: Ct -> [Coercion] -> Set CType -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct])) -evMagic ct deps knW preds = do - holeWanteds <- evSubtPreds (ctLoc ct) preds - knWanted <- mapM (mkKnWanted (ctLoc ct)) (toList knW) - let newWant = knWanted ++ holeWanteds - case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 t2 -> - let ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") deps Nominal t1 t2 - in return (Just ((EvExpr (Coercion ctEv), ct),newWant)) - IrredPred p -> - let t1 = mkTyConApp (cTupleTyCon 0) [] - co = mkUnivCo (PluginProv "ghc-typelits-natnormalise") deps Representational t1 p - dcApp = evId (dataConWrapId (cTupleDataCon 0)) - in return (Just ((evCast dcApp co, ct),newWant)) - _ -> return Nothing - -mkNonCanonical' :: CtLoc -> CtEvidence -> Ct -mkNonCanonical' origCtl ev = - let ct_ls = ctLocSpan origCtl - ctl = ctEvLoc ev - in mkNonCanonical (setCtEvLoc ev (setCtLocSpan ctl ct_ls)) - -mkKnWanted - :: CtLoc - -> CType - -> TcPluginM Ct -mkKnWanted loc (CType ty) = do - kc_clas <- tcLookupClass knownNatClassName - let kn_pred = mkClassPred kc_clas [ty] - wantedCtEv <- newWanted loc kn_pred - let wanted' = mkNonCanonical' loc wantedCtEv - return wanted' diff --git a/src-ghc-9.4/GHC/TypeLits/Normalise.hs b/src-ghc-9.4/GHC/TypeLits/Normalise.hs deleted file mode 100644 --- a/src-ghc-9.4/GHC/TypeLits/Normalise.hs +++ /dev/null @@ -1,740 +0,0 @@ -{-| -Copyright : (C) 2015-2016, University of Twente, - 2017 , QBayLogic B.V. -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij - -A type checker plugin for GHC that can solve /equalities/ of types of kind -'GHC.TypeLits.Nat', where these types are either: - -* Type-level naturals -* Type variables -* Applications of the arithmetic expressions @(+,-,*,^)@. - -It solves these equalities by normalising them to /sort-of/ -'GHC.TypeLits.Normalise.SOP.SOP' (Sum-of-Products) form, and then perform a -simple syntactic equality. - -For example, this solver can prove the equality between: - -@ -(x + 2)^(y + 2) -@ - -and - -@ -4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2 -@ - -Because the latter is actually the 'GHC.TypeLits.Normalise.SOP.SOP' normal form -of the former. - -To use the plugin, add - -@ -{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\} -@ - -To the header of your file. - -== Treating subtraction as addition with a negated number - -If you are absolutely sure that your subtractions can /never/ lead to (a locally) -negative number, you can ask the plugin to treat subtraction as addition with -a negated operand by additionally adding: - -@ -{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\} -@ - -to the header of your file, thereby allowing to use associativity and -commutativity rules when proving constraints involving subtractions. Note that -this option can lead to unsound behaviour and should be handled with extreme -care. - -=== When it leads to unsound behaviour - -For example, enabling the /allow-negated-numbers/ feature would allow -you to prove: - -@ -(n - 1) + 1 ~ n -@ - -/without/ a @(1 <= n)@ constraint, even though when /n/ is set to /0/ the -subtraction @n-1@ would be locally negative and hence not be a natural number. - -This would allow the following erroneous definition: - -@ -data Fin (n :: Nat) where - FZ :: Fin (n + 1) - FS :: Fin n -> Fin (n + 1) - -f :: forall n . Natural -> Fin n -f n = case of - 0 -> FZ - x -> FS (f \@(n-1) (x - 1)) - -fs :: [Fin 0] -fs = f \<$\> [0..] -@ - -=== When it might be Okay - -This example is taken from the -library. - -When you have: - -@ --- | Singleton type for the number of repetitions of an element. -data Times (n :: Nat) where - T :: Times n - --- | An element of a "run-length encoded" vector, containing the value and --- the number of repetitions -data Elem :: Type -> Nat -> Type where - (:*) :: t -> Times n -> Elem t n - --- | A length-indexed vector, optimised for repetitions. -data OptVector :: Type -> Nat -> Type where - End :: OptVector t 0 - (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n -@ - -And you want to define: - -@ --- | Append two optimised vectors. -type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where - ys ++ End = ys - End ++ ys = ys - (x :- xs) ++ ys = x :- (xs ++ ys) -@ - -then the last line will give rise to the constraint: - -@ -(n-l)+m ~ (n+m)-l -@ - -because: - -@ -x :: Elem t l -xs :: OptVector t (n-l) -ys :: OptVector t m -@ - -In this case it's okay to add - -@ -{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\} -@ - -if you can convince yourself you will never be able to construct a: - -@ -xs :: OptVector t (n-l) -@ - -where /n-l/ is a negative number. --} - -{-# LANGUAGE CPP #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE TemplateHaskellQuotes #-} - -{-# OPTIONS_HADDOCK show-extensions #-} - -module GHC.TypeLits.Normalise - ( plugin ) -where - --- external -import Control.Arrow (second) -import Control.Monad ((<=<), forM) -import Control.Monad.Trans.Writer.Strict -import Data.Either (partitionEithers, rights) -import Data.IORef -import Data.List (intersect, partition, stripPrefix, find) -import Data.Maybe (mapMaybe, catMaybes) -import Data.Set (Set, empty, toList, notMember, fromList, union) -import Text.Read (readMaybe) -import qualified Data.Type.Ord -import qualified GHC.TypeError - -import GHC.TcPluginM.Extra (tracePlugin, newGiven, newWanted) - --- GHC API -import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey) -import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon) -import GHC.Builtin.Types.Literals - (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon) -import GHC.Builtin.Types (naturalTy, cTupleDataCon, cTupleTyCon) -import GHC.Builtin.Types.Literals (typeNatCmpTyCon) -import GHC.Core (Expr (..)) -import GHC.Core.Class (className) -import GHC.Core.Coercion (Role (..), mkUnivCo) -import GHC.Core.DataCon (dataConWrapId) -import GHC.Core.Predicate - (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType, mkClassPred, - mkPrimEqPred, isEqPred, isEqPrimPred, getClassPredTys_maybe) -import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..)) -import GHC.Core.TyCon (TyCon) -#if MIN_VERSION_ghc(9,6,0) -import GHC.Core.Type - (Kind, PredType, mkTyVarTy, tyConAppTyCon_maybe, typeKind, mkTyConApp) -import GHC.Core.TyCo.Compare - (eqType) -#else -import GHC.Core.Type - (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe, typeKind, mkTyConApp) -#endif -import GHC.Data.IOEnv (getEnv) -import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin) -import GHC.Plugins (thNameToGhcNameIO, HscEnv (hsc_NC)) -import GHC.Tc.Plugin - (TcPluginM, tcLookupClass, tcPluginTrace, tcPluginIO, newEvVar) -import GHC.Tc.Plugin (tcLookupTyCon, unsafeTcPluginTcM) -import GHC.Tc.Types (TcPlugin (..), TcPluginSolveResult(..), Env (env_top)) -import GHC.Tc.Types.Constraint - (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence, - ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLocSpan, - isWantedCt, ctEvLoc, ctEvPred, ctEvExpr, emptyRewriterSet, setCtEvLoc) -import GHC.Tc.Types.Evidence (EvBindsVar, EvTerm (..), evCast, evId) -import GHC.Types.Unique.FM (emptyUFM) -import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text) -import GHC (Name) - --- template-haskell -import qualified Language.Haskell.TH as TH - --- internal -import GHC.TypeLits.Normalise.SOP -import GHC.TypeLits.Normalise.Unify hiding (subtractionToPred) - -isEqPredClass :: PredType -> Bool -isEqPredClass ty = case tyConAppTyCon_maybe ty of - Just tc -> tc `hasKey` eqTyConKey || tc `hasKey` heqTyConKey - _ -> False - --- | To use the plugin, add --- --- @ --- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\} --- @ --- --- To the header of your file. -plugin :: Plugin -plugin - = defaultPlugin - { tcPlugin = fmap (normalisePlugin . foldr id defaultOpts) . traverse parseArgument - , pluginRecompile = purePlugin - } - where - parseArgument "allow-negated-numbers" = Just (\ opts -> opts { negNumbers = True }) - parseArgument (readMaybe <=< stripPrefix "depth=" -> Just depth) = Just (\ opts -> opts { depth }) - parseArgument _ = Nothing - defaultOpts = Opts { negNumbers = False, depth = 5 } - -data Opts = Opts { negNumbers :: Bool, depth :: Word } - -normalisePlugin :: Opts -> TcPlugin -normalisePlugin opts = tracePlugin "ghc-typelits-natnormalise" - TcPlugin { tcPluginInit = lookupExtraDefs - , tcPluginSolve = decideEqualSOP opts - , tcPluginRewrite = const emptyUFM - , tcPluginStop = const (return ()) - } - -type ExtraDefs = (IORef (Set CType), (TyCon,TyCon,TyCon)) - -lookupExtraDefs :: TcPluginM ExtraDefs -lookupExtraDefs = do - ref <- tcPluginIO (newIORef empty) - ordCond <- lookupTHName ''Data.Type.Ord.OrdCond >>= tcLookupTyCon - leqT <- lookupTHName ''(Data.Type.Ord.<=) >>= tcLookupTyCon - assertT <- lookupTHName ''GHC.TypeError.Assert >>= tcLookupTyCon - return (ref, (leqT,assertT,ordCond)) - -lookupTHName :: TH.Name -> TcPluginM Name -lookupTHName th = do - nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv) - res <- tcPluginIO $ thNameToGhcNameIO nc th - maybe (fail $ "Failed to lookup " ++ show th) return res - -decideEqualSOP - :: Opts - -> ExtraDefs - -- ^ 1. Givens that is already generated. - -- We have to generate new givens at most once; - -- otherwise GHC will loop indefinitely. - -- - -- - -- 2. For GHc 9.2: TyCon of Data.Type.Ord.OrdCond - -- For older: TyCon of GHC.TypeLits.<=? - -> EvBindsVar - -> [Ct] - -> [Ct] - -> TcPluginM TcPluginSolveResult - --- Simplification phase: Derives /simplified/ givens; --- we can reduce given constraints like @Show (Foo (n + 2))@ --- to its normal form @Show (Foo (2 + n))@, which is eventually --- useful in solving phase. --- --- This helps us to solve /indirect/ constraints; --- without this phase, we cannot derive, e.g., --- @IsVector UVector (Fin (n + 1))@ from --- @Unbox (1 + n)@! -decideEqualSOP opts (gen'd,(leqT,_,_)) ev givens [] = do - done <- tcPluginIO $ readIORef gen'd - let reds = - filter (\(_,(_,_,v)) -> null v || negNumbers opts) $ - reduceGivens opts leqT done givens - newlyDone = map (\(_,(prd, _,_)) -> CType prd) reds - tcPluginIO $ - modifyIORef' gen'd $ union (fromList newlyDone) - newGivens <- forM reds $ \(origCt, (pred', evTerm, _)) -> - mkNonCanonical' (ctLoc origCt) <$> newGiven ev (ctLoc origCt) pred' evTerm - return (TcPluginOk [] newGivens) - --- Solving phase. --- Solves in/equalities on Nats and simplifiable constraints --- containing naturals. -decideEqualSOP opts (gen'd,tcs@(leqT,_,_)) ev givens wanteds = do - let unit_wanteds = mapMaybe (toNatEquality tcs) wanteds - nonEqs = filter ( not - . (\p -> isEqPred p || isEqPrimPred p) - . ctEvPred - . ctEvidence ) - wanteds - done <- tcPluginIO $ readIORef gen'd - let redGs = reduceGivens opts leqT done givens - newlyDone = map (\(_,(prd, _,_)) -> CType prd) redGs - redGivens <- forM redGs $ \(origCt, (pred', evTerm, _)) -> - mkNonCanonical' (ctLoc origCt) <$> newGiven ev (ctLoc origCt) pred' evTerm - reducible_wanteds - <- catMaybes <$> mapM (\ct -> fmap (ct,) <$> - reduceNatConstr (givens ++ redGivens) ct) - nonEqs - if null unit_wanteds && null reducible_wanteds - then return $ TcPluginOk [] [] - else do - -- Since reducible wanteds also can have some negation/subtraction - -- subterms, we have to make sure appropriate inequalities to hold. - -- Here, we generate such additional inequalities for reduction - -- that is to be added to new [W]anteds. - ineqForRedWants <- fmap concat $ forM redGs $ \(ct, (_,_, ws)) -> forM ws $ - fmap (mkNonCanonical' (ctLoc ct)) . newWanted (ctLoc ct) - tcPluginIO $ - modifyIORef' gen'd $ union (fromList newlyDone) - let unit_givens = mapMaybe - (toNatEquality tcs) - givens - sr <- simplifyNats opts leqT unit_givens unit_wanteds - tcPluginTrace "normalised" (ppr sr) - reds <- forM reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do - wants <- evSubtPreds (ctLoc origCt) $ subToPred opts leqT ws - return ((term, origCt), wDicts ++ wants) - case sr of - Simplified evs -> do - let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs - -- Only solve derived when we solved a wanted - simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of - [] -> [] - _ -> simpld - (solved',newWanteds) = second concat (unzip $ simpld1 ++ reds) - return (TcPluginOk solved' $ newWanteds ++ ineqForRedWants) - Impossible eq -> return (TcPluginContradiction [fromNatEquality eq]) - -type NatEquality = (Ct,CoreSOP,CoreSOP) -type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool)) - -reduceGivens :: Opts -> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))] -reduceGivens opts leqT done givens = - let nonEqs = - [ ct - | ct <- givens - , let ev = ctEvidence ct - prd = ctEvPred ev - , isGiven ev - , not $ (\p -> isEqPred p || isEqPrimPred p || isEqPredClass p) prd - ] - in filter - (\(_, (prd, _, _)) -> - notMember (CType prd) done - ) - $ mapMaybe - (\ct -> (ct,) <$> tryReduceGiven opts leqT givens ct) - nonEqs - -tryReduceGiven - :: Opts -> TyCon -> [Ct] -> Ct - -> Maybe (PredType, EvTerm, [PredType]) -tryReduceGiven opts leqT simplGivens ct = do - let (mans, ws) = - runWriter $ normaliseNatEverywhere $ - ctEvPred $ ctEvidence ct - ws' = [ p - | p <- subToPred opts leqT ws - , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens - ] - pred' <- mans - return (pred', toReducedDict (ctEvidence ct) pred', ws') - -fromNatEquality :: Either NatEquality NatInEquality -> Ct -fromNatEquality (Left (ct, _, _)) = ct -fromNatEquality (Right (ct, _)) = ct - -reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct])) -reduceNatConstr givens ct = do - let pred0 = ctEvPred $ ctEvidence ct - (mans, tests) = runWriter $ normaliseNatEverywhere pred0 - case mans of - Nothing -> return Nothing - Just pred' -> do - case find ((`eqType` pred') .ctEvPred . ctEvidence) givens of - -- No existing evidence found - Nothing -> case getClassPredTys_maybe pred' of - -- Are we trying to solve a class instance? - Just (cls,_) | className cls /= knownNatClassName -> do - -- Create new evidence binding for normalized class constraint - evVar <- newEvVar pred' - -- Bind the evidence to a new wanted normalized class constraint - let wDict = mkNonCanonical - (CtWanted pred' (EvVarDest evVar) (ctLoc ct) emptyRewriterSet) - -- Evidence for current wanted is simply the coerced binding for - -- the new binding - evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise") - Representational - pred' pred0 - ev = evId evVar `evCast` evCo - -- Use newly created coerced wanted as evidence, and emit the - -- normalized wanted as a new constraint to solve. - return (Just (ev, tests, [wDict])) - _ -> return Nothing - -- Use existing evidence - Just c -> return (Just (toReducedDict (ctEvidence c) pred0, tests, [])) - -toReducedDict :: CtEvidence -> PredType -> EvTerm -toReducedDict ct pred' = - let pred0 = ctEvPred ct - evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise") - Representational - pred0 pred' - ev = ctEvExpr ct - `evCast` evCo - in ev - -data SimplifyResult - = Simplified [((EvTerm,Ct),[Ct])] - | Impossible (Either NatEquality NatInEquality) - -instance Outputable SimplifyResult where - ppr (Simplified evs) = text "Simplified" $$ ppr evs - ppr (Impossible eq) = text "Impossible" <+> ppr eq - -simplifyNats - :: Opts - -- ^ Allow negated numbers (potentially unsound!) - -> TyCon - -- * TyCon of Data.Type.Ord.<= - -> [(Either NatEquality NatInEquality,[(Type,Type)])] - -- ^ Given constraints - -> [(Either NatEquality NatInEquality,[(Type,Type)])] - -- ^ Wanted constraints - -> TcPluginM SimplifyResult -simplifyNats opts@Opts {..} leqT eqsG eqsW = do - let eqsG1 = map (second (const ([] :: [(Type,Type)]))) eqsG - (varEqs,otherEqs) = partition isVarEqs eqsG1 - fancyGivens = concatMap (makeGivensSet otherEqs) varEqs - case varEqs of - [] -> do - let eqs = otherEqs ++ eqsW - tcPluginTrace "simplifyNats" (ppr eqs) - simples [] [] [] [] eqs - _ -> do - tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")") - (ppr varEqs) - - allSimplified <- forM fancyGivens $ \v -> do - let eqs = v ++ eqsW - tcPluginTrace "simplifyNats" (ppr eqs) - simples [] [] [] [] eqs - - pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified) - where - simples :: [CoreUnify] - -> [((EvTerm, Ct), [Ct])] - -> [(CoreSOP,CoreSOP,Bool)] - -> [(Either NatEquality NatInEquality,[(Type,Type)])] - -> [(Either NatEquality NatInEquality,[(Type,Type)])] - -> TcPluginM SimplifyResult - simples _subst evs _leqsG _xs [] = return (Simplified evs) - simples subst evs leqsG xs (eq@(Left (ct,u,v),k):eqs') = do - let u' = substsSOP subst u - v' = substsSOP subst v - ur <- unifyNats ct u' v' - tcPluginTrace "unifyNats result" (ppr ur) - case ur of - Win -> do - evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred opts leqT k) - simples subst evs' leqsG [] (xs ++ eqs') - Lose -> if null evs && null eqs' - then return (Impossible (fst eq)) - else simples subst evs leqsG xs eqs' - Draw [] -> simples subst evs [] (eq:xs) eqs' - Draw subst' -> do - evM <- evMagic ct empty (map unifyItemToPredType subst' ++ - subToPred opts leqT k) - let leqsG' | isGiven (ctEvidence ct) = eqToLeq u' v' ++ leqsG - | otherwise = leqsG - case evM of - Nothing -> simples subst evs leqsG' xs eqs' - Just ev -> - simples (substsSubst subst' subst ++ subst') - (ev:evs) leqsG' [] (xs ++ eqs') - simples subst evs leqsG xs (eq@(Right (ct,u@(x,y,b)),k):eqs') = do - let u' = substsSOP subst (subtractIneq u) - x' = substsSOP subst x - y' = substsSOP subst y - uS = (x',y',b) - leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG - | otherwise = leqsG - ineqs = concat [ leqsG - , map (substLeq subst) leqsG - , map snd (rights (map fst eqsG)) - ] - tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs)) - case runWriterT (isNatural u') of - Just (True,knW) -> do - evs' <- maybe evs (:evs) <$> evMagic ct knW (subToPred opts leqT k) - simples subst evs' leqsG' xs eqs' - - Just (False,_) | null k -> return (Impossible (fst eq)) - _ -> do - let solvedIneq = mapMaybe runWriterT - -- it is an inequality that can be instantly solved, such as - -- `1 <= x^y` - -- OR - (instantSolveIneq depth u: - instantSolveIneq depth uS: - -- This inequality is either a given constraint, or it is a wanted - -- constraint, which in normal form is equal to another given - -- constraint, hence it can be solved. - -- OR - map (solveIneq depth u) ineqs ++ - -- The above, but with valid substitutions applied to the wanted. - map (solveIneq depth uS) ineqs) - smallest = solvedInEqSmallestConstraint solvedIneq - case smallest of - (True,kW) -> do - evs' <- maybe evs (:evs) <$> evMagic ct kW (subToPred opts leqT k) - simples subst evs' leqsG' xs eqs' - _ -> simples subst evs leqsG (eq:xs) eqs' - - eqToLeq x y = [(x,y,True),(y,x,True)] - substLeq s (x,y,b) = (substsSOP s x, substsSOP s y, b) - - isVarEqs (Left (_,S [P [V _]], S [P [V _]]), _) = True - isVarEqs _ = False - - makeGivensSet otherEqs varEq - = let (noMentionsV,mentionsV) = partitionEithers - (map (matchesVarEq varEq) otherEqs) - (mentionsLHS,mentionsRHS) = partitionEithers mentionsV - vS = swapVar varEq - givensLHS = case mentionsLHS of - [] -> [] - _ -> [mentionsLHS ++ ((varEq:mentionsRHS) ++ noMentionsV)] - givensRHS = case mentionsRHS of - [] -> [] - _ -> [mentionsRHS ++ (vS:mentionsLHS ++ noMentionsV)] - in case mentionsV of - [] -> [noMentionsV] - _ -> givensLHS ++ givensRHS - - matchesVarEq (Left (_, S [P [V v1]], S [P [V v2]]),_) r = case r of - (Left (_,S [P [V v3]],_),_) - | v1 == v3 -> Right (Left r) - | v2 == v3 -> Right (Right r) - (Left (_,_,S [P [V v3]]),_) - | v1 == v3 -> Right (Left r) - | v2 == v3 -> Right (Right r) - (Right (_,(S [P [V v3]],_,_)),_) - | v1 == v3 -> Right (Left r) - | v2 == v3 -> Right (Right r) - (Right (_,(_,S [P [V v3]],_)),_) - | v1 == v3 -> Right (Left r) - | v2 == v3 -> Right (Right r) - _ -> Left r - matchesVarEq _ _ = error "internal error" - - swapVar (Left (ct,S [P [V v1]], S [P [V v2]]),ps) = - (Left (ct,S [P [V v2]], S [P [V v1]]),ps) - swapVar _ = error "internal error" - - findFirstSimpliedWanted (Impossible e) _ = Impossible e - findFirstSimpliedWanted (Simplified evs) s2 - | any (isWantedCt . snd . fst) evs - = Simplified evs - | otherwise - = s2 - --- If we allow negated numbers we simply do not emit the inequalities --- derived from the subtractions that are converted to additions with a --- negated operand -subToPred :: Opts -> TyCon -> [(Type, Type)] -> [PredType] -subToPred Opts{..} leqT - | negNumbers = const [] - | otherwise = map leq - where - leq (a,b) = - let lhs = TyConApp leqT [naturalTy,b,a] - rhs = TyConApp (cTupleTyCon 0) [] - in mkPrimEqPred lhs rhs - --- Extract the Nat equality constraints -toNatEquality :: (TyCon,TyCon,TyCon) -> Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)]) -toNatEquality (_,assertT,ordCond) ct = case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 t2 - -> go t1 t2 - IrredPred p - -> go2 p - _ -> Nothing - where - go (TyConApp tc xs) (TyConApp tc' ys) - | tc == tc' - , null ([tc,tc'] `intersect` [typeNatAddTyCon,typeNatSubTyCon - ,typeNatMulTyCon,typeNatExpTyCon]) - = case filter (not . uncurry eqType) (zip xs ys) of - [(x,y)] - | isNatKind (typeKind x) - , isNatKind (typeKind y) - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - -> Just (Left (ct, x', y'),k1 ++ k2) - _ -> Nothing - | tc == ordCond - , [_,cmp,lt,eq,gt] <- xs - , TyConApp tcCmpNat [x,y] <- cmp - , tcCmpNat == typeNatCmpTyCon - , TyConApp ltTc [] <- lt - , ltTc == promotedTrueDataCon - , TyConApp eqTc [] <- eq - , eqTc == promotedTrueDataCon - , TyConApp gtTc [] <- gt - , gtTc == promotedFalseDataCon - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - , let ks = k1 ++ k2 - = case tc' of - _ | tc' == promotedTrueDataCon - -> Just (Right (ct, (x', y', True)), ks) - _ | tc' == promotedFalseDataCon - -> Just (Right (ct, (x', y', False)), ks) - _ -> Nothing - | tc == assertT - , tc' == (cTupleTyCon 0) - , [] <- ys - , [TyConApp ordCondTc zs, _] <- xs - , ordCondTc == ordCond - , [_,cmp,lt,eq,gt] <- zs - , TyConApp tcCmpNat [x,y] <- cmp - , tcCmpNat == typeNatCmpTyCon - , TyConApp ltTc [] <- lt - , ltTc == promotedTrueDataCon - , TyConApp eqTc [] <- eq - , eqTc == promotedTrueDataCon - , TyConApp gtTc [] <- gt - , gtTc == promotedFalseDataCon - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - , let ks = k1 ++ k2 - = Just (Right (ct, (x', y', True)), ks) - - go x y - | isNatKind (typeKind x) - , isNatKind (typeKind y) - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - = Just (Left (ct,x',y'),k1 ++ k2) - | otherwise - = Nothing - - go2 (TyConApp tc ys) - | tc == assertT - , [TyConApp ordCondTc xs, _] <- ys - , ordCondTc == ordCond - , [_,cmp,lt,eq,gt] <- xs - , TyConApp tcCmpNat [x,y] <- cmp - , tcCmpNat == typeNatCmpTyCon - , TyConApp ltTc [] <- lt - , ltTc == promotedTrueDataCon - , TyConApp eqTc [] <- eq - , eqTc == promotedTrueDataCon - , TyConApp gtTc [] <- gt - , gtTc == promotedFalseDataCon - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - , let ks = k1 ++ k2 - = Just (Right (ct, (x', y', True)), ks) - - go2 _ = Nothing - - isNatKind :: Kind -> Bool - isNatKind = (`eqType` naturalTy) - -unifyItemToPredType :: CoreUnify -> PredType -unifyItemToPredType ui = mkPrimEqPred ty1 ty2 - where - ty1 = case ui of - SubstItem {..} -> mkTyVarTy siVar - UnifyItem {..} -> reifySOP siLHS - ty2 = case ui of - SubstItem {..} -> reifySOP siSOP - UnifyItem {..} -> reifySOP siRHS - -evSubtPreds :: CtLoc -> [PredType] -> TcPluginM [Ct] -evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc) - -evMagic :: Ct -> Set CType -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct])) -evMagic ct knW preds = do - holeWanteds <- evSubtPreds (ctLoc ct) preds - knWanted <- mapM (mkKnWanted (ctLoc ct)) (toList knW) - let newWant = knWanted ++ holeWanteds - case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 t2 -> - let ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2 - in return (Just ((EvExpr (Coercion ctEv), ct),newWant)) - IrredPred p -> - let t1 = mkTyConApp (cTupleTyCon 0) [] - co = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Representational t1 p - dcApp = evId (dataConWrapId (cTupleDataCon 0)) - in return (Just ((evCast dcApp co, ct),newWant)) - _ -> return Nothing - -mkNonCanonical' :: CtLoc -> CtEvidence -> Ct -mkNonCanonical' origCtl ev = - let ct_ls = ctLocSpan origCtl - ctl = ctEvLoc ev - in mkNonCanonical (setCtEvLoc ev (setCtLocSpan ctl ct_ls)) - -mkKnWanted - :: CtLoc - -> CType - -> TcPluginM Ct -mkKnWanted loc (CType ty) = do - kc_clas <- tcLookupClass knownNatClassName - let kn_pred = mkClassPred kc_clas [ty] - wantedCtEv <- newWanted loc kn_pred - let wanted' = mkNonCanonical' loc wantedCtEv - return wanted' diff --git a/src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs b/src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs deleted file mode 100644 --- a/src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs +++ /dev/null @@ -1,862 +0,0 @@ -{-| -Copyright : (C) 2015-2016, University of Twente, - 2017 , QBayLogic B.V. -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij - -A type checker plugin for GHC that can solve /equalities/ of types of kind -'GHC.TypeLits.Nat', where these types are either: - -* Type-level naturals -* Type variables -* Applications of the arithmetic expressions @(+,-,*,^)@. - -It solves these equalities by normalising them to /sort-of/ -'GHC.TypeLits.Normalise.SOP.SOP' (Sum-of-Products) form, and then perform a -simple syntactic equality. - -For example, this solver can prove the equality between: - -@ -(x + 2)^(y + 2) -@ - -and - -@ -4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2 -@ - -Because the latter is actually the 'GHC.TypeLits.Normalise.SOP.SOP' normal form -of the former. - -To use the plugin, add - -@ -{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\} -@ - -To the header of your file. - -== Treating subtraction as addition with a negated number - -If you are absolutely sure that your subtractions can /never/ lead to (a locally) -negative number, you can ask the plugin to treat subtraction as addition with -a negated operand by additionally adding: - -@ -{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\} -@ - -to the header of your file, thereby allowing to use associativity and -commutativity rules when proving constraints involving subtractions. Note that -this option can lead to unsound behaviour and should be handled with extreme -care. - -=== When it leads to unsound behaviour - -For example, enabling the /allow-negated-numbers/ feature would allow -you to prove: - -@ -(n - 1) + 1 ~ n -@ - -/without/ a @(1 <= n)@ constraint, even though when /n/ is set to /0/ the -subtraction @n-1@ would be locally negative and hence not be a natural number. - -This would allow the following erroneous definition: - -@ -data Fin (n :: Nat) where - FZ :: Fin (n + 1) - FS :: Fin n -> Fin (n + 1) - -f :: forall n . Natural -> Fin n -f n = case of - 0 -> FZ - x -> FS (f \@(n-1) (x - 1)) - -fs :: [Fin 0] -fs = f \<$\> [0..] -@ - -=== When it might be Okay - -This example is taken from the -library. - -When you have: - -@ --- | Singleton type for the number of repetitions of an element. -data Times (n :: Nat) where - T :: Times n - --- | An element of a "run-length encoded" vector, containing the value and --- the number of repetitions -data Elem :: Type -> Nat -> Type where - (:*) :: t -> Times n -> Elem t n - --- | A length-indexed vector, optimised for repetitions. -data OptVector :: Type -> Nat -> Type where - End :: OptVector t 0 - (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n -@ - -And you want to define: - -@ --- | Append two optimised vectors. -type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where - ys ++ End = ys - End ++ ys = ys - (x :- xs) ++ ys = x :- (xs ++ ys) -@ - -then the last line will give rise to the constraint: - -@ -(n-l)+m ~ (n+m)-l -@ - -because: - -@ -x :: Elem t l -xs :: OptVector t (n-l) -ys :: OptVector t m -@ - -In this case it's okay to add - -@ -{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\} -@ - -if you can convince yourself you will never be able to construct a: - -@ -xs :: OptVector t (n-l) -@ - -where /n-l/ is a negative number. --} - -{-# LANGUAGE CPP #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE ViewPatterns #-} - -{-# OPTIONS_HADDOCK show-extensions #-} - -module GHC.TypeLits.Normalise - ( plugin ) -where - --- external -import Control.Arrow (second) -import Control.Monad ((<=<), forM) -#if !MIN_VERSION_ghc(8,4,1) -import Control.Monad (replicateM) -#endif -import Control.Monad.Trans.Writer.Strict -import Data.Either (partitionEithers, rights) -import Data.IORef -import Data.List (intersect, partition, stripPrefix, find) -import Data.Maybe (mapMaybe, catMaybes) -import Data.Set (Set, empty, toList, notMember, fromList, union) -import GHC.TcPluginM.Extra (tracePlugin, newGiven, newWanted) -#if MIN_VERSION_ghc(9,2,0) -import GHC.TcPluginM.Extra (lookupModule, lookupName) -#endif -import qualified GHC.TcPluginM.Extra as TcPluginM -#if MIN_VERSION_ghc(8,4,0) -import GHC.TcPluginM.Extra (flattenGivens) -#endif -import Text.Read (readMaybe) - --- GHC API -#if MIN_VERSION_ghc(9,0,0) -import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey) -import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon) -import GHC.Builtin.Types.Literals - (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon) -#if MIN_VERSION_ghc(9,2,0) -import GHC.Builtin.Types (naturalTy) -import GHC.Builtin.Types.Literals (typeNatCmpTyCon) -#else -import GHC.Builtin.Types (typeNatKind) -import GHC.Builtin.Types.Literals (typeNatLeqTyCon) -#endif -import GHC.Core (Expr (..)) -import GHC.Core.Class (className) -import GHC.Core.Coercion (CoercionHole, Role (..), mkUnivCo) -import GHC.Core.Predicate - (EqRel (NomEq), Pred (EqPred), classifyPredType, getEqPredTys, mkClassPred, - mkPrimEqPred, isEqPred, isEqPrimPred, getClassPredTys_maybe) -import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..)) -import GHC.Core.TyCon (TyCon) -import GHC.Core.Type - (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe, typeKind) -import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin) -import GHC.Tc.Plugin - (TcPluginM, newCoercionHole, tcLookupClass, tcPluginTrace, tcPluginIO, - newEvVar) -#if MIN_VERSION_ghc(9,2,0) -import GHC.Tc.Plugin (tcLookupTyCon) -#endif -import GHC.Tc.Types (TcPlugin (..), TcPluginResult (..)) -import GHC.Tc.Types.Constraint - (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ShadowInfo (WDeriv), ctEvidence, - ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan, - isWantedCt, ctEvLoc, ctEvPred, ctEvExpr) -import GHC.Tc.Types.Evidence (EvTerm (..), evCast, evId) -#if MIN_VERSION_ghc(9,2,0) -import GHC.Data.FastString (fsLit) -import GHC.Types.Name.Occurrence (mkTcOcc) -import GHC.Unit.Module (mkModuleName) -#endif -import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text) -#else -#if MIN_VERSION_ghc(8,5,0) -import CoreSyn (Expr (..)) -#endif -import Outputable (Outputable (..), (<+>), ($$), text) -import Plugins (Plugin (..), defaultPlugin) -#if MIN_VERSION_ghc(8,6,0) -import Plugins (purePlugin) -#endif -import PrelNames (hasKey, knownNatClassName) -import PrelNames (eqTyConKey, heqTyConKey) -import TcEvidence (EvTerm (..)) -#if MIN_VERSION_ghc(8,6,0) -import TcEvidence (evCast, evId) -#endif -#if !MIN_VERSION_ghc(8,4,0) -import TcPluginM (zonkCt) -#endif -import TcPluginM (TcPluginM, tcPluginTrace, tcPluginIO) -import Type - (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe) -import TysWiredIn (typeNatKind) - -import Coercion (CoercionHole, Role (..), mkUnivCo) -import Class (className) -import TcPluginM (newCoercionHole, tcLookupClass, newEvVar) -import TcRnTypes (TcPlugin (..), TcPluginResult(..)) -import TyCoRep (UnivCoProvenance (..)) -import TcType (isEqPred) -import TyCon (TyCon) -import TyCoRep (Type (..)) -import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, - typeNatSubTyCon) - -import TcTypeNats (typeNatLeqTyCon) -import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon) - -#if MIN_VERSION_ghc(8,10,0) -import Constraint - (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence, ctEvLoc, ctEvPred, - ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan, - isWantedCt) -import Predicate - (EqRel (NomEq), Pred (EqPred), classifyPredType, getEqPredTys, mkClassPred, - mkPrimEqPred, getClassPredTys_maybe) -import Type (typeKind) -#else -import TcRnTypes - (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence, ctEvLoc, ctEvPred, - ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan, - isWantedCt) -import TcType (typeKind) -import Type - (EqRel (NomEq), PredTree (EqPred), classifyPredType, mkClassPred, mkPrimEqPred, - getClassPredTys_maybe) -#if MIN_VERSION_ghc(8,4,0) -import Type (getEqPredTys) -#endif -#endif - -#if MIN_VERSION_ghc(8,10,0) -import Constraint (ctEvExpr) -#elif MIN_VERSION_ghc(8,6,0) -import TcRnTypes (ctEvExpr) -#else -import TcRnTypes (ctEvTerm) -#endif - -#if MIN_VERSION_ghc(8,2,0) -#if MIN_VERSION_ghc(8,10,0) -import Constraint (ShadowInfo (WDeriv)) -#else -import TcRnTypes (ShadowInfo (WDeriv)) -#endif -#endif - -#if MIN_VERSION_ghc(8,10,0) -import TcType (isEqPrimPred) -#endif -#endif - --- internal -import GHC.TypeLits.Normalise.SOP -import GHC.TypeLits.Normalise.Unify - -#if MIN_VERSION_ghc(9,2,0) -typeNatKind :: Type -typeNatKind = naturalTy -#endif - -#if !MIN_VERSION_ghc(8,10,0) -isEqPrimPred :: PredType -> Bool -isEqPrimPred = isEqPred -#endif - -isEqPredClass :: PredType -> Bool -isEqPredClass ty = case tyConAppTyCon_maybe ty of - Just tc -> tc `hasKey` eqTyConKey || tc `hasKey` heqTyConKey - _ -> False - --- | To use the plugin, add --- --- @ --- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\} --- @ --- --- To the header of your file. -plugin :: Plugin -plugin - = defaultPlugin - { tcPlugin = fmap (normalisePlugin . foldr id defaultOpts) . traverse parseArgument -#if MIN_VERSION_ghc(8,6,0) - , pluginRecompile = purePlugin -#endif - } - where - parseArgument "allow-negated-numbers" = Just (\ opts -> opts { negNumbers = True }) - parseArgument (readMaybe <=< stripPrefix "depth=" -> Just depth) = Just (\ opts -> opts { depth }) - parseArgument _ = Nothing - defaultOpts = Opts { negNumbers = False, depth = 5 } - -data Opts = Opts { negNumbers :: Bool, depth :: Word } - -normalisePlugin :: Opts -> TcPlugin -normalisePlugin opts = tracePlugin "ghc-typelits-natnormalise" - TcPlugin { tcPluginInit = lookupExtraDefs - , tcPluginSolve = decideEqualSOP opts - , tcPluginStop = const (return ()) - } -newtype OrigCt = OrigCt { runOrigCt :: Ct } - -type ExtraDefs = (IORef (Set CType), TyCon) - -lookupExtraDefs :: TcPluginM ExtraDefs -lookupExtraDefs = do - ref <- tcPluginIO (newIORef empty) -#if !MIN_VERSION_ghc(9,2,0) - return (ref, typeNatLeqTyCon) -#else - md <- lookupModule myModule myPackage - ordCond <- look md "OrdCond" - return (ref, ordCond) - where - look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s) - myModule = mkModuleName "Data.Type.Ord" - myPackage = fsLit "base" -#endif - -decideEqualSOP - :: Opts - -> ExtraDefs - -- ^ 1. Givens that is already generated. - -- We have to generate new givens at most once; - -- otherwise GHC will loop indefinitely. - -- - -- - -- 2. For GHc 9.2: TyCon of Data.Type.Ord.OrdCond - -- For older: TyCon of GHC.TypeLits.<=? - -> [Ct] - -> [Ct] - -> [Ct] - -> TcPluginM TcPluginResult - --- Simplification phase: Derives /simplified/ givens; --- we can reduce given constraints like @Show (Foo (n + 2))@ --- to its normal form @Show (Foo (2 + n))@, which is eventually --- useful in solving phase. --- --- This helps us to solve /indirect/ constraints; --- without this phase, we cannot derive, e.g., --- @IsVector UVector (Fin (n + 1))@ from --- @Unbox (1 + n)@! -decideEqualSOP opts (gen'd,ordCond) givens _deriveds [] = do - done <- tcPluginIO $ readIORef gen'd -#if MIN_VERSION_ghc(8,4,0) - let simplGivens = flattenGivens givens -#else - simplGivens <- mapM zonkCt givens -#endif - let reds = - filter (\(_,(_,_,v)) -> null v || negNumbers opts) $ - reduceGivens opts ordCond done simplGivens - newlyDone = map (\(_,(prd, _,_)) -> CType prd) reds - tcPluginIO $ - modifyIORef' gen'd $ union (fromList newlyDone) - newGivens <- forM reds $ \(origCt, (pred', evTerm, _)) -> - mkNonCanonical' (ctLoc origCt) <$> newGiven (ctLoc origCt) pred' evTerm - return (TcPluginOk [] newGivens) - --- Solving phase. --- Solves in/equalities on Nats and simplifiable constraints --- containing naturals. -decideEqualSOP opts (gen'd,ordCond) givens deriveds wanteds = do - -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out - let flat_wanteds0 = map (\ct -> (OrigCt ct, ct)) wanteds -#if MIN_VERSION_ghc(8,4,0) - -- flattenGivens should actually be called unflattenGivens - let simplGivens = givens ++ flattenGivens givens - subst = fst $ unzip $ TcPluginM.mkSubst' givens - unflattenWanted (oCt, ct) = (oCt, TcPluginM.substCt subst ct) - unflat_wanteds0 = map unflattenWanted flat_wanteds0 -#else - let unflat_wanteds0 = flat_wanteds0 - simplGivens <- mapM zonkCt givens -#endif - let unflat_wanteds1 = filter (isWanted . ctEvidence . snd) unflat_wanteds0 - -- only return solve deriveds when there are wanteds to solve - unflat_wanteds2 = case unflat_wanteds1 of - [] -> [] - w -> w ++ (map (\a -> (OrigCt a,a)) deriveds) - unit_wanteds = mapMaybe (toNatEquality ordCond) unflat_wanteds2 - nonEqs = filter (not . (\p -> isEqPred p || isEqPrimPred p) . ctEvPred . ctEvidence.snd) - $ filter (isWanted. ctEvidence.snd) unflat_wanteds0 - done <- tcPluginIO $ readIORef gen'd - let redGs = reduceGivens opts ordCond done simplGivens - newlyDone = map (\(_,(prd, _,_)) -> CType prd) redGs - redGivens <- forM redGs $ \(origCt, (pred', evTerm, _)) -> - mkNonCanonical' (ctLoc origCt) <$> newGiven (ctLoc origCt) pred' evTerm - reducible_wanteds - <- catMaybes <$> - mapM - (\(origCt, ct) -> fmap (runOrigCt origCt,) <$> - reduceNatConstr (simplGivens ++ redGivens) ct - ) - nonEqs - if null unit_wanteds && null reducible_wanteds - then return $ TcPluginOk [] [] - else do - -- Since reducible wanteds also can have some negation/subtraction - -- subterms, we have to make sure appropriate inequalities to hold. - -- Here, we generate such additional inequalities for reduction - -- that is to be added to new [W]anteds. - ineqForRedWants <- fmap concat $ forM redGs $ \(ct, (_,_, ws)) -> forM ws $ - fmap (mkNonCanonical' (ctLoc ct)) . newWanted (ctLoc ct) - tcPluginIO $ - modifyIORef' gen'd $ union (fromList newlyDone) - let unit_givens = mapMaybe - (toNatEquality ordCond) - (map (\a -> (OrigCt a, a)) simplGivens) - sr <- simplifyNats opts ordCond unit_givens unit_wanteds - tcPluginTrace "normalised" (ppr sr) - reds <- forM reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do - wants <- evSubtPreds origCt $ subToPred opts ordCond ws - return ((term, origCt), wDicts ++ wants) - case sr of - Simplified evs -> do - let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs - -- Only solve derived when we solved a wanted - simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of - [] -> [] - _ -> simpld - (solved',newWanteds) = second concat (unzip $ simpld1 ++ reds) - return (TcPluginOk solved' $ newWanteds ++ ineqForRedWants) - Impossible eq -> return (TcPluginContradiction [fromNatEquality eq]) - -type NatEquality = (Ct,CoreSOP,CoreSOP) -type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool)) - -reduceGivens :: Opts -> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))] -reduceGivens opts ordCond done givens = - let nonEqs = - [ ct - | ct <- givens - , let ev = ctEvidence ct - prd = ctEvPred ev - , isGiven ev - , not $ (\p -> isEqPred p || isEqPrimPred p || isEqPredClass p) prd - ] - in filter - (\(_, (prd, _, _)) -> - notMember (CType prd) done - ) - $ mapMaybe - (\ct -> (ct,) <$> tryReduceGiven opts ordCond givens ct) - nonEqs - -tryReduceGiven - :: Opts -> TyCon -> [Ct] -> Ct - -> Maybe (PredType, EvTerm, [PredType]) -tryReduceGiven opts ordCond simplGivens ct = do - let (mans, ws) = - runWriter $ normaliseNatEverywhere $ - ctEvPred $ ctEvidence ct - ws' = [ p - | (p, _) <- subToPred opts ordCond ws - , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens - ] - pred' <- mans - return (pred', toReducedDict (ctEvidence ct) pred', ws') - -fromNatEquality :: Either NatEquality NatInEquality -> Ct -fromNatEquality (Left (ct, _, _)) = ct -fromNatEquality (Right (ct, _)) = ct - -reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct])) -reduceNatConstr givens ct = do - let pred0 = ctEvPred $ ctEvidence ct - (mans, tests) = runWriter $ normaliseNatEverywhere pred0 - case mans of - Nothing -> return Nothing - Just pred' -> do - case find ((`eqType` pred') .ctEvPred . ctEvidence) givens of - -- No existing evidence found - Nothing -> case getClassPredTys_maybe pred' of - -- Are we trying to solve a class instance? - Just (cls,_) | className cls /= knownNatClassName -> do - -- Create new evidence binding for normalized class constraint - evVar <- newEvVar pred' - -- Bind the evidence to a new wanted normalized class constraint - let wDict = mkNonCanonical - (CtWanted pred' (EvVarDest evVar) -#if MIN_VERSION_ghc(8,2,0) - WDeriv -#endif - (ctLoc ct)) - -- Evidence for current wanted is simply the coerced binding for - -- the new binding - evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise") - Representational - pred' pred0 -#if MIN_VERSION_ghc(8,6,0) - ev = evId evVar `evCast` evCo -#else - ev = EvId evVar `EvCast` evCo -#endif - -- Use newly created coerced wanted as evidence, and emit the - -- normalized wanted as a new constraint to solve. - return (Just (ev, tests, [wDict])) - _ -> return Nothing - -- Use existing evidence - Just c -> return (Just (toReducedDict (ctEvidence c) pred0, tests, [])) - -toReducedDict :: CtEvidence -> PredType -> EvTerm -toReducedDict ct pred' = - let pred0 = ctEvPred ct - evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise") - Representational - pred0 pred' -#if MIN_VERSION_ghc(8,6,0) - ev = ctEvExpr ct - `evCast` evCo -#else - ev = ctEvTerm ct `EvCast` evCo -#endif - in ev - -data SimplifyResult - = Simplified [((EvTerm,Ct),[Ct])] - | Impossible (Either NatEquality NatInEquality) - -instance Outputable SimplifyResult where - ppr (Simplified evs) = text "Simplified" $$ ppr evs - ppr (Impossible eq) = text "Impossible" <+> ppr eq - -simplifyNats - :: Opts - -- ^ Allow negated numbers (potentially unsound!) - -> TyCon - -- ^ For GHc 9.2: TyCon of Data.Type.Ord.OrdCond - -- For older: TyCon of GHC.TypeLits.<=? - -> [(Either NatEquality NatInEquality,[(Type,Type)])] - -- ^ Given constraints - -> [(Either NatEquality NatInEquality,[(Type,Type)])] - -- ^ Wanted constraints - -> TcPluginM SimplifyResult -simplifyNats opts@Opts {..} ordCond eqsG eqsW = do - let eqsG1 = map (second (const ([] :: [(Type,Type)]))) eqsG - (varEqs,otherEqs) = partition isVarEqs eqsG1 - fancyGivens = concatMap (makeGivensSet otherEqs) varEqs - case varEqs of - [] -> do - let eqs = otherEqs ++ eqsW - tcPluginTrace "simplifyNats" (ppr eqs) - simples [] [] [] [] eqs - _ -> do - tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")") - (ppr varEqs) - - allSimplified <- forM fancyGivens $ \v -> do - let eqs = v ++ eqsW - tcPluginTrace "simplifyNats" (ppr eqs) - simples [] [] [] [] eqs - - pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified) - where - simples :: [CoreUnify] - -> [((EvTerm, Ct), [Ct])] - -> [(CoreSOP,CoreSOP,Bool)] - -> [(Either NatEquality NatInEquality,[(Type,Type)])] - -> [(Either NatEquality NatInEquality,[(Type,Type)])] - -> TcPluginM SimplifyResult - simples _subst evs _leqsG _xs [] = return (Simplified evs) - simples subst evs leqsG xs (eq@(Left (ct,u,v),k):eqs') = do - let u' = substsSOP subst u - v' = substsSOP subst v - ur <- unifyNats ct u' v' - tcPluginTrace "unifyNats result" (ppr ur) - case ur of - Win -> do - evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred opts ordCond k) - simples subst evs' leqsG [] (xs ++ eqs') - Lose -> if null evs && null eqs' - then return (Impossible (fst eq)) - else simples subst evs leqsG xs eqs' - Draw [] -> simples subst evs [] (eq:xs) eqs' - Draw subst' -> do - evM <- evMagic ct empty (map unifyItemToPredType subst' ++ - subToPred opts ordCond k) - let leqsG' | isGiven (ctEvidence ct) = eqToLeq u' v' ++ leqsG - | otherwise = leqsG - case evM of - Nothing -> simples subst evs leqsG' xs eqs' - Just ev -> - simples (substsSubst subst' subst ++ subst') - (ev:evs) leqsG' [] (xs ++ eqs') - simples subst evs leqsG xs (eq@(Right (ct,u@(x,y,b)),k):eqs') = do - let u' = substsSOP subst (subtractIneq u) - x' = substsSOP subst x - y' = substsSOP subst y - uS = (x',y',b) - leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG - | otherwise = leqsG - ineqs = concat [ leqsG - , map (substLeq subst) leqsG - , map snd (rights (map fst eqsG)) - ] - tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs)) - case runWriterT (isNatural u') of - Just (True,knW) -> do - evs' <- maybe evs (:evs) <$> evMagic ct knW (subToPred opts ordCond k) - simples subst evs' leqsG' xs eqs' - - Just (False,_) | null k -> return (Impossible (fst eq)) - _ -> do - let solvedIneq = mapMaybe runWriterT - -- it is an inequality that can be instantly solved, such as - -- `1 <= x^y` - -- OR - (instantSolveIneq depth u: - instantSolveIneq depth uS: - -- This inequality is either a given constraint, or it is a wanted - -- constraint, which in normal form is equal to another given - -- constraint, hence it can be solved. - -- OR - map (solveIneq depth u) ineqs ++ - -- The above, but with valid substitutions applied to the wanted. - map (solveIneq depth uS) ineqs) - smallest = solvedInEqSmallestConstraint solvedIneq - case smallest of - (True,kW) -> do - evs' <- maybe evs (:evs) <$> evMagic ct kW (subToPred opts ordCond k) - simples subst evs' leqsG' xs eqs' - _ -> simples subst evs leqsG (eq:xs) eqs' - - eqToLeq x y = [(x,y,True),(y,x,True)] - substLeq s (x,y,b) = (substsSOP s x, substsSOP s y, b) - - isVarEqs (Left (_,S [P [V _]], S [P [V _]]), _) = True - isVarEqs _ = False - - makeGivensSet otherEqs varEq - = let (noMentionsV,mentionsV) = partitionEithers - (map (matchesVarEq varEq) otherEqs) - (mentionsLHS,mentionsRHS) = partitionEithers mentionsV - vS = swapVar varEq - givensLHS = case mentionsLHS of - [] -> [] - _ -> [mentionsLHS ++ ((varEq:mentionsRHS) ++ noMentionsV)] - givensRHS = case mentionsRHS of - [] -> [] - _ -> [mentionsRHS ++ (vS:mentionsLHS ++ noMentionsV)] - in case mentionsV of - [] -> [noMentionsV] - _ -> givensLHS ++ givensRHS - - matchesVarEq (Left (_, S [P [V v1]], S [P [V v2]]),_) r = case r of - (Left (_,S [P [V v3]],_),_) - | v1 == v3 -> Right (Left r) - | v2 == v3 -> Right (Right r) - (Left (_,_,S [P [V v3]]),_) - | v1 == v3 -> Right (Left r) - | v2 == v3 -> Right (Right r) - (Right (_,(S [P [V v3]],_,_)),_) - | v1 == v3 -> Right (Left r) - | v2 == v3 -> Right (Right r) - (Right (_,(_,S [P [V v3]],_)),_) - | v1 == v3 -> Right (Left r) - | v2 == v3 -> Right (Right r) - _ -> Left r - matchesVarEq _ _ = error "internal error" - - swapVar (Left (ct,S [P [V v1]], S [P [V v2]]),ps) = - (Left (ct,S [P [V v2]], S [P [V v1]]),ps) - swapVar _ = error "internal error" - - findFirstSimpliedWanted (Impossible e) _ = Impossible e - findFirstSimpliedWanted (Simplified evs) s2 - | any (isWantedCt . snd . fst) evs - = Simplified evs - | otherwise - = s2 - --- If we allow negated numbers we simply do not emit the inequalities --- derived from the subtractions that are converted to additions with a --- negated operand -subToPred :: Opts -> TyCon -> [(Type, Type)] -> [(PredType, Kind)] -subToPred Opts{..} ordCond - | negNumbers = const [] - | otherwise = map (subtractionToPred ordCond) - --- Extract the Nat equality constraints -toNatEquality :: TyCon -> (OrigCt, Ct) -> Maybe (Either NatEquality NatInEquality,[(Type,Type)]) -toNatEquality ordCond (OrigCt oCt, ct) = case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 t2 - -> go t1 t2 - _ -> Nothing - where - go (TyConApp tc xs) (TyConApp tc' ys) - | tc == tc' - , null ([tc,tc'] `intersect` [typeNatAddTyCon,typeNatSubTyCon - ,typeNatMulTyCon,typeNatExpTyCon]) - = case filter (not . uncurry eqType) (zip xs ys) of - [(x,y)] - | isNatKind (typeKind x) - , isNatKind (typeKind y) - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - -> Just (Left (oCt, x', y'),k1 ++ k2) - _ -> Nothing -#if MIN_VERSION_ghc(9,2,0) - | tc == ordCond - , [_,cmp,lt,eq,gt] <- xs - , TyConApp tcCmpNat [x,y] <- cmp - , tcCmpNat == typeNatCmpTyCon - , TyConApp ltTc [] <- lt - , ltTc == promotedTrueDataCon - , TyConApp eqTc [] <- eq - , eqTc == promotedTrueDataCon - , TyConApp gtTc [] <- gt - , gtTc == promotedFalseDataCon - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - , let ks = k1 ++ k2 - = case tc' of - _ | tc' == promotedTrueDataCon - -> Just (Right (oCt, (x', y', True)), ks) - _ | tc' == promotedFalseDataCon - -> Just (Right (oCt, (x', y', False)), ks) - _ -> Nothing -#else - | tc == ordCond - , [x,y] <- xs - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - , let ks = k1 ++ k2 - = case tc' of - _ | tc' == promotedTrueDataCon - -> Just (Right (oCt, (x', y', True)), ks) - _ | tc' == promotedFalseDataCon - -> Just (Right (oCt, (x', y', False)), ks) - _ -> Nothing -#endif - - go x y - | isNatKind (typeKind x) - , isNatKind (typeKind y) - , let (x',k1) = runWriter (normaliseNat x) - , let (y',k2) = runWriter (normaliseNat y) - = Just (Left (oCt,x',y'),k1 ++ k2) - | otherwise - = Nothing - - isNatKind :: Kind -> Bool - isNatKind = (`eqType` typeNatKind) - -unifyItemToPredType :: CoreUnify -> (PredType,Kind) -unifyItemToPredType ui = - (mkPrimEqPred ty1 ty2,typeNatKind) - where - ty1 = case ui of - SubstItem {..} -> mkTyVarTy siVar - UnifyItem {..} -> reifySOP siLHS - ty2 = case ui of - SubstItem {..} -> reifySOP siSOP - UnifyItem {..} -> reifySOP siRHS - -evSubtPreds :: Ct -> [(PredType,Kind)] -> TcPluginM [Ct] -evSubtPreds ct preds = do - let predTypes = map fst preds -#if MIN_VERSION_ghc(8,4,1) - holes <- mapM (newCoercionHole . uncurry mkPrimEqPred . getEqPredTys) predTypes -#else - holes <- replicateM (length preds) newCoercionHole -#endif - return (zipWith (unifyItemToCt (ctLoc ct)) predTypes holes) - -evMagic :: Ct -> Set CType -> [(PredType,Kind)] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct])) -evMagic ct knW preds = case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 t2 -> do - holeWanteds <- evSubtPreds ct preds - knWanted <- mapM (mkKnWanted ct) (toList knW) - let newWant = knWanted ++ holeWanteds - ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2 -#if MIN_VERSION_ghc(8,5,0) - return (Just ((EvExpr (Coercion ctEv), ct),newWant)) -#else - return (Just ((EvCoercion ctEv, ct),newWant)) -#endif - _ -> return Nothing - -mkNonCanonical' :: CtLoc -> CtEvidence -> Ct -mkNonCanonical' origCtl ev = - let ct_ls = ctLocSpan origCtl - ctl = ctEvLoc ev - in setCtLoc (mkNonCanonical ev) (setCtLocSpan ctl ct_ls) - -mkKnWanted - :: Ct - -> CType - -> TcPluginM Ct -mkKnWanted ct (CType ty) = do - kc_clas <- tcLookupClass knownNatClassName - let kn_pred = mkClassPred kc_clas [ty] - wantedCtEv <- TcPluginM.newWanted (ctLoc ct) kn_pred - let wanted' = mkNonCanonical' (ctLoc ct) wantedCtEv - return wanted' - -unifyItemToCt :: CtLoc - -> PredType - -> CoercionHole - -> Ct -unifyItemToCt loc pred_type hole = - mkNonCanonical - (CtWanted - pred_type - (HoleDest hole) -#if MIN_VERSION_ghc(8,2,0) - WDeriv -#endif - loc) diff --git a/src/GHC/TypeLits/Normalise.hs b/src/GHC/TypeLits/Normalise.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits/Normalise.hs @@ -0,0 +1,966 @@ +{-| +Copyright : (C) 2015-2016, University of Twente, + 2017 , QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij + +A type checker plugin for GHC that can solve /equalities/ of types of kind +'GHC.TypeLits.Nat', where these types are either: + +* Type-level naturals +* Type variables +* Applications of the arithmetic expressions @(+,-,*,^)@. + +It solves these equalities by normalising them to /sort-of/ +'GHC.TypeLits.Normalise.SOP.SOP' (Sum-of-Products) form, and then perform a +simple syntactic equality. + +For example, this solver can prove the equality between: + +@ +(x + 2)^(y + 2) +@ + +and + +@ +4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2 +@ + +Because the latter is actually the 'GHC.TypeLits.Normalise.SOP.SOP' normal form +of the former. + +To use the plugin, add + +@ +{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\} +@ + +To the header of your file. + +== Treating subtraction as addition with a negated number + +If you are absolutely sure that your subtractions can /never/ lead to (a locally) +negative number, you can ask the plugin to treat subtraction as addition with +a negated operand by additionally adding: + +@ +{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\} +@ + +to the header of your file, thereby allowing to use associativity and +commutativity rules when proving constraints involving subtractions. Note that +this option can lead to unsound behaviour and should be handled with extreme +care. + +=== When it leads to unsound behaviour + +For example, enabling the /allow-negated-numbers/ feature would allow +you to prove: + +@ +(n - 1) + 1 ~ n +@ + +/without/ a @(1 <= n)@ constraint, even though when /n/ is set to /0/ the +subtraction @n-1@ would be locally negative and hence not be a natural number. + +This would allow the following erroneous definition: + +@ +data Fin (n :: Nat) where + FZ :: Fin (n + 1) + FS :: Fin n -> Fin (n + 1) + +f :: forall n . Natural -> Fin n +f n = case of + 0 -> FZ + x -> FS (f \@(n-1) (x - 1)) + +fs :: [Fin 0] +fs = f \<$\> [0..] +@ + +=== When it might be Okay + +This example is taken from the +library. + +When you have: + +@ +-- | Singleton type for the number of repetitions of an element. +data Times (n :: Nat) where + T :: Times n + +-- | An element of a "run-length encoded" vector, containing the value and +-- the number of repetitions +data Elem :: Type -> Nat -> Type where + (:*) :: t -> Times n -> Elem t n + +-- | A length-indexed vector, optimised for repetitions. +data OptVector :: Type -> Nat -> Type where + End :: OptVector t 0 + (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n +@ + +And you want to define: + +@ +-- | Append two optimised vectors. +type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where + ys ++ End = ys + End ++ ys = ys + (x :- xs) ++ ys = x :- (xs ++ ys) +@ + +then the last line will give rise to the constraint: + +@ +(n-l)+m ~ (n+m)-l +@ + +because: + +@ +x :: Elem t l +xs :: OptVector t (n-l) +ys :: OptVector t m +@ + +In this case it's okay to add + +@ +{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\} +@ + +if you can convince yourself you will never be able to construct a: + +@ +xs :: OptVector t (n-l) +@ + +where /n-l/ is a negative number. +-} + +{-# LANGUAGE CPP #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TemplateHaskellQuotes #-} + +{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-} +{-# OPTIONS_HADDOCK show-extensions #-} + +module GHC.TypeLits.Normalise + ( plugin ) +where + +-- base +import Control.Arrow + ( second ) +import Control.Monad + ( (<=<), unless ) +import Control.Monad.Trans.Writer.Strict + ( WriterT(runWriterT), runWriter ) +import Data.Either + ( rights, partitionEithers ) +import Data.Foldable +import Data.List + ( stripPrefix, partition ) +import Data.Maybe + ( mapMaybe, catMaybes, fromMaybe, isJust ) +import Data.Traversable + ( for ) +import Text.Read + ( readMaybe ) + +-- containers +import Data.Set + ( Set ) +import qualified Data.Set as Set + ( elems, empty ) +import Data.Map.Strict + ( Map ) +import qualified Data.Map.Strict as Map + ( empty, insertWith, traverseWithKey ) + +-- ghc +import GHC.Builtin.Names + ( knownNatClassName ) +import GHC.Builtin.Types.Literals + ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon ) +import GHC.Core.TyCon + ( Injectivity (..), tyConInjectivityInfo, tyConArity ) +import GHC.Utils.Misc + ( filterByList ) + +-- ghc-tcplugin-api +import GHC.TcPlugin.API +import GHC.TcPlugin.API.TyConSubst + ( TyConSubst, mkTyConSubst ) +import GHC.Plugins + ( Plugin(..), defaultPlugin, purePlugin, allVarSet, isEmptyVarSet, tyCoVarsOfType ) +import GHC.Utils.Outputable + +-- ghc-typelits-natnormalise +import GHC.TypeLits.Normalise.Compat +import GHC.TypeLits.Normalise.SOP + ( SOP(S), Product(P), Symbol(V) ) +import GHC.TypeLits.Normalise.Unify + +-- transformers +import Control.Monad.Trans.Class + ( lift ) +import Control.Monad.Trans.State.Strict + ( StateT, evalStateT, get, modify ) + +-------------------------------------------------------------------------------- + +-- | To use the plugin, add +-- +-- @ +-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\} +-- @ +-- +-- To the header of your file. +plugin :: Plugin +plugin + = defaultPlugin + { tcPlugin = \ p -> do opts <- foldr id defaultOpts <$> traverse parseArgument p + return $ mkTcPlugin $ normalisePlugin opts + , pluginRecompile = purePlugin + } + where + parseArgument "allow-negated-numbers" = Just (\ opts -> opts { negNumbers = True }) + parseArgument (readMaybe <=< stripPrefix "depth=" -> Just depth) = Just (\ opts -> opts { depth }) + parseArgument _ = Nothing + defaultOpts = Opts { negNumbers = False, depth = 5 } + +data Opts = Opts { negNumbers :: Bool, depth :: Word } + +normalisePlugin :: Opts -> TcPlugin +normalisePlugin opts = + TcPlugin { tcPluginInit = lookupExtraDefs + , tcPluginSolve = decideEqualSOP opts + , tcPluginRewrite = const emptyUFM + , tcPluginPostTc = const (return ()) + , tcPluginShutdown = const (return ()) + } + +data ExtraDefs + = ExtraDefs + { tyCons :: LookedUpTyCons } + +lookupExtraDefs :: TcPluginM Init ExtraDefs +lookupExtraDefs = do + tcs <- lookupTyCons + return $ + ExtraDefs + { tyCons = tcs } + +decideEqualSOP + :: Opts + -> ExtraDefs + -- ^ 1. Givens that is already generated. + -- We have to generate new givens at most once; + -- otherwise GHC will loop indefinitely. + -- + -- + -- 2. For GHc 9.2: TyCon of Data.Type.Ord.OrdCond + -- For older: TyCon of GHC.TypeLits.<=? + -> [Ct] + -> [Ct] + -> TcPluginM Solve TcPluginSolveResult +-- Simplification phase: Derives /simplified/ givens; +-- we can reduce given constraints like @Show (Foo (n + 2))@ +-- to its normal form @Show (Foo (2 + n))@, which is eventually +-- useful in solving phase. +-- +-- This helps us to solve /indirect/ constraints; +-- without this phase, we cannot derive, e.g., +-- @IsVector UVector (Fin (n + 1))@ from +-- @Unbox (1 + n)@! +decideEqualSOP opts (ExtraDefs { tyCons = tcs }) givens [] = + do + let + givensTyConSubst = mkTyConSubst givens + (redGivens, _) <- reduceGivens False opts tcs givens + + tcPluginTrace "decideEqualSOP Givens {" $ + vcat [ text "givens:" <+> ppr givens ] + + -- Try to find contradictory Givens, to improve pattern match warnings. + SimplifyResult { simplifiedWanteds, contradictions, newGivens } <- + simplifyNats opts tcs [] $ + concatMap (toNatEquality opts tcs givensTyConSubst) redGivens + + -- Only add new Givens that are genuinely new, i.e. that GHC doesn't + -- already know. + -- + -- For example, in #116 we had: [G] m ~ n, [G] n ~ 0. Recalling that + -- the inert set in GHC is a /not necessarily idempotent/ terminating + -- generalised substitution (see Note [The KickOut Criteria] in GHC.Tc.Solver.InertSet), + -- we don't want to emit a new Given [G] m ~ 0: GHC already knows this, and + -- if we repeatedly emit this Given we will cause a typechecker loop (as in #116). + let + isSolvedGiven subst ct = + case classifyPredType $ substTy subst (ctPred ct) of + EqPred _rel t1 t2 -> t1 `eqType` t2 + _ -> False + tyEqLit ct = + case classifyPredType (ctPred ct) of + EqPred NomEq t1 t2 -> isTyVarTy t1 && isJust (isNumLitTy t2) + _ -> False + givensSubst = ctsSubst givens -- Computes the idempotent substitution from the Givens + actuallyNewGivens = + filter + (\ ct -> + tyEqLit ct + -- For now, only admit improved Givens in the form of `n ~ L`, + -- where `n` is a type variable and `L` is a numeric literal. + && + not (isSolvedGiven givensSubst ct) + -- Ensure this Given is genuinely new information to GHC, to + -- avoid repeatedly emitting facts that GHC already knows, + -- which can cause the typechecker to loop (#116). + ) + newGivens + + tcPluginTrace "decideEqualSOP Givens }" $ + vcat [ text "givens:" <+> ppr givens + , text "simpls:" <+> ppr simplifiedWanteds + , text "contra:" <+> ppr contradictions + , text "new:" <+> ppr actuallyNewGivens + ] + return $ + mkTcPluginSolveResult +#if MIN_VERSION_ghc(9,14,0) + ( map fromNatEquality contradictions ) +#else + [] +#endif + [] -- no solved Givens + actuallyNewGivens + +-- Solving phase. +-- Solves in/equalities on Nats and simplifiable constraints +-- containing naturals. +decideEqualSOP opts (ExtraDefs { tyCons = tcs }) givens wanteds0 = do + deriveds <- askDeriveds + let wanteds = if null wanteds0 + then [] + else wanteds0 ++ deriveds + givensTyConSubst = mkTyConSubst givens + unit_wanteds0 = concatMap (toNatEquality opts tcs givensTyConSubst) wanteds + nonEqs = filter ( not + . (\p -> isEqPred p || isEqClassPred p) + . ctEvPred + . ctEvidence ) + wanteds + + (redGivens, negWanteds) <- reduceGivens True opts tcs givens + reducible_wanteds + <- catMaybes <$> mapM (\ct -> fmap (ct,) <$> + reduceNatConstr redGivens ct) + nonEqs + + tcPluginTrace "decideEqualSOP Wanteds {" $ + vcat [ text "givens:" <+> ppr givens + , text "new reduced givens:" <+> ppr redGivens + , text $ replicate 80 '-' + , text "wanteds:" <+> ppr wanteds + , text "unit_wanteds:" <+> ppr unit_wanteds0 + , text "reducible_wanteds:" <+> ppr reducible_wanteds + ] + if null unit_wanteds0 && null reducible_wanteds + then return $ TcPluginOk [] [] + else do + -- Since reducible Wanteds also can have some negation/subtraction + -- subterms, we have to make sure appropriate inequalities to hold. + -- Here, we generate such additional inequalities for reduction + -- that is to be added to new [W]anteds. + let mkNegWanted ( CType wtdPred ) loc = mkNonCanonical <$> newWanted loc wtdPred + ineqForRedWants <- Map.traverseWithKey mkNegWanted negWanteds + let unit_givens = concatMap (toNatEquality opts tcs givensTyConSubst) redGivens + unit_wanteds = unit_wanteds0 ++ concatMap (toNatEquality opts tcs givensTyConSubst) ineqForRedWants + sr@SimplifyResult{simplifiedWanteds, contradictions} <- + simplifyNats opts tcs unit_givens unit_wanteds + tcPluginTrace "normalised" (ppr sr) + reds <- for reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do + wants <- evSubtPreds (ctLoc origCt) $ subToPred opts tcs ws + return ((term, origCt), wDicts ++ wants) + let -- Only solve a Derived when there are Wanteds in play + simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) simplifiedWanteds ++ reds of + [] -> [] + _ -> simplifiedWanteds + (solved,newWanteds) = second concat (unzip $ simpld1 ++ reds) + + tcPluginTrace "decideEqualSOP Wanteds }" $ + vcat [ text "givens:" <+> ppr givens + , text "new reduced givens:" <+> ppr redGivens + , text "unit givens:" <+> ppr unit_givens + , text $ replicate 80 '-' + , text "wanteds:" <+> ppr wanteds + , text "ineqForRedWants:" <+> ppr ineqForRedWants + , text "unit_wanteds:" <+> ppr unit_wanteds + , text "reducible_wanteds:" <+> ppr reducible_wanteds + , text $ replicate 80 '=' + , text "solved:" <+> ppr solved + , text "newWanteds:" <+> ppr newWanteds + ] + return $ + mkTcPluginSolveResult + (map fromNatEquality contradictions) + solved + newWanteds + +type NatEquality = (Ct,CoreSOP,CoreSOP) +type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool)) + +reduceGivens :: Bool -- ^ allow generating new "non-negative" Wanteds + -> Opts -> LookedUpTyCons + -> [Ct] + -> TcPluginM Solve ([Ct], Map CType CtLoc) +reduceGivens gen_wanteds opts tcs origGivens = go [] Map.empty origGivens + where + go rev_acc_gs acc_ws [] = return ( reverse rev_acc_gs, acc_ws ) + go rev_acc_gs acc_ws (g:gs) = + case tryReduceGiven opts tcs origGivens g of + Just ( pred', evExpr, ws ) + | gen_wanteds || null ws || negNumbers opts + -> do + let loc = ctLoc g + g' <- mkNonCanonical <$> newGiven loc pred' evExpr + let !acc' = foldl' (insertWanted loc) acc_ws ws + go ( g' : rev_acc_gs ) acc' gs + _ -> + go ( g : rev_acc_gs ) acc_ws gs + + insertWanted :: CtLoc -> Map CType CtLoc -> Type -> Map CType CtLoc + insertWanted loc acc w = + Map.insertWith (\ _new old -> old) (CType w) loc acc + +tryReduceGiven + :: Opts -> LookedUpTyCons + -> [Ct] -> Ct + -> Maybe (PredType, EvTerm, [PredType]) +tryReduceGiven opts tcs simplGivens ct = do + let (mans, ws) = + runWriter $ normaliseNatEverywhere $ + ctEvPred $ ctEvidence ct + ws' = [ p + | p <- subToPred opts tcs ws + , all (not . (`eqType` p) . ctEvPred . ctEvidence) simplGivens + ] + -- deps = unitDVarSet (ctEvId ct) + (pred', deps) <- mans + case classifyPredType pred' of + EqPred _ l r + | l `eqType` r + -> Nothing + _ -> return (pred', toReducedDict (ctEvidence ct) pred' deps, ws') + +fromNatEquality :: Either NatEquality NatInEquality -> Ct +fromNatEquality (Left (ct, _, _)) = ct +fromNatEquality (Right (ct, _)) = ct + +reduceNatConstr :: [Ct] -> Ct -> TcPluginM Solve (Maybe (EvTerm, [(Type, Type)], [Ct])) +reduceNatConstr givens ct = do + let pred0 = ctEvPred $ ctEvidence ct + (mans, tests) = runWriter $ normaliseNatEverywhere pred0 + + -- Even if we didn't rewrite the Wanted, + -- we may still be able to solve it from a (rewritten) Given. + (pred', deps') = fromMaybe (pred0, []) mans + case find ((`eqType` pred') . ctEvPred . ctEvidence) givens of + -- No existing evidence found + Nothing + | ClassPred cls _ <- classifyPredType pred' + , className cls /= knownNatClassName + + -- We actually did do some rewriting/normalisation. + , Just {} <- mans + -> do + -- Create new evidence binding for normalized class constraint + wtdDictCt <- mkNonCanonical <$> newWanted (ctLoc ct) pred' + -- Evidence for current wanted is simply the coerced binding for + -- the new binding + let evCo = mkPluginUnivCo "ghc-typelits-natnormalise" + Representational + deps' + pred' pred0 + ev = evCast (evId $ ctEvId wtdDictCt) evCo + -- Use newly created coerced wanted as evidence, and emit the + -- normalized wanted as a new constraint to solve. + return (Just (EvExpr ev, tests, [wtdDictCt])) + | otherwise + -> return Nothing + -- Use existing evidence + Just c -> return (Just (toReducedDict (ctEvidence c) pred0 deps', tests, [])) + +toReducedDict :: CtEvidence -> PredType -> [Coercion] -> EvTerm +toReducedDict ct pred' deps' = + let pred0 = ctEvPred ct + evCo = mkPluginUnivCo "ghc-typelits-natnormalise" + Representational + deps' + pred0 pred' + ev = evCast (ctEvExpr ct) evCo + in EvExpr ev + +data SimplifyResult + = SimplifyResult + { simplifiedWanteds :: [((EvTerm,Ct),[Ct])] + -- ^ List of: + -- * Tuple of: + -- * Evidence for: + -- * The solved Wanted + -- * Preconditions (in the for of new Wanteds) + , contradictions :: [Either NatEquality NatInEquality] + -- ^ List of contradictions + , newGivens :: [Ct] + -- ^ Givens derived in the improve givens stage + } + +instance Outputable SimplifyResult where + ppr (SimplifyResult { simplifiedWanteds, contradictions, newGivens }) = + text "SimplifyResult { simplified =" <+> ppr simplifiedWanteds + <+> text ", impossible =" <+> ppr contradictions + <+> text ", new_givens =" <+> ppr newGivens <+> text "}" + +data NatCt + = NatCt + { predicate :: Either NatEquality NatInEquality + -- ^ Predicate: either an equality or inequality + , preconds :: [PredType] + -- ^ Preconditions (in the form of inequalities encoded as PredTypes) + , ctDeps :: [Coercion] + -- ^ Coercion(s) from which the predicate is derived, needed so that evidence + -- doesn't float above the coercions from which it is derived. + } + +instance Outputable NatCt where + ppr (NatCt {predicate, preconds, ctDeps}) = + text "NatCt { predicate = " <+> ppr predicate + <+> text ", preconditions = " <+> ppr preconds + <+> text ", dependencies = " <+> ppr ctDeps <+> text "}" + +data SimplifyState + = SimplifyState + { stDeps :: [Coercion] + -- ^ Coercions on which the simplified evidence depends, this needs to be + -- kept around because sometimes we solving one constraint (which has a + -- depedency) is used to solve another constraint + , subst :: [CoreUnify] + -- ^ Derived simplifications (i.e. b ~ c derived from (a + b) ~ (a + c)), + -- and substitutions (i.e. n := 0 derived from y ^ n ~ 1) + , evs :: [((EvTerm,Ct),[Ct])] + -- ^ Collected evidence + , leqsG :: [(CoreSOP,CoreSOP,Bool)] + -- ^ Given inequalities + , unsolved :: [NatCt] + -- ^ Tried, but unsolved predicates. We keep them around in case we solve a + -- new predicate which could lead to a substitution that enables a solve. + , derivedGivens :: [Ct] + -- ^ Unifiers derived from Givens. E.g. when we have /[G] x ^ n ~ 1/, this + -- field will hold a derived /[G] n ~ 0/. + } + +emptySimplifyState :: SimplifyState +emptySimplifyState + = SimplifyState + { stDeps = [] + , subst = [] + , evs = [] + , leqsG = [] + , unsolved = [] + , derivedGivens = [] + } + +simplifyNats + :: Opts + -- ^ Allow negated numbers (potentially unsound!) + -> LookedUpTyCons + -> [NatCt] + -- ^ Given constraints + -> [NatCt] + -- ^ Wanted constraints + -> TcPluginM Solve SimplifyResult +simplifyNats Opts{depth} tcs eqsG eqsW = do + let eqsG1 = map (\nCt -> nCt{preconds = []}) eqsG + (varEqs, otherEqs) = partition (isVarEqs . predicate) eqsG1 + fancyGivens = concatMap (makeGivensSet otherEqs) varEqs + case varEqs of + [] -> do + let eqs = otherEqs ++ eqsW + tcPluginTrace "simplifyNats" (ppr eqs) + evalStateT (simples eqs) emptySimplifyState + _ -> do + tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")") + (ppr varEqs) + + allSimplified <- for fancyGivens $ \v -> do + let eqs = v ++ eqsW + tcPluginTrace "simplifyNats" (ppr eqs) + evalStateT (simples eqs) emptySimplifyState + + pure (foldr findFirstSimpliedWanted (SimplifyResult [] [] []) allSimplified) + where + simples :: + [NatCt] -> + StateT SimplifyState (TcPluginM Solve) SimplifyResult + simples [] = do + SimplifyState{evs, derivedGivens} <- get + return SimplifyResult { simplifiedWanteds = evs + , contradictions = [] + , newGivens = derivedGivens + } + simples (eq@NatCt{predicate=(Left (ct,u,v)), preconds, ctDeps}:eqs) = do + SimplifyState{stDeps, subst, evs, leqsG, unsolved, derivedGivens} <- get + let allDeps = stDeps ++ ctDeps + + let u' = substsSOP subst u + v' = substsSOP subst v + ur <- lift (unifyNats ct u' v') + lift (tcPluginTrace "unifyNats result" (ppr ur)) + case ur of + Win -> do + -- Do note record "new" evidence for given constraints. + unless (isGiven (ctEvidence ct)) $ do + -- Only recorde evidence for wanted contstraints + evM <- lift (evMagic tcs ct allDeps mempty preconds) + lift $ tcPluginTrace "unifyNats Win" $ + vcat [ text "evM:" <+> ppr evM + , text "ct:" <+> ppr ct + ] + modify (\s -> s {evs = maybe evs (:evs) evM}) + simples eqs + Lose -> + addContra (predicate eq) <$> simples eqs + Draw [] -> do + -- No progress made, add it to the "unsolved" list, in the hope we + -- can make progress when we later find a new substitution + modify (\s -> s {unsolved = eq:unsolved}) + simples eqs + Draw unifications -> do -- We made some progress in the form of a unifier + + -- As the derived unifiers we record here can lead to solving another + -- equation, we add it and its dependencies to the list of global + -- dependencies which we use when creating new evidence + let stDeps1 = ctEvCoercion (ctEvidence ct):allDeps + -- We add apply the derived unification in the existing set of + -- unification, and also add the derived unificaiton to the global + -- state; to be used in solving later equations. + let subst1 = substsSubst unifications subst ++ unifications + if isGiven (ctEvidence ct) then do + if null preconds then do + -- We only record the unification derived from a given constraint + -- when it has no preconditions in order for this unification to + -- hold. The reason for that is that we can currently not record + -- new Wanteds to be emitted at the end of the solve. + givensU <- lift (mapM (unifyItemToGiven (ctLoc ct) allDeps) unifications) + modify (\s -> s { stDeps = stDeps1 + , subst = subst1 + , leqsG = eqToLeq u' v' ++ leqsG + , unsolved = [] + , derivedGivens = givensU ++ derivedGivens + }) + simples (unsolved ++ eqs) + else + simples eqs + else do + let allPreconds = map unifyItemToPredType unifications ++ preconds + evM <- lift (evMagic tcs ct allDeps Set.empty allPreconds) + case evM of + Nothing -> + simples eqs + Just ev -> do + -- We only record the unification derived from a wanted constraint + -- when we can actually record evidence for a succesful solve. + modify (\s -> s { stDeps = stDeps1 + , subst = subst1 + , evs = ev:evs + , unsolved = [] + }) + simples (unsolved ++ eqs) + + simples (eq@NatCt{predicate=Right (ct,u@(x,y,b)), preconds, ctDeps}:eqs) = do + SimplifyState{stDeps, subst, evs, leqsG, unsolved} <- get + let u' = substsSOP subst (subtractIneq u) + x' = substsSOP subst x + y' = substsSOP subst y + uS = (x',y',b) + leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG + | otherwise = leqsG + ineqs = concat [ leqsG + , map (substLeq subst) leqsG + , map snd (rights (map predicate eqsG)) + ] + allDeps = stDeps ++ ctDeps + lift (tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs))) + case runWriterT (isNatural u') of + Just (True,knW) -> do + evs' <- maybe evs (:evs) <$> lift (evMagic tcs ct allDeps knW preconds) + modify (\s -> s {evs = evs', leqsG = leqsG'}) + simples eqs + + Just (False,_) | null preconds -> + addContra (predicate eq) <$> simples eqs + _ -> do + let solvedIneq = mapMaybe runWriterT + -- it is an inequality that can be instantly solved, such as + -- `1 <= x^y` + -- OR + (instantSolveIneq depth u: + instantSolveIneq depth uS: + -- This inequality is either a given constraint, or it is a wanted + -- constraint, which in normal form is equal to another given + -- constraint, hence it can be solved. + -- OR + map (solveIneq depth u) ineqs ++ + -- The above, but with valid substitutions applied to the wanted. + map (solveIneq depth uS) ineqs) + smallest = solvedInEqSmallestConstraint solvedIneq + case smallest of + (True,kW) -> do + evs' <- maybe evs (:evs) <$> lift (evMagic tcs ct allDeps kW preconds) + modify (\s -> s { stDeps = allDeps + , evs = evs' + , leqsG = leqsG' + }) + simples eqs + _ -> do + modify (\s -> s {unsolved = eq:unsolved}) + simples eqs + + eqToLeq x y = [(x,y,True),(y,x,True)] + substLeq s (x,y,b) = (substsSOP s x, substsSOP s y, b) + + isVarEqs (Left (_,S [P [V _]], S [P [V _]])) = True + isVarEqs _ = False + + makeGivensSet :: [NatCt] -> NatCt -> [[NatCt]] + makeGivensSet otherEqs varEq + = let (noMentionsV,mentionsV) = partitionEithers + (map (matchesVarEq varEq) otherEqs) + (mentionsLHS,mentionsRHS) = partitionEithers mentionsV + vS = varEq {predicate = swapVar (predicate varEq)} + givensLHS = case mentionsLHS of + [] -> [] + _ -> [mentionsLHS ++ ((varEq:mentionsRHS) ++ noMentionsV)] + givensRHS = case mentionsRHS of + [] -> [] + _ -> [mentionsRHS ++ (vS:mentionsLHS ++ noMentionsV)] + in case mentionsV of + [] -> [noMentionsV] + _ -> givensLHS ++ givensRHS + + matchesVarEq :: NatCt + -> NatCt + -> Either NatCt (Either NatCt NatCt) + matchesVarEq NatCt{predicate = Left (_, S [P [V v1]], S [P [V v2]])} r@(NatCt e _ _) = + case e of + Left (_,S [P [V v3]],_) + | v1 == v3 -> Right (Left r) + | v2 == v3 -> Right (Right r) + Left (_,_,S [P [V v3]]) + | v1 == v3 -> Right (Left r) + | v2 == v3 -> Right (Right r) + Right (_,(S [P [V v3]],_,_)) + | v1 == v3 -> Right (Left r) + | v2 == v3 -> Right (Right r) + Right (_,(_,S [P [V v3]],_)) + | v1 == v3 -> Right (Left r) + | v2 == v3 -> Right (Right r) + _ -> Left r + matchesVarEq _ _ = error "internal error" + + swapVar (Left (ct,S [P [V v1]], S [P [V v2]])) = + Left (ct,S [P [V v2]], S [P [V v1]]) + swapVar _ = error "internal error" + + findFirstSimpliedWanted s1@(SimplifyResult {simplifiedWanteds, contradictions}) s2 + | not (null contradictions) + || any (isWanted . ctEvidence . snd . fst) simplifiedWanteds + = s1 + | otherwise + = s2 + +addContra :: Either NatEquality NatInEquality -> SimplifyResult -> SimplifyResult +addContra contra sr = sr { contradictions = contra : contradictions sr } + +-- If we allow negated numbers we simply do not emit the inequalities +-- derived from the subtractions that are converted to additions with a +-- negated operand +subToPred :: Opts -> LookedUpTyCons -> [(Type, Type)] -> [PredType] +subToPred Opts{..} tcs + | negNumbers = const [] + | otherwise = + -- Given 'a - b', require 'b <= a'. + map (\ (a, b) -> mkLEqNat tcs b a) + +-- | Extract all Nat equality and inequality constraints from another constraint. +toNatEquality :: Opts -> LookedUpTyCons -> TyConSubst -> Ct -> [NatCt] +toNatEquality opts tcs givensTyConSubst ct0 + | Just (((x,y), mbLTE), cos0) <- isNatRel tcs givensTyConSubst pred0 + , let + ((x', cos1),k1) = runWriter (normaliseNat x) + ((y', cos2),k2) = runWriter (normaliseNat y) + preds = subToPred opts tcs (k1 ++ k2) + = case mbLTE of + Nothing -> + -- Equality constraint: x ~ y + [NatCt (Left (ct0, x', y')) preds (cos0 ++ cos1 ++ cos2)] + Just b -> + -- Inequality constraint: (x <=? y) ~ b + [NatCt (Right (ct0, (x', y', b))) preds (cos0 ++ cos1 ++ cos2)] + | otherwise + = case classifyPredType pred0 of + EqPred NomEq t1 t2 + -> goNomEq t1 t2 + ClassPred kn [x] + -- From [G] KnownNat blah, also produce [G] 0 <= blah + -- See https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94. + | isGiven (ctEvidence ct0) + , className kn == knownNatClassName + , let ((x', cos0), ks) = runWriter (normaliseNat x) + , let preds = subToPred opts tcs ks + -> [NatCt (Right (ct0, (S [], x', True))) preds cos0] + _ -> [] + where + pred0 = ctPred ct0 + -- x ~ y + goNomEq :: Type -> Type -> [NatCt] + goNomEq lhs rhs + -- Recur into a TyCon application for TyCons that we **do not** rewrite, + -- e.g. peek inside the Maybe in 'Maybe (x + y) ~ Maybe (y + x)'. + | Just (tc , xs) <- splitTyConApp_maybe lhs + , Just (tc', ys) <- splitTyConApp_maybe rhs + , tc == tc' + , not $ tc `elem` [typeNatAddTyCon, typeNatSubTyCon, typeNatMulTyCon, typeNatExpTyCon] + , let xys = zip xs ys + -- Make sure not to recur into non-injective positions of type families, + -- e.g. if we know 'F n ~ F m' that doesn't mean 'n ~ m'. + subs = + filter (not . uncurry eqType) $ + case tyConInjectivityInfo tc of + Injective inj -> + filterByList (inj ++ repeat True) xys + _ -> + -- However, it is okay to recur in the following specific + -- exception: + let (tcArgs,rest) = splitAt (tyConArity tc) xys + diffs = filter (not . uncurry eqType) tcArgs + in case diffs of + -- 1. The types only differ in one argument position + [(x,y)] + | let xFVs = tyCoVarsOfType x + , let yFVs = tyCoVarsOfType y + -- 2. The argument must have variables, and they must + -- all be skolem variables. + , not (isEmptyVarSet xFVs) + , allVarSet isSkolemTyVar xFVs + -- 3. The variables in both argument postions must + -- be the same. + , xFVs == yFVs + -> (x,y):rest + _ -> rest + = case concatMap (uncurry rewrite) subs of + [] -> [] + [rw] -> [rw] + rws -> + -- For Given Cts, it's fine to extract multiple (in)equalities. However, + -- for Wanted Cts we should not claim to solve the entire Ct when we + -- only solve a part of the Ct. So when we can extra two or more inequalities + -- from a Wanted Ct, we conservatively choose not to solve any of them. + if isGiven (ctEvidence ct0) then + rws + else + [] + | otherwise + = rewrite lhs rhs + + rewrite :: Type -> Type -> [NatCt] + rewrite x y + | isNatKind (typeKind x) + , isNatKind (typeKind y) + , let ((x', cos1),k1) = runWriter (normaliseNat x) + , let ((y', cos2),k2) = runWriter (normaliseNat y) + , let preds = subToPred opts tcs (k1 ++ k2) + = [NatCt (Left (ct0,x',y')) preds (cos1 ++ cos2)] + | otherwise + = [] + + isNatKind :: Kind -> Bool + isNatKind = (`eqType` natKind) + +unifyItemToPredType :: CoreUnify -> PredType +unifyItemToPredType ui = mkEqPredRole Nominal ty1 ty2 + where + ty1 = case ui of + SubstItem {..} -> mkTyVarTy siVar + UnifyItem {..} -> reifySOP siLHS + ty2 = case ui of + SubstItem {..} -> reifySOP siSOP + UnifyItem {..} -> reifySOP siRHS + + +unifyItemToGiven :: CtLoc -> [Coercion] -> CoreUnify -> TcPluginM Solve Ct +unifyItemToGiven loc deps ui = mkNonCanonical <$> newGiven loc pty (EvExpr (Coercion co)) + where + ty1 = case ui of + SubstItem {..} -> mkTyVarTy siVar + UnifyItem {..} -> reifySOP siLHS + ty2 = case ui of + SubstItem {..} -> reifySOP siSOP + UnifyItem {..} -> reifySOP siRHS + + pty = mkEqPredRole Nominal ty1 ty2 + co = mkPluginUnivCo "ghc-typelits-natnormalise" Nominal deps ty1 ty2 + +evSubtPreds :: CtLoc -> [PredType] -> TcPluginM Solve [Ct] +evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc) + +evMagic :: + -- | Known TyCon environment + LookedUpTyCons -> + -- | Constraint for which we are creating evidence + Ct -> + -- | Coercions in which the evidence depends + [Coercion] -> + -- | Types that we should be known to be a Natural + Set CType -> + -- | Inequalities that should hold + [PredType] -> + TcPluginM Solve (Maybe ((EvTerm, Ct), [Ct])) +evMagic tcs ct deps knW preds = do + holeWanteds <- evSubtPreds (ctLoc ct) preds + knWanted <- mapM (mkKnWanted (ctLoc ct)) (Set.elems knW) + let newWant = knWanted ++ holeWanteds + case classifyPredType $ ctEvPred $ ctEvidence ct of + EqPred NomEq t1 t2 -> + let ctEv = mkPluginUnivCo "ghc-typelits-natnormalise" Nominal deps t1 t2 + in return (Just ((EvExpr (Coercion ctEv), ct),newWant)) + IrredPred p -> + let t1 = mkTyConApp (c0TyCon tcs) [] + co = mkPluginUnivCo "ghc-typelits-natnormalise" Representational deps t1 p + dcApp = evDataConApp (c0DataCon tcs) [] [] + in return (Just ((EvExpr $ evCast dcApp co, ct),newWant)) + _ -> return Nothing + +mkKnWanted + :: CtLoc + -> CType + -> TcPluginM Solve Ct +mkKnWanted loc (CType ty) = do + kc_clas <- tcLookupClass knownNatClassName + let kn_pred = mkClassPred kc_clas [ty] + wantedCtEv <- newWanted loc kn_pred + return $ mkNonCanonical wantedCtEv diff --git a/src/GHC/TypeLits/Normalise/Compat.hs b/src/GHC/TypeLits/Normalise/Compat.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits/Normalise/Compat.hs @@ -0,0 +1,399 @@ + +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TemplateHaskellQuotes #-} + +{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-} + +module GHC.TypeLits.Normalise.Compat + ( LookedUpTyCons(..), lookupTyCons + , upToGivens + , mkLEqNat + , Relation, isNatRel + + , UniqMap, intersectUniqMap_C, listToUniqMap, nonDetUniqMapToList + + , mkTcPluginSolveResult + + ) where + +-- base +import Control.Arrow + ( second ) +import qualified Data.List.NonEmpty as NE + ( toList ) +import Data.Foldable + ( asum ) +import GHC.TypeNats + ( CmpNat ) +#if MIN_VERSION_ghc(9,3,0) +import qualified GHC.TypeError + ( Assert ) +#endif +#if MIN_VERSION_ghc(9,1,0) +import qualified Data.Type.Ord + ( OrdCond, type (<=) ) + +#else +import GHC.TypeNats + ( type (<=), type (<=?) ) +#endif + +-- ghc +import GHC.Builtin.Types + ( isCTupleTyConName + , promotedFalseDataCon, promotedTrueDataCon + , promotedLTDataCon, promotedEQDataCon, promotedGTDataCon + ) +#if MIN_VERSION_ghc(9,1,0) +import GHC.Builtin.Types + ( cTupleTyCon, cTupleDataCon ) +#else +import GHC.Builtin.Types + ( cTupleTyConName ) +#endif +#if MIN_VERSION_ghc(9,7,0) +import GHC.Types.Unique.Map + ( UniqMap, intersectUniqMap_C, listToUniqMap, nonDetUniqMapToList ) +#else +import GHC.Types.Unique + ( Uniquable ) +import GHC.Types.Unique.FM + ( intersectUFM_C, nonDetEltsUFM ) +#endif + +-- ghc-tcplugin-api +import GHC.TcPlugin.API +import GHC.TcPlugin.API.TyConSubst + ( TyConSubst, splitTyConApp_upTo ) + +-------------------------------------------------------------------------------- + +data LookedUpTyCons + = LookedUpTyCons + { +#if MIN_VERSION_ghc(9,3,0) + assertTyCon :: TyCon, +#endif +#if MIN_VERSION_ghc(9,1,0) + -- | @<= :: k -> k -> Constraint@ + ordCondTyCon :: TyCon, + leqTyCon :: TyCon, +#else + -- | @<= :: Nat -> Nat -> Constraint@ + leqNatTyCon :: TyCon, + -- | @<=? :: Nat -> Nat -> Constraint@ + leqQNatTyCon :: TyCon, +#endif + cmpNatTyCon :: TyCon, + c0TyCon :: TyCon, + c0DataCon :: DataCon + } + +lookupTyCons :: TcPluginM Init LookedUpTyCons +lookupTyCons = do + cmpNatT <- lookupTHName ''GHC.TypeNats.CmpNat >>= tcLookupTyCon +#if MIN_VERSION_ghc(9,3,0) + assertT <- lookupTHName ''GHC.TypeError.Assert >>= tcLookupTyCon +#endif +#if MIN_VERSION_ghc(9,1,0) + leqT <- lookupTHName ''(Data.Type.Ord.<=) >>= tcLookupTyCon + ordCond <- lookupTHName ''Data.Type.Ord.OrdCond >>= tcLookupTyCon + return $ + LookedUpTyCons + { leqTyCon = leqT + , ordCondTyCon = ordCond +# if MIN_VERSION_ghc(9,3,0) + , assertTyCon = assertT +# endif + , cmpNatTyCon = cmpNatT + , c0TyCon = cTupleTyCon 0 + , c0DataCon = cTupleDataCon 0 + } +#else + leqT <- lookupTHName ''(GHC.TypeNats.<=) >>= tcLookupTyCon + leqQT <- lookupTHName ''(GHC.TypeNats.<=?) >>= tcLookupTyCon + c0T <- tcLookupTyCon (cTupleTyConName 0) + let c0D = tyConSingleDataCon c0T + -- somehow looking up the 0-tuple data constructor fails + -- with interface file errors, so use tyConSingleDataCon + return $ + LookedUpTyCons + { leqNatTyCon = leqT + , leqQNatTyCon = leqQT + , c0TyCon = c0T + , c0DataCon = c0D + , cmpNatTyCon = cmpNatT + } +#endif + +-- | The constraint @(a <= b)@. +mkLEqNat :: LookedUpTyCons -> Type -> Type -> PredType +mkLEqNat tcs a b = +#if MIN_VERSION_ghc(9,1,0) + mkTyConApp (leqTyCon tcs) [natKind, a, b] +#else + mkTyConApp (leqNatTyCon tcs) [a, b] +#endif + +-- | Is this type 'True' or 'False'? +boolean_maybe :: TyConSubst -> Type -> Maybe (Bool, [Coercion]) +boolean_maybe givensTyConSubst = + upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys ) + where + go tc [] + | tc == promotedTrueDataCon + = Just True + | tc == promotedFalseDataCon + = Just False + go _ _ = Nothing + +-- | Is this type 'LT', 'EQ' or 'GT'? +ordering_maybe :: TyConSubst -> Type -> Maybe (Ordering, [Coercion]) +ordering_maybe givensTyConSubst = + upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys ) + where + go tc [] + | tc == promotedLTDataCon + = Just LT + | tc == promotedEQDataCon + = Just EQ + | tc == promotedGTDataCon + = Just GT + go _ _ = Nothing + +#if MIN_VERSION_ghc(9,1,0) +cmpNat_maybe :: LookedUpTyCons -> TyConSubst -> Type -> Maybe ((Type, Type), [Coercion]) +cmpNat_maybe tcs givensTyConSubst = + upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys ) + where + go tc [x,y] + | tc == cmpNatTyCon tcs + = Just (x,y) + go _ _ = Nothing +#endif + +-- | Is this type @() :: Constraint@? +unitCTuple_maybe :: TyConSubst -> PredType -> Maybe ((), [Coercion]) +unitCTuple_maybe givensTyConSubst = + upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys ) + where + go tc [] + | isCTupleTyConName (tyConName tc) + = Just () + go _ _ = Nothing + +-- | A relation between two natural numbers, @((x,y), mbRel)@. +-- +-- The @mbRel@ value indicates the kind of relation: +-- +-- - @Nothing@ <=> @x ~ y@, +-- - @Just b@ <=> @(x <=? y) ~ b@. +type Relation = ((Type, Type), Maybe Bool) + +{- Note [Recognising Nat inequalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Recognising whether a type is an inequality between two natural numbers is +not as straightforward as one might initially think. The problem is that there +are many different built-in types that can be used to represent an equality of +natural numbers: + + 1. GHC.TypeNats.CmpNat, returning Ordering. + This type family is primitive (on all GHC versions). + 2. GHC.TypeNats.<=?, returning a Boolean. + This type family is primitive prior to GHC 9.1, but is defined in + terms of the 'OrdCond' type family starting in GHC 9.1. + + (NB: it also becomes poly-kinded starting in GHC 9.1.) + 3. GHC.TypeNats.<=, which is defined: + (a) as @x <= y@ <=> @(x <=? y) ~ True@ in GHC prior to 9.3. + (b) as @Assert (x <=? y) ...@ in GHC 9.3 and above. + +To catch all of these, we must thus handle all of the following type families: + + Case 1. CmpNat. + Case 2. (<=?) in GHC 9.1 and prior. + Case 3. OrdCond in GHC 9.1 and later. + Case 4. Assert, in GHC 9.3 and later. + +These are all the built-in type families defined in GHC used to express +inequalities between natural numbers. +-} + +-- | Is this an equality or inequality between two natural numbers? +-- +-- See Note [Recognising Nat inequalities]. +isNatRel :: LookedUpTyCons -> TyConSubst -> PredType -> Maybe (Relation, [Coercion]) +isNatRel tcs givensTyConSubst ty0 + | EqPred NomEq x y <- classifyPredType ty0 + = if + -- (expr1 :: Nat) ~ (expr2 :: Nat) + | all ( ( `eqType` natKind ) . typeKind ) [ x, y ] + -> Just $ ( ( ( x, y ), Nothing ), [] ) + -- (b :: Bool) ~ y + | Just ( b, cos1 ) <- boolean_maybe givensTyConSubst x + -> second ( ++ cos1 ) <$> booleanRel b y + -- x ~ (b :: Bool) + | Just ( b, cos1 ) <- boolean_maybe givensTyConSubst y + -> second ( ++ cos1 ) <$> booleanRel b x + | Just ( o, cos1 ) <- ordering_maybe givensTyConSubst x + -- (o :: Ordering) ~ y + -> second ( ++ cos1 ) <$> orderingRel o y + | Just ( o, cos1 ) <- ordering_maybe givensTyConSubst y + -- x ~ (o :: Ordering) + -> second ( ++ cos1 ) <$> orderingRel o x + -- (() :: Constraint) ~ y + | Just ( (), cos1 ) <- unitCTuple_maybe givensTyConSubst x + -> second ( ++ cos1 ) <$> goTy y + -- x ~ (() :: Constraint) + | Just ( (), cos1 ) <- unitCTuple_maybe givensTyConSubst y + -> second ( ++ cos1 ) <$> goTy x + | otherwise + -> Nothing + | otherwise + = goTy ty0 + where + goTy :: PredType -> Maybe (Relation, [Coercion]) + goTy = upToGivens givensTyConSubst goTc + + goTc :: TyCon -> [Type] -> Maybe (Relation, [Coercion]) + goTc _tc _tys +#if MIN_VERSION_ghc(9,3,0) + -- Look through 'Assert'. + -- Case 4 in Note [Recognising Nat inequalities] + | _tc == assertTyCon tcs + , [ty, _] <- _tys + = booleanRel True ty +#endif + | otherwise + = Nothing + + -- Recognise whether @(b :: Bool) ~ ty@ is an equality/inequality + booleanRel :: Bool -> Type -> Maybe (Relation, [Coercion]) + booleanRel b = upToGivens givensTyConSubst (goBoolean b) + + goBoolean :: Bool -> TyCon -> [Type] -> Maybe (Relation, [Coercion]) + goBoolean b tc tys +#if MIN_VERSION_ghc(9,1,0) + -- OrdCond (CmpNat x y) lt eq gt ~ b + -- Case 3 in Note [Recognising Nat inequalities] + | tc == ordCondTyCon tcs + , [_,cmp,ltTy,eqTy,gtTy] <- tys + , Just (lt, cos1) <- boolean_maybe givensTyConSubst ltTy + , Just (eq, cos2) <- boolean_maybe givensTyConSubst eqTy + , Just (gt, cos3) <- boolean_maybe givensTyConSubst gtTy + , Just ((x,y), cos4) <- cmpNat_maybe tcs givensTyConSubst cmp + = ( , cos1 ++ cos2 ++ cos3 ++ cos4 ) <$> + if -- (x <= y) ~ b + | lt && eq && not gt + -> Just ((x,y), Just b) + -- (x < y) ~ b + -- <=> + -- (y <= x) ~ not b + | lt && not eq && not gt + -> Just ((y,x), Just $ not b) + -- (x >= y) ~ b + -- <=> + -- (y <= x) ~ b + | not lt && eq && gt + -> Just ((y,x), Just b) + -- (x > y) ~ b + -- <=> + -- (x <= y) ~ not b + | not lt && not eq && gt + -> Just ((x,y), Just $ not b) + -- x ~ y + | ( b && not lt && eq && not gt ) + || ( not b && lt && not eq && gt ) + -> Just ((x,y), Nothing) + | otherwise + -> Nothing +#else + -- (x <=? y) ~ b + -- Case 2 in Note [Recognising Nat inequalities] + | tc == leqQNatTyCon tcs + , [x,y] <- tys + = Just (((x,y), Just b), []) +#endif + | otherwise + = Nothing + + -- Recognise whether @(o :: Ordering) ~ ty@ is an equality/inequality + orderingRel :: Ordering -> Type -> Maybe (Relation, [Coercion]) + orderingRel o = upToGivens givensTyConSubst (goOrdering o) + + goOrdering :: Ordering -> TyCon -> [Type] -> Maybe (Relation, [Coercion]) + goOrdering o tc tys + -- CmpNat x y ~ o + -- Case 1 in Note [Recognising Nat inequalities] + | tc == cmpNatTyCon tcs + , [x,y] <- tys + = ( , [] ) <$> + case o of + EQ -> + -- x ~ y + Just ((x,y), Nothing) + LT -> + -- x < y <=> (y <= x) ~ False + Just ((y,x), Just False) + GT -> + -- x > y <=> (x <= y) ~ False + Just ((x,y), Just False) + | otherwise + = Nothing + +upToGivens :: TyConSubst -> (TyCon -> [Type] -> Maybe (a, [Coercion])) -> Type -> Maybe (a, [Coercion]) +upToGivens givensTyConSubst f ty = + asum $ map ( \ (tc, tys, deps) -> second ( deps ++ ) <$> f tc tys ) $ + maybe [] NE.toList $ splitTyConApp_upTo givensTyConSubst ty + +-------------------------------------------------------------------------------- + +#if !MIN_VERSION_ghc(9,7,0) + +newtype UniqMap k a = UniqMap ( UniqFM k (k, a) ) + deriving (Eq, Functor) +type role UniqMap nominal representational + +intersectUniqMap_C :: (a -> b -> c) -> UniqMap k a -> UniqMap k b -> UniqMap k c +intersectUniqMap_C f (UniqMap m1) (UniqMap m2) = UniqMap $ intersectUFM_C (\(k, a) (_, b) -> (k, f a b)) m1 m2 +{-# INLINE intersectUniqMap_C #-} + +listToUniqMap :: Uniquable k => [(k,a)] -> UniqMap k a +listToUniqMap kvs = UniqMap (listToUFM [ (k,(k,v)) | (k,v) <- kvs]) +{-# INLINE listToUniqMap #-} + +nonDetUniqMapToList :: UniqMap k a -> [(k, a)] +nonDetUniqMapToList (UniqMap m) = nonDetEltsUFM m +{-# INLINE nonDetUniqMapToList #-} + +#endif + +-------------------------------------------------------------------------------- + +mkTcPluginSolveResult :: [Ct] -> [(EvTerm, Ct)] -> [Ct] + -> TcPluginSolveResult +#if MIN_VERSION_ghc(9,3,0) +mkTcPluginSolveResult = TcPluginSolveResult +#else +mkTcPluginSolveResult contras solved new = + -- On GHC 9.2 and below, it's not possible to return + -- both contradictions and solved/new constraints. + -- + -- In general, we prefer returning solved constraints over contradictions. + if null solved && not (null contras) + then TcPluginContradiction contras + else TcPluginOk solved new +#endif + +-------------------------------------------------------------------------------- diff --git a/src/GHC/TypeLits/Normalise/SOP.hs b/src/GHC/TypeLits/Normalise/SOP.hs --- a/src/GHC/TypeLits/Normalise/SOP.hs +++ b/src/GHC/TypeLits/Normalise/SOP.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE LambdaCase #-} {-| Copyright : (C) 2015-2016, University of Twente, 2017 , QBayLogic B.V. @@ -74,8 +75,6 @@ @ -} -{-# LANGUAGE CPP #-} - module GHC.TypeLits.Normalise.SOP ( -- * SOP types Symbol (..) @@ -92,17 +91,18 @@ ) where --- External -import Data.Either (partitionEithers) -import Data.List (sort) +-- base +import Data.Either + ( partitionEithers ) +import Data.List + ( sort ) --- GHC API -#if MIN_VERSION_ghc(9,0,0) -import GHC.Utils.Outputable (Outputable (..), (<+>), text, hcat, integer, punctuate) -#else -import Outputable (Outputable (..), (<+>), text, hcat, integer, punctuate) -#endif +-- ghc-tcplugin-api +import GHC.Utils.Outputable + ( Outputable (..), (<+>), text, hcat, integer, punctuate ) +-------------------------------------------------------------------------------- + data Symbol v c = I Integer -- ^ Integer constant | C c -- ^ Non-integer constant @@ -128,7 +128,8 @@ (S ps1) == (S ps2) = ps1 == ps2 instance (Outputable v, Outputable c) => Outputable (SOP v c) where - ppr = hcat . punctuate (text " + ") . map ppr . unS + ppr (S []) = integer 0 + ppr (S s) = hcat . punctuate (text " + ") . map ppr $ s instance (Outputable v, Outputable c) => Outputable (Product v c) where ppr = hcat . punctuate (text " * ") . map ppr . unP @@ -160,7 +161,7 @@ -- 2^3 ==> 8 -- (k ^ i) ^ j ==> k ^ (i * j) -- @ -reduceExp :: (Ord v, Ord c) => Symbol v c -> Symbol v c +reduceExp :: (Outputable v, Outputable c, Ord v, Ord c) => Symbol v c -> Symbol v c reduceExp (E _ (P [(I 0)])) = I 1 -- x^0 ==> 1 reduceExp (E (S [P [I 0]]) _ ) = I 0 -- 0^x ==> 0 reduceExp (E (S [P [(I i)]]) (P [(I j)])) @@ -189,7 +190,7 @@ -- x^4 * x ==> x^5 -- y*y ==> y^2 -- @ -mergeS :: (Ord v, Ord c) => Symbol v c -> Symbol v c +mergeS :: (Outputable v, Outputable c, Ord v, Ord c) => Symbol v c -> Symbol v c -> Either (Symbol v c) (Symbol v c) mergeS (I i) (I j) = Left (I (i * j)) -- 8 * 7 ==> 56 mergeS (I 1) r = Left r -- 1 * x ==> x @@ -245,7 +246,8 @@ -- xy + 2xy ==> 3xy -- xy + xy ==> 2xy -- @ -mergeP :: (Eq v, Eq c) => Product v c -> Product v c +mergeP :: (Eq v, Eq c, Outputable v, Outputable c) + => Product v c -> Product v c -> Either (Product v c) (Product v c) -- 2xy + 3xy ==> 5xy mergeP (P ((I i):is)) (P ((I j):js)) @@ -272,7 +274,7 @@ -- (x + 2)^(2x) ==> (x^2 + 4xy + 4)^x -- (x + 2)^(y + 2) ==> 4x(2 + x)^y + 4(2 + x)^y + (2 + x)^yx^2 -- @ -normaliseExp :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c +normaliseExp :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c -- b^1 ==> b normaliseExp b (S [P [I 1]]) = b @@ -296,7 +298,7 @@ normaliseExp b (S [e]) = S [P [reduceExp (E b e)]] -- (x + 2)^(y + 2) ==> 4x(2 + x)^y + 4(2 + x)^y + (2 + x)^yx^2 -normaliseExp b (S e) = foldr1 mergeSOPMul (map (normaliseExp b . S . (:[])) e) +normaliseExp b (S es) = foldr1 mergeSOPMul (map (normaliseExp b . S . (:[])) es) zeroP :: Product v c -> Bool zeroP (P ((I 0):_)) = True @@ -311,7 +313,7 @@ -- * 'mergeS' -- * 'mergeP' -- * 'reduceExp' -simplifySOP :: (Ord v, Ord c) => SOP v c -> SOP v c +simplifySOP :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c simplifySOP = repeatF go where go = mkNonEmpty @@ -329,12 +331,12 @@ {-# INLINEABLE simplifySOP #-} -- | Merge two SOP terms by additions -mergeSOPAdd :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c +mergeSOPAdd :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c mergeSOPAdd (S sop1) (S sop2) = simplifySOP $ S (sop1 ++ sop2) {-# INLINEABLE mergeSOPAdd #-} -- | Merge two SOP terms by multiplication -mergeSOPMul :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c +mergeSOPMul :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c mergeSOPMul (S sop1) (S sop2) = simplifySOP . S diff --git a/src/GHC/TypeLits/Normalise/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs --- a/src/GHC/TypeLits/Normalise/Unify.hs +++ b/src/GHC/TypeLits/Normalise/Unify.hs @@ -5,15 +5,14 @@ Maintainer : Christiaan Baaij -} -{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TupleSections #-} -{-# OPTIONS_GHC -fno-warn-unused-imports #-} -#if __GLASGOW_HASKELL__ < 801 -#define nonDetCmpType cmpType -#endif +{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-} module GHC.TypeLits.Normalise.Unify ( -- * 'Nat' expressions \<-\> 'SOP' terms @@ -38,90 +37,60 @@ , subtractIneq , solveIneq , ineqToSubst - , subtractionToPred , instantSolveIneq , solvedInEqSmallestConstraint + , negateProd -- * Properties , isNatural ) where --- External -import Control.Arrow (first, second) -import Control.Monad.Trans.Writer.Strict -import Data.Function (on) -import Data.List ((\\), intersect, nub) -import Data.Maybe (fromMaybe, mapMaybe, isJust) -import Data.Set (Set) -import qualified Data.Set as Set +-- base +import Control.Arrow + ( first, second ) +import Control.Monad + ( guard, zipWithM ) +import Data.Either + ( partitionEithers ) +import Data.List + ( (\\), intersect, nub, sort ) +import Data.Maybe + ( fromMaybe, mapMaybe, isJust ) +import GHC.Base + ( (==#), isTrue# ) +import GHC.Integer + ( smallInteger ) +import GHC.Integer.Logarithms + ( integerLogBase# ) -import GHC.Base (isTrue#,(==#)) -import GHC.Integer (smallInteger) -import GHC.Integer.Logarithms (integerLogBase#) +-- containers +import Data.Set + ( Set ) +import qualified Data.Set as Set --- GHC API -#if MIN_VERSION_ghc(9,0,0) -import GHC.Builtin.Types (boolTy, promotedTrueDataCon) +-- ghc import GHC.Builtin.Types.Literals - (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon) -#if MIN_VERSION_ghc(9,2,0) -import GHC.Builtin.Types (naturalTy, promotedFalseDataCon) -import GHC.Builtin.Types.Literals (typeNatCmpTyCon) -#else -import GHC.Builtin.Types (typeNatKind) -import GHC.Builtin.Types.Literals (typeNatLeqTyCon) -#endif -import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType, mkPrimEqPred) -import GHC.Core.TyCon (TyCon) -#if MIN_VERSION_ghc(9,6,0) -import GHC.Core.Type - (PredType, TyVar, coreView, mkNumLitTy, mkTyConApp, mkTyVarTy, typeKind) -import GHC.Core.TyCo.Compare - (eqType, nonDetCmpType) -#else -import GHC.Core.Type - (PredType, TyVar, coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy, nonDetCmpType, typeKind) -#endif -import GHC.Core.TyCo.Rep (Kind, Type (..), TyLit (..)) -import GHC.Tc.Plugin (TcPluginM, tcPluginTrace) -import GHC.Tc.Types.Constraint (Ct, ctEvidence, ctEvId, ctEvPred, isGiven) + ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon + ) import GHC.Types.Unique.Set - (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets, unitUniqSet) -import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text) -#else -import Outputable (Outputable (..), (<+>), ($$), text) -import TcPluginM (TcPluginM, tcPluginTrace) -import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, - typeNatSubTyCon, typeNatLeqTyCon) -import TyCon (TyCon) -import Type (TyVar, - coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy, - nonDetCmpType, PredType, typeKind) -import TyCoRep (Kind, Type (..), TyLit (..)) -import TysWiredIn (boolTy, promotedTrueDataCon, typeNatKind) -import UniqSet (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets, - unitUniqSet) + ( UniqSet + , emptyUniqSet, unionManyUniqSets, unionUniqSets, unitUniqSet + , nonDetEltsUniqSet, elementOfUniqSet + ) -#if MIN_VERSION_ghc(8,10,0) -import Constraint (Ct, ctEvidence, ctEvId, ctEvPred, isGiven) -import Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType, mkPrimEqPred) -#else -import TcRnMonad (Ct, ctEvidence, isGiven) -import TcRnTypes (ctEvPred) -import Type (EqRel (NomEq), PredTree (EqPred), classifyPredType, mkPrimEqPred) -#endif -#endif +-- ghc-tcplugin-api +import GHC.TcPlugin.API +import GHC.Utils.Outputable --- Internal + +-- ghc-typelits-natnormalise import GHC.TypeLits.Normalise.SOP --- Used for haddock -import GHC.TypeLits (Nat) +-- transformers +import Control.Monad.Trans.Writer.Strict + ( Writer, WriterT(..), runWriter, tell ) -#if MIN_VERSION_ghc(9,2,0) -typeNatKind :: Type -typeNatKind = naturalTy -#endif +-------------------------------------------------------------------------------- newtype CType = CType { unCType :: Type } deriving Outputable @@ -137,27 +106,46 @@ type CoreProduct = Product TyVar CType type CoreSymbol = Symbol TyVar CType --- | Convert a type of /kind/ 'GHC.TypeLits.Nat' to an 'SOP' term, but --- only when the type is constructed out of: --- --- * literals --- * type variables --- * Applications of the arithmetic operators @(+,-,*,^)@ -normaliseNat :: Type -> Writer [(Type,Type)] CoreSOP -normaliseNat ty | Just ty1 <- coreView ty = normaliseNat ty1 -normaliseNat (TyVarTy v) = return (S [P [V v]]) -normaliseNat (LitTy (NumTyLit i)) = return (S [P [I i]]) -normaliseNat (TyConApp tc [x,y]) - | tc == typeNatAddTyCon = mergeSOPAdd <$> normaliseNat x <*> normaliseNat y - | tc == typeNatSubTyCon = do - tell [(x,y)] - mergeSOPAdd <$> normaliseNat x - <*> (mergeSOPMul (S [P [I (-1)]]) <$> normaliseNat y) - | tc == typeNatMulTyCon = mergeSOPMul <$> normaliseNat x <*> normaliseNat y - | tc == typeNatExpTyCon = normaliseExp <$> normaliseNat x <*> normaliseNat y -normaliseNat t = return (S [P [C (CType t)]]) +-- | Convert a type of /kind/ 'GHC.TypeLits.Nat' to an 'SOP' term +normaliseNat :: Type -> Writer [(Type,Type)] (CoreSOP, [Coercion]) +normaliseNat ty + | Just (tc, xs) <- splitTyConApp_maybe ty + = goTyConApp tc xs + | Just i <- isNumLitTy ty + = return (S [P [I i]], []) + | Just v <- getTyVar_maybe ty + = return (S [P [V v]], []) + | otherwise + = return (S [P [C (CType ty)]], []) + where + goTyConApp :: TyCon -> [Type] -> Writer [(Type,Type)] (CoreSOP, [Coercion]) + goTyConApp tc [x,y] + | tc == typeNatAddTyCon = + do (x', cos1) <- normaliseNat x + (y', cos2) <- normaliseNat y + return (mergeSOPAdd x' y', cos1 ++ cos2) + | tc == typeNatSubTyCon = do + (x', cos1) <- normaliseNat x + (y', cos2) <- normaliseNat y + tell [(reifySOP $ simplifySOP x', reifySOP $ simplifySOP y')] + return (mergeSOPAdd x' (mergeSOPMul (S [P [I (-1)]]) y'), cos1 ++ cos2) + | tc == typeNatMulTyCon = + do (x', cos1) <- normaliseNat x + (y', cos2) <- normaliseNat y + return (mergeSOPMul x' y', cos1 ++ cos2) + | tc == typeNatExpTyCon = + do (x', cos1) <- normaliseNat x + (y', cos2) <- normaliseNat y + return (normaliseExp x' y', cos1 ++ cos2) + goTyConApp tc xs + = do (xs', cos') <- fmap unzip (traverse normaliseSimplifyNat xs) + return (S [P [C (CType (mkTyConApp tc xs'))]], concat cos') --- | Runs writer action. If the result /Nothing/ writer actions will be +knownTyCons :: [TyCon] +knownTyCons = [typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon, typeNatAddTyCon] + + +-- | Runs writer action. If the result is /Nothing/, writer actions will be -- discarded. maybeRunWriter :: Monoid a @@ -171,43 +159,55 @@ -- | Applies 'normaliseNat' and 'simplifySOP' to type or predicates to reduce -- any occurrences of sub-terms of /kind/ 'GHC.TypeLits.Nat'. If the result is -- the same as input, returns @'Nothing'@. -normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe Type) +normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion])) normaliseNatEverywhere ty0 - | TyConApp tc _fields <- ty0 - , tc `elem` knownTyCons = do - -- Normalize under current type constructor application. 'go' skips all - -- known type constructors. - ty1M <- maybeRunWriter (go ty0) - let ty1 = fromMaybe ty0 ty1M + | Just (tc, fields) <- splitTyConApp_maybe ty0 + = if tc `elem` knownTyCons + then do + -- Normalize under current type constructor application. 'go' skips all + -- known type constructors. + ty1M <- maybeRunWriter (go tc fields) + let (ty1, cos1) = fromMaybe (ty0, []) ty1M + -- Normalize (subterm-normalized) type given to 'normaliseNatEverywhere' + (ty2, cos2) <- normaliseSimplifyNat ty1 + -- TODO: 'normaliseNat' could keep track whether it changed anything. That's + -- TODO: probably cheaper than checking for equality here. + pure $ + if ty2 `eqType` ty1 + then second (cos1 ++) <$> ty1M + else Just (ty2, cos1 ++ cos2) + else + go tc fields - -- Normalize (subterm-normalized) type given to 'normaliseNatEverywhere' - ty2 <- normaliseSimplifyNat ty1 - -- TODO: 'normaliseNat' could keep track whether it changed anything. That's - -- TODO: probably cheaper than checking for equality here. - pure (if ty2 `eqType` ty1 then ty1M else Just ty2) - | otherwise = go ty0 + | otherwise + = pure Nothing where - knownTyCons :: [TyCon] - knownTyCons = [typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon, typeNatAddTyCon] -- Normalize given type, but ignore all top-level - go :: Type -> Writer [(Type, Type)] (Maybe Type) - go (TyConApp tc_ fields0_) = do + go :: TyCon -> [Type] -> Writer [(Type, Type)] (Maybe (Type, [Coercion])) + go tc_ fields0_ = do fields1_ <- mapM (maybeRunWriter . cont) fields0_ - if any isJust fields1_ then - pure (Just (TyConApp tc_ (zipWith fromMaybe fields0_ fields1_))) + if any isJust fields1_ + then do + let cos' = concat $ mapMaybe (fmap snd) fields1_ + ty' = mkTyConApp tc_ (zipWith (\ f0 f1 -> maybe f0 fst f1) fields0_ fields1_) + pure (Just (ty', cos')) else pure Nothing where - cont = if tc_ `elem` knownTyCons then go else normaliseNatEverywhere - go _ = pure Nothing + cont ty' + | tc_ `elem` knownTyCons + , Just (tc', flds') <- splitTyConApp_maybe ty' + = go tc' flds' + | otherwise + = normaliseNatEverywhere ty' -normaliseSimplifyNat :: Type -> Writer [(Type, Type)] Type +normaliseSimplifyNat :: Type -> Writer [(Type, Type)] (Type, [Coercion]) normaliseSimplifyNat ty - | typeKind ty `eqType` typeNatKind = do - ty' <- normaliseNat ty - return $ reifySOP $ simplifySOP ty' - | otherwise = return ty + | typeKind ty `eqType` natKind = do + (ty', cos1) <- normaliseNat ty + return $ (reifySOP $ simplifySOP ty', cos1) + | otherwise = return (ty, []) -- | Convert a 'SOP' term back to a type of /kind/ 'GHC.TypeLits.Nat' reifySOP :: CoreSOP -> Type @@ -257,11 +257,26 @@ -- at the "2 ^ -1" because of the negative exponent. mergeExp :: CoreSymbol -> [Either CoreSymbol (CoreSOP,[CoreProduct])] -> [Either CoreSymbol (CoreSOP,[CoreProduct])] - mergeExp (E s p) [] = [Right (s,[p])] + mergeExp (E (S [P [I 1]]) _) ys = ys + mergeExp (E s p) [] = [Right (s,[p])] + mergeExp (E (S [P [I s1]]) p1) (y:ys) + | Right ((S [P [I s2]]), p2s) <- y + , let s = gcd s1 s2 + t1 = s1 `quot` s + t2 = s2 `quot` s + , s > 1 + -- Deal with e.g. "2 ^ -1 * 6 ^ x", where the bases differ. + -- + -- (s * t1) ^ p1 * (s * t2) ^ (p2 + ...) * rest + -- ===> + -- s ^ (p1 + p2 + ...) * t1 ^ p1 * t2 ^ (p2 + ..) * rest + = Right (S [P [I s]], (p1:p2s)) : + mergeExp (E (S [P [I t1]]) p1) + (Right ((S [P [I t2]]), p2s):ys) mergeExp (E s1 p1) (y:ys) - | Right (s2,p2) <- y + | Right (s2,p2s) <- y , s1 == s2 - = Right (s1,(p1:p2)) : ys + = Right (s1,(p1:p2s)) : ys | otherwise = Right (s1,[p1]) : y : ys mergeExp x ys = Left x : ys @@ -276,43 +291,68 @@ ,reifySOP (S s2) ] +-- | Simplify an inequality by first calling 'subtractIneq', producing a SOP +-- term, and then creating a new inequality by moving all the terms with +-- negative coefficients to one side. +-- +-- Returns 'Nothing' if it is not able to simplify the original inequality. +simplifyIneq :: Ineq -> Maybe Ineq +simplifyIneq ineq@(x, y, isLE) + = if x' == x && y' == y + then Nothing + else Just (x', y', isLE) + where + S ps = subtractIneq ineq + -- We need to sort the products in order to retain our canonical form, + -- not sorting would result in the following rewrite: + -- + -- 2 * a + b ~ 5 ==> + -- 5 + -1 * b + -2 * a ==> + -- b + 2 * a ~ 5 + -- + -- Which lead to issue #113 + (sort -> neg, sort -> pos) = partitionEithers $ map classify ps + (x', y') = + if isLE + then ( S neg, S pos ) + else ( S pos, S neg ) + classify :: CoreProduct -> Either CoreProduct CoreProduct + classify p@(P (I i : _)) + | i < 0 + = Left $ negateProd p + classify prod + = Right prod + +negateProd :: CoreProduct -> CoreProduct +negateProd (P (I i : r)) = + -- preserve normal form + if i == (-1) + then + if null r + then P [I 1] + else P r + else P $ I (negate i) : r +negateProd (P r) = P $ I (-1) : r + -- | Subtract an inequality, in order to either: -- -- * See if the smallest solution is a natural number -- * Cancel sums, i.e. monotonicity of addition -- -- @ --- subtractIneq (2*y <=? 3*x ~ True) = (-2*y + 3*x) --- subtractIneq (2*y <=? 3*x ~ False) = (-3*x + (-1) + 2*y) +-- subtractIneq (2*y <=? 3*x ~ True) = 3*x + (-2)*y +-- subtractIneq (2*y <=? 3*x ~ False) = -3*x + (-2)*y -- @ subtractIneq :: (CoreSOP, CoreSOP, Bool) -> CoreSOP subtractIneq (x,y,isLE) | isLE - = mergeSOPAdd y (mergeSOPMul (S [P [I (-1)]]) x) + -- NB: keep orientations + = mergeSOPAdd (mergeSOPMul (S [P [I (-1)]]) x) y | otherwise = mergeSOPAdd x (mergeSOPMul (S [P [I (-1)]]) (mergeSOPAdd y (S [P [I 1]]))) --- | Try to reverse the process of 'subtractIneq' --- --- E.g. --- --- @ --- subtractIneq (2*y <=? 3*x ~ True) = (-2*y + 3*x) --- sopToIneq (-2*y+3*x) = Just (2*x <=? 3*x ~ True) --- @ -sopToIneq - :: CoreSOP - -> Maybe Ineq -sopToIneq (S [P ((I i):l),r]) - | i < 0 - = Just (mergeSOPMul (S [P [I (negate i)]]) (S [P l]),S [r],True) -sopToIneq (S [r,P ((I i:l))]) - | i < 0 - = Just (mergeSOPMul (S [P [I (negate i)]]) (S [P l]),S [r],True) -sopToIneq _ = Nothing - -- | Give the smallest solution for an inequality ineqToSubst :: Ineq @@ -322,25 +362,6 @@ ineqToSubst _ = Nothing -subtractionToPred - :: TyCon - -> (Type,Type) - -> (PredType, Kind) -subtractionToPred ordCond (x,y) = -#if MIN_VERSION_ghc(9,2,0) - let cmpNat = mkTyConApp typeNatCmpTyCon [y,x] - trueTc = mkTyConApp promotedTrueDataCon [] - falseTc = mkTyConApp promotedFalseDataCon [] - ordCmp = mkTyConApp ordCond - [boolTy,cmpNat,trueTc,trueTc,falseTc] - predTy = mkPrimEqPred ordCmp trueTc - in (predTy,boolTy) -#else - (mkPrimEqPred (mkTyConApp ordCond [y,x]) - (mkTyConApp promotedTrueDataCon []) - ,boolTy) -#endif - -- | A substitution is essentially a list of (variable, 'SOP') pairs, -- but we keep the original 'Ct' that lead to the substitution being -- made, for use when turning the substitution back into constraints. @@ -359,18 +380,18 @@ ppr (UnifyItem {..}) = ppr siLHS <+> text " :~ " <+> ppr siRHS -- | Apply a substitution to a single normalised 'SOP' term -substsSOP :: (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c +substsSOP :: (Outputable v, Outputable c, Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c substsSOP [] u = u substsSOP ((SubstItem {..}):s) u = substsSOP s (substSOP siVar siSOP u) substsSOP ((UnifyItem {}):s) u = substsSOP s u -substSOP :: (Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c -substSOP tv e = foldr1 mergeSOPAdd . map (substProduct tv e) . unS +substSOP :: (Outputable v, Outputable c, Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c +substSOP tv e = foldr mergeSOPAdd (S []) . map (substProduct tv e) . unS -substProduct :: (Ord v, Ord c) => v -> SOP v c -> Product v c -> SOP v c +substProduct :: (Outputable v, Outputable c, Ord v, Ord c) => v -> SOP v c -> Product v c -> SOP v c substProduct tv e = foldr1 mergeSOPMul . map (substSymbol tv e) . unP -substSymbol :: (Ord v, Ord c) => v -> SOP v c -> Symbol v c -> SOP v c +substSymbol :: (Outputable v, Outputable c, Ord v, Ord c) => v -> SOP v c -> Symbol v c -> SOP v c substSymbol _ _ s@(I _) = S [P [s]] substSymbol _ _ s@(C _) = S [P [s]] substSymbol tv e (V tv') @@ -379,7 +400,7 @@ substSymbol tv e (E s p) = normaliseExp (substSOP tv e s) (substProduct tv e p) -- | Apply a substitution to a substitution -substsSubst :: (Ord v, Ord c) => [UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c] +substsSubst :: (Outputable v, Outputable c, Ord v, Ord c) => [UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c] substsSubst s = map subt where subt si@(SubstItem {..}) = si {siSOP = substsSOP s siSOP} @@ -402,28 +423,33 @@ -- same, then we 'Win' if @u@ and @v@ are equal, and 'Lose' otherwise. -- -- If @u@ and @v@ do not have the same free variables, we result in a 'Draw', --- ware @u@ and @v@ are only equal when the returned 'CoreSubst' holds. -unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult +-- where @u@ and @v@ are only equal when the returned 'CoreSubst' holds. +unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM Solve UnifyResult unifyNats ct u v = do tcPluginTrace "unifyNats" (ppr ct $$ ppr u $$ ppr v) return (unifyNats' ct u v) unifyNats' :: Ct -> CoreSOP -> CoreSOP -> UnifyResult unifyNats' ct u v - = if eqFV u v - then if containsConstants u || containsConstants v - then if u == v - then Win - else Draw (filter diffFromConstraint (unifiers ct u v)) - else if u == v - then Win - else Lose - else Draw (filter diffFromConstraint (unifiers ct u v)) + | u == v + = Win + | Just unifs <- unifiers ct u v + , let newUnifs = if isGiven (ctEvidence ct) + then unifs + else filter diffFromConstraint unifs + = Draw newUnifs + | otherwise + = Lose where - -- A unifier is only a unifier if differs from the original constraint + + -- A unifier is only a unifier if it differs from the original constraint diffFromConstraint (UnifyItem x y) = not (x == u && y == v) - diffFromConstraint _ = True + -- SubstItems can be in different orders + diffFromConstraint (SubstItem x y) = + not $ (S [P [V x]] == u && y == v) + || (S [P [V x]] == v && y == u) + -- | Find unifiers for two SOP terms -- -- Can find the following unifiers: @@ -457,39 +483,40 @@ -- @ -- [a := b] -- @ -unifiers :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify] +unifiers :: Ct -> CoreSOP -> CoreSOP -> Maybe [CoreUnify] unifiers ct u@(S [P [V x]]) v - = case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 _ - | CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct) -> [SubstItem x v] - _ -> [] + | EqPred NomEq t1 _ <- classifyPredType $ ctEvPred $ ctEvidence ct + , CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct) + = return [SubstItem x v] unifiers ct u v@(S [P [V x]]) - = case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq _ t2 - | CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct) -> [SubstItem x u] - _ -> [] + | EqPred NomEq _ t2 <- classifyPredType $ ctEvPred $ ctEvidence ct + , CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct) + = return [SubstItem x u] unifiers ct u@(S [P [C _]]) v - = case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 t2 - | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 -> [UnifyItem u v] - _ -> [] + | EqPred NomEq t1 t2 <- classifyPredType $ ctEvPred $ ctEvidence ct + , CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 + = return [UnifyItem u v] unifiers ct u v@(S [P [C _]]) - = case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 t2 - | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 -> [UnifyItem u v] - _ -> [] + | EqPred NomEq t1 t2 <- classifyPredType $ ctEvPred $ ctEvidence ct + , CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 + = return [UnifyItem u v] unifiers ct u v = unifiers' ct u v -unifiers' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify] -unifiers' _ct (S [P [V x]]) (S []) = [SubstItem x (S [P [I 0]])] -unifiers' _ct (S []) (S [P [V x]]) = [SubstItem x (S [P [I 0]])] - -unifiers' _ct (S [P [V x]]) s = [SubstItem x s] -unifiers' _ct s (S [P [V x]]) = [SubstItem x s] +unifiers' :: Ct -> CoreSOP -> CoreSOP -> Maybe [CoreUnify] +unifiers' _ct (S []) (S []) = return [] -unifiers' _ct s1@(S [P [C _]]) s2 = [UnifyItem s1 s2] -unifiers' _ct s1 s2@(S [P [C _]]) = [UnifyItem s1 s2] +unifiers' _ct (S [P [V x]]) (S []) = return [SubstItem x (S [P [I 0]])] +unifiers' _ct (S []) (S [P [V x]]) = return [SubstItem x (S [P [I 0]])] +unifiers' _ct (S [P [V x]]) s = do + guard $ canBeNatural s + return [SubstItem x s] +unifiers' _ct s (S [P [V x]]) = do + guard $ canBeNatural s + return [SubstItem x s] +unifiers' _ct s1@(S [P [C {}]]) s2@(S [P [C {}]]) + | s1 == s2 + = return [] -- (z ^ a) ~ (z ^ b) ==> [a := b] unifiers' ct (S [P [E s1 p1]]) (S [P [E s2 p2]]) @@ -500,56 +527,54 @@ | all (`elem` p2) s1 = let base = intersect s1 p2 diff = p2 \\ s1 - in unifiers ct (S [P diff]) (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) + in unifiers' ct (S [P diff]) (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) unifiers' ct (S [P p2]) (S [P [E (S [P s1]) p1]]) | all (`elem` p2) s1 = let base = intersect s1 p2 diff = p2 \\ s1 - in unifiers ct (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) (S [P diff]) + in unifiers' ct (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) (S [P diff]) -- (i ^ a) ~ j ==> [a := round (logBase i j)], when `i` and `j` are integers, -- and `ceiling (logBase i j) == floor (logBase i j)` unifiers' ct (S [P [E (S [P [I i]]) p]]) (S [P [I j]]) - = case integerLogBase i j of - Just k -> unifiers' ct (S [p]) (S [P [I k]]) - Nothing -> [] + | Just k <- integerLogBase i j + = unifiers' ct (S [p]) (S [P [I k]]) unifiers' ct (S [P [I j]]) (S [P [E (S [P [I i]]) p]]) - = case integerLogBase i j of - Just k -> unifiers' ct (S [p]) (S [P [I k]]) - Nothing -> [] + | Just k <- integerLogBase i j + = unifiers' ct (S [p]) (S [P [I k]]) -- a^d * a^e ~ a^c ==> [c := d + e] -unifiers' ct (S [P [E s1 p1]]) (S [p2]) = case collectBases p2 of - Just (b:bs,ps) | all (== s1) (b:bs) -> - unifiers' ct (S [p1]) (S ps) - _ -> [] +unifiers' ct (S [P [E s1 p1]]) (S [p2]) + | Just (b:bs,ps) <- collectBases p2 + , all (== s1) (b:bs) + = unifiers' ct (S [p1]) (S ps) -unifiers' ct (S [p2]) (S [P [E s1 p1]]) = case collectBases p2 of - Just (b:bs,ps) | all (== s1) (b:bs) -> - unifiers' ct (S ps) (S [p1]) - _ -> [] +unifiers' ct (S [p2]) (S [P [E s1 p1]]) + | Just (b:bs,ps) <- collectBases p2 + , all (== s1) (b:bs) + = unifiers' ct (S ps) (S [p1]) -- (i * a) ~ j ==> [a := div j i] -- Where 'a' is a variable, 'i' and 'j' are integer literals, and j `mod` i == 0 -unifiers' ct (S [P ((I i):ps)]) (S [P [I j]]) = - case safeDiv j i of - Just k -> unifiers' ct (S [P ps]) (S [P [I k]]) - _ -> [] +unifiers' ct (S [P ((I i):ps)]) (S [P [I j]]) + | Just k <- safeDiv j i + , not (null ps) + = unifiers' ct (S [P ps]) (S [P [I k]]) -unifiers' ct (S [P [I j]]) (S [P ((I i):ps)]) = - case safeDiv j i of - Just k -> unifiers' ct (S [P ps]) (S [P [I k]]) - _ -> [] +unifiers' ct (S [P [I j]]) (S [P ((I i):ps)]) + | Just k <- safeDiv j i + , not (null ps) + = unifiers' ct (S [P ps]) (S [P [I k]]) -- (2*a) ~ (2*b) ==> [a := b] -- unifiers' ct (S [P (p:ps1)]) (S [P (p':ps2)]) -- | p == p' = unifiers' ct (S [P ps1]) (S [P ps2]) -- | otherwise = [] unifiers' ct (S [P ps1]) (S [P ps2]) - | null psx = [] - | otherwise = unifiers' ct (S [P ps1'']) (S [P ps2'']) + | not $ null psx + = unifiers' ct (S [P ps1'']) (S [P ps2'']) where ps1' = ps1 \\ psx ps2' = ps2 \\ psx @@ -559,32 +584,25 @@ | otherwise = ps2' psx = intersect ps1 ps2 --- (2 + a) ~ 5 ==> [a := 3] -unifiers' ct (S ((P [I i]):ps1)) (S ((P [I j]):ps2)) - | i < j = unifiers' ct (S ps1) (S ((P [I (j-i)]):ps2)) - | i > j = unifiers' ct (S ((P [I (i-j)]):ps1)) (S ps2) - -- (a + c) ~ (b + c) ==> [a := b] -unifiers' ct s1@(S ps1) s2@(S ps2) = case sopToIneq k1 of - Just (s1',s2',_) - | s1' /= s1 || s2' /= s1 - , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s1')) - , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s2')) - -> unifiers' ct s1' s2' - _ | null psx - , length ps1 == length ps2 - -> case nub (concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2)) of - [] -> unifiers'' ct (S ps1) (S ps2) - [k] | length ps1 == length ps2 -> [k] - _ -> [] - | null psx - , isGiven (ctEvidence ct) - -> unifiers'' ct (S ps1) (S ps2) - | null psx - -> [] - _ -> unifiers' ct (S ps1'') (S ps2'') +-- +-- NB: this also handles situations such as (2 + x) ~ 5 ==> [x := 3]. +unifiers' ct s1@(S ps1) s2@(S ps2) + | not $ null psx + = unifiers' ct (S ps1'') (S ps2'') + | Just (s1',s2',_) <- simplifyIneq (s1, s2, True) + = unifiers' ct s1' s2' + | Just term_unifs <- termByTerm ct ps1 ps2 + = Just term_unifs + -- If there are only two variables, try to collect them on either side. + -- This makes 'termByTerm' more likely to succeed. + | Just (S coll1, S coll2) <- partitionTerms ps1 ps2 + , Just term_unifs <- termByTerm ct coll1 coll2 + = Just term_unifs + | null psx + , isGiven (ctEvidence ct) + = unifiers'' ct (S ps1) (S ps2) where - k1 = subtractIneq (s1,s2,True) ps1' = ps1 \\ psx ps2' = ps2 \\ psx ps1'' | null ps1' = [P [I 0]] @@ -593,12 +611,86 @@ | otherwise = ps2' psx = intersect ps1 ps2 -unifiers'' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify] +-- Don't generate unify items where one of the sides is an empty sum (i.e.) zero +-- Doing so leads to poor error messages, see #114 +unifiers' _ (S []) _ = return [] +unifiers' _ _ (S []) = return [] +unifiers' _ s1 s2 = return [UnifyItem s1 s2] + +-- | Try to match the two expressions term-by-term. +-- If this produces a **single unifier**, then we succeed. +-- +-- Example: x + 3^(x+2) ~ 2*y - 3^(2*(y+1)) +-- +-- We recur on each pair, (x, 2*y), (3^(x+2),3^(2*(y+1))). +-- This produces a single unifier "x ~ 2*y", so we proceed. +-- +-- NB: this is somewhat fragile: if one moves the terms with negative +-- coefficients to the other side, due to the variable ordering x < y, +-- we would get: +-- +-- x + 3^(2*(y+1)) ~ 3^(x+2) + 2*y +-- +-- for which the same approach fails. So we use 'partitionTerms' as a heuristic +-- in the case there are only two free variables. +-- See https://github.com/clash-lang/ghc-typelits-natnormalise/issues/96. +termByTerm :: Ct -> [CoreProduct] -> [CoreProduct] -> Maybe [CoreUnify] +termByTerm ct ps1 ps2 + | length ps1 == length ps2 + , length ps1 > 1 + , Just u@[_] <- unifs + = Just u + | otherwise + = Nothing + where + unifs = fmap (nub . concat) (zipWithM (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2) + +-- | If an equality only contains two free variables, try to collect +-- terms with either FV on either side of the equality. +-- +-- This makes 'termByTerm' more likely to succeed. +partitionTerms :: [CoreProduct] -> [CoreProduct] -> Maybe (CoreSOP, CoreSOP) +partitionTerms lhs rhs + | [fv1, fv2] <- fvs + , Just (lhs1, lhs2) <- mbPairs fv1 fv2 lhs + , Just (rhs1, rhs2) <- mbPairs fv1 fv2 rhs + = Just $ + let (lhs', rhs') = + if length rhs1 + length lhs2 <= length lhs1 + length rhs2 + then (lhs1 ++ map negateProd rhs1, map negateProd lhs2 ++ rhs2) + else (map negateProd lhs1 ++ rhs1, lhs2 ++ map negateProd rhs2) + in (simplifySOP (S lhs'), simplifySOP (S rhs')) + | otherwise + = Nothing + where + fvs :: [TyVar] + fvs = nonDetEltsUniqSet $ fvSOP (S $ lhs ++ rhs) + + mbPairs :: TyVar -> TyVar -> [CoreProduct] -> Maybe ([CoreProduct], [CoreProduct]) + mbPairs fv1 fv2 x = partitionEithers <$> traverse ( collect fv1 fv2 ) x + + collect :: TyVar -> TyVar -> CoreProduct -> Maybe (Either CoreProduct CoreProduct) + collect fv1 fv2 tm = + let tmFvs = fvProduct tm + in case (fv1 `elementOfUniqSet` tmFvs, fv2 `elementOfUniqSet` tmFvs) of + (True, False) -> Just $ Left tm + (False, True) -> Just $ Right tm + _ -> Nothing + +unifiers'' :: Ct -> CoreSOP -> CoreSOP -> Maybe [CoreUnify] unifiers'' ct (S [P [I i],P [V v]]) s2 - | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate i)]]))] + | isGiven (ctEvidence ct) + , let s' = mergeSOPAdd s2 (S [P [I (negate i)]]) + = if canBeNatural s' + then Just [SubstItem v s'] + else Nothing unifiers'' ct s1 (S [P [I i],P [V v]]) - | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate i)]]))] -unifiers'' _ _ _ = [] + | isGiven (ctEvidence ct) + , let s' = mergeSOPAdd s1 (S [P [I (negate i)]]) + = if canBeNatural s' + then Just [SubstItem v s'] + else Nothing +unifiers'' _ _ _ = Just [] collectBases :: CoreProduct -> Maybe ([CoreSOP],[CoreProduct]) collectBases = fmap unzip . traverse go . unP @@ -619,18 +711,6 @@ fvSymbol (V v) = unitUniqSet v fvSymbol (E s p) = fvSOP s `unionUniqSets` fvProduct p -eqFV :: CoreSOP -> CoreSOP -> Bool -eqFV = (==) `on` fvSOP - -containsConstants :: CoreSOP -> Bool -containsConstants = - any (any symbolContainsConstant . unP) . unS - where - symbolContainsConstant c = case c of - C {} -> True - E s p -> containsConstants s || containsConstants (S [p]) - _ -> False - safeDiv :: Integer -> Integer -> Maybe Integer safeDiv i j | j == 0 = Just 0 @@ -650,12 +730,38 @@ else Just (smallInteger z1) integerLogBase _ _ = Nothing +-- | Might this be a natural number? +-- +-- Equivalently: it is not the case that this is definitely not a natural number. +-- +-- For example, @-1@ is definitely not a natural number, while @α@ or +-- @-2 * β@ could both be natural numbers (where @α, β@ are metavariables). +canBeNatural :: CoreSOP -> Bool +canBeNatural = maybe True fst . runWriterT . isNatural + +-- | Is this a natural number? +-- +-- - @Just True@ <=> definitely a natural number +-- - @Just False@ <=> definitely not a natural number +-- - @Nothing@ <=> not sure +-- +-- The 'Set CType' writer accumulator returns inner types that must also be +-- positive for the overall 'CoreSOP' to be positive. isNatural :: CoreSOP -> WriterT (Set CType) Maybe Bool isNatural (S []) = return True isNatural (S [P []]) = return True -isNatural (S [P (I i:ps)]) - | i >= 0 = isNatural (S [P ps]) - | otherwise = return False +isNatural (S [P (I i:ps)]) = + case compare i 0 of + EQ -> return True + GT -> + -- NB: assumes the SOP term has been normalised, so no possibly of + -- a second negative constant factor to cancel out this one. + isNatural (S [P ps]) + LT -> + -- '-1 * ty' can be a natural number if 'ty' ends up being zero + if any canBeZero ps + then WriterT Nothing + else return False isNatural (S [P (V _:ps)]) = isNatural (S [P ps]) isNatural (S [P (E s p:ps)]) = do sN <- isNatural s @@ -678,6 +784,23 @@ -- if one is natural and the other isn't, then their sum *might* be natural, -- but we simply cant be sure. +-- | Can this 'CoreSymbol' be zero? +-- +-- Examples: +-- +-- - the literal '0', +-- - a metavariable, +-- - a type family application. +canBeZero :: CoreSymbol -> Bool +canBeZero (I i) = i == 0 +canBeZero (C {}) = True -- e.g. 'F 3' where 'F' is a type family +canBeZero (E (S es) _) + | [P bs] <- es + = any canBeZero bs + | otherwise + = True +canBeZero (V {}) = True -- e.g. 'tau' where 'tau' is an unfilled metavariable + -- | Try to solve inequalities solveIneq :: Word @@ -797,14 +920,12 @@ -- * SOP version: -2 + x -- * Convert back to inequality: 2 <= x plusMonotone :: IneqRule -plusMonotone want have - | Just want' <- sopToIneq (subtractIneq want) - , want' /= want - = pure [(want',have)] - | Just have' <- sopToIneq (subtractIneq have) - , have' /= have - = pure [(want,have')] -plusMonotone _ _ = noRewrite +plusMonotone want have = + case (simplifyIneq want, simplifyIneq have) of + (Just want', Just have') -> pure [(want', have')] + (Just want', _ ) -> pure [(want', have )] + (_ , Just have') -> pure [(want , have')] + _ -> noRewrite -- | Make the `a` of a given `a <= b` smaller haveSmaller :: IneqRule diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs deleted file mode 100644 --- a/tests/ErrorTests.hs +++ /dev/null @@ -1,523 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} - -#if __GLASGOW_HASKELL__ >= 805 -{-# LANGUAGE NoStarIsType #-} -#endif - -{-# OPTIONS_GHC -fdefer-type-errors #-} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} -module ErrorTests where - -import Data.Proxy -import GHC.TypeLits -#if __GLASGOW_HASKELL__ >= 904 -import GHC.Types -#endif - -import GHC.IO.Encoding (getLocaleEncoding, textEncodingName, utf8) -import Language.Haskell.TH (litE, stringL) -import Language.Haskell.TH.Syntax (runIO) - -#if __GLASGOW_HASKELL__ >= 901 -import qualified Data.Type.Ord -#endif - -testProxy1 :: Proxy (x + 1) -> Proxy (2 + x) -testProxy1 = id - -testProxy1Errors = -#if __GLASGOW_HASKELL__ >= 900 - ["Expected: Proxy (x + 1) -> Proxy (2 + x)" - ," Actual: Proxy (x + 1) -> Proxy (x + 1)" - ] -#else - ["Expected type: Proxy (x + 1) -> Proxy (2 + x)" - ,"Actual type: Proxy (2 + x) -> Proxy (2 + x)" - ] -#endif - -type family GCD (x :: Nat) (y :: Nat) :: Nat -type instance GCD 6 8 = 2 -type instance GCD 9 6 = 3 - -testProxy2 :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6) -testProxy2 = id - -testProxy2Errors = -#if __GLASGOW_HASKELL__ >= 900 - ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)" - ," Actual: Proxy (2 + x) -> Proxy (2 + x)" - ] -#else - ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)" - ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)" - ] -#endif - -proxyFun3 :: Proxy (x + x + x) -> () -proxyFun3 = const () - -testProxy3 :: Proxy 8 -> () -testProxy3 = proxyFun3 - -testProxy3Errors = -#if __GLASGOW_HASKELL__ >= 900 - ["Expected: Proxy 8 -> ()" - ," Actual: Proxy ((x0 + x0) + x0) -> ()" - ] -#else - ["Expected type: Proxy 8 -> ()" - ,"Actual type: Proxy ((x0 + x0) + x0) -> ()" - ] -#endif - -proxyFun4 :: Proxy ((2*y)+4) -> () -proxyFun4 = const () - -testProxy4 :: Proxy 2 -> () -testProxy4 = proxyFun4 - -testProxy4Errors = -#if __GLASGOW_HASKELL__ >= 900 - ["Expected: Proxy 2 -> ()" - ," Actual: Proxy ((2 * y0) + 4) -> ()" - ] -#else - ["Expected type: Proxy 2 -> ()" - ,"Actual type: Proxy ((2 * y0) + 4) -> ()" - ] -#endif - -testProxy5 :: Proxy 7 -> () -testProxy5 = proxyFun4 - -testProxy5Errors = -#if __GLASGOW_HASKELL__ >= 900 - ["Expected: Proxy 7 -> ()" - ," Actual: Proxy ((2 * y1) + 4) -> ()" - ] -#else - ["Expected type: Proxy 7 -> ()" - ,"Actual type: Proxy ((2 * y1) + 4) -> ()" - ] -#endif - -proxyFun6 :: Proxy (2^k) -> Proxy (2^k) -proxyFun6 = const Proxy - -testProxy6 :: Proxy 7 -testProxy6 = proxyFun6 (Proxy :: Proxy 7) - -testProxy6Errors = -#if __GLASGOW_HASKELL__ >= 902 - ["Expected: Proxy 7" - ," Actual: Proxy (2 ^ k0)" - ] -#elif __GLASGOW_HASKELL__ >= 900 - ["Expected: Proxy (2 ^ k0)" - ," Actual: Proxy 7" - ] -#else - ["Expected type: Proxy (2 ^ k0)" - ,"Actual type: Proxy 7" - ] -#endif - -proxyFun7 :: Proxy (2^k) -> Proxy k -proxyFun7 = const Proxy - -testProxy8 :: Proxy x -> Proxy (y + x) -testProxy8 = id - -testProxy8Errors = -#if __GLASGOW_HASKELL__ >= 900 - ["Expected: Proxy x -> Proxy (y + x)" - ," Actual: Proxy x -> Proxy x" - ] -#else - ["Expected type: Proxy x -> Proxy (y + x)" - ,"Actual type: Proxy x -> Proxy x" - ] -#endif - -#if __GLASGOW_HASKELL__ >= 904 -proxyInEq :: ((a <= b) ~ (() :: Constraint)) => Proxy (a :: Nat) -> Proxy b -> () -#else -proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> () -#endif -proxyInEq _ _ = () - -proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> () -proxyInEq' _ _ = () - -testProxy9 :: Proxy (a + 1) -> Proxy a -> () -testProxy9 = proxyInEq - -testProxy9Errors = -#if __GLASGOW_HASKELL__ >= 904 - ["Cannot satisfy: a + 1 <= a"] -#elif __GLASGOW_HASKELL__ >= 902 - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond" - else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "(CmpNat (a + 1) a) 'True 'True 'False’" - else litE $ stringL "(CmpNat (a + 1) a) 'True 'True 'False'" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "with ‘'True’" - else litE $ stringL "with 'True" - ) - ] -#else - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘(a + 1) <=? a’ with ‘'True’" - else litE $ stringL "Couldn't match type `(a + 1) <=? a' with 'True" - )] -#endif - -testProxy10 :: Proxy (a :: Nat) -> Proxy (a + 2) -> () -testProxy10 = proxyInEq' - -testProxy10Errors = -#if __GLASGOW_HASKELL__ >= 910 - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond" - else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "(CmpNat a (a + 2)) True True False’" - else litE $ stringL "(CmpNat a (a + 2)) True True False'" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "with ‘False" - else litE $ stringL "with `False" - ) - ] -#elif __GLASGOW_HASKELL__ >= 906 - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond" - else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "(CmpNat a (a + 2)) True True False’" - else litE $ stringL "(CmpNat a (a + 2)) True True False'" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "with ‘False" - else litE $ stringL "with False" - ) - ] -#elif __GLASGOW_HASKELL__ >= 902 - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond" - else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "(CmpNat a (a + 2)) 'True 'True 'False’" - else litE $ stringL "(CmpNat a (a + 2)) 'True 'True 'False'" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "with ‘'False" - else litE $ stringL "with 'False" - ) - ] -#else - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘a <=? (a + 2)’ with ‘'False’" - else litE $ stringL "Couldn't match type `a <=? (a + 2)' with 'False" - )] -#endif - -testProxy11 :: Proxy (a :: Nat) -> Proxy a -> () -testProxy11 = proxyInEq' - -testProxy11Errors = - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 -#if __GLASGOW_HASKELL__ >= 910 - then litE $ stringL "Couldn't match type ‘True’ with ‘False’" - else litE $ stringL "Couldn't match type `True' with `False'" -#elif __GLASGOW_HASKELL__ >= 906 - then litE $ stringL "Couldn't match type ‘True’ with ‘False’" - else litE $ stringL "Couldn't match type True with False" -#else - then litE $ stringL "Couldn't match type ‘'True’ with ‘'False’" - else litE $ stringL "Couldn't match type 'True with 'False" -#endif - )] - -testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> () -testProxy12 = proxyInEq - -testProxy12Errors = -#if __GLASGOW_HASKELL__ >= 904 - ["Cannot satisfy: a + b <= a + c"] -#elif __GLASGOW_HASKELL__ >= 902 - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond" - else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "(CmpNat (a + b) (a + c)) 'True 'True 'False’" - else litE $ stringL "(CmpNat (a + b) (a + c)) 'True 'True 'False'" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "with ‘'True’" - else litE $ stringL "with 'True" - ) - ] -#else - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘(a + b) <=? (a + c)’ with ‘'True’" - else litE $ stringL "Couldn't match type `(a + b) <=? (a + c)' with 'True" - )] -#endif - -testProxy13 :: Proxy (4*a) -> Proxy (2*a) ->() -testProxy13 = proxyInEq - -testProxy13Errors = -#if __GLASGOW_HASKELL__ >= 904 - ["Cannot satisfy: 4 * a <= 2 * a"] -#elif __GLASGOW_HASKELL__ >= 902 - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond" - else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "(CmpNat (4 * a) (2 * a)) 'True 'True 'False’" - else litE $ stringL "(CmpNat (4 * a) (2 * a)) 'True 'True 'False'" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "with ‘'True’" - else litE $ stringL "with 'True" - ) - ] -#else - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘(4 * a) <=? (2 * a)’ with ‘'True’" - else litE $ stringL "Couldn't match type `(4 * a) <=? (2 * a)' with 'True" - )] -#endif - -testProxy14 :: Proxy (2*a) -> Proxy (4*a) -> () -testProxy14 = proxyInEq' - -testProxy14Errors = -#if __GLASGOW_HASKELL__ >= 910 - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond" - else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False’" - else litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False'" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "with ‘False" - else litE $ stringL "with `False" - ) - ] -#elif __GLASGOW_HASKELL__ >= 906 - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond" - else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False’" - else litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False'" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "with ‘False" - else litE $ stringL "with False" - ) - ] -#elif __GLASGOW_HASKELL__ >= 902 - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond" - else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "(CmpNat (2 * a) (4 * a)) 'True 'True 'False’" - else litE $ stringL "(CmpNat (2 * a) (4 * a)) 'True 'True 'False'" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "with ‘'False" - else litE $ stringL "with 'False" - ) - ] -#else - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘(2 * a) <=? (4 * a)’ with ‘'False’" - else litE $ stringL "Couldn't match type `(2 * a) <=? (4 * a)' with 'False" - )] -#endif - -type family CLog (b :: Nat) (x :: Nat) :: Nat -type instance CLog 2 2 = 1 - -testProxy15 :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d) -testProxy15 = id - -testProxy15Errors = -#if __GLASGOW_HASKELL__ >= 900 - ["Expected: Proxy n -> Proxy (n + d)" - ," Actual: Proxy n -> Proxy n" - ] -#else - ["Expected type: Proxy n -> Proxy (n + d)" - ,"Actual type: Proxy n -> Proxy n" - ] -#endif - -data Fin (n :: Nat) where - FZ :: Fin (n + 1) - FS :: Fin n -> Fin (n + 1) - -test16 :: forall n . Integer -> Fin n -test16 n = case n of - 0 -> FZ - x -> FS (test16 @(n-1) (x-1)) - -test16Errors = -#if __GLASGOW_HASKELL__ >= 904 - ["Cannot satisfy: 1 <= n"] -#elif __GLASGOW_HASKELL__ >= 902 - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond" - else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "(CmpNat 1 n) 'True 'True 'False’" - else litE $ stringL "(CmpNat 1 n) 'True 'True 'False'" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "with ‘'True’" - else litE $ stringL "with 'True" - ) - ] -#else - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘1 <=? n’ with ‘'True’" - else litE $ stringL "Couldn't match type `1 <=? n' with 'True" - )] -#endif - -data Dict c where - Dict :: c => Dict c -deriving instance Show (Dict c) -data Boo (n :: Nat) = Boo - -test17 :: Show (Boo n) => Proxy n -> Boo (n - 1 + 1) -> String -test17 = const show - -testProxy17 :: String - -testProxy17 = test17 (Proxy :: Proxy 17) Boo -test17Errors = test16Errors - -#if __GLASGOW_HASKELL__ >= 904 -test19f :: ((1 <= n) ~ (() :: Constraint)) -#else -test19f :: (1 <= n) -#endif - => Proxy n -> Proxy n -test19f = id - -testProxy19 :: (1 <= m, m <= rp) - => Proxy m - -> Proxy rp - -> Proxy (rp - m) - -> Proxy (rp - m) -testProxy19 _ _ = test19f - -test19Errors = -#if __GLASGOW_HASKELL__ >= 904 - [ "Cannot satisfy: 1 <= rp - m" ] -#elif __GLASGOW_HASKELL__ >= 902 - [ "Could not deduce: Data.Type.Ord.OrdCond" - , "(CmpNat 1 (rp - m)) 'True 'True 'False" - , "~ 'True" - ] -#else - ["Could not deduce: (1 <=? (rp - m)) ~ 'True"] -#endif - -testProxy20 :: Proxy 1 -> Proxy (m ^ 2) -> () -testProxy20 = proxyInEq - -testProxy20Errors = -#if __GLASGOW_HASKELL__ >= 904 - ["Cannot satisfy: 1 <= m ^ 2"] -#elif __GLASGOW_HASKELL__ >= 902 - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond" - else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "(CmpNat 1 (m ^ 2)) 'True 'True 'False’" - else litE $ stringL "(CmpNat 1 (m ^ 2)) 'True 'True 'False'" - ) - ,$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "with ‘'True’" - else litE $ stringL "with 'True" - ) - ] -#else - [$(do localeEncoding <- runIO (getLocaleEncoding) - if textEncodingName localeEncoding == textEncodingName utf8 - then litE $ stringL "Couldn't match type ‘1 <=? (m ^ 2)’ with ‘'True’" - else litE $ stringL "Couldn't match type `1 <=? (m ^ 2)' with 'True" - )] -#endif diff --git a/tests/ShouldError.hs b/tests/ShouldError.hs new file mode 100644 --- /dev/null +++ b/tests/ShouldError.hs @@ -0,0 +1,597 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE QuasiQuotes #-} + +module ShouldError (tests) where + +import Data.String.Interpolate (i) +import ShouldError.Tasty (assertCompileError) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase) + +tests :: TestTree +tests = testGroup "ShouldError" + [ test1 + , test2 + , test3 + , test4 + , test5 + , test6 + , test7 + , test8 + , test9 + , test10 + , test11 + , testIssue126 + , inequalityTests + ] + +preamble :: String +preamble = [i| +import Data.Kind (Constraint) +import Data.Proxy +import GHC.TypeLits +|] <> "\n" + +source1 :: String +source1 = preamble <> [i| +test :: Proxy (x + 1) -> Proxy (2 + x) +test = id +|] + +expected1 :: [String] +expected1 = +#if __GLASGOW_HASKELL__ >= 914 + ["Expected: Proxy (2 + x)" + ," Actual: Proxy (x + 1)" + ] +#elif __GLASGOW_HASKELL__ >= 900 + ["Expected: Proxy (x + 1) -> Proxy (2 + x)" + ," Actual: Proxy (x + 1) -> Proxy (x + 1)" + ] +#else + ["Expected type: Proxy (x + 1) -> Proxy (2 + x)" + ,"Actual type: Proxy (2 + x) -> Proxy (2 + x)" + ] +#endif + +test1 :: TestTree +test1 = testCase "x + 1 /~ 2 + x" $ assertCompileError source1 expected1 + +source2 :: String +source2 = preamble <> [i| +type family GCD (x :: Nat) (y :: Nat) :: Nat +type instance GCD 6 8 = 2 +type instance GCD 9 6 = 3 + +test :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6) +test = id +|] + +expected2 :: [String] +expected2 = +#if __GLASGOW_HASKELL__ >= 914 + ["Expected: Proxy (x + GCD 9 6)" + ," Actual: Proxy (2 + x)" + ] +#elif __GLASGOW_HASKELL__ >= 900 + ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)" + ," Actual: Proxy (2 + x) -> Proxy (2 + x)" + ] +#else + ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)" + ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)" + ] +#endif + +test2 :: TestTree +test2 = testCase "GCD 6 8 + x /~ x + GCD 9 6" $ assertCompileError source2 expected2 + +source3 :: String +source3 = preamble <> [i| +proxyFun :: Proxy (x + x + x) -> () +proxyFun = const () + +test :: Proxy 8 -> () +test = proxyFun +|] + +expected3 :: [String] +expected3 = +#if __GLASGOW_HASKELL__ >= 914 + ["Expected: Proxy ((x0 + x0) + x0)" + ," Actual: Proxy 8" + ] +#elif __GLASGOW_HASKELL__ >= 900 + ["Expected: Proxy 8 -> ()" + ," Actual: Proxy ((x0 + x0) + x0) -> ()" + ] +#else + ["Expected type: Proxy 8 -> ()" + ,"Actual type: Proxy ((x0 + x0) + x0) -> ()" + ] +#endif + +test3 :: TestTree +test3 = testCase "Unify \"x + x + x\" with \"8\"" $ assertCompileError source3 expected3 + +source4 :: String +source4 = preamble <> [i| +proxyFun :: Proxy ((2*y)+4) -> () +proxyFun = const () + +test :: Proxy 2 -> () +test = proxyFun +|] + +expected4 :: [String] +expected4 = +#if __GLASGOW_HASKELL__ >= 914 + ["Expected: Proxy ((2 * y0) + 4)" + ," Actual: Proxy 2" + ] +#elif __GLASGOW_HASKELL__ >= 900 + ["Expected: Proxy 2 -> ()" + ," Actual: Proxy ((2 * y0) + 4) -> ()" + ] +#else + ["Expected type: Proxy 2 -> ()" + ,"Actual type: Proxy ((2 * y0) + 4) -> ()" + ] +#endif + +test4 :: TestTree +test4 = testCase "Unify \"(2*x)+4\" with \"2\"" $ assertCompileError source4 expected4 + +source5 :: String +source5 = preamble <> [i| +proxyFun :: Proxy ((2*y)+4) -> () +proxyFun = const () + +test :: Proxy 7 -> () +test = proxyFun +|] + +expected5 :: [String] +expected5 = +#if __GLASGOW_HASKELL__ >= 914 + ["Expected: Proxy ((2 * y" + ,"Actual: Proxy 7" + ] +#elif __GLASGOW_HASKELL__ >= 900 + ["Expected: Proxy 7 -> ()" + ,"Actual: Proxy ((2 * y" + ] +#else + ["Expected type: Proxy 7 -> ()" + ,"Actual type: Proxy ((2 * y" + ] +#endif + +test5 :: TestTree +test5 = testCase "Unify \"(2*x)+4\" with \"7\"" $ assertCompileError source5 expected5 + +source6 :: String +source6 = preamble <> [i| +proxyFun :: Proxy (2^k) -> Proxy (2^k) +proxyFun = const Proxy + +test :: Proxy 7 +test = proxyFun (Proxy :: Proxy 7) +|] + +expected6 :: [String] +expected6 = +#if __GLASGOW_HASKELL__ >= 902 + ["Expected: Proxy 7" + ," Actual: Proxy (2 ^ k0)" + ] +#elif __GLASGOW_HASKELL__ >= 900 + ["Expected: Proxy (2 ^ k0)" + ," Actual: Proxy 7" + ] +#else + ["Expected type: Proxy (2 ^ k0)" + ,"Actual type: Proxy 7" + ] +#endif + +test6 :: TestTree +test6 = testCase "Unify \"2^k\" with \"7\"" $ assertCompileError source6 expected6 + +source7 :: String +source7 = preamble <> [i| +test :: Proxy x -> Proxy (y + x) +test = id +|] + +expected7 :: [String] +expected7 = +#if __GLASGOW_HASKELL__ >= 914 + ["Expected: Proxy (y + x)" + ," Actual: Proxy x" + ] +#elif __GLASGOW_HASKELL__ >= 900 + ["Expected: Proxy x -> Proxy (y + x)" + ," Actual: Proxy x -> Proxy x" + ] +#else + ["Expected type: Proxy x -> Proxy (y + x)" + ,"Actual type: Proxy x -> Proxy x" + ] +#endif + +test7 :: TestTree +test7 = testCase "x /~ y + x" $ assertCompileError source7 expected7 + +source8 :: String +source8 = preamble <> [i| +type family CLog (b :: Nat) (x :: Nat) :: Nat +type instance CLog 2 2 = 1 + +test :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d) +test = id +|] + +expected8 :: [String] +expected8 = +#if __GLASGOW_HASKELL__ >= 914 + ["Expected: Proxy (n + d)" + ," Actual: Proxy n" + ] +#elif __GLASGOW_HASKELL__ >= 900 + ["Expected: Proxy n -> Proxy (n + d)" + ," Actual: Proxy n -> Proxy n" + ] +#else + ["Expected type: Proxy n -> Proxy (n + d)" + ,"Actual type: Proxy n -> Proxy n" + ] +#endif + +test8 :: TestTree +test8 = testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n /~ n + d" $ + assertCompileError source8 expected8 + +source9 :: String +source9 = preamble <> [i| +data Fin (n :: Nat) where + FZ :: Fin (n + 1) + FS :: Fin n -> Fin (n + 1) + +test :: forall n . Integer -> Fin n +test n = case n of + 0 -> FZ + x -> FS (test @(n-1) (x-1)) +|] + +expected9 :: [String] +expected9 = +#if __GLASGOW_HASKELL__ >= 904 + ["Cannot satisfy: 1 <= n"] +#elif __GLASGOW_HASKELL__ >= 902 + [ "Couldn't match type Data.Type.Ord.OrdCond" + , "(CmpNat 1 n) True True False" + , "with True" + ] +#else + [ "Couldn't match type 1 <=? n with True" ] +#endif + +test9 :: TestTree +test9 = testCase "(n - 1) + 1 ~ n implies (1 <= n)" $ assertCompileError source9 expected9 + +source10 :: String +source10 = preamble <> [i| +type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where + Drop 0 xs = xs + Drop n (x ': xs) = Drop (n-1) xs + Drop n '[] = '[] + +test :: Proxy ns -> Proxy (Drop 1 ns) -> Proxy (Drop 2 ns) +test _ px = px +|] + +expected10 :: [String] +expected10 = +#if __GLASGOW_HASKELL__ >= 811 + [ "Couldn't match type: Drop 1 ns" + , " with: Drop 2 ns" + , "Expected: Proxy (Drop 2 ns)" + , " Actual: Proxy (Drop 1 ns)" + , "Drop is a non-injective type family" + ] +#else + [ "Couldn't match type Drop 1 ns with Drop 2 ns" + , "Expected type: Proxy (Drop 2 ns)" + , " Actual type: Proxy (Drop 1 ns)" + , "Drop is a non-injective type family" + ] +#endif + +test10 :: TestTree +test10 = testCase "Do not unify in non-injective positions" $ assertCompileError source10 expected10 + +source11 :: String +source11 = preamble <> [i| +test :: Proxy a -> Proxy b -> Proxy ((2 * a) + b) -> Proxy 5 +test _ _ = id +|] + +expected11 :: [String] +expected11 = +#if __GLASGOW_HASKELL__ >= 914 + ["Expected: Proxy 5" + ," Actual: Proxy ((2 * a) + b)" + ] +#elif __GLASGOW_HASKELL__ >= 900 + ["Expected: Proxy ((2 * a) + b) -> Proxy 5" + ," Actual: Proxy 5 -> Proxy 5" + ] +#else + ["Expected type: Proxy ((2 * a) + b) -> Proxy 5" + ,"Actual type: Proxy 5 -> Proxy 5" + ] +#endif + +test11 :: TestTree +test11 = testCase "Do not rewrite constraint to itself" $ assertCompileError source11 expected11 + +-- ((3 * (n - 1)) + 1) simplifies to (3 * n - 2), so +-- the equality would require b0 ~ -2, which is impossible at kind Nat. +sourceIssue126 :: String +sourceIssue126 = preamble <> [i| +data Index (n :: Nat) = Index + +truncateB :: Index (a + b) -> Index a +truncateB = undefined + +mul :: Index 4 -> Index n -> Index ((3 * (n - 1)) + 1) +mul _ _ = Index + +zeroExtendTimesThree :: (1 <= n) => Index n -> Index (n * 3) +zeroExtendTimesThree = truncateB . (mul Index) +|] + +expectedIssue126 :: [String] +expectedIssue126 = +#if __GLASGOW_HASKELL__ >= 906 + [ "Could not deduce ((n * 3) + b0) ~ ((3 * (n - 1)) + 1)" +#elif __GLASGOW_HASKELL__ >= 904 + [ "Could not deduce (((n * 3) + b0) ~ ((3 * (n - 1)) + 1))" +#elif __GLASGOW_HASKELL__ >= 902 + [ "Could not deduce: ((n * 3) + b0) ~ ((3 * (n - 1)) + 1)" +#else + [ "Could not deduce: ((3 * (n - 1)) + 1) ~ ((n * 3) + b0)" +#endif + , "from the context: 1 <= n" + ] + + + +testIssue126 :: TestTree +testIssue126 = + testCase "Issue 126 regression reproducer" $ + assertCompileError sourceIssue126 expectedIssue126 + +proxyInEqDef :: String +proxyInEqDef = +#if __GLASGOW_HASKELL__ >= 904 + [i| +proxyInEq :: ((a <= b) ~ (() :: Constraint)) => Proxy (a :: Nat) -> Proxy b -> () +proxyInEq _ _ = () +|] +#else + [i| +proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> () +proxyInEq _ _ = () +|] +#endif + +proxyInEq'Def :: String +proxyInEq'Def = [i| +proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> () +proxyInEq' _ _ = () +|] + +source12 :: String +source12 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i| +test :: Proxy (a + 1) -> Proxy a -> () +test = proxyInEq +|] + +expected12 :: [String] +expected12 = +#if __GLASGOW_HASKELL__ >= 904 + ["Cannot satisfy: a + 1 <= a"] +#elif __GLASGOW_HASKELL__ >= 902 + [ "Couldn't match type Data.Type.Ord.OrdCond" + , "(CmpNat (a + 1) a) True True False" + , "with True" + ] +#else + [ "Couldn't match type (a + 1) <=? a with True" ] +#endif + +test12 :: TestTree +test12 = testCase "a+1 <= a" $ assertCompileError source12 expected12 + +source13 :: String +source13 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i| +test :: Proxy (a :: Nat) -> Proxy (a + 2) -> () +test = proxyInEq' +|] + +expected13 :: [String] +expected13 = +#if __GLASGOW_HASKELL__ >= 902 + [ "Data.Type.Ord.OrdCond" + , "(CmpNat a (a + 2)) True True False" + , "with False" + ] +#else + [ "Couldn't match type a <=? (a + 2) with False" ] +#endif + +test13 :: TestTree +test13 = testCase "(a <=? a+1) ~ False" $ assertCompileError source13 expected13 + +source14 :: String +source14 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i| +test :: Proxy (a :: Nat) -> Proxy a -> () +test = proxyInEq' +|] + +expected14 :: [String] +expected14 = [ "Couldn't match type True with False" ] + +test14 :: TestTree +test14 = testCase "(a <=? a) ~ False" $ assertCompileError source14 expected14 + +source15 :: String +source15 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i| +test :: Proxy (a + b) -> Proxy (a + c) -> () +test = proxyInEq +|] + +expected15 :: [String] +expected15 = +#if __GLASGOW_HASKELL__ >= 904 + ["Cannot satisfy: a + b <= a + c"] +#elif __GLASGOW_HASKELL__ >= 902 + [ "Couldn't match type Data.Type.Ord.OrdCond" + , "(CmpNat (a + b) (a + c)) True True False" + , "with True" + ] +#else + [ "Couldn't match type (a + b) <=? (a + c) with True" ] +#endif + +test15 :: TestTree +test15 = testCase "() => (a+b <= a+c)" $ assertCompileError source15 expected15 + +source16 :: String +source16 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i| +test :: Proxy (4*a) -> Proxy (2*a) -> () +test = proxyInEq +|] + +expected16 :: [String] +expected16 = +#if __GLASGOW_HASKELL__ >= 904 + ["Cannot satisfy: 4 * a <= 2 * a"] +#elif __GLASGOW_HASKELL__ >= 902 + [ "Couldn't match type Data.Type.Ord.OrdCond" + , "(CmpNat (4 * a) (2 * a)) True True False" + , "with True" + ] +#else + [ "Couldn't match type (4 * a) <=? (2 * a) with True" ] +#endif + +test16 :: TestTree +test16 = testCase "4a <= 2a" $ assertCompileError source16 expected16 + +source17 :: String +source17 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i| +test :: Proxy (2*a) -> Proxy (4*a) -> () +test = proxyInEq' +|] + +expected17 :: [String] +expected17 = +#if __GLASGOW_HASKELL__ >= 902 + [ "Data.Type.Ord.OrdCond" + , "(CmpNat (2 * a) (4 * a)) True True False" + , "with False" + ] +#else + [ "Couldn't match type (2 * a) <=? (4 * a) with False" ] +#endif + +test17 :: TestTree +test17 = testCase "2a <=? 4a ~ False" $ assertCompileError source17 expected17 + +source18 :: String +source18 = preamble <> [i| +data Boo (n :: Nat) = Boo + +test :: Show (Boo n) => Proxy n -> Boo (n - 1 + 1) -> String +test = const show +|] + +expected18 :: [String] +expected18 = expected9 + +test18 :: TestTree +test18 = testCase "Show (Boo n) => Show (Boo (n - 1 + 1))" $ assertCompileError source18 expected18 + +test19fDef :: String +test19fDef = +#if __GLASGOW_HASKELL__ >= 904 + [i| +test19f :: ((1 <= n) ~ (() :: Constraint)) => Proxy n -> Proxy n +test19f = id +|] +#else + [i| +test19f :: (1 <= n) => Proxy n -> Proxy n +test19f = id +|] +#endif + +source19 :: String +source19 = preamble <> test19fDef <> [i| +test :: (1 <= m, m <= rp) => Proxy m -> Proxy rp -> Proxy (rp - m) -> Proxy (rp - m) +test _ _ = test19f +|] + +expected19 :: [String] +expected19 = +#if __GLASGOW_HASKELL__ >= 904 + [ "Cannot satisfy: 1 <= rp - m" ] +#elif __GLASGOW_HASKELL__ >= 902 + [ "Could not deduce: Data.Type.Ord.OrdCond" + , "(CmpNat 1 (rp - m)) True True False" + , "~ True" + ] +#else + [ "Could not deduce: (1 <=? (rp - m)) ~ True" ] +#endif + +test19 :: TestTree +test19 = testCase "1 <= m, m <= rp implies 1 <= rp - m" $ assertCompileError source19 expected19 + +source20 :: String +source20 = preamble <> proxyInEqDef <> [i| +test :: Proxy 1 -> Proxy (m ^ 2) -> () +test = proxyInEq +|] + +expected20 :: [String] +expected20 = +#if __GLASGOW_HASKELL__ >= 904 + ["Cannot satisfy: 1 <= m ^ 2"] +#elif __GLASGOW_HASKELL__ >= 902 + [ "Couldn't match type Data.Type.Ord.OrdCond" + , "(CmpNat 1 (m ^ 2)) True True False" + , "with True" + ] +#else + [ "Couldn't match type 1 <=? (m ^ 2) with True" ] +#endif + +test20 :: TestTree +test20 = testCase "Vacuously: 1 <= m ^ 2 ~ True" $ assertCompileError source20 expected20 + +inequalityTests :: TestTree +inequalityTests = testGroup "Inequality" + [ test12 + , test13 + , test14 + , test15 + , test16 + , test17 + , test18 + , test19 + , test20 + ] 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,58 @@ +{-# LANGUAGE CPP #-} + +module ShouldError.Tasty where + +import Data.List (isInfixOf) +import Data.Maybe (fromMaybe) +import System.Environment (lookupEnv) +import System.Exit +import System.IO +import System.IO.Temp +import System.Process +import Test.Tasty.HUnit + +-- | Assert that a Haskell code snippet fails to compile with expected error messages +assertCompileError :: String -> [String] -> Assertion +assertCompileError source expectedErrors = do + -- XXX: This will pick the wrong GHC if the HC environment variable (as seen on CI) + -- isn't set and the test suite is compiled with a GHC compiler other than the + -- system's default. + hc <- fromMaybe "ghc" <$> lookupEnv "HC" + withSystemTempFile "ShouldError.hs" $ \tempFile tempHandle -> do + hPutStr tempHandle source + hClose tempHandle + (exitCode, _, stderrOutput) <- readProcessWithExitCode hc + [ "-XCPP" + , "-XAllowAmbiguousTypes" + , "-XConstraintKinds" + , "-XDataKinds" + , "-XFlexibleContexts" + , "-XGADTs" + , "-XScopedTypeVariables" + , "-XStandaloneDeriving" + , "-XTypeApplications" + , "-XTypeFamilies" + , "-XTypeOperators" + , "-XUndecidableInstances" + , "-XNoStarIsType" + , "-fno-code" + , "-fplugin", "GHC.TypeLits.Normalise" + , tempFile + ] "" + case exitCode of + ExitSuccess -> assertFailure "Expected compilation to fail but it succeeded" + ExitFailure _ -> + let cleanedStderr = removeProblemChars stderrOutput + cleanedExpected = map removeProblemChars expectedErrors + in if all (`isInfixOf` cleanedStderr) cleanedExpected + then return () + else assertFailure $ "Error message mismatch:\n" ++ + "Expected substrings: " ++ show expectedErrors ++ "\n" ++ + "Actual output:\n" ++ stderrOutput + +-- | Remove problematic characters that vary depending on locale +-- The kind and amount of quotes in GHC error messages changes depending on +-- whether or not our locale supports unicode. +removeProblemChars :: String -> String +removeProblemChars = filter (`notElem` problemChars) + where problemChars = "‘’`'" diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -23,6 +23,7 @@ {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -dcore-lint #-} +{-# OPTIONS_GHC -Wno-unused-top-binds #-} import GHC.TypeLits #if MIN_VERSION_base(4,18,0) @@ -33,14 +34,17 @@ import Prelude hiding (head,tail,init,(++),splitAt,concat,drop) import qualified Prelude as P -import Data.Kind (Type) -import Data.List (isInfixOf) +#if MIN_VERSION_base(4,16,0) +import Data.Type.Ord +#endif + +import Data.Kind (Type, Constraint) import Data.Proxy -import Control.Exception +import Data.Type.Equality ((:~:)(..)) import Test.Tasty import Test.Tasty.HUnit -import ErrorTests +import qualified ShouldError data Vec :: Nat -> Type -> Type where Nil :: Vec 0 a @@ -118,6 +122,7 @@ -- 1 head :: Vec (n + 1) a -> a head (x :> _) = x +head Nil = error "head: impossible" head' :: forall n a @@ -132,6 +137,7 @@ -- <2,3> tail :: Vec (n + 1) a -> Vec n a tail (_ :> xs) = xs +tail Nil = error "tail: impossible" tail' :: (1 <= m) => Vec m a -> Vec (m-1) a tail' = tail @@ -143,6 +149,7 @@ init :: Vec (n + 1) a -> Vec n a init (_ :> Nil) = Nil init (x :> y :> ys) = x :> init (y :> ys) +init Nil = error "init: impossible" init' :: (1 <= m) => Vec m a -> Vec (m-1) a init' = init @@ -169,6 +176,7 @@ splitAtU UZero ys = (Nil,ys) splitAtU (USucc s) (y :> ys) = let (as,bs) = splitAtU s ys in (y :> as, bs) +splitAtU (USucc _) Nil = error "splitAtU: impossible" {-# INLINE splitAtI #-} -- | Split a vector into two vectors where the length of the two is determined @@ -244,6 +252,8 @@ merge :: Vec n a -> Vec n a -> Vec (n + n) a merge Nil Nil = Nil merge (x :> xs) (y :> ys) = x :> y :> merge xs ys +merge Nil (_ :> _) = error "merge: impossible" +merge (_ :> _) Nil = error "merge: impossible" -- | 'drop' @n xs@ returns the suffix of @xs@ after the first @n@ elements -- @@ -304,6 +314,15 @@ a' -> B0 a' predBNat (B0 x) = B1 (predBNat x) +proxyFun3 :: Proxy (x + x + x) -> () +proxyFun3 = const () + +proxyFun4 :: Proxy ((2*y)+4) -> () +proxyFun4 = const () + +proxyFun7 :: Proxy (2^k) -> Proxy k +proxyFun7 = const Proxy + -- issue 52 begin type role Signal nominal representational data Signal (dom :: Symbol) a = a :- Signal dom a @@ -321,6 +340,12 @@ issue52 = bundle -- issue 52 end +proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> () +proxyInEq _ _ = () + +proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> () +proxyInEq' _ _ = () + proxyInEq1 :: Proxy a -> Proxy (a+1) -> () proxyInEq1 = proxyInEq @@ -359,7 +384,7 @@ . ((x + 1) ~ (2 * y), 1 <= y) => Proxy x -> Proxy y - -> Proxy (((2 * (y - 1)) + 1)) + -> Proxy ((2 * (y - 1)) + 1) -> Proxy x proxyEq3 _ _ x = x @@ -374,12 +399,12 @@ proxyEq4 = theProxy where theProxy - :: forall a b c - . (KnownNat (((a - b) + c) + (b - c)), c <= b, b <= a) - => Proxy b - -> Proxy c - -> Proxy a - -> Proxy (((a - b) + c) + (b - c)) + :: forall a' b' c' + . (KnownNat (((a' - b') + c') + (b' - c')), c' <= b', b' <= a') + => Proxy b' + -> Proxy c' + -> Proxy a' + -> Proxy (((a' - b') + c') + (b' - c')) theProxy _ _ = id proxyInEqImplication :: (2 <= (2 ^ (n + d))) @@ -449,6 +474,14 @@ succAtMost :: AtMost n -> AtMost (n + 1) succAtMost (AtMost (Proxy :: Proxy a)) = AtMost (Proxy :: Proxy a) +data Dict c where + Dict :: c => Dict c + +instance Show (Dict c) where + show Dict = "Dict" + +data Boo (n :: Nat) = Boo + eqReduceForward :: Eq (Boo (n + 1)) => Dict (Eq (Boo (n + 2 - 1))) @@ -469,6 +502,9 @@ => Dict (Eq (Boo (m + 3))) eqReduceBackward' = Dict +type family CLog (b :: Nat) (x :: Nat) :: Nat +type instance CLog 2 2 = 1 + proxyInEq8fun :: (1 <= (n + CLog 2 n)) => Proxy n @@ -481,13 +517,13 @@ -> Proxy n proxyInEq8 = proxyInEq8fun -data H2 = H2 { p :: Nat } +data H2 = H2 { pNat :: Nat } class Q (dom :: Symbol) where type G2 dom :: H2 type family P (c :: H2) :: Nat where - P ('H2 p) = p + P ('H2 pNat) = pNat type F2 (dom :: Symbol) = P (G2 dom) @@ -506,8 +542,22 @@ oneLtPowSubst = go where go :: 1 <= b => Proxy a -> Proxy a - go = id + go = id +type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where + Drop 0 xs = xs + Drop n (x ': xs) = Drop (n-1) xs + Drop n '[] = '[] + +isOkay :: + forall x y sh . + Proxy x -> + Proxy y -> + Proxy sh -> + Proxy (Drop (x + y) sh) -> + Proxy (Drop (y + x) sh) +isOkay _ _ _ px = px + main :: IO () main = defaultMain tests @@ -515,25 +565,25 @@ tests = testGroup "ghc-typelits-natnormalise" [ testGroup "Basic functionality" [ testCase "show (head (1:>2:>3:>Nil))" $ - show (head (1:>2:>3:>Nil)) @?= + show (head ((1 :: Integer):>2:>3:>Nil)) @?= "1" , testCase "show (tail (1:>2:>3:>Nil))" $ - show (tail (1:>2:>3:>Nil)) @?= + show (tail ((1 :: Integer):>2:>3:>Nil)) @?= "<2,3>" , testCase "show (init (1:>2:>3:>Nil))" $ - show (init (1:>2:>3:>Nil)) @?= + show (init ((1 :: Integer):>2:>3:>Nil)) @?= "<1,2>" , testCase "show ((1:>2:>3:>Nil) ++ (7:>8:>Nil))" $ - show ((1:>2:>3:>Nil) ++ (7:>8:>Nil)) @?= + show (((1 :: Integer):>2:>3:>Nil) ++ (7:>8:>Nil)) @?= "<1,2,3,7,8>" , testCase "show (splitAt (snat :: SNat 3) (1:>2:>3:>7:>8:>Nil))" $ - show (splitAt (snat :: SNat 3) (1:>2:>3:>7:>8:>Nil)) @?= + show (splitAt (snat :: SNat 3) ((1 :: Integer):>2:>3:>7:>8:>Nil)) @?= "(<1,2,3>,<7,8>)" , testCase "show (concat ((1:>2:>3:>Nil) :> (4:>5:>6:>Nil) :> (7:>8:>9:>Nil) :> (10:>11:>12:>Nil) :> Nil))" $ - show (concat ((1:>2:>3:>Nil) :> (4:>5:>6:>Nil) :> (7:>8:>9:>Nil) :> (10:>11:>12:>Nil) :> Nil)) @?= + show (concat (((1 :: Integer):>2:>3:>Nil) :> (4:>5:>6:>Nil) :> (7:>8:>9:>Nil) :> (10:>11:>12:>Nil) :> Nil)) @?= "<1,2,3,4,5,6,7,8,9,10,11,12>" , testCase "show (unconcat (snat :: SNat 4) (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil))" $ - show (unconcat (snat :: SNat 4) (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)) @?= + show (unconcat (snat :: SNat 4) ((1 :: Integer):>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)) @?= "<<1,2,3,4>,<5,6,7,8>,<9,10,11,12>>" , testCase "show (proxyFun3 (Proxy :: Proxy 9))" $ show (proxyFun3 (Proxy :: Proxy 9)) @?= @@ -552,6 +602,9 @@ , testCase "(((2 ^ x) - 2) * (2 ^ (x + x))) ~ ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1))))" $ show (proxyEq2 @2 Proxy) @?= "Proxy" + , testCase "Unify in non-injective positions under specific conditions" $ + show (isOkay @2 @3 @'[] Proxy Proxy Proxy Proxy) @?= + "Proxy" ] , testGroup "Implications" [ testCase "(x + 1) ~ (2 * y)) implies (((2 * (y - 1)) + 1)) ~ x" $ @@ -612,45 +665,9 @@ show (oneLtPowSubst (Proxy :: Proxy 0)) @?= "Proxy" ] - , testGroup "errors" - [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors - , testCase "GCD 6 8 + x ~ x + GCD 9 6" $ testProxy2 `throws` testProxy2Errors - , testCase "Unify \"x + x + x\" with \"8\"" $ testProxy3 `throws` testProxy3Errors - , testCase "Unify \"(2*x)+4\" with \"2\"" $ testProxy4 `throws` testProxy4Errors - , testCase "Unify \"(2*x)+4\" with \"7\"" $ testProxy5 `throws` testProxy5Errors - , testCase "Unify \"2^k\" with \"7\"" $ testProxy6 `throws` testProxy6Errors - , testCase "x ~ y + x" $ testProxy8 `throws` testProxy8Errors - , testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n ~ (n+d)" $ - testProxy15 (Proxy :: Proxy 1) `throws` testProxy15Errors - , testCase "(n - 1) + 1 ~ n implies (1 <= n)" $ test16 `throws` test16Errors - , testGroup "Inequality" - [ testCase "a+1 <= a" $ testProxy9 `throws` testProxy9Errors - , testCase "(a <=? a+1) ~ False" $ testProxy10 `throws` testProxy10Errors - , testCase "(a <=? a) ~ False" $ testProxy11 `throws` testProxy11Errors - , testCase "() => (a+b <= a+c)" $ testProxy12 `throws` testProxy12Errors - , testCase "4a <= 2a" $ testProxy13 `throws` testProxy13Errors - , testCase "2a <=? 4a ~ False" $ testProxy14 `throws` testProxy14Errors - , testCase "Show (Boo n) => Show (Boo (n - 1 + 1))" $ - testProxy17 `throws` test17Errors - , testCase "1 <= m, m <= rp implies 1 <= rp - m" $ (testProxy19 (Proxy @1) (Proxy @1)) `throws` test19Errors - , testCase "Vacuously: 1 <= m ^ 2 ~ True" $ testProxy20 `throws` testProxy20Errors - ] - ] + , ShouldError.tests ] --- | Assert that evaluation of the first argument (to WHNF) will throw --- an exception whose string representation contains the given --- substrings. -throws :: a -> [String] -> Assertion -throws v xs = do - result <- try (evaluate v) - case result of - Right _ -> assertFailure "No exception!" - Left (TypeError msg) -> - if all (`isInfixOf` msg) xs - then return () - else assertFailure msg - showFin :: forall n. KnownNat n => Fin n -> String showFin f = mconcat [ show (finToInt f) @@ -662,6 +679,10 @@ finToInt FZ = 0 finToInt (FS fn) = finToInt fn + 1 +data Fin (n :: Nat) where + FZ :: Fin (n + 1) + FS :: Fin n -> Fin (n + 1) + predFin :: Fin (n + 2) -> Fin (n + 1) predFin (FS fn) = fn predFin FZ = FZ @@ -709,3 +730,115 @@ touchVector = WFV . touchVector . unWrap instance FakeUnbox (n + 1) => IsMVector WrapFakeMVector n where touchMVector = MWFV . touchMVector . unWrapM + +#if MIN_VERSION_base(4,16,0) +-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/70 +libFunc :: forall (i :: Nat) d. i < d => Proxy i -> Proxy d -> () +libFunc _ _ = () +useFunc :: forall (d :: Nat). Proxy d -> () +useFunc _ = libFunc (Proxy @0) (Proxy @(d+1)) +#endif + +-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/71 +t71_aux :: (((1 + m1) + n1) ~ (1 + (m2 + n2))) => Proxy '(m1, n1, m2, n2) -> () +t71_aux _ = () +t71 :: ((m1 + n1) ~ (m2 + n2)) => Proxy '(m1, n1, m2, n2) -> () +t71 px = t71_aux px + +-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94 +t94 :: + (KnownNat n, KnownNat m, KnownNat s, s ~ (m - n)) => + Proxy m -> Proxy n -> Proxy (s + 2) -> Proxy (s + 2) +t94 _ _ = t94_aux + +t94_aux :: (1 <= n) => Proxy n -> Proxy n +t94_aux px = px + +-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/96 +t96 + :: ( 2 <= x, 2 <= y + , ( 4 * x + 2 * 2^y ) ~ ( 4 * y + 2 * 2^x ) + ) + => Proxy x -> Proxy y +t96 x = x + +type family TF (a :: Nat) (b :: Nat) :: Nat + +proxyEq5 + :: forall a b + . KnownNat (TF (a * 3) b * 3) + => Proxy a + -> Proxy b + -> Proxy (3 * TF (3 * a) b) +proxyEq5 = theProxy + where + theProxy + :: forall a' b' + . KnownNat (TF (2 * a' + a') b' + (2 * TF (a' + 2 * a') b')) + => Proxy a' + -> Proxy b' + -> Proxy (3 * TF (3 * a') b') + theProxy _ _ = Proxy + +type family Rank sh where + Rank '[] = 0 + Rank (_ : sh) = Rank sh + 1 +foo :: ( ( 1 + Rank sh ) ~ ( 1 + n ) ) + => Proxy sh -> Proxy n -> Proxy (Rank sh) -> Proxy n +foo _ _ px = px + +noContra :: ((Rank sh + 2) <= 2) => Proxy sh -> () +noContra _ = () + +-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/97 +t97 :: ( (1 + n) ~ m, ( m - 1 ) ~ n ) => Proxy m -> Proxy n -> () +t97 _ _ = () + +t97b + :: ( n ~ (m - 2) + , (n + 1) ~ (m - 1) + , m ~ (n + 2) + ) + => Proxy n -> Proxy m -> () +t97b _ _ = () + +-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/116 +t116 :: forall n m l. m :~: n -> n :~: 0 -> l :~: 1 -> Float +t116 a b c = + case a of + Refl -> + case b of + Refl -> + case c of + Refl -> + 3.0 + +type family Foo (n :: Nat) :: Nat + +t119a :: Proxy n -> Proxy (Foo (n + 2)) -> Proxy (Foo (2 + n)) +t119a _ = id + +--Only applicable for GHC >= 9.4 as prior InEq constraints are of the form `a <=? b ~ 'True` +#if __GLASGOW_HASKELL__ >= 904 +t119b :: + (1 <= a) => + (1 <= Foo (a + 1)) => + Proxy a -> + Proxy a +t119b a = go a + where + go :: + ((1 <= Foo (c + 1)) ~ (() :: Constraint)) => + Proxy c -> + Proxy c + go _ = Proxy +#endif + +data NatPhantom (n :: Nat) = NatPhantom + +-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/124 +t124 :: 1 <= n => NatPhantom m -> NatPhantom (m + n - 1) +t124 x = go x + where + go :: NatPhantom a -> NatPhantom (b + a) + go _ = NatPhantom