Note [Multiplicity in deep subsumption]
Consider
t1 ->{mt} t2 <= s1 ->{ms} s2
At the moment we /unify/ ms~mt, via tcEqMult.
Arguably we should use `tcSubMult`. But then if mt=m0 (a unification
variable) and ms=Many, `tcSubMult` is a no-op (since anything is a
sub-multiplicty of Many). But then `m0` may never get unified with
anything. It is then skolemised by the zonker; see GHC.HsToCore.Binds
Note [Free tyvars on rule LHS]. So we in RULE foldr/app in GHC.Base
we get this
"foldr/app" [1] forall ys m1 m2. foldr (\x{m1} \xs{m2}. (:) x xs) ys
= \xs -> xs ++ ys
where we eta-expanded that (:). But now foldr expects an argument
with ->{Many} and gets an argument with ->{m1} or ->{m2}, and Lint
complains.
The easiest solution was to unify the multiplicities in tc_sub_type_deep,
insisting on equality. This is only in the DeepSubsumption code anyway. References 1
- Free tyvars on rule LHS GHC.Tc.Zonk.Type
Referenced by 1
- GHC.Tc.Utils.Unify call site