Implicit constraints in type declaration

Implicit constraints in type declaration

[Alain Frisch]

Hello,

I don't understand why the following type declaration implies a
constraint:

# type 'a t = int and b = int t;;
type 'a t = int constraint 'a = int
type b = int t

Also, I don't understand this error message (I can imagine why
the declaration is illegal):

# type 'a t = u and u = int;;
                    ^^^^^^^
A type variable is unbound in this type declaration


-- 
  Alain Frisch

Re: Implicit constraints in type declaration

[Pierre Weis]

> Hello,
> 
> I don't understand why the following type declaration implies a
> constraint:
> 
> # type 'a t = int and b = int t;;
> type 'a t = int constraint 'a = int
> type b = int t
> 
> Also, I don't understand this error message (I can imagine why
> the declaration is illegal):
> 
> # type 'a t = u and u = int;;
>                     ^^^^^^^
> A type variable is unbound in this type declaration
> 
> 
> -- 
>   Alain Frisch

All those glitches were due to a strange way of type cheking type
definitions using unification. Jacques (Garrigue) reimplemented the
old semantics for ordinary type definitions. Thus, your examples now
work fine in the working version of the compiler:

        Objective Caml version 3.00+20 (2000-12-03)

# type 'a t = int and b = int t;;
type 'a t = int
type b = int t
# type 'a t = u and u = int;;
type 'a t = u
type u = int

Best regards,

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis/