ghc-typelits-natnormalise 0.8.0 → 0.8.1
raw patch · 7 files changed
+515/−263 lines, 7 filesdep ~ghc-tcplugin-apiPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: ghc-tcplugin-api
API changes (from Hackage documentation)
+ GHC.TypeLits.Normalise.Unify: negateProd :: CoreProduct -> CoreProduct
- GHC.TypeLits.Normalise.Unify: unifiers :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
+ GHC.TypeLits.Normalise.Unify: unifiers :: Ct -> CoreSOP -> CoreSOP -> Maybe [CoreUnify]
Files
- CHANGELOG.md +7/−0
- ghc-typelits-natnormalise.cabal +15/−14
- src/GHC/TypeLits/Normalise.hs +131/−97
- src/GHC/TypeLits/Normalise/Compat.hs +25/−0
- src/GHC/TypeLits/Normalise/Unify.hs +254/−147
- tests/ErrorTests.hs +40/−0
- tests/Tests.hs +43/−5
CHANGELOG.md view
@@ -1,5 +1,12 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.8.1 *October 1st 2025*+* Fixes [#85](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/85) Deriving equalities from inequalities produces a misleading error message+* Fixes [#94](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94) Normalization fails when adding an equality constraint with substraction+* Fixes [#96](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/96) Unification fails when variables occur on both LHS and RHS+* Fixes [#99](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/99) ghc-typelits-natnormalise erroneously unifies under type families+* Fixes [100](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/100) stack space overflow with ghc-typelits-natnormalize 0.8+ ## 0.8 *September 8th 2025* * Uses https://hackage.haskell.org/package/ghc-tcplugin-api to make supporting new GHC versions easier * Support for GHC versions older than 8.8 is dropped
ghc-typelits-natnormalise.cabal view
@@ -1,40 +1,40 @@ cabal-version: 3.0 name: ghc-typelits-natnormalise-version: 0.8.0+version: 0.8.1 synopsis: GHC typechecker plugin for types of kind GHC.TypeLits.Nat description: A type checker plugin for GHC that can solve /equalities/ and /inequalities/ of types of kind @Nat@, where these types are either:- .+ * Type-level naturals- .+ * Type variables- .+ * Applications of the arithmetic expressions @(+,-,*,^)@.- .+ It solves these equalities by normalising them to /sort-of/ @SOP@ (Sum-of-Products) form, and then perform a simple syntactic equality.- .+ For example, this solver can prove the equality between:- .+ @ (x + 2)^(y + 2) @- .+ and- .+ @ 4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2 @- .+ Because the latter is actually the @SOP@ normal form of the former.- .+ To use the plugin, add the- .+ @ OPTIONS_GHC -fplugin GHC.TypeLits.Normalise @- .+ Pragma to the header of your file. homepage: http://www.clash-lang.org/ bug-reports: http://github.com/clash-lang/ghc-typelits-natnormalise/issues@@ -70,7 +70,7 @@ build-depends: base >=4.9 && <5, containers >=0.5.7.1 && <0.8, ghc >=8.8.1 && <9.15,- ghc-tcplugin-api >=0.17.0 && <0.18,+ ghc-tcplugin-api >=0.18.0 && <0.19, transformers >=0.5.2.0 && < 0.7 if impl(ghc >= 9.0.0) build-depends: ghc-bignum >=1.0 && <1.5@@ -83,6 +83,7 @@ , TyCon as GHC.Core.TyCon , TysWiredIn as GHC.Builtin.Types , Unique as GHC.Types.Unique+ , Util as GHC.Utils.Misc ) hs-source-dirs: src
src/GHC/TypeLits/Normalise.hs view
@@ -143,6 +143,7 @@ where /n-l/ is a negative number. -} +{-# LANGUAGE BangPatterns #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ExplicitNamespaces #-} {-# LANGUAGE FlexibleContexts #-}@@ -169,9 +170,9 @@ ( WriterT(runWriterT), runWriter ) import Data.Either ( rights, partitionEithers )+import Data.Foldable import Data.List- ( stripPrefix, find, partition )-import qualified Data.List.NonEmpty as NE+ ( stripPrefix, partition ) import Data.Maybe ( mapMaybe, catMaybes, fromMaybe ) import Data.Traversable@@ -184,21 +185,28 @@ ( Set ) import qualified Data.Set as Set ( elems, empty )+import Data.Map.Strict+ ( Map )+import qualified Data.Map.Strict as Map+ ( empty, insertWith, traverseWithKey ) -- ghc import GHC.Builtin.Names ( knownNatClassName ) import GHC.Builtin.Types.Literals ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon )+import GHC.Core.TyCon+ ( Injectivity (..), tyConInjectivityInfo, tyConArity )+import GHC.Utils.Misc+ ( filterByList ) -- ghc-tcplugin-api import GHC.TcPlugin.API import GHC.TcPlugin.API.TyConSubst- ( TyConSubst, mkTyConSubst, splitTyConApp_upTo )+ ( TyConSubst, mkTyConSubst ) import GHC.Plugins ( Plugin(..), defaultPlugin, purePlugin ) import GHC.Utils.Outputable- ( ($$), (<+>), text, vcat ) -- ghc-typelits-natnormalise import GHC.TypeLits.Normalise.Compat@@ -273,30 +281,26 @@ -- @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+ let+ givensTyConSubst = mkTyConSubst givens+ (redGivens, _) <- reduceGivens False opts tcs givensTyConSubst 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 [] []+ SimplifyResult _simpls contras <-+ simplifyNats opts tcs [] $+ concatMap (toNatEquality tcs givensTyConSubst) redGivens+ tcPluginTrace "decideEqualSOP Givens }" $+ vcat [ text "givens:" <+> ppr givens+ , text "simpls:" <+> ppr _simpls+ , text "contra:" <+> ppr contras ]+ return $+ mkTcPluginSolveResult+ ( map fromNatEquality contras )+ [] -- no solved Givens+ [] -- no new Givens -- Solving phase. -- Solves in/equalities on Nats and simplifiable constraints@@ -313,18 +317,16 @@ . ctEvPred . ctEvidence ) wanteds- let newRedGs = reduceGivens opts tcs givensTyConSubst givens- redGivens <- for newRedGs $ \(origCt, (pred', evExpr, _)) ->- mkNonCanonical <$> newGiven (ctLoc origCt) pred' evExpr++ (redGivens, negWanteds) <- reduceGivens True opts tcs givensTyConSubst givens reducible_wanteds <- catMaybes <$> mapM (\ct -> fmap (ct,) <$>- reduceNatConstr givensTyConSubst (givens ++ redGivens) ct)+ reduceNatConstr givensTyConSubst 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@@ -337,61 +339,67 @@ -- 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+ let mkNegWanted ( CType wtdPred ) loc = mkNonCanonical <$> newWanted loc wtdPred+ ineqForRedWants <- Map.traverseWithKey mkNegWanted negWanteds+ let unit_givens = concatMap (toNatEquality tcs givensTyConSubst) redGivens unit_wanteds = unit_wanteds0 ++ concatMap (toNatEquality tcs givensTyConSubst) ineqForRedWants- sr <- simplifyNats opts tcs unit_givens unit_wanteds+ sr@(SimplifyResult evs contras) <- 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- ]+ 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) - return (TcPluginOk solved $ newWanteds)- Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])+ tcPluginTrace "decideEqualSOP Wanteds }" $+ vcat [ text "givens:" <+> ppr givens+ , text "new reduced givens:" <+> ppr redGivens+ , text "unit givens:" <+> ppr unit_givens+ , text $ replicate 80 '-'+ , text "wanteds:" <+> ppr wanteds+ , text "ineqForRedWants:" <+> ppr ineqForRedWants+ , text "unit_wanteds:" <+> ppr unit_wanteds+ , text "reducible_wanteds:" <+> ppr reducible_wanteds+ , text $ replicate 80 '='+ , text "solved:" <+> ppr solved+ , text "newWanteds:" <+> ppr newWanteds+ ]+ return $+ mkTcPluginSolveResult+ (map fromNatEquality contras)+ solved+ newWanteds 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+reduceGivens :: Bool -- ^ allow generating new "non-negative" Wanteds+ -> Opts -> LookedUpTyCons -> TyConSubst+ -> [Ct]+ -> TcPluginM Solve ([Ct], Map CType CtLoc)+reduceGivens gen_wanteds opts tcs givensTyConSubst origGivens = go [] Map.empty origGivens+ where+ go rev_acc_gs acc_ws [] = return ( reverse rev_acc_gs, acc_ws )+ go rev_acc_gs acc_ws (g:gs) =+ case tryReduceGiven opts tcs givensTyConSubst origGivens g of+ Just ( pred', evExpr, ws )+ | gen_wanteds || null ws || negNumbers opts+ -> do+ let loc = ctLoc g+ g' <- mkNonCanonical <$> newGiven loc pred' evExpr+ let !acc' = foldl' (insertWanted loc) acc_ws ws+ go ( g' : rev_acc_gs ) acc' gs+ _ ->+ go ( g : rev_acc_gs ) acc_ws gs + insertWanted :: CtLoc -> Map CType CtLoc -> Type -> Map CType CtLoc+ insertWanted loc acc w =+ Map.insertWith (\ _new old -> old) (CType w) loc acc+ tryReduceGiven :: Opts -> LookedUpTyCons -> TyConSubst@@ -403,11 +411,15 @@ ctEvPred $ ctEvidence ct ws' = [ p | p <- subToPred opts tcs ws- , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens+ , all (not . (`eqType` p) . ctEvPred . ctEvidence) simplGivens ] -- deps = unitDVarSet (ctEvId ct) (pred', deps) <- mans- return (pred', toReducedDict (ctEvidence ct) pred' deps, ws')+ case classifyPredType pred' of+ EqPred _ l r+ | l `eqType` r+ -> Nothing+ _ -> return (pred', toReducedDict (ctEvidence ct) pred' deps, ws') fromNatEquality :: Either NatEquality NatInEquality -> Ct fromNatEquality (Left (ct, _, _)) = ct@@ -458,12 +470,15 @@ in EvExpr ev data SimplifyResult- = Simplified [((EvTerm,Ct),[Ct])]- | Impossible (Either NatEquality NatInEquality)+ = 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+ ppr (SimplifyResult { simplified, impossible }) =+ text "SimplifyResult { simplified =" <+> ppr simplified+ <+> text ", impossible =" <+> ppr impossible <+> text "}" type NatCt = (Either NatEquality NatInEquality, [(Type,Type)], [Coercion]) @@ -494,7 +509,7 @@ tcPluginTrace "simplifyNats" (ppr eqs) simples [] [] [] [] [] eqs - pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified)+ pure (foldr findFirstSimpliedWanted (SimplifyResult [] []) allSimplified) where simples :: [Coercion] -> [CoreUnify]@@ -503,7 +518,7 @@ -> [NatCt] -> [NatCt] -> TcPluginM Solve SimplifyResult- simples _ _subst evs _leqsG _xs [] = return (Simplified evs)+ simples _ _subst evs _leqsG _xs [] = return (SimplifyResult 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@@ -512,10 +527,14 @@ case ur of Win -> do evs' <- maybe evs (:evs) <$> evMagic tcs ct (deps ++ deps2) Set.empty (subToPred opts tcs k)+ tcPluginTrace "unifyNats Win" $+ vcat [ text "evs:" <+> ppr evs+ , text "evs':" <+> ppr evs'+ , text "ct:" <+> ppr ct+ ] 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'+ Lose ->+ addContra lr <$> 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' ++@@ -552,7 +571,8 @@ 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)+ Just (False,_) | null k ->+ addContra lr <$> simples deps subst evs leqsG xs eqs' _ -> do let solvedIneq = mapMaybe runWriterT -- it is an inequality that can be instantly solved, such as@@ -621,13 +641,16 @@ (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+ findFirstSimpliedWanted s1@(SimplifyResult evs imposs) s2+ | not (null imposs)+ || any (isWanted . ctEvidence . snd . fst) evs+ = s1 | otherwise = s2 +addContra :: Either NatEquality NatInEquality -> SimplifyResult -> SimplifyResult+addContra contra sr = sr { impossible = contra : impossible sr }+ -- If we allow negated numbers we simply do not emit the inequalities -- derived from the subtractions that are converted to additions with a -- negated operand@@ -657,6 +680,13 @@ = case classifyPredType pred0 of EqPred NomEq t1 t2 -> goNomEq t1 t2+ ClassPred kn [x]+ -- From [G] KnownNat blah, also produce [G] 0 <= blah+ -- See https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94.+ | isGiven (ctEvidence ct0)+ , className kn == knownNatClassName+ , let ((x', cos0), ks) = runWriter (normaliseNat givensTyConSubst x)+ -> [(Right (ct0, (S [], x', True)), ks, cos0)] _ -> [] where pred0 = ctPred ct0@@ -665,16 +695,20 @@ 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+ | Just (tc , xs) <- splitTyConApp_maybe lhs+ , Just (tc', ys) <- splitTyConApp_maybe rhs+ , tc == tc' , 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+ , let xys = zip xs ys+ -- Make sure not to recur into non-injective positions of type families,+ -- e.g. if we know 'F n ~ F m' that doesn't mean 'n ~ m'.+ subs =+ filter (not . uncurry eqType) $+ case tyConInjectivityInfo tc of+ Injective inj ->+ filterByList (inj ++ repeat True) xys+ _ -> drop (tyConArity tc) xys+ = concatMap (uncurry rewrite) subs | otherwise = rewrite lhs rhs
src/GHC/TypeLits/Normalise/Compat.hs view
@@ -23,6 +23,8 @@ , UniqMap, intersectUniqMap_C, listToUniqMap, nonDetUniqMapToList + , mkTcPluginSolveResult+ ) where -- base@@ -242,6 +244,9 @@ isNatRel tcs givensTyConSubst ty0 | EqPred NomEq x y <- classifyPredType ty0 = if+ -- (expr1 :: Nat) ~ (expr2 :: Nat)+ | all ( ( `eqType` natKind ) . typeKind ) [ x, y ]+ -> Just $ ( ( ( x, y ), Nothing ), [] ) -- (b :: Bool) ~ y | Just ( b, cos1 ) <- boolean_maybe givensTyConSubst x -> second ( ++ cos1 ) <$> booleanRel b y@@ -360,6 +365,7 @@ maybe [] NE.toList $ splitTyConApp_upTo givensTyConSubst ty --------------------------------------------------------------------------------+ #if !MIN_VERSION_ghc(9,7,0) newtype UniqMap k a = UniqMap ( UniqFM k (k, a) )@@ -379,3 +385,22 @@ {-# INLINE nonDetUniqMapToList #-} #endif++--------------------------------------------------------------------------------++mkTcPluginSolveResult :: [Ct] -> [(EvTerm, Ct)] -> [Ct]+ -> TcPluginSolveResult+#if MIN_VERSION_ghc(9,3,0)+mkTcPluginSolveResult = TcPluginSolveResult+#else+mkTcPluginSolveResult contras solved new =+ -- On GHC 9.2 and below, it's not possible to return+ -- both contradictions and solved/new constraints.+ --+ -- In general, we prefer returning solved constraints over contradictions.+ if null solved && not (null contras)+ then TcPluginContradiction contras+ else TcPluginOk solved new+#endif++--------------------------------------------------------------------------------
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -11,7 +11,6 @@ {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TupleSections #-} - {-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-} module GHC.TypeLits.Normalise.Unify@@ -39,6 +38,7 @@ , ineqToSubst , instantSolveIneq , solvedInEqSmallestConstraint+ , negateProd -- * Properties , isNatural )@@ -47,19 +47,14 @@ -- base import Control.Arrow ( first, second )-import Control.Monad.Trans.Writer.Strict- ( Writer, WriterT(..), runWriter, tell )-import Data.Foldable- ( asum )-import Data.Function- ( on )+import Control.Monad+ ( guard, zipWithM )+import Data.Either+ ( partitionEithers ) 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@@ -79,17 +74,23 @@ import GHC.Types.Unique.Set ( UniqSet , emptyUniqSet, unionManyUniqSets, unionUniqSets, unitUniqSet+ , nonDetEltsUniqSet, elementOfUniqSet )-import GHC.Utils.Outputable- ( ($$), (<+>), text ) -- ghc-tcplugin-api import GHC.TcPlugin.API-import GHC.TcPlugin.API.TyConSubst (TyConSubst, splitTyConApp_upTo)+import GHC.TcPlugin.API.TyConSubst+ ( TyConSubst )+import GHC.Utils.Outputable + -- ghc-typelits-natnormalise import GHC.TypeLits.Normalise.SOP +-- transformers+import Control.Monad.Trans.Writer.Strict+ ( Writer, WriterT(..), runWriter, tell )+ -------------------------------------------------------------------------------- newtype CType = CType { unCType :: Type }@@ -114,9 +115,8 @@ -- * Applications of the arithmetic operators @(+,-,*,^)@ 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 (tc, xs) <- splitTyConApp_maybe ty+ = goTyConApp tc xs | Just i <- isNumLitTy ty = return (S [P [I i]], []) | Just v <- getTyVar_maybe ty@@ -143,8 +143,8 @@ 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)]], [])+ goTyConApp tc xs+ = return (S [P [C (CType $ mkTyConApp tc xs)]], []) knownTyCons :: [TyCon] knownTyCons = [typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon, typeNatAddTyCon]@@ -166,20 +166,24 @@ -- the same as input, returns @'Nothing'@. 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+ | Just (tc, fields) <- splitTyConApp_maybe ty0+ = if tc `elem` knownTyCons then do -- Normalize under current type constructor application. 'go' skips all -- known type constructors. ty1M <- maybeRunWriter (go tc fields)- let (ty1, cos2) = fromMaybe (ty0, []) ty1M+ let (ty1, cos1) = fromMaybe (ty0, []) ty1M -- Normalize (subterm-normalized) type given to 'normaliseNatEverywhere'- (ty2, cos3) <- normaliseSimplifyNat givensTyConSubst ty1+ (ty2, cos2) <- 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+ pure $+ if ty2 `eqType` ty1+ then second (cos1 ++) <$> ty1M+ else Just (ty2, cos1 ++ cos2)+ else+ go tc fields+ | otherwise = pure Nothing where@@ -188,17 +192,18 @@ go :: TyCon -> [Type] -> Writer [(Type, Type)] (Maybe (Type, [Coercion])) go tc_ fields0_ = do fields1_ <- mapM (maybeRunWriter . cont) fields0_- if any isJust fields1_ then+ if any isJust fields1_+ then do let cos' = concat $ mapMaybe (fmap snd) fields1_- in- pure (Just (mkTyConApp tc_ (zipWith (\ f0 f1 -> maybe f0 fst f1) fields0_ fields1_), cos'))+ ty' = mkTyConApp tc_ (zipWith (\ f0 f1 -> maybe f0 fst f1) fields0_ fields1_)+ pure (Just (ty', cos')) else pure Nothing where 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'+ , Just (tc', flds') <- splitTyConApp_maybe ty'+ = go tc' flds' | otherwise = normaliseNatEverywhere givensTyConSubst ty' @@ -291,43 +296,60 @@ ,reifySOP (S s2) ] +-- | Simplify an inequality by first calling 'subtractIneq', producing a SOP+-- term, and then creating a new inequality by moving all the terms with+-- negative coefficients to one side.+--+-- Returns 'Nothing' if it is not able to simplify the original inequality.+simplifyIneq :: Ineq -> Maybe Ineq+simplifyIneq ineq@(x, y, isLE)+ = if x' == x && y' == y+ then Nothing+ else Just (x', y', isLE)+ where+ S ps = subtractIneq ineq+ (neg, pos) = partitionEithers $ map classify ps+ (x', y') =+ if isLE+ then ( S neg, S pos )+ else ( S pos, S neg )+ classify :: CoreProduct -> Either CoreProduct CoreProduct+ classify p@(P (I i : _))+ | i < 0+ = Left $ negateProd p+ classify prod+ = Right prod++negateProd :: CoreProduct -> CoreProduct+negateProd (P (I i : r)) =+ -- preserve normal form+ if i == (-1)+ then+ if null r+ then P [I 1]+ else P r+ else P $ I (negate i) : r+negateProd (P r) = P $ I (-1) : r+ -- | Subtract an inequality, in order to either: -- -- * See if the smallest solution is a natural number -- * Cancel sums, i.e. monotonicity of addition -- -- @--- subtractIneq (2*y <=? 3*x ~ True) = (-2*y + 3*x)--- subtractIneq (2*y <=? 3*x ~ False) = (-3*x + (-1) + 2*y)+-- subtractIneq (2*y <=? 3*x ~ True) = 3*x + (-2)*y+-- subtractIneq (2*y <=? 3*x ~ False) = -3*x + (-2)*y -- @ subtractIneq :: (CoreSOP, CoreSOP, Bool) -> CoreSOP subtractIneq (x,y,isLE) | isLE- = mergeSOPAdd y (mergeSOPMul (S [P [I (-1)]]) x)+ -- NB: keep orientations+ = mergeSOPAdd (mergeSOPMul (S [P [I (-1)]]) x) y | otherwise = mergeSOPAdd x (mergeSOPMul (S [P [I (-1)]]) (mergeSOPAdd y (S [P [I 1]]))) --- | Try to reverse the process of 'subtractIneq'------ E.g.------ @--- subtractIneq (2*y <=? 3*x ~ True) = (-2*y + 3*x)--- sopToIneq (-2*y+3*x) = Just (2*x <=? 3*x ~ True)--- @-sopToIneq- :: CoreSOP- -> Maybe Ineq-sopToIneq (S [P ((I i):l),r])- | i < 0- = Just (mergeSOPMul (S [P [I (negate i)]]) (S [P l]),S [r],True)-sopToIneq (S [r,P ((I i:l))])- | i < 0- = Just (mergeSOPMul (S [P [I (negate i)]]) (S [P l]),S [r],True)-sopToIneq _ = Nothing- -- | Give the smallest solution for an inequality ineqToSubst :: Ineq@@ -361,7 +383,7 @@ substsSOP ((UnifyItem {}):s) u = substsSOP s u 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+substSOP tv e = foldr mergeSOPAdd (S []) . map (substProduct tv e) . unS 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@@ -406,20 +428,25 @@ unifyNats' :: Ct -> CoreSOP -> CoreSOP -> UnifyResult unifyNats' ct u v- = if eqFV u v- then if containsConstants u || containsConstants v- then if u == v- then Win- else Draw (filter diffFromConstraint (unifiers ct u v))- else if u == v- then Win- else Lose- else Draw (filter diffFromConstraint (unifiers ct u v))+ | u == v+ = Win+ | Just unifs <- unifiers ct u v+ , let newUnifs = if isGiven (ctEvidence ct)+ then unifs+ else filter diffFromConstraint unifs+ = Draw newUnifs+ | otherwise+ = Lose where- -- A unifier is only a unifier if differs from the original constraint++ -- A unifier is only a unifier if it differs from the original constraint diffFromConstraint (UnifyItem x y) = not (x == u && y == v)- diffFromConstraint (SubstItem x y) = not (S [P [V x]] == u && y == v) + -- SubstItems can be in different orders+ diffFromConstraint (SubstItem x y) =+ not $ (S [P [V x]] == u && y == v)+ || (S [P [V x]] == v && y == u)+ -- | Find unifiers for two SOP terms -- -- Can find the following unifiers:@@ -453,46 +480,40 @@ -- @ -- [a := b] -- @-unifiers :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]+unifiers :: Ct -> CoreSOP -> CoreSOP -> Maybe [CoreUnify] unifiers ct u@(S [P [V x]]) v- = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 _- | CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct)- -> [SubstItem x v]- _ -> []+ | EqPred NomEq t1 _ <- classifyPredType $ ctEvPred $ ctEvidence ct+ , CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct)+ = return [SubstItem x v] unifiers ct u v@(S [P [V x]])- = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq _ t2- | CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct)- -> [SubstItem x u]- _ -> []+ | EqPred NomEq _ t2 <- classifyPredType $ ctEvPred $ ctEvidence ct+ , CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct)+ = return [SubstItem x u] unifiers ct u@(S [P [C _]]) v- = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2- | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2- -> [UnifyItem u v]- _ -> []+ | EqPred NomEq t1 t2 <- classifyPredType $ ctEvPred $ ctEvidence ct+ , CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2+ = return [UnifyItem u v] unifiers ct u v@(S [P [C _]])- = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2- | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2- -> [UnifyItem u v]- _ -> []+ | EqPred NomEq t1 t2 <- classifyPredType $ ctEvPred $ ctEvidence ct+ , CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2+ = return [UnifyItem u v] unifiers ct u v = unifiers' ct u v -unifiers' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]-unifiers' _ct (S []) (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 -> CoreSOP -> CoreSOP -> Maybe [CoreUnify]+unifiers' _ct (S []) (S []) = return [] -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]+unifiers' _ct (S [P [V x]]) (S []) = return [SubstItem x (S [P [I 0]])]+unifiers' _ct (S []) (S [P [V x]]) = return [SubstItem x (S [P [I 0]])] +unifiers' _ct (S [P [V x]]) s = do+ guard $ canBeNatural s+ return [SubstItem x s]+unifiers' _ct s (S [P [V x]]) = do+ guard $ canBeNatural s+ return [SubstItem x s]+unifiers' _ct s1@(S [P [C {}]]) s2@(S [P [C {}]])+ | s1 == s2+ = return [] -- (z ^ a) ~ (z ^ b) ==> [a := b] unifiers' ct (S [P [E s1 p1]]) (S [P [E s2 p2]])@@ -503,13 +524,13 @@ | all (`elem` p2) s1 = let base = intersect s1 p2 diff = p2 \\ s1- in unifiers ct (S [P diff]) (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]])+ in unifiers' ct (S [P diff]) (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) unifiers' ct (S [P p2]) (S [P [E (S [P s1]) p1]]) | all (`elem` p2) s1 = let base = intersect s1 p2 diff = p2 \\ s1- in unifiers ct (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) (S [P diff])+ in unifiers' ct (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) (S [P diff]) -- (i ^ a) ~ j ==> [a := round (logBase i j)], when `i` and `j` are integers, -- and `ceiling (logBase i j) == floor (logBase i j)`@@ -558,36 +579,25 @@ | otherwise = ps2' psx = intersect ps1 ps2 --- (2 + a) ~ 5 ==> [a := 3]-unifiers' ct (S ((P [I i]):ps1)) (S ((P [I j]):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]+--+-- NB: this also handles situations such as (2 + x) ~ 5 ==> [x := 3]. 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'))+ | Just (s1',s2',_) <- simplifyIneq (s1, s2, True) = 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"+ | Just term_unifs <- termByTerm ct ps1 ps2+ = Just term_unifs+ -- If there are only two variables, try to collect them on either side.+ -- This makes 'termByTerm' more likely to succeed.+ | Just (S coll1, S coll2) <- partitionTerms ps1 ps2+ , Just term_unifs <- termByTerm ct coll1 coll2+ = Just term_unifs | null psx , isGiven (ctEvidence ct) = unifiers'' ct (S ps1) (S ps2) | not $ null psx = unifiers' ct (S ps1'') (S ps2'') where- k1 = subtractIneq (s1,s2,True) ps1' = ps1 \\ psx ps2' = ps2 \\ psx ps1'' | null ps1' = [P [I 0]]@@ -596,14 +606,82 @@ | otherwise = ps2' psx = intersect ps1 ps2 -unifiers' _ s1 s2 = [UnifyItem s1 s2]+unifiers' _ s1 s2 = return [UnifyItem s1 s2] -unifiers'' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]+-- | Try to match the two expressions term-by-term.+-- If this produces a **single unifier**, then we succeed.+--+-- Example: x + 3^(x+2) ~ 2*y - 3^(2*(y+1))+--+-- We recur on each pair, (x, 2*y), (3^(x+2),3^(2*(y+1))).+-- This produces a single unifier "x ~ 2*y", so we proceed.+--+-- NB: this is somewhat fragile: if one moves the terms with negative+-- coefficients to the other side, due to the variable ordering x < y,+-- we would get:+--+-- x + 3^(2*(y+1)) ~ 3^(x+2) + 2*y+--+-- for which the same approach fails. So we use 'partitionTerms' as a heuristic+-- in the case there are only two free variables.+-- See https://github.com/clash-lang/ghc-typelits-natnormalise/issues/96.+termByTerm :: Ct -> [CoreProduct] -> [CoreProduct] -> Maybe [CoreUnify]+termByTerm ct ps1 ps2+ | length ps1 == length ps2+ , length ps1 > 1+ , Just u@[_] <- unifs+ = Just u+ | otherwise+ = Nothing+ where+ unifs = fmap (nub . concat) (zipWithM (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2)++-- | If an equality only contains two free variables, try to collect+-- terms with either FV on either side of the equality.+--+-- This makes 'termByTerm' more likely to succeed.+partitionTerms :: [CoreProduct] -> [CoreProduct] -> Maybe (CoreSOP, CoreSOP)+partitionTerms lhs rhs+ | [fv1, fv2] <- fvs+ , Just (lhs1, lhs2) <- mbPairs fv1 fv2 lhs+ , Just (rhs1, rhs2) <- mbPairs fv1 fv2 rhs+ = Just $+ let (lhs', rhs') =+ if length rhs1 + length lhs2 <= length lhs1 + length rhs2+ then (lhs1 ++ map negateProd rhs1, map negateProd lhs2 ++ rhs2)+ else (map negateProd lhs1 ++ rhs1, lhs2 ++ map negateProd rhs2)+ in (simplifySOP (S lhs'), simplifySOP (S rhs'))+ | otherwise+ = Nothing+ where+ fvs :: [TyVar]+ fvs = nonDetEltsUniqSet $ fvSOP (S $ lhs ++ rhs)++ mbPairs :: TyVar -> TyVar -> [CoreProduct] -> Maybe ([CoreProduct], [CoreProduct])+ mbPairs fv1 fv2 x = partitionEithers <$> traverse ( collect fv1 fv2 ) x++ collect :: TyVar -> TyVar -> CoreProduct -> Maybe (Either CoreProduct CoreProduct)+ collect fv1 fv2 tm =+ let tmFvs = fvProduct tm+ in case (fv1 `elementOfUniqSet` tmFvs, fv2 `elementOfUniqSet` tmFvs) of+ (True, False) -> Just $ Left tm+ (False, True) -> Just $ Right tm+ _ -> Nothing++unifiers'' :: Ct -> CoreSOP -> CoreSOP -> Maybe [CoreUnify] unifiers'' ct (S [P [I i],P [V v]]) s2- | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate i)]]))]+ | isGiven (ctEvidence ct)+ , let s' = mergeSOPAdd s2 (S [P [I (negate i)]])+ = if canBeNatural s'+ then Just [SubstItem v s']+ else Nothing unifiers'' ct s1 (S [P [I i],P [V v]])- | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate i)]]))]-unifiers'' _ _ _ = []+ | isGiven (ctEvidence ct)+ , let s' = mergeSOPAdd s1 (S [P [I (negate i)]])+ = if canBeNatural s'+ then Just [SubstItem v s']+ else Nothing+unifiers'' _ _ _ = Just [] collectBases :: CoreProduct -> Maybe ([CoreSOP],[CoreProduct]) collectBases = fmap unzip . traverse go . unP@@ -624,18 +702,6 @@ fvSymbol (V v) = unitUniqSet v fvSymbol (E s p) = fvSOP s `unionUniqSets` fvProduct p -eqFV :: CoreSOP -> CoreSOP -> Bool-eqFV = (==) `on` fvSOP--containsConstants :: CoreSOP -> Bool-containsConstants =- any (any symbolContainsConstant . unP) . unS- where- symbolContainsConstant c = case c of- C {} -> True- E s p -> containsConstants s || containsConstants (S [p])- _ -> False- safeDiv :: Integer -> Integer -> Maybe Integer safeDiv i j | j == 0 = Just 0@@ -655,12 +721,38 @@ else Just (smallInteger z1) integerLogBase _ _ = Nothing +-- | Might this be a natural number?+--+-- Equivalently: it is not the case that this is definitely not a natural number.+--+-- For example, @-1@ is definitely not a natural number, while @α@ or+-- @-2 * β@ could both be natural numbers (where @α, β@ are metavariables).+canBeNatural :: CoreSOP -> Bool+canBeNatural = maybe True fst . runWriterT . isNatural++-- | Is this a natural number?+--+-- - @Just True@ <=> definitely a natural number+-- - @Just False@ <=> definitely not a natural number+-- - @Nothing@ <=> not sure+--+-- The 'Set CType' writer accumulator returns inner types that must also be+-- positive for the overall 'CoreSOP' to be positive. isNatural :: CoreSOP -> WriterT (Set CType) Maybe Bool isNatural (S []) = return True isNatural (S [P []]) = return True-isNatural (S [P (I i:ps)])- | i >= 0 = isNatural (S [P ps])- | otherwise = return False+isNatural (S [P (I i:ps)]) =+ case compare i 0 of+ EQ -> return True+ GT ->+ -- NB: assumes the SOP term has been normalised, so no possibly of+ -- a second negative constant factor to cancel out this one.+ isNatural (S [P ps])+ LT ->+ -- '-1 * ty' can be a natural number if 'ty' ends up being zero+ if any canBeZero ps+ then WriterT Nothing+ else return False isNatural (S [P (V _:ps)]) = isNatural (S [P ps]) isNatural (S [P (E s p:ps)]) = do sN <- isNatural s@@ -683,6 +775,23 @@ -- if one is natural and the other isn't, then their sum *might* be natural, -- but we simply cant be sure. +-- | Can this 'CoreSymbol' be zero?+--+-- Examples:+--+-- - the literal '0',+-- - a metavariable,+-- - a type family application.+canBeZero :: CoreSymbol -> Bool+canBeZero (I i) = i == 0+canBeZero (C {}) = True -- e.g. 'F 3' where 'F' is a type family+canBeZero (E (S es) _)+ | [P bs] <- es+ = any canBeZero bs+ | otherwise+ = True+canBeZero (V {}) = True -- e.g. 'tau' where 'tau' is an unfilled metavariable+ -- | Try to solve inequalities solveIneq :: Word@@ -802,14 +911,12 @@ -- * SOP version: -2 + x -- * Convert back to inequality: 2 <= x plusMonotone :: IneqRule-plusMonotone want have- | Just want' <- sopToIneq (subtractIneq want)- , want' /= want- = pure [(want',have)]- | Just have' <- sopToIneq (subtractIneq have)- , have' /= have- = pure [(want,have')]-plusMonotone _ _ = noRewrite+plusMonotone want have =+ case (simplifyIneq want, simplifyIneq have) of+ (Just want', Just have') -> pure [(want', have')]+ (Just want', _ ) -> pure [(want', have )]+ (_ , Just have') -> pure [(want , have')]+ _ -> noRewrite -- | Make the `a` of a given `a <= b` smaller haveSmaller :: IneqRule
tests/ErrorTests.hs view
@@ -9,6 +9,7 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances#-} #if __GLASGOW_HASKELL__ >= 805 {-# LANGUAGE NoStarIsType #-}@@ -523,4 +524,43 @@ then litE $ stringL "Couldn't match type ‘1 <=? (m ^ 2)’ with ‘'True’" else litE $ stringL "Couldn't match type `1 <=? (m ^ 2)' with 'True" )]+#endif++type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where+ Drop 0 xs = xs+ Drop n (x ': xs) = Drop (n-1) xs+ Drop n '[] = '[]++t99 :: Proxy ns -> Proxy ( Drop 1 ns ) -> Proxy ( Drop 2 ns )+t99 _ px = px++-- Don't want an error of the form 'Couldn't match 1 with 0'+-- because that means the plugin turned [W] Drop 1 ns ~ Drop 2 ns+-- into 1 ~ 2, which is not valid as Drop is not injective.+t99_errors =+#if __GLASGOW_HASKELL__ >= 811+ [ "Couldn't match type: Drop 1 ns"+ , " with: Drop 2 ns"+ , "Expected: Proxy (Drop 2 ns)"+ , " Actual: Proxy (Drop 1 ns)"+ , $(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "‘Drop’ is a non-injective type family"+ else litE $ stringL "`Drop' is a non-injective type family"+ )+ ]+#else+ [ $(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘Drop 1 ns’ with ‘Drop 2 ns’"+ else litE $ stringL "Couldn't match type `Drop 1 ns' with `Drop 2 ns'"+ )+ , "Expected type: Proxy (Drop 2 ns)"+ , " Actual type: Proxy (Drop 1 ns)"+ , $(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "‘Drop’ is a non-injective type family"+ else litE $ stringL "`Drop' is a non-injective type family"+ )+ ] #endif
tests/Tests.hs view
@@ -363,7 +363,7 @@ . ((x + 1) ~ (2 * y), 1 <= y) => Proxy x -> Proxy y- -> Proxy (((2 * (y - 1)) + 1))+ -> Proxy ((2 * (y - 1)) + 1) -> Proxy x proxyEq3 _ _ x = x @@ -627,6 +627,7 @@ , testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n ~ (n+d)" $ testProxy15 (Proxy :: Proxy 1) `throws` testProxy15Errors , testCase "(n - 1) + 1 ~ n implies (1 <= n)" $ test16 `throws` test16Errors+ , testCase "Do not unify in non-injective positions" $ t99 `throws` t99_errors , testGroup "Inequality" [ testCase "a+1 <= a" $ testProxy9 `throws` testProxy9Errors , testCase "(a <=? a+1) ~ False" $ testProxy10 `throws` testProxy10Errors@@ -723,13 +724,28 @@ #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+t71_aux :: (((1 + m1) + n1) ~ (1 + (m2 + n2))) => Proxy '(m1, n1, m2, n2) -> ()+t71_aux _ = ()+t71 :: ((m1 + n1) ~ (m2 + n2)) => Proxy '(m1, n1, m2, n2) -> ()+t71 px = t71_aux px +-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94+t94 ::+ (KnownNat n, KnownNat m, KnownNat s, s ~ (m - n)) =>+ Proxy m -> Proxy n -> Proxy (s + 2) -> Proxy (s + 2)+t94 _ _ = t94_aux +t94_aux :: (1 <= n) => Proxy n -> Proxy n+t94_aux px = px +-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/96+t96+ :: ( 2 <= x, 2 <= y+ , ( 4 * x + 2 * 2^y ) ~ ( 4 * y + 2 * 2^x )+ )+ => Proxy x -> Proxy y+t96 x = x+ type family TF (a :: Nat) (b :: Nat) :: Nat proxyEq5@@ -747,3 +763,25 @@ -> Proxy b -> Proxy (3 * TF (3 * a) b) theProxy _ _ = Proxy++type family Rank sh where+ Rank '[] = 0+ Rank (_ : sh) = Rank sh + 1+foo :: ( ( 1 + Rank sh ) ~ ( 1 + n ) )+ => Proxy sh -> Proxy n -> Proxy (Rank sh) -> Proxy n+foo _ _ px = px++noContra :: ((Rank sh + 2) <= 2) => Proxy sh -> ()+noContra _ = ()++-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/97+t97 :: ( (1 + n) ~ m, ( m - 1 ) ~ n ) => Proxy m -> Proxy n -> ()+t97 _ _ = ()++t97b+ :: ( n ~ (m - 2)+ , (n + 1) ~ (m - 1)+ , m ~ (n + 2)+ )+ => Proxy n -> Proxy m -> ()+t97b _ _ = ()