diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,12 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 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,5 +1,6 @@ +cabal-version: 3.0 name: ghc-typelits-natnormalise -version: 0.7.12 +version: 0.8.0 synopsis: GHC typechecker plugin for types of kind GHC.TypeLits.Nat description: A type checker plugin for GHC that can solve /equalities/ and /inequalities/ @@ -37,7 +38,7 @@ 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 @@ -47,11 +48,9 @@ build-type: Simple extra-source-files: README.md CHANGELOG.md -cabal-version: >=1.10 -tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5, - GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8, - GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1, - GHC == 9.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 @@ -67,24 +66,26 @@ exposed-modules: GHC.TypeLits.Normalise, GHC.TypeLits.Normalise.SOP, GHC.TypeLits.Normalise.Unify + other-modules: GHC.TypeLits.Normalise.Compat build-depends: base >=4.9 && <5, containers >=0.5.7.1 && <0.8, - ghc >=8.0.1 && <9.13, - ghc-tcplugins-extra >=0.5, + ghc >=8.8.1 && <9.15, + ghc-tcplugin-api >=0.17.0 && <0.18, transformers >=0.5.2.0 && < 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 + ) + 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 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,731 @@ +{-| +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 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 + ( (<=<) ) +import Control.Monad.Trans.Writer.Strict + ( WriterT(runWriterT), runWriter ) +import Data.Either + ( rights, partitionEithers ) +import Data.List + ( stripPrefix, find, partition ) +import qualified Data.List.NonEmpty as NE +import Data.Maybe + ( mapMaybe, catMaybes, fromMaybe ) +import Data.Traversable + ( for ) +import Text.Read + ( readMaybe ) + +-- containers +import Data.Set + ( Set ) +import qualified Data.Set as Set + ( elems, empty ) + +-- ghc +import GHC.Builtin.Names + ( knownNatClassName ) +import GHC.Builtin.Types.Literals + ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon ) + +-- ghc-tcplugin-api +import GHC.TcPlugin.API +import GHC.TcPlugin.API.TyConSubst + ( TyConSubst, mkTyConSubst, splitTyConApp_upTo ) +import GHC.Plugins + ( Plugin(..), defaultPlugin, purePlugin ) +import GHC.Utils.Outputable + ( ($$), (<+>), text, vcat ) + +-- ghc-typelits-natnormalise +import GHC.TypeLits.Normalise.Compat +import GHC.TypeLits.Normalise.SOP + ( SOP(S), Product(P), Symbol(V) ) +import GHC.TypeLits.Normalise.Unify + +-------------------------------------------------------------------------------- + +-- | 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 + , tcPluginStop = 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 + reds = + filter + (\(_,(_,_,v)) -> null v || negNumbers opts) $ + reduceGivens opts tcs (mkTyConSubst givens) givens + + tcPluginTrace "decideEqualSOP Givens {" $ + vcat [ text "givens:" <+> ppr givens ] + + newGivens <- for reds $ \(origCt, (pred', evTerm, _)) -> + mkNonCanonical <$> newGiven (ctLoc origCt) pred' evTerm + -- Try to find contradictory Givens, to improve pattern match warnings. + sr <- simplifyNats opts tcs [] $ concatMap (toNatEquality tcs givensTyConSubst) (givens ++ newGivens) + case sr of + Impossible eq -> do + let contra = fromNatEquality eq + tcPluginTrace "decideEqualSOP Givens (FAIL) }" $ + vcat [ text "givens:" <+> ppr givens + , text "contra:" <+> ppr contra ] + return $ TcPluginContradiction [contra] + Simplified {} -> do + tcPluginTrace "decideEqualSOP Givens (OK) }" $ + vcat [ text "givens:" <+> ppr givens ] + return $ TcPluginOk [] [] + +-- 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 tcs givensTyConSubst) wanteds + nonEqs = filter ( not + . (\p -> isEqPred p || isEqClassPred p) + . ctEvPred + . ctEvidence ) + wanteds + let newRedGs = reduceGivens opts tcs givensTyConSubst givens + redGivens <- for newRedGs $ \(origCt, (pred', evExpr, _)) -> + mkNonCanonical <$> newGiven (ctLoc origCt) pred' evExpr + reducible_wanteds + <- catMaybes <$> mapM (\ct -> fmap (ct,) <$> + reduceNatConstr givensTyConSubst (givens ++ redGivens) ct) + nonEqs + + tcPluginTrace "decideEqualSOP Wanteds {" $ + vcat [ text "givens:" <+> ppr givens + , text "new reduced givens:" <+> ppr redGivens + , text "newRedGs:" <+> ppr newRedGs + , 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. + ineqForRedWants <- fmap concat $ for newRedGs $ \(ct, (_,_, ws)) -> for ws $ + fmap mkNonCanonical . newWanted (ctLoc ct) + let unit_givens = concatMap (toNatEquality tcs givensTyConSubst) givens + unit_wanteds = unit_wanteds0 ++ concatMap (toNatEquality tcs givensTyConSubst) ineqForRedWants + sr <- 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) + case sr of + Simplified evs -> do + let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs + -- Only solve a Derived when there are Wanteds in play + simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of + [] -> [] + _ -> simpld + (solved,newWanteds) = second concat (unzip $ simpld1 ++ reds) + + tcPluginTrace "decideEqualSOP Wanteds }" $ + vcat [ text "givens:" <+> ppr givens + , text "new reduced givens:" <+> ppr redGivens + , text "newRedGs:" <+> ppr newRedGs + , text $ replicate 80 '-' + , text "wanteds:" <+> ppr wanteds + , text "ineqForRedWants:" <+> ppr ineqForRedWants + , text "unit_wanteds0:" <+> ppr (map (toNatEquality tcs givensTyConSubst) wanteds) + , text "unit_wanteds:" <+> ppr unit_wanteds + , text "reducible_wanteds:" <+> ppr reducible_wanteds + , text $ replicate 80 '=' + , text "solved:" <+> ppr solved + , text "newWanteds:" <+> ppr newWanteds + ] + + return (TcPluginOk solved $ newWanteds) + Impossible eq -> return (TcPluginContradiction [fromNatEquality eq]) + +type NatEquality = (Ct,CoreSOP,CoreSOP) +type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool)) + +reduceGivens :: Opts -> LookedUpTyCons + -> TyConSubst + -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))] +reduceGivens opts tcs givensTyConSubst givens = + let nonEqs = + [ ct + | ct <- givens + , let ev = ctEvidence ct + prd = ctEvPred ev + , isGiven ev + , not $ (\p -> isEqPred p || isEqClassPred p ) prd + ] + in mapMaybe + (\ct -> (ct,) <$> tryReduceGiven opts tcs givensTyConSubst givens ct) + nonEqs + +tryReduceGiven + :: Opts -> LookedUpTyCons + -> TyConSubst + -> [Ct] -> Ct + -> Maybe (PredType, EvTerm, [PredType]) +tryReduceGiven opts tcs givensTyConSubst simplGivens ct = do + let (mans, ws) = + runWriter $ normaliseNatEverywhere givensTyConSubst $ + ctEvPred $ ctEvidence ct + ws' = [ p + | p <- subToPred opts tcs ws + , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens + ] + -- deps = unitDVarSet (ctEvId ct) + (pred', deps) <- mans + return (pred', toReducedDict (ctEvidence ct) pred' deps, ws') + +fromNatEquality :: Either NatEquality NatInEquality -> Ct +fromNatEquality (Left (ct, _, _)) = ct +fromNatEquality (Right (ct, _)) = ct + +reduceNatConstr :: TyConSubst -> [Ct] -> Ct -> TcPluginM Solve (Maybe (EvTerm, [(Type, Type)], [Ct])) +reduceNatConstr givensTyConSubst givens ct = do + let pred0 = ctEvPred $ ctEvidence ct + (mans, tests) = runWriter $ normaliseNatEverywhere givensTyConSubst 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 + = 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 + +type NatCt = (Either NatEquality NatInEquality, [(Type,Type)], [Coercion]) + +simplifyNats + :: Opts + -- ^ Allow negated numbers (potentially unsound!) + -> LookedUpTyCons + -> [NatCt] + -- ^ Given constraints + -> [NatCt] + -- ^ Wanted constraints + -> TcPluginM Solve SimplifyResult +simplifyNats opts@Opts {..} tcs eqsG eqsW = do + let eqsG1 = map (\ (eq, _, deps) -> (eq, [] :: [(Type, Type)], deps)) 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 <- for 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)] + -> [NatCt] + -> [NatCt] + -> TcPluginM Solve SimplifyResult + simples _ _subst evs _leqsG _xs [] = return (Simplified evs) + simples deps subst evs leqsG xs (eq@(lr@(Left (ct,u,v)),k,deps2):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 tcs ct (deps ++ deps2) Set.empty (subToPred opts tcs k) + simples deps subst evs' leqsG [] (xs ++ eqs') + Lose -> if null evs && null eqs' + then return (Impossible lr) + else simples deps subst evs leqsG xs eqs' + Draw [] -> simples deps subst evs [] (eq:xs) eqs' + Draw subst' -> do + evM <- evMagic tcs ct deps Set.empty (map unifyItemToPredType subst' ++ + subToPred opts tcs k) + + tcPluginTrace "unifyNats: Draw (non-empty subst)" $ + vcat [ text "subst':" <+> ppr subst' + , text "evM:" <+> ppr evM ] + + 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 ++ deps2) + (substsSubst subst' subst ++ subst') + (ev:evs) leqsG1 [] (xs ++ eqs') + simples deps subst evs leqsG xs (eq@(lr@(Right (ct,u@(x,y,b))),k,deps2):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 (\ (lr', _, _) -> lr') eqsG)) + ] + tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs)) + case runWriterT (isNatural u') of + Just (True,knW) -> do + evs' <- maybe evs (:evs) <$> evMagic tcs ct deps knW (subToPred opts tcs k) + simples deps subst evs' leqsG' xs eqs' + + Just (False,_) | null k -> return (Impossible lr) + _ -> 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 + let deps' = deps ++ deps2 + evs' <- maybe evs (:evs) <$> evMagic tcs ct deps' kW (subToPred opts tcs 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 :: [NatCt] -> NatCt -> [[NatCt]] + 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 :: NatCt + -> NatCt + -> Either NatCt (Either NatCt NatCt) + matchesVarEq (Left (_, S [P [V v1]], S [P [V v2]]), _, _) r@(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]]), ps, deps) = + (Left (ct,S [P [V v2]], S [P [V v1]]), ps, deps) + swapVar _ = error "internal error" + + findFirstSimpliedWanted (Impossible e) _ = Impossible e + findFirstSimpliedWanted (Simplified evs) s2 + | any (isWanted . ctEvidence . 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 -> 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 :: LookedUpTyCons -> TyConSubst -> Ct -> [(Either NatEquality NatInEquality, [(Type,Type)], [Coercion])] +toNatEquality tcs givensTyConSubst ct0 + | Just (((x,y), mbLTE), cos0) <- isNatRel tcs givensTyConSubst pred0 + , let + ((x', cos1),k1) = runWriter (normaliseNat givensTyConSubst x) + ((y', cos2),k2) = runWriter (normaliseNat givensTyConSubst y) + ks = k1 ++ k2 + = case mbLTE of + Nothing -> + -- Equality constraint: x ~ y + [(Left (ct0, x', y'), ks, cos0 ++ cos1 ++ cos2)] + Just b -> + -- Inequality constraint: (x <=? y) ~ b + [(Right (ct0, (x', y', b)), ks, cos0 ++ cos1 ++ cos2)] + | otherwise + = case classifyPredType pred0 of + EqPred NomEq t1 t2 + -> goNomEq t1 t2 + _ -> [] + where + pred0 = ctPred ct0 + -- x ~ y + goNomEq :: Type -> Type -> [(Either NatEquality NatInEquality, [(Type,Type)], [Coercion])] + 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 tcApps1 <- splitTyConApp_upTo givensTyConSubst lhs + , Just tcApps2 <- splitTyConApp_upTo givensTyConSubst rhs + , let tcAppsMap1 = listToUniqMap $ map (\ (tc, tys, deps) -> (tc, (tys, deps))) $ NE.toList tcApps1 + tcAppsMap2 = listToUniqMap $ map (\ (tc, tys, deps) -> (tc, (tys, deps))) $ NE.toList tcApps2 + tcAppPairs = intersectUniqMap_C (,) tcAppsMap1 tcAppsMap2 + , (tc, ((xs, cos1), (ys, cos2))):_ <- nonDetUniqMapToList tcAppPairs + , not $ tc `elem` [typeNatAddTyCon, typeNatSubTyCon, typeNatMulTyCon, typeNatExpTyCon] + , let subs = filter (not . uncurry eqType) (zip xs ys) + = (\ (eq, ws, deps) -> (eq, ws, cos1 ++ cos2 ++ deps)) <$> + concatMap (uncurry rewrite) subs + | otherwise + = rewrite lhs rhs + + rewrite :: Type -> Type -> [(Either NatEquality NatInEquality, [(Type,Type)], [Coercion])] + rewrite x y + | isNatKind (typeKind x) + , isNatKind (typeKind y) + , let ((x', cos1),k1) = runWriter (normaliseNat givensTyConSubst x) + , let ((y', cos2),k2) = runWriter (normaliseNat givensTyConSubst y) + = [(Left (ct0,x',y'),k1 ++ k2, 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 + +evSubtPreds :: CtLoc -> [PredType] -> TcPluginM Solve [Ct] +evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc) + +evMagic :: LookedUpTyCons -> Ct -> [Coercion] -> Set CType -> [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,381 @@ + +{-# 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 + + ) 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,3,0) + -- Starting from GHC 9.3, (a <= b) turns into 'Assert (a <=? b) msg'. + -- We prefer to emit 'Assert (a <=? b) msg ~ (() :: Constraint)', + -- in order to avoid creating an Irred constraint. + mkEqPredRole Nominal + (mkTyConApp (leqTyCon tcs) [natKind, a, b]) + (mkTyConTy $ c0TyCon tcs) +#elif 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 + -- (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 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 @@ -160,7 +160,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 +189,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 +245,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 +273,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 +297,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 +312,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 +330,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,16 +5,15 @@ Maintainer : Christiaan Baaij -} -{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE RecordWildCards #-} +{-# 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 CType (..) @@ -38,7 +37,6 @@ , subtractIneq , solveIneq , ineqToSubst - , subtractionToPred , instantSolveIneq , solvedInEqSmallestConstraint -- * Properties @@ -46,82 +44,53 @@ ) where --- External -import Control.Arrow (first, second) +-- base +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 + ( Writer, WriterT(..), runWriter, tell ) +import Data.Foldable + ( asum ) +import Data.Function + ( on ) +import Data.List + ( (\\), intersect, nub ) +import qualified Data.List.NonEmpty as NE +import Data.Maybe + ( fromMaybe, mapMaybe, isJust ) +import Data.Traversable + ( for ) +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 + ) +import GHC.Utils.Outputable + ( ($$), (<+>), text ) -#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.TcPlugin.API.TyConSubst (TyConSubst, splitTyConApp_upTo) --- Internal +-- ghc-typelits-natnormalise import GHC.TypeLits.Normalise.SOP --- Used for haddock -import GHC.TypeLits (Nat) - -#if MIN_VERSION_ghc(9,2,0) -typeNatKind :: Type -typeNatKind = naturalTy -#endif +-------------------------------------------------------------------------------- newtype CType = CType { unCType :: Type } deriving Outputable @@ -143,21 +112,45 @@ -- * 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)]]) +normaliseNat :: TyConSubst -> Type -> Writer [(Type,Type)] (CoreSOP, [Coercion]) +normaliseNat givensTyConSubst ty + | Just tc_apps <- splitTyConApp_upTo givensTyConSubst ty + , (tc, xs, cos0) : _ <- NE.filter (( \ ( tc, _, _) -> tc `elem` knownTyCons)) tc_apps + = second ( ++ cos0 ) <$> 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 givensTyConSubst x + (y', cos2) <- normaliseNat givensTyConSubst y + return (mergeSOPAdd x' y', cos1 ++ cos2) + | tc == typeNatSubTyCon = do + (x', cos1) <- normaliseNat givensTyConSubst x + (y', cos2) <- normaliseNat givensTyConSubst 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 givensTyConSubst x + (y', cos2) <- normaliseNat givensTyConSubst y + return (mergeSOPMul x' y', cos1 ++ cos2) + | tc == typeNatExpTyCon = + do (x', cos1) <- normaliseNat givensTyConSubst x + (y', cos2) <- normaliseNat givensTyConSubst y + return (normaliseExp x' y', cos1 ++ cos2) + goTyConApp tc xs = + return (S [P [C (CType $ mkTyConApp tc xs)]], []) --- | 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 +164,50 @@ -- | 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 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 - - -- 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 +normaliseNatEverywhere :: TyConSubst -> Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion])) +normaliseNatEverywhere givensTyConSubst ty0 + | Just tc_apps <- splitTyConApp_upTo givensTyConSubst ty0 + = fmap asum $ for tc_apps $ \ (tc, fields, cos1) -> + 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, cos2) = fromMaybe (ty0, []) ty1M + -- Normalize (subterm-normalized) type given to 'normaliseNatEverywhere' + (ty2, cos3) <- normaliseSimplifyNat givensTyConSubst 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 ++ cos2) ++) <$> ty1M else Just (ty2, cos1 ++ cos2 ++ cos3)) + else go tc fields + | 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_))) + let cos' = concat $ mapMaybe (fmap snd) fields1_ + in + pure (Just (mkTyConApp tc_ (zipWith (\ f0 f1 -> maybe f0 fst f1) fields0_ fields1_), cos')) else pure Nothing where - cont = if tc_ `elem` knownTyCons then go else normaliseNatEverywhere - go _ = pure Nothing + cont ty' + | tc_ `elem` knownTyCons + , Just tc_apps' <- splitTyConApp_upTo givensTyConSubst ty' + = asum <$> traverse ( \ (tc', flds', cos') -> fmap (second (cos' ++)) <$> go tc' flds') tc_apps' + | otherwise + = normaliseNatEverywhere givensTyConSubst ty' -normaliseSimplifyNat :: Type -> Writer [(Type, Type)] Type -normaliseSimplifyNat ty - | typeKind ty `eqType` typeNatKind = do - ty' <- normaliseNat ty - return $ reifySOP $ simplifySOP ty' - | otherwise = return ty +normaliseSimplifyNat :: TyConSubst -> Type -> Writer [(Type, Type)] (Type, [Coercion]) +normaliseSimplifyNat givensTyConSubst ty + | typeKind ty `eqType` natKind = do + (ty', cos1) <- normaliseNat givensTyConSubst 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 @@ -322,25 +337,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 +355,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 :: (Outputable v, Outputable c, Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c substSOP tv e = foldr1 mergeSOPAdd . 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 +375,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,8 +398,8 @@ -- 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) @@ -422,7 +418,7 @@ where -- A unifier is only a unifier if differs from the original constraint diffFromConstraint (UnifyItem x y) = not (x == u && y == v) - diffFromConstraint _ = True + diffFromConstraint (SubstItem x y) = not (S [P [V x]] == u && y == v) -- | Find unifiers for two SOP terms -- @@ -461,32 +457,39 @@ 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] + | CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct) + -> [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] + | CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct) + -> [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] + | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 + -> [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] + | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 + -> [UnifyItem u v] _ -> [] unifiers ct u v = unifiers' ct u v unifiers' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify] +unifiers' _ct (S []) (S []) = [] + 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 (S [P [C {}]]) (S [P [C {}]]) = [] unifiers' _ct s1@(S [P [C _]]) s2 = [UnifyItem s1 s2] unifiers' _ct s1 s2@(S [P [C _]]) = [UnifyItem s1 s2] @@ -511,45 +514,41 @@ -- (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 + = 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 + = 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 @@ -561,28 +560,32 @@ -- (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) + = case compare i j of + EQ -> unifiers' ct (S ps1) (S ps2) + LT -> unifiers' ct (S ps1) (S ((P [I (j-i)]):ps2)) + GT -> 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'') +unifiers' ct s1@(S ps1) s2@(S ps2) + | Just (s1',s2',_) <- sopToIneq k1 + , s1' /= s1 || s2' /= s2 + , 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 + , length ps1 > 1 + , let unifs = nub $ concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2) + , length unifs <= 1 + = case unifs of + [] -> unifiers'' ct (S ps1) (S ps2) + [k] -> [k] + _ -> error "impossible" + | null psx + , isGiven (ctEvidence ct) + = unifiers'' ct (S ps1) (S ps2) + | not $ null psx + = unifiers' ct (S ps1'') (S ps2'') where k1 = subtractIneq (s1,s2,True) ps1' = ps1 \\ psx @@ -592,6 +595,8 @@ ps2'' | null ps2' = [P [I 0]] | otherwise = ps2' psx = intersect ps1 ps2 + +unifiers' _ s1 s2 = [UnifyItem s1 s2] unifiers'' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify] unifiers'' ct (S [P [I i],P [V v]]) s2 diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs --- a/tests/ErrorTests.hs +++ b/tests/ErrorTests.hs @@ -20,13 +20,16 @@ import Data.Proxy import GHC.TypeLits -#if __GLASGOW_HASKELL__ >= 904 +#if __GLASGOW_HASKELL__ >= 903 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 #if __GLASGOW_HASKELL__ >= 901 import qualified Data.Type.Ord @@ -90,11 +93,11 @@ testProxy4Errors = #if __GLASGOW_HASKELL__ >= 900 ["Expected: Proxy 2 -> ()" - ," Actual: Proxy ((2 * y0) + 4) -> ()" + ," Actual: Proxy ((2 * 0) + 4) -> ()" ] #else ["Expected type: Proxy 2 -> ()" - ,"Actual type: Proxy ((2 * y0) + 4) -> ()" + ,"Actual type: Proxy ((2 * 0) + 4) -> ()" ] #endif @@ -104,11 +107,11 @@ testProxy5Errors = #if __GLASGOW_HASKELL__ >= 900 ["Expected: Proxy 7 -> ()" - ," Actual: Proxy ((2 * y1) + 4) -> ()" + ," Actual: Proxy ((2 * y0) + 4) -> ()" ] #else ["Expected type: Proxy 7 -> ()" - ,"Actual type: Proxy ((2 * y1) + 4) -> ()" + ,"Actual type: Proxy ((2 * y0) + 4) -> ()" ] #endif diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -33,6 +33,10 @@ import Prelude hiding (head,tail,init,(++),splitAt,concat,drop) import qualified Prelude as P +#if MIN_VERSION_base(4,16,0) +import Data.Type.Ord +#endif + import Data.Kind (Type) import Data.List (isInfixOf) import Data.Proxy @@ -506,7 +510,7 @@ oneLtPowSubst = go where go :: 1 <= b => Proxy a -> Proxy a - go = id + go = id main :: IO () main = defaultMain tests @@ -709,3 +713,37 @@ 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 +t1 :: (((1 + m1) + n1) ~ (1 + (m2 + n2))) => Proxy '(m1, n1, m2, n2) -> () +t1 _ = () +t2 :: ((m1 + n1) ~ (m2 + n2)) => Proxy '(m1, n1, m2, n2) -> () +t2 px = t1 px + + + +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