type parameter of polymorphic variant types

type parameter of polymorphic variant types

[Keiko Nakata]

Hello.

Why I cannot have these type definitions?

#type ('a,'b) t = ['a | 'b] constraint 'a =[>] constraint 'b = [>];;
#type ('a,'b) t = A of 'a * 'b constraint 'a = [>'b];;


Moreover, for the type definition 

#type ('a, 'b) u = 'a constraint 'a = [>`A | 'b] ;;

the type checker reports an error 

  Characters 48-50:
    type ('a,'b) t = A of 'a * 'b constraint 'a = [>'b];;
                                                    ^^
  The type 'a is not a polymorphic variant type

Is this a kind of typo of 'a for 'b or an intention?


Regards,
Keiko.

Re: [Caml-list] type parameter of polymorphic variant types

[Jacques Garrigue]

From: Keiko Nakata <keiko@kurims.kyoto-u.ac.jp>

> Why I cannot have these type definitions?
> 
> #type ('a,'b) t = ['a | 'b] constraint 'a =[>] constraint 'b = [>];;
> #type ('a,'b) t = A of 'a * 'b constraint 'a = [>'b];;

See the manual, section 6.4, variant types:

  In all three cases, tags may be either specified directly in the
  `tag-name [...] form, or indirectly through a type expression. In
  this last case, the type expression must expand to an exact variant
  type, whose tag specifications are inserted in its place.

The important point here is that type expressions must expand to
_exact_ variant types, which are defined as fully specified variant
types that cannot be refined anymore. This certainly does not include
type variables.

> Moreover, for the type definition 
> 
> #type ('a, 'b) u = 'a constraint 'a = [>`A | 'b] ;;
> 
> the type checker reports an error 
> 
>   Characters 48-50:
>     type ('a,'b) t = A of 'a * 'b constraint 'a = [>'b];;
>                                                     ^^
>   The type 'a is not a polymorphic variant type
> 
> Is this a kind of typo of 'a for 'b or an intention?

There seems to be a typo in your report: you say that you are defining
a type u, and the type checker reports a problem about a type t.
There are known problems with type variable names, but not with
type names.
If I try your code, I get

  # type ('a, 'b) u = 'a constraint 'a = [>`A | 'b] ;;
                                                ^^
  The type 'a is not a polymorphic variant type

The variable name does not match. This is not surprising, as the type
checker does not remember variable names when they are converted to an
internal form. This will have to be fixed someday...

Jacques Garrigue