Re: [Caml-list] A confusing example with modules and polymorphic variants

[Yaron Minsky <yminsky@janestreet.com>]

Thanks!  That all makes perfect sense, now that you say it.  Not sure
why it was so hard for me to figure it out on my own.

One interesting bit is that a very similar example can be made to work
without resorting to these kinds of tricks.  In particular, if we
change the [< `Foo] to [> `Foo], then, we can get the polymorphism we
need back by using a cast:

    module type S = sig
      val z : [> `Foo ]
    end

    let f z =
      let module M : S = struct
        let z = (z : [`Foo] :> [> `Foo])
      end in
      ()

But this doesn't really help in the case I'm after.

y


On Fri, Oct 19, 2012 at 6:10 PM, Jeremy Yallop <yallop@gmail.com> wrote:
> On 19 October 2012 22:18, Yaron Minsky <yminsky@janestreet.com> wrote:
>> We've been running into some troubles with polymorphic variants,
>> modules, and the value restriction, that we're not quite able to
>> unravel.  Here's a stripped down version of the problem.
>>
>>     module type S = sig
>>       val z : [< `Foo ]
>>     end
>>
>>     let f z =
>>       let module M : S = struct let z = z end in ()
>
> I believe the problem here is the monomorphic parameter restriction: the type
> of S requires the field z to be polymorphic, but type inference only assigns
> monomorhpic types to function parameters.  That is, your example doesn't type
> check for essentially the same reason that the following code doesn't type
> check:
>
>     type s = {
>       z : 'a. 'a -> 'a
>     }
>
>     let f z =
>       let s = {
>         z = z
>       } in
>       ()
>
> One way to work around the monomorphic parameter assumption is to wrap the
> parameter in a record with a polymorphic field.
>
>     type z_type = { field : 'a. 'a -> 'a}
>
>     let f z =
>       let s = {
>         z = z.field
>       } in
>       ()
>
> The parameter is still assigned a monomorphic type (z_type), but the projected
> field is polymorphic, as required.
>
> I don't see how to make that work in your case, though, because of the nature
> of the polymorphism -- i.e. it's based on a row variable rather than a
> standard type variable, and there isn't any syntax for quantifying it.
>
> However, you *can* modify your example so that it passes type checking by
> wrapping the argument in a first-class module, since module fields can be
> row-polymorphic.  The easiest way in the cut-down example is to reuse the
> signature you already have:
>
>     module type S = sig
>       val z : [< `Foo ]
>     end
>
>     let f (module Z : S) =
>       let module M : S =
>           struct
>             let z = Z.z
>           end
>       in ()