Type constraints

[Pascal Brisset <brisset@recherche.enac.fr>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 852 bytes --]

Ernesto Posse writes:
« type 'a node = {x: 'a; y: t1}
« and t1 = A | B of t1*t1
« and t2 = C | D of (string * t2) node | E of bool node
« 
« I obtain this message:
« 
« Characters 98-102:
« This type parameter bool should be an instance of type string * t2

It may be compared to a similar expression at the term level:

# let rec f = fun x -> x
  and g = f 1, f "1";;
                 ^^^
This expression has type string but is here used with type int

In a recursive definition, occurrences of the defined idents have the
same type everywhere, i.e. the generalization (in your case, 'a is any
type) is done only ``at the end'' of the definition.

At the term level, ML+ is the (undecidable) solution to this kind of
recursive definition. I guess problems are similar at the type level.

A more precise answer from a Caml guru ?

--Pascal Brisset