[Caml-list] Problem with GADTs and escaping types

[Caml-list] Problem with GADTs and escaping types

[Kaspar Rohrer]

[-- Attachment #1: Type: text/plain, Size: 1665 bytes --]

Hi all

I was playing around with GADTs over the last few days and encountered the following problem (reduced to a minimal case here): 

> 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}

Note that I am using inlined records, which are only available in the unreleased 4.03 version. But I get the same error when using a separate record in OCaml 4.01, i.e.:

> type t = App : 'a app_t -> t
> and 'a app_t = { k : 't. 'a->'t->'t; s:'a }

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

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

I can work around this whole problem by inlining the munge function:

> let transform_inline = function
>   | App {k;s} -> let k' s r = k s r in App {k=k';s}

This works but it is not ideal for my case, as it leads to somewhat unwieldy match expressions.

Can somebody explain to me why the first case does not work? Especially when considering that the types should be equal (substituting the identity function for munge produces the the same error).

Thank you in advance

	Kaspar M. Rohrer


[-- Attachment #2: Type: text/html, Size: 4802 bytes --]

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

[Leo White]

>     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