Make [list_labels] pure

[goldfirere]

In the handling of the unerasable argument warning, we have to check whether a function has any unlabeled arguments remaining. The check requires expansion, which affects GADT typing. This update makes the list_labels function pure, avoiding a degradation in typing from the unerasable argument check.

The first commit adds the failing test; the second commit fixes the bug and updates the test.

[gasche]

Two quick comments:

• It is not obvious to me that this is correct. list_labels does rely on looking inside GADT equalities, so it could introduce a dependency on them. The patch changes it to not track these dependencies, which might introduce principality issues.
• I don't understand why the example breaks. The example uses a function type fun ?x:_ (() : a) -> (), which has a type of the form ?x:_ -> a -> unit. Listing the labels requires expanding types on the spine of the function type, but the example fails (I think?) because the definition a = unit is expanded in the process. That should not be necessary, why does it happen?

[goldfirere]

You make a good point. I think list_labels should not be pure in the way I have done in this patch.

I understand the example differently, though. There are two examples in the added tests with optional parameters:

1. fun ?x:_ () : a -> ()
2. fun () ?x:_ : a -> ()

In both cases, the return type of the function is a, and so looking for labels in the spine of the function requires expanding a. In the first case, we already know there is a nonlabeled argument before looking at a, but the check in the code does not short-circuit. In the second case, expanding a really is necessary in order to get the warning right.

However, it seems quite unfortunate that the unerasable argument warning should cause a type error in cases like this. Instead, I think it might be an improvement for the unerasable argument check to produce one of three possibilities: 1. all good (there is a non-labeled argument following the optional one); 2. bad (there is definitely not a non-labeled following argument); or 3. not sure (there is not an obvious non-labeled argument, but perhaps by expanding through types, there would be). We could warn in cases 2 and 3 (with different warnings). If a programmer hits case 3 and the warning is wrong, presumably a different type annotation would silence the warning. One challenge here is that I don't easily know how to expand non-gadt equalities while not expand gadt equalities.

Or maybe the existing behavior is OK, in which case I still think checking in the tests would be good. (A recent patch on our branch caused a bug around here, which the attached test cases would have caught.)

[gasche]

Ah, the example has fun ?x () -> (() : a) and not fun ?x (() : a) -> () as I read too quickly. Thanks!

(One thing this PR reminded me is that the code to type-check labels remains a bit messy. I thought that @lpw25 had proposed a refactoring of it, but I haven't found a trace of it yet in open and closed PR so I must misremember.)

[goldfirere]

So.... what are we thinking here? Probably the easiest thing to do is to check in the tests, with no change in behavior. This is slightly unfortunate, in that it means that the unerasable-argument warning affects whether or not a program is accepted. But that's not new today, and no one has actively complained about it. (I'm not actively complaining; the reason I'm here is that I had a nearby bug, but not this one in specific.) The alternative seems hard to work out, and would probably give a worse user experience in the common case.

[garrigue]

Since we backtrack, the expansion is not visible from outside the scope of the potential equations, so this is fine.
This information is only used to select different behaviors of the type checker.

[gasche]

@goldfirere and @garrigue, you both have merge rights and understand this change better than I do. I think that one of you should merge it.

[goldfirere]

Yes, I had semantically merged this by adding the "merge-me" label, which I understood as meaning "if anyone with merge rights sees this, and CI is green, just click merge". I kept checking for CI to go green, then timed out, and hadn't wandered back. Thanks for noticing. I have now syntactically merged, as well. :)