Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2013/07/04, at 17:14, Alain Frisch <alain@frisch.fr> wrote:

> On 07/04/2013 03:00 AM, Jacques Garrigue wrote:
>> In theory, it would be OK to assume that all pattern-matchings may contain GADT type constructors.
>> The only real problem is with let's: if they contain GADTs, we must use the code for pattern-matching, which doesn't handle unused definition warnings in the same way… Having all non recursive let's go through this code would have a high impact on warnings.
> 
> If this is the only problem with the direct approach (not depending on backtracking), maybe the treatment of warnings can be parametrized to behave as expected?

This does not remove the need for backtracking, as the backtracking occurs in the code for typing pattern-matching.
It is needed to detect where GADTs are actually used.
(By the way this backtracking concerns only the typing of pattern-matching, and it is not costly, so there is no real need to avoid it).
The goal is to allow to switch between the code for let-in and the code for match freely.

>> If unused definition warnings could be separated from type checking this would be much easier.
> 
> Maybe I'm wrong, but it seems to me that achieving the same behavior would require to duplicate of lot of the "data-flow" logic in the type-checker, thus increasing the global complexity (and the risk to have diverging behaviors).

I just mean that if it could abstracted so that one could call the same use-tracking function for type_cases and type_let, things would be simpler. The goal here is factoring, not duplicating.

Jacques Garrigue