Example of delayed resolution of multiplicity constraints
Merge request reports
Activity
requested review from @simonpj
mentioned in issue #25130
1550 1550 How can we check that every call to `tcSubMult` returns `Refl`? 1551 1551 It might not be `Refl` *yet*. 1552 1552 1553 [TODO: add counterexample #25130] 1553 For instance 1554 1555 f :: T -> String 1556 f x = case x of 1557 MkT y -> "" 1558 1559 data T = forall a. MkT a 1560 1561 Here the case expression generates a unification variable p, for the 1562 multiplicity at which it consumes the scrutinee, and gives y multiplicity 1563 p. Since y isn't used, p is unified with Many. However, because of the I don't understand this. Here
fhas a type signaturef :: T %n-> String, where I have made explicit the multiplicity. But what isn? It's a complete type signature, so there is nothing unknown about it.Anyway
xends up in the envt with that multiplicity:x ::_n T, I think. Correct?OK now we get to the case expression. Maybe at a
caseexpression we always make up a fresh multiplicitypto say how the scrutinee is used? (Is this described anywhere?) Let's suppose we do that.Now we have the pattern
MkT y. Does that "see"pin any way? If so how? Maybe you are saying that we addyto the envt with typey ::_p a, whereais the existentially bound variable?"Since y isn't used, p is unified with Many". Where does that happen?
This section is all about submultiplicty constraints being Refl. In this example, precisely which bit of code generates the submultiplicity-constraint-that-must-be-Ref?
TL;DR: I think more detail would help. Perhaps a simpler example to start with? The simpler example can ignore the "might only be unified later" issue -- that topic can be the follow up ... "you might think that we can check for Refl right away, but this example shows..."
I don't understand this. Here
fhas a type signaturef :: T %n-> String, where I have made explicit the multiplicity. But what isn? It's a complete type signature, so there is nothing unknown about it.The meaning
T -> Stringis alwaysT %Many -> String.Anyway
xends up in the envt with that multiplicity:x ::_n T, I think. Correct?Yes. Where
nisManyOK now we get to the case expression. Maybe at a
caseexpression we always make up a fresh multiplicitypto say how the scrutinee is used? (Is this described anywhere?) Let's suppose we do that.Indeed, this is what happens. I'm lacking a name for that (a lot of my documentation on linear types is plagued by my lack of creativity with naming stuff). The fact that case expressions have a multiplicity like this is described in the paper and the Linear Core document. The fact that this multiplicity is inferred is described in the proposal (we have not, on the other hand, even designed a syntax for making this multiplicity explicit
Now we have the pattern
MkT y. Does that "see"pin any way? If so how? Maybe you are saying that we addyto the envt with typey ::_p a, whereais the existentially bound variable?Indeed. Specifically, the multiplicity of
yin the environment is the multiplicity of the field (here1), multiplied by the multiplicity of the case (herep)."Since y isn't used, p is unified with Many". Where does that happen?
Are you looking for the precise function? It happens here: https://gitlab.haskell.org/ghc/ghc/-/blob/076c1a104f55750a49de03694786180bd78eb9b6/compiler/GHC/Tc/Gen/Pat.hs#L626-627 .
This section is all about submultiplicty constraints being Refl. In this example, precisely which bit of code generates the submultiplicity-constraint-that-must-be-Ref?
Every binder generates submultiplicity constraints, here it's the
ybinder which is our concern.TL;DR: I think more detail would help. Perhaps a simpler example to start with? The simpler example can ignore the "might only be unified later" issue -- that topic can be the follow up ... "you might think that we can check for Refl right away, but this example shows..."
The goal of this example was specifically to answer this recurring question: why do we need to emit a constraint at all and can't solve submultiplicity constraints eagerly. Ok to move it a little out of the way if it feels distracting. I'm not too sure that this note needs another example, though. What an example of would it be?
why do we need to emit a constraint at all and can't solve submultiplicity constraints eagerly
Exactly. So I need to see spot in the code where we say
co <- unify m1 m2; emitMultiplicityCheck co, where it would not be OK to sayzonk t1; zonk t2; compare them for equality.My point is that it'd be great to show an example where that is ok; but then show another where it isn't. At the moment, despite your explanation, I can't see the spot where that unification-that-should-be-refl takes place in GHC's source code, for the particular example you chose.
