Re: [Caml-list] constructor disambiguation for gadts

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

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