ghc-typelits-natnormalise 0.9.1 → 0.9.2
raw patch · 6 files changed
+336/−106 lines, 6 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
+ GHC.TypeLits.Normalise: instance GHC.Utils.Outputable.Outputable GHC.TypeLits.Normalise.NatCt
Files
- CHANGELOG.md +4/−0
- ghc-typelits-natnormalise.cabal +1/−1
- src/GHC/TypeLits/Normalise.hs +282/−98
- src/GHC/TypeLits/Normalise/Unify.hs +2/−0
- tests/ErrorTests.hs +35/−7
- tests/Tests.hs +12/−0
CHANGELOG.md view
@@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.9.2 *December 2nd 2025*+* Fixes [#108](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/108) Type error after plugin update+* Fixes [#111](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/111) Exception for unifying under non-injective type families+ ## 0.9.1 *October 21st 2025* * Fixes [#105](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/105) Unsound derived contradiction with 0.9.0 * Support for GHC 9.14
ghc-typelits-natnormalise.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: ghc-typelits-natnormalise-version: 0.9.1+version: 0.9.2 synopsis: GHC typechecker plugin for types of kind GHC.TypeLits.Nat description: A type checker plugin for GHC that can solve /equalities/ and /inequalities/
src/GHC/TypeLits/Normalise.hs view
@@ -143,6 +143,7 @@ where /n-l/ is a negative number. -} +{-# LANGUAGE CPP #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ExplicitNamespaces #-}@@ -165,7 +166,7 @@ import Control.Arrow ( second ) import Control.Monad- ( (<=<) )+ ( (<=<), unless ) import Control.Monad.Trans.Writer.Strict ( WriterT(runWriterT), runWriter ) import Data.Either@@ -174,7 +175,7 @@ import Data.List ( stripPrefix, partition ) import Data.Maybe- ( mapMaybe, catMaybes, fromMaybe )+ ( mapMaybe, catMaybes, fromMaybe, isJust ) import Data.Traversable ( for ) import Text.Read@@ -205,7 +206,7 @@ import GHC.TcPlugin.API.TyConSubst ( TyConSubst, mkTyConSubst ) import GHC.Plugins- ( Plugin(..), defaultPlugin, purePlugin )+ ( Plugin(..), defaultPlugin, purePlugin, allVarSet, isEmptyVarSet, tyCoVarsOfType ) import GHC.Utils.Outputable -- ghc-typelits-natnormalise@@ -214,6 +215,12 @@ ( SOP(S), Product(P), Symbol(V) ) import GHC.TypeLits.Normalise.Unify +-- transformers+import Control.Monad.Trans.Class+ ( lift )+import Control.Monad.Trans.State.Strict+ ( StateT, evalStateT, get, modify )+ -------------------------------------------------------------------------------- -- | To use the plugin, add@@ -289,18 +296,40 @@ vcat [ text "givens:" <+> ppr givens ] -- Try to find contradictory Givens, to improve pattern match warnings.- SimplifyResult _simpls contras <-+ SimplifyResult { simplifiedWanteds, contradictions, newGivens } <- simplifyNats opts tcs [] $- concatMap (toNatEquality tcs givensTyConSubst) redGivens+ concatMap (toNatEquality opts tcs givensTyConSubst) redGivens++ -- Only enter actual new evidence into the solver loop, i.e. we could derive+ -- a new given in our solver loop for which there already is existing evidence.+ -- We have no use for two different proofs of the same fact.+ let givensPreds = map (CType . ctEvPred . ctEvidence) givens+ actuallyNewGivens =+ filter ((`notElem` givensPreds) . CType . ctEvPred . ctEvidence) newGivens+ -- For now, only admit improved givens in the form of `n ~ L`, where `n` is+ -- a type variable and `L` is a numeric literal.+ let simplNewGivens = filter+ ( \case {EqPred NomEq t1 t2 -> isTyVarTy t1 && isJust (isNumLitTy t2); _ -> False}+ . classifyPredType+ . ctEvPred+ . ctEvidence+ ) actuallyNewGivens+ tcPluginTrace "decideEqualSOP Givens }" $ vcat [ text "givens:" <+> ppr givens- , text "simpls:" <+> ppr _simpls- , text "contra:" <+> ppr contras ]+ , text "simpls:" <+> ppr simplifiedWanteds+ , text "contra:" <+> ppr contradictions+ , text "new:" <+> ppr simplNewGivens+ ] return $ mkTcPluginSolveResult- ( map fromNatEquality contras )+#if MIN_VERSION_ghc(9,14,0)+ ( map fromNatEquality contradictions )+#else+ []+#endif [] -- no solved Givens- [] -- no new Givens+ simplNewGivens -- Solving phase. -- Solves in/equalities on Nats and simplifiable constraints@@ -311,7 +340,7 @@ then [] else wanteds0 ++ deriveds givensTyConSubst = mkTyConSubst givens- unit_wanteds0 = concatMap (toNatEquality tcs givensTyConSubst) wanteds+ unit_wanteds0 = concatMap (toNatEquality opts tcs givensTyConSubst) wanteds nonEqs = filter ( not . (\p -> isEqPred p || isEqClassPred p) . ctEvPred@@ -341,18 +370,18 @@ -- that is to be added to new [W]anteds. let mkNegWanted ( CType wtdPred ) loc = mkNonCanonical <$> newWanted loc wtdPred ineqForRedWants <- Map.traverseWithKey mkNegWanted negWanteds- let unit_givens = concatMap (toNatEquality tcs givensTyConSubst) redGivens- unit_wanteds = unit_wanteds0 ++ concatMap (toNatEquality tcs givensTyConSubst) ineqForRedWants- sr@(SimplifyResult evs contras) <- simplifyNats opts tcs unit_givens unit_wanteds+ let unit_givens = concatMap (toNatEquality opts tcs givensTyConSubst) redGivens+ unit_wanteds = unit_wanteds0 ++ concatMap (toNatEquality opts tcs givensTyConSubst) ineqForRedWants+ sr@SimplifyResult{simplifiedWanteds, contradictions} <-+ simplifyNats opts tcs unit_givens unit_wanteds tcPluginTrace "normalised" (ppr sr) reds <- for reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do wants <- evSubtPreds (ctLoc origCt) $ subToPred opts tcs ws return ((term, origCt), wDicts ++ wants)- let 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+ let -- Only solve a Derived when there are Wanteds in play+ simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) simplifiedWanteds ++ reds of [] -> []- _ -> simpld+ _ -> simplifiedWanteds (solved,newWanteds) = second concat (unzip $ simpld1 ++ reds) tcPluginTrace "decideEqualSOP Wanteds }" $@@ -370,7 +399,7 @@ ] return $ mkTcPluginSolveResult- (map fromNatEquality contras)+ (map fromNatEquality contradictions) solved newWanteds @@ -470,17 +499,73 @@ data SimplifyResult = SimplifyResult- { simplified :: [((EvTerm,Ct),[Ct])]- , impossible :: [Either NatEquality NatInEquality]+ { simplifiedWanteds :: [((EvTerm,Ct),[Ct])]+ -- ^ List of:+ -- * Tuple of:+ -- * Evidence for:+ -- * The solved Wanted+ -- * Preconditions (in the for of new Wanteds)+ , contradictions :: [Either NatEquality NatInEquality]+ -- ^ List of contradictions+ , newGivens :: [Ct]+ -- ^ Givens derived in the improve givens stage } instance Outputable SimplifyResult where- ppr (SimplifyResult { simplified, impossible }) =- text "SimplifyResult { simplified =" <+> ppr simplified- <+> text ", impossible =" <+> ppr impossible <+> text "}"+ ppr (SimplifyResult { simplifiedWanteds, contradictions, newGivens }) =+ text "SimplifyResult { simplified =" <+> ppr simplifiedWanteds+ <+> text ", impossible =" <+> ppr contradictions+ <+> text ", new_givens =" <+> ppr newGivens <+> text "}" -type NatCt = (Either NatEquality NatInEquality, [(Type,Type)], [Coercion])+data NatCt+ = NatCt+ { predicate :: Either NatEquality NatInEquality+ -- ^ Predicate: either an equality or inequality+ , preconds :: [PredType]+ -- ^ Preconditions (in the form of inequalities encoded as PredTypes)+ , ctDeps :: [Coercion]+ -- ^ Coercion(s) from which the predicate is derived, needed so that evidence+ -- doesn't float above the coercions from which it is derived.+ } +instance Outputable NatCt where+ ppr (NatCt {predicate, preconds, ctDeps}) =+ text "NatCt { predicate = " <+> ppr predicate+ <+> text ", preconditions = " <+> ppr preconds+ <+> text ", dependencies = " <+> ppr ctDeps <+> text "}"++data SimplifyState+ = SimplifyState+ { stDeps :: [Coercion]+ -- ^ Coercions on which the simplified evidence depends, this needs to be+ -- kept around because sometimes we solving one constraint (which has a+ -- depedency) is used to solve another constraint+ , subst :: [CoreUnify]+ -- ^ Derived simplifications (i.e. b ~ c derived from (a + b) ~ (a + c)),+ -- and substitutions (i.e. n := 0 derived from y ^ n ~ 1)+ , evs :: [((EvTerm,Ct),[Ct])]+ -- ^ Collected evidence+ , leqsG :: [(CoreSOP,CoreSOP,Bool)]+ -- ^ Given inequalities+ , unsolved :: [NatCt]+ -- ^ Tried, but unsolved predicates. We keep them around in case we solve a+ -- new predicate which could lead to a substitution that enables a solve.+ , derivedGivens :: [Ct]+ -- ^ Unifiers derived from Givens. E.g. when we have /[G] x ^ n ~ 1/, this+ -- field will hold a derived /[G] n ~ 0/.+ }++emptySimplifyState :: SimplifyState+emptySimplifyState+ = SimplifyState+ { stDeps = []+ , subst = []+ , evs = []+ , leqsG = []+ , unsolved = []+ , derivedGivens = []+ }+ simplifyNats :: Opts -- ^ Allow negated numbers (potentially unsound!)@@ -490,15 +575,15 @@ -> [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+simplifyNats Opts{depth} tcs eqsG eqsW = do+ let eqsG1 = map (\nCt -> nCt{preconds = []}) eqsG+ (varEqs, otherEqs) = partition (isVarEqs . predicate) eqsG1 fancyGivens = concatMap (makeGivensSet otherEqs) varEqs case varEqs of [] -> do let eqs = otherEqs ++ eqsW tcPluginTrace "simplifyNats" (ppr eqs)- simples [] [] [] [] [] eqs+ evalStateT (simples eqs) emptySimplifyState _ -> do tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")") (ppr varEqs)@@ -506,54 +591,90 @@ allSimplified <- for fancyGivens $ \v -> do let eqs = v ++ eqsW tcPluginTrace "simplifyNats" (ppr eqs)- simples [] [] [] [] [] eqs+ evalStateT (simples eqs) emptySimplifyState - pure (foldr findFirstSimpliedWanted (SimplifyResult [] []) allSimplified)+ pure (foldr findFirstSimpliedWanted (SimplifyResult [] [] []) allSimplified) where- simples :: [Coercion]- -> [CoreUnify]- -> [((EvTerm, Ct), [Ct])]- -> [(CoreSOP,CoreSOP,Bool)]- -> [NatCt]- -> [NatCt]- -> TcPluginM Solve SimplifyResult- simples _ _subst evs _leqsG _xs [] = return (SimplifyResult evs [])- simples deps subst evs leqsG xs (eq@(lr@(Left (ct,u,v)),k,deps2):eqs') = do+ simples ::+ [NatCt] ->+ StateT SimplifyState (TcPluginM Solve) SimplifyResult+ simples [] = do+ SimplifyState{evs, derivedGivens} <- get+ return SimplifyResult { simplifiedWanteds = evs+ , contradictions = []+ , newGivens = derivedGivens+ }+ simples (eq@NatCt{predicate=(Left (ct,u,v)), preconds, ctDeps}:eqs) = do+ SimplifyState{stDeps, subst, evs, leqsG, unsolved, derivedGivens} <- get+ let allDeps = stDeps ++ ctDeps+ let u' = substsSOP subst u v' = substsSOP subst v- ur <- unifyNats ct u' v'- tcPluginTrace "unifyNats result" (ppr ur)+ ur <- lift (unifyNats ct u' v')+ lift (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)- tcPluginTrace "unifyNats Win" $- vcat [ text "evs:" <+> ppr evs- , text "evs':" <+> ppr evs'- , text "ct:" <+> ppr ct- ]- simples deps subst evs' leqsG [] (xs ++ eqs')+ -- Do note record "new" evidence for given constraints.+ unless (isGiven (ctEvidence ct)) $ do+ -- Only recorde evidence for wanted contstraints+ evM <- lift (evMagic tcs ct allDeps mempty preconds)+ lift $ tcPluginTrace "unifyNats Win" $+ vcat [ text "evM:" <+> ppr evM+ , text "ct:" <+> ppr ct+ ]+ modify (\s -> s {evs = maybe evs (:evs) evM})+ simples eqs Lose ->- addContra 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' ++- subToPred opts tcs k)+ addContra (predicate eq) <$> simples eqs+ Draw [] -> do+ -- No progress made, add it to the "unsolved" list, in the hope we+ -- can make progress when we later find a new substitution+ modify (\s -> s {unsolved = eq:unsolved})+ simples eqs+ Draw unifications -> do -- We made some progress in the form of a unifier - tcPluginTrace "unifyNats: Draw (non-empty subst)" $- vcat [ text "subst':" <+> ppr subst'- , text "evM:" <+> ppr evM ]+ -- As the derived unifiers we record here can lead to solving another+ -- equation, we add it and its dependencies to the list of global+ -- dependencies which we use when creating new evidence+ let stDeps1 = ctEvCoercion (ctEvidence ct):allDeps+ -- We add apply the derived unification in the existing set of+ -- unification, and also add the derived unificaiton to the global+ -- state; to be used in solving later equations.+ let subst1 = substsSubst unifications subst ++ unifications+ if isGiven (ctEvidence ct) then do+ if null preconds then do+ -- We only record the unification derived from a given constraint+ -- when it has no preconditions in order for this unification to+ -- hold. The reason for that is that we can currently not record+ -- new Wanteds to be emitted at the end of the solve.+ givensU <- lift (mapM (unifyItemToGiven (ctLoc ct) allDeps) unifications)+ modify (\s -> s { stDeps = stDeps1+ , subst = subst1+ , leqsG = eqToLeq u' v' ++ leqsG+ , unsolved = []+ , derivedGivens = givensU ++ derivedGivens+ })+ simples (unsolved ++ eqs)+ else+ simples eqs+ else do+ let allPreconds = map unifyItemToPredType unifications ++ preconds+ evM <- lift (evMagic tcs ct allDeps Set.empty allPreconds)+ case evM of+ Nothing ->+ simples eqs+ Just ev -> do+ -- We only record the unification derived from a wanted constraint+ -- when we can actually record evidence for a succesful solve.+ modify (\s -> s { stDeps = stDeps1+ , subst = subst1+ , evs = ev:evs+ , unsolved = []+ })+ simples (unsolved ++ eqs) - 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+ simples (eq@NatCt{predicate=Right (ct,u@(x,y,b)), preconds, ctDeps}:eqs) = do+ SimplifyState{stDeps, subst, evs, leqsG, unsolved} <- get let u' = substsSOP subst (subtractIneq u) x' = substsSOP subst x y' = substsSOP subst y@@ -562,16 +683,18 @@ | otherwise = leqsG ineqs = concat [ leqsG , map (substLeq subst) leqsG- , map snd (rights (map (\ (lr', _, _) -> lr') eqsG))+ , map snd (rights (map predicate eqsG)) ]- tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs))+ allDeps = stDeps ++ ctDeps+ lift (tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs))) case runWriterT (isNatural u') of Just (True,knW) -> do- evs' <- maybe evs (:evs) <$> evMagic tcs ct deps knW (subToPred opts tcs k)- simples deps subst evs' leqsG' xs eqs'+ evs' <- maybe evs (:evs) <$> lift (evMagic tcs ct allDeps knW preconds)+ modify (\s -> s {evs = evs', leqsG = leqsG'})+ simples eqs - Just (False,_) | null k ->- addContra lr <$> simples deps subst evs leqsG xs eqs'+ Just (False,_) | null preconds ->+ addContra (predicate eq) <$> simples eqs _ -> do let solvedIneq = mapMaybe runWriterT -- it is an inequality that can be instantly solved, such as@@ -589,15 +712,20 @@ 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'+ evs' <- maybe evs (:evs) <$> lift (evMagic tcs ct allDeps kW preconds)+ modify (\s -> s { stDeps = allDeps+ , evs = evs'+ , leqsG = leqsG'+ })+ simples eqs+ _ -> do+ modify (\s -> s {unsolved = eq:unsolved})+ simples eqs eqToLeq x y = [(x,y,True),(y,x,True)] substLeq s (x,y,b) = (substsSOP s x, substsSOP s y, b) - isVarEqs (Left (_,S [P [V _]], S [P [V _]]), _, _) = True+ isVarEqs (Left (_,S [P [V _]], S [P [V _]])) = True isVarEqs _ = False makeGivensSet :: [NatCt] -> NatCt -> [[NatCt]]@@ -605,7 +733,7 @@ = let (noMentionsV,mentionsV) = partitionEithers (map (matchesVarEq varEq) otherEqs) (mentionsLHS,mentionsRHS) = partitionEithers mentionsV- vS = swapVar varEq+ vS = varEq {predicate = swapVar (predicate varEq)} givensLHS = case mentionsLHS of [] -> [] _ -> [mentionsLHS ++ ((varEq:mentionsRHS) ++ noMentionsV)]@@ -619,7 +747,7 @@ matchesVarEq :: NatCt -> NatCt -> Either NatCt (Either NatCt NatCt)- matchesVarEq (Left (_, S [P [V v1]], S [P [V v2]]), _, _) r@(e, _, _) =+ matchesVarEq NatCt{predicate = Left (_, S [P [V v1]], S [P [V v2]])} r@(NatCt e _ _) = case e of Left (_,S [P [V v3]],_) | v1 == v3 -> Right (Left r)@@ -636,19 +764,19 @@ _ -> 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 (Left (ct,S [P [V v1]], S [P [V v2]])) =+ Left (ct,S [P [V v2]], S [P [V v1]]) swapVar _ = error "internal error" - findFirstSimpliedWanted s1@(SimplifyResult evs imposs) s2- | not (null imposs)- || any (isWanted . ctEvidence . snd . fst) evs+ findFirstSimpliedWanted s1@(SimplifyResult {simplifiedWanteds, contradictions}) s2+ | not (null contradictions)+ || any (isWanted . ctEvidence . snd . fst) simplifiedWanteds = s1 | otherwise = s2 addContra :: Either NatEquality NatInEquality -> SimplifyResult -> SimplifyResult-addContra contra sr = sr { impossible = contra : impossible sr }+addContra contra sr = sr { contradictions = contra : contradictions sr } -- If we allow negated numbers we simply do not emit the inequalities -- derived from the subtractions that are converted to additions with a@@ -661,20 +789,20 @@ 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+toNatEquality :: Opts -> LookedUpTyCons -> TyConSubst -> Ct -> [NatCt]+toNatEquality opts tcs givensTyConSubst ct0 | Just (((x,y), mbLTE), cos0) <- isNatRel tcs givensTyConSubst pred0 , let ((x', cos1),k1) = runWriter (normaliseNat x) ((y', cos2),k2) = runWriter (normaliseNat y)- ks = k1 ++ k2+ preds = subToPred opts tcs (k1 ++ k2) = case mbLTE of Nothing -> -- Equality constraint: x ~ y- [(Left (ct0, x', y'), ks, cos0 ++ cos1 ++ cos2)]+ [NatCt (Left (ct0, x', y')) preds (cos0 ++ cos1 ++ cos2)] Just b -> -- Inequality constraint: (x <=? y) ~ b- [(Right (ct0, (x', y', b)), ks, cos0 ++ cos1 ++ cos2)]+ [NatCt (Right (ct0, (x', y', b))) preds (cos0 ++ cos1 ++ cos2)] | otherwise = case classifyPredType pred0 of EqPred NomEq t1 t2@@ -685,12 +813,13 @@ | isGiven (ctEvidence ct0) , className kn == knownNatClassName , let ((x', cos0), ks) = runWriter (normaliseNat x)- -> [(Right (ct0, (S [], x', True)), ks, cos0)]+ , let preds = subToPred opts tcs ks+ -> [NatCt (Right (ct0, (S [], x', True))) preds cos0] _ -> [] where pred0 = ctPred ct0 -- x ~ y- goNomEq :: Type -> Type -> [(Either NatEquality NatInEquality, [(Type,Type)], [Coercion])]+ goNomEq :: Type -> Type -> [NatCt] goNomEq lhs rhs -- Recur into a TyCon application for TyCons that we **do not** rewrite, -- e.g. peek inside the Maybe in 'Maybe (x + y) ~ Maybe (y + x)'.@@ -706,18 +835,48 @@ case tyConInjectivityInfo tc of Injective inj -> filterByList (inj ++ repeat True) xys- _ -> drop (tyConArity tc) xys- = concatMap (uncurry rewrite) subs+ _ ->+ -- However, it is okay to recur in the following specific+ -- exception:+ let (tcArgs,rest) = splitAt (tyConArity tc) xys+ diffs = filter (not . uncurry eqType) tcArgs+ in case diffs of+ -- 1. The types only differ in one argument position+ [(x,y)]+ | let xFVs = tyCoVarsOfType x+ , let yFVs = tyCoVarsOfType y+ -- 2. The argument must have variables, and they must+ -- all be skolem variables.+ , not (isEmptyVarSet xFVs)+ , allVarSet isSkolemTyVar xFVs+ -- 3. The variables in both argument postions must+ -- be the same.+ , xFVs == yFVs+ -> (x,y):rest+ _ -> rest+ = case concatMap (uncurry rewrite) subs of+ [] -> []+ [rw] -> [rw]+ rws ->+ -- For Given Cts, it's fine to extract multiple (in)equalities. However,+ -- for Wanted Cts we should not claim to solve the entire Ct when we+ -- only solve a part of the Ct. So when we can extra two or more inequalities+ -- from a Wanted Ct, we conservatively choose not to solve any of them.+ if isGiven (ctEvidence ct0) then+ rws+ else+ [] | otherwise = rewrite lhs rhs - rewrite :: Type -> Type -> [(Either NatEquality NatInEquality, [(Type,Type)], [Coercion])]+ rewrite :: Type -> Type -> [NatCt] rewrite x y | isNatKind (typeKind x) , isNatKind (typeKind y) , let ((x', cos1),k1) = runWriter (normaliseNat x) , let ((y', cos2),k2) = runWriter (normaliseNat y)- = [(Left (ct0,x',y'),k1 ++ k2, cos1 ++ cos2)]+ , let preds = subToPred opts tcs (k1 ++ k2)+ = [NatCt (Left (ct0,x',y')) preds (cos1 ++ cos2)] | otherwise = [] @@ -734,10 +893,35 @@ SubstItem {..} -> reifySOP siSOP UnifyItem {..} -> reifySOP siRHS ++unifyItemToGiven :: CtLoc -> [Coercion] -> CoreUnify -> TcPluginM Solve Ct+unifyItemToGiven loc deps ui = mkNonCanonical <$> newGiven loc pty (EvExpr (Coercion co))+ where+ ty1 = case ui of+ SubstItem {..} -> mkTyVarTy siVar+ UnifyItem {..} -> reifySOP siLHS+ ty2 = case ui of+ SubstItem {..} -> reifySOP siSOP+ UnifyItem {..} -> reifySOP siRHS++ pty = mkEqPredRole Nominal ty1 ty2+ co = mkPluginUnivCo "ghc-typelits-natnormalise" Nominal deps ty1 ty2+ evSubtPreds :: CtLoc -> [PredType] -> TcPluginM Solve [Ct] evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc) -evMagic :: LookedUpTyCons -> Ct -> [Coercion] -> Set CType -> [PredType] -> TcPluginM Solve (Maybe ((EvTerm, Ct), [Ct]))+evMagic ::+ -- | Known TyCon environment+ LookedUpTyCons ->+ -- | Constraint for which we are creating evidence+ Ct ->+ -- | Coercions in which the evidence depends+ [Coercion] ->+ -- | Types that we should be known to be a Natural+ Set CType ->+ -- | Inequalities that should hold+ [PredType] ->+ TcPluginM Solve (Maybe ((EvTerm, Ct), [Ct])) evMagic tcs ct deps knW preds = do holeWanteds <- evSubtPreds (ctLoc ct) preds knWanted <- mapM (mkKnWanted (ctLoc ct)) (Set.elems knW)
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -555,10 +555,12 @@ -- 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]]) | Just k <- safeDiv j i+ , not (null ps) = unifiers' ct (S [P ps]) (S [P [I k]]) unifiers' ct (S [P [I j]]) (S [P ((I i):ps)]) | Just k <- safeDiv j i+ , not (null ps) = unifiers' ct (S [P ps]) (S [P [I k]]) -- (2*a) ~ (2*b) ==> [a := b]
tests/ErrorTests.hs view
@@ -40,7 +40,11 @@ testProxy1 = id testProxy1Errors =-#if __GLASGOW_HASKELL__ >= 900+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (2 + x)"+ ," Actual: Proxy (x + 1)"+ ]+#elif __GLASGOW_HASKELL__ >= 900 ["Expected: Proxy (x + 1) -> Proxy (2 + x)" ," Actual: Proxy (x + 1) -> Proxy (x + 1)" ]@@ -58,7 +62,11 @@ testProxy2 = id testProxy2Errors =-#if __GLASGOW_HASKELL__ >= 900+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (x + GCD 9 6)"+ ," Actual: Proxy (2 + x)"+ ]+#elif __GLASGOW_HASKELL__ >= 900 ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)" ," Actual: Proxy (2 + x) -> Proxy (2 + x)" ]@@ -75,7 +83,11 @@ testProxy3 = proxyFun3 testProxy3Errors =-#if __GLASGOW_HASKELL__ >= 900+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy ((x0 + x0) + x0)"+ ," Actual: Proxy 8"+ ]+#elif __GLASGOW_HASKELL__ >= 900 ["Expected: Proxy 8 -> ()" ," Actual: Proxy ((x0 + x0) + x0) -> ()" ]@@ -92,7 +104,11 @@ testProxy4 = proxyFun4 testProxy4Errors =-#if __GLASGOW_HASKELL__ >= 900+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy ((2 * 0) + 4)"+ ," Actual: Proxy 2"+ ]+#elif __GLASGOW_HASKELL__ >= 900 ["Expected: Proxy 2 -> ()" ," Actual: Proxy ((2 * 0) + 4) -> ()" ]@@ -106,7 +122,11 @@ testProxy5 = proxyFun4 testProxy5Errors =-#if __GLASGOW_HASKELL__ >= 900+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy ((2 * y0) + 4)"+ ," Actual: Proxy 7"+ ]+#elif __GLASGOW_HASKELL__ >= 900 ["Expected: Proxy 7 -> ()" ," Actual: Proxy ((2 * y0) + 4) -> ()" ]@@ -144,7 +164,11 @@ testProxy8 = id testProxy8Errors =-#if __GLASGOW_HASKELL__ >= 900+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (y + x)"+ ," Actual: Proxy x"+ ]+#elif __GLASGOW_HASKELL__ >= 900 ["Expected: Proxy x -> Proxy (y + x)" ," Actual: Proxy x -> Proxy x" ]@@ -408,7 +432,11 @@ testProxy15 = id testProxy15Errors =-#if __GLASGOW_HASKELL__ >= 900+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (n + d)"+ ," Actual: Proxy n"+ ]+#elif __GLASGOW_HASKELL__ >= 900 ["Expected: Proxy n -> Proxy (n + d)" ," Actual: Proxy n -> Proxy n" ]
tests/Tests.hs view
@@ -512,6 +512,15 @@ go :: 1 <= b => Proxy a -> Proxy a go = id +isOkay ::+ forall x y sh .+ Proxy x ->+ Proxy y ->+ Proxy sh ->+ Proxy (Drop (x + y) sh) ->+ Proxy (Drop (y + x) sh)+isOkay _ _ _ px = px+ main :: IO () main = defaultMain tests @@ -555,6 +564,9 @@ "Proxy" , testCase "(((2 ^ x) - 2) * (2 ^ (x + x))) ~ ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1))))" $ show (proxyEq2 @2 Proxy) @?=+ "Proxy"+ , testCase "Unify in non-injective positions under specific conditions" $+ show (isOkay @2 @3 @'[] Proxy Proxy Proxy Proxy) @?= "Proxy" ] , testGroup "Implications"