difference of [< `A of & int] and [< `A of int] ?

difference of [< `A of & int] and [< `A of int] ?

[Hendrik Tews]

Hi,

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] ?


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?

Bye,

Hendrik

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

[Jacques Garrigue]

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

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

[Hendrik Tews]

Thanks for this quick and enlightening answer!

Jacques Garrigue writes:
   Date: Tue, 21 Sep 2010 21:41:01 +0900
   Subject: Re: [Caml-list] difference of [< `A of & int] and [< `A of int] ?
   
   > [< `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.

Actually, this type expression is not covered by the grammar in
the reference manual. The rule

   tag-spec-full ::= `tag-name  [ of typexpr ]  { & typexpr }

does not produce it, because typexpr cannot produce the empty
string.

I believe a sentence about this special case in the manual would
be helpful.

   > 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 ]
   
   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.
   
However, the following impossible type

   type 'a t = [< `A of int & string] as 'a

is accepted by the compiler. Is there a reason for treating these
two impossible types differently?

Bye,

Hendrik