Re: [Caml-list] Expansion of type-constructors in ctype.ml

[Jeremy Yallop <yallop@gmail.com>]

On 22 August 2015 at 08:42, Christoph Höger
<christoph.hoeger@tu-berlin.de> wrote:
> 1. In the case of equality, it seems fairly simple. Iff the path of two
> constructors is the same and both argument lists are equal, the types
> are equal, right?

"If", but not "iff", unless you expand first.  Consider

   type 'a t = unit

Then 'int t' and 'float t' should be considered equal, since they both
expand to 'unit', even though the argument lists are unequal

> 2. In the case of unification, if both paths are the same, the argument
> lists are of the same length, we can directly unify the arguments, right?

Again, you need to expand the path first.  Consider the following
function, using the same definition of 't' as above:

   fun (a : 'a) (b : 'b) ->
      let c : 'a t = ()
      and d : 'b t = () in
      ignore [c; d];

The last line involves unifying the types 'a t and 'b t.  Unifying the
type arguments 'a and 'b results in the following type for the
function:

    'a -> 'a -> unit

Expanding 't' before unifying means that 'a and 'b are not unified,
and the function can be given the more general type:

    'a -> 'b -> unit