[Caml-list] constructor disambiguation for gadts

[Caml-list] constructor disambiguation for gadts

[Milan Stanojević]

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.

Re: [Caml-list] constructor disambiguation for gadts

[Jacques Garrigue]

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

Re: [Caml-list] constructor disambiguation for gadts

[Milan Stanojević]

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

Re: [Caml-list] constructor disambiguation for gadts

[Goswin von Brederlow]

On Tue, Oct 07, 2014 at 12:14:01PM -0400, 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.

Shouldn't that be A.I and A.S? You didn't open module A.

MfG
	Goswin