Re: [Caml-list] constructor disambiguation for gadts

["Milan Stanojević" <milanst@gmail.com>]

Thanks for the answer.
Is there any hope this might get fixed in the future?

On Tue, Oct 7, 2014 at 11:29 PM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> On 2014/10/08 01:14, Milan Stanojević wrote:
>>
>> I was wondering what are technical difficulties that prevent
>> constructor disambiguation for GADTs?
>>
>> I got an interesting error today, where it is clear that compiler
>> knows the type but because it is GADT it is still asking me to qualify
>> the constructor.
>>
>> Here is the simple example.
>> module A : sig
>>  type _ t =
>>    | I : int t
>>    | S : string t
>> end = struct
>>  type _ t =
>>    | I : int t
>>    | S : string t
>> end
>>
>> let add : type a . a A.t -> a -> a -> a =
>>  fun w a1 a2 ->
>>    match w with
>>    | I -> a1 + a2
>>    | S -> String.concat "" [a1; a2]
>> ;;
>>
>> I get File "foo.ml", line 14, characters 6-7:
>> Error: The GADT constructor I of type A.t must be qualified in this pattern.
>>
>> I'm not sure what extra information I'm giving to the type checker by
>> qualifying the constructor.
>
> Typing of GADT patterns follows a slightly different path, which makes
> harder to insert constructor disambiguation.
> To be more precise, the type-checker first looks at the patterns, and
> tries to guess whether there are some GADT constructors inside it.
> If some constructors are ambiguous, it may guess wrongly that there
> are none, and take the non-GADT path, to find later that it should have
> taken the GADT path.
>
> Jacques Garrigue