Re: [Caml-list] difference of [< `A of & int] and [< `A of int] ?

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

On 2010/09/21, at 21:16, Hendrik Tews wrote:
> I am trying to grasp the camlp4 constructor for types TyOfAmp,
> which is declared as 
> 
>    | TyOfAmp of loc and ctyp and ctyp (* t of & t *)
> 
> in camlp4/Camlp4/Camlp4Ast.partial.ml. It is used in the ast of 
> ``[< `A of & int]''.
> 
> Can somebody explain the meaning of [< `A of & int]? What is the
> difference between [< `A of & int]  and  [< `A of int] ?

This is an (impossible) conjunctive type. 
Basically it says that `A is both a constant constructor (taking no argument),
and a constructor taking an argument of type int.
This artefact is needed to make type inference principal, but this type
is not useful in itself.

(Well, one can think of some uses, like unifying types conditionally, but
the behaviour is rather restricted.)

> And why does 
> 
>  type 'a t = [< `A of & int] as 'a
> 
> produce the weird error 
> 
> File "test/x.ml", line 1, characters 0-1:
> Error: The implementation test/x.ml
>       does not match the interface (inferred signature):
>       Type declarations do not match:
>         type 'a t = 'a constraint 'a = [< `A of & int ]
>       is not included in
>         type 'a t = 'a constraint 'a = [< `A of & int ]
> 
> ? Is this a bug or a feature?

Err, it is actually a feature, but I agree this is not very intuitive.
When checking types against an interface, such conjunctive types are
not allowed. So the type checker attemps to unify all possibilities, but
since no argument is not unifiable with anything else, it fails.
Unfortunately, the error message is not very explicit about the cause.

	Jacques Garrigue