Keiko Nakata wrote:
> I am very interested in this subject.
> Since 1) I can define type abbreviations almost artitrary,
> as in  type t = < m : t > ; and 2) type abbreviations can have parameters
> as in type 'a t = < m : 'a > , 
> just keeping a list/set of visited nodes does not seem to be enough,
> especially for structual types.

Structural loops (those that don't cross a datatype) cannot be
arbitrary. The parameters cannot change:

# type 'a t = < m : 'a t >;;
type 'a t = < m : 'a t >
# type 'a t = < m : ('a * 'a) t>;;
In the definition of t, type ('a * 'a) t should be 'a t

The restriction ensures that structural recursive types are necessarily
regular. So standard coinductive algorithms (implemented by keeping
track of visited nodes or by memoization) are ok.

-- Alain