Note [Multiplicity in deep subsumption]

GHC/Tc/Utils/Unify.hs:1835 compiler

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

Referenced by 1