Re: [Caml-list] Problem with GADTs and escaping types

[Leo White <lpw25@cam.ac.uk>]

>     type t =
>       | App : {k:'t . 'a->'t->'t; s:'a} -> t
>
>     let munge : ('a->'t->'t as 'k) -> 'k = fun k -> fun s r -> k s r
>
>     let transform = function
>       | App {k;s} -> App {k=munge k;s}
>
> OCaml will choke on the transform function with the following error:
>
>     Error: This field value has type a#17 -> 'b -> 'b which is less general than
>              't. 'a -> 't -> 't

This is an example of the value restriction. A function application
(like `munge k`) is not a syntactic value so it cannot be considered
polymorphic. Since `App` requires `k` to be polymorphic, you get an
error.

The simplest solution in your case is probably to make `munge` work
directly on the record type:

    let munge {k; s} = {k = (fun s r -> k s r); s}

You could also create another record type containing only `k`, and have
`munge` operate on that.

>
> If I add type annotations like so:
>
>     let transform_annotated = function
>       | App {k;s} -> App {k=(munge k : 'a->'t->'t);s=(s:'a)}
>
> OCaml will instead give me an error about escaping types:
>
>     Error: This expression has type a#19 -> 'a -> 'a
>            but an expression was expected of type a#19 -> 't -> 't
>            The type constructor a#19 would escape its scope

This is an example of the slightly surprising scoping of type
variables. It sometimes surprises people, but any type variable (e.g. 'a
in your above code), is given the same scope as the enclosing top-level
definition (e.g. `transform_annotated`). Since it would not be safe for
the existential type `'a` in the definition of `App` to escape outside
of its match case this results in a slightly surprising error.

Note that the annotation you have added does not actually do what you
want anyway. You are trying to enforce the result of `munge k` to have
the *polymorphic* type `'t. 'a -> 't -> 't`, but `'a -> 't -> 't` just
ensures that both 't types are equal, it does not ensure that they are
polymorphic. In fact, thanks to the top-level scope of type variables,
your annotation is having the opposite effect, forcing `'t` to be
considered monomorphic within the scope of the top-level definition.

Hope that clears things up for you. You've managed to hit two slightly
complicated parts of the type system in a single example.

Regards,

Leo