Signature mismatch 'a list -> 'a Core.Std.List.t is not included in 'a list -> 'a t

Question

I'm working on chapter 11 of the book "More Ocaml", where you try to implement a set in various ways. This code is largely from the book, but I've changed it to use Core (and Core's List) instead of the stdlib.

open Core.Std;;
open Printf;;

module SetList :
  sig
    type 'a t;;
    val set_of_list : 'a list -> 'a t;;
    val list_of_set : 'a t -> 'a list;;
    val insert : 'a -> 'a t -> 'a t;;
    val size : 'a t -> int;;
    val member : 'a t -> 'a -> bool;;
  end
=
  struct
    type 'a t = 'a list;;

    let member = List.mem ~equal:(=);;

    let insert x l = if member l x then l else x::l;;

    let rec set_of_list l = match l with
      [] -> []
      |h::t -> insert h (set_of_list t);;

    let list_of_set x = x;;

    let size = List.length;;
  end;;

This gives me an error Values do not match: val set_of_list : '_a list -> '_a Core.Std.List.t is not included in val set_of_list : 'a list -> 'a t.

First question, what do I do to fix that error? Second and more important, why doesn't the compiler realize that 'a Core.Std.List.t equals 'a t and match the values given the definition on line 15.

Answer 1

You are mistaken on the error. If we give the option -short-path (which tries to find the smallest type alias when giving a type error) we get the following error instead:

   Values do not match:
     val set_of_list : '_a t -> '_a t
   is not included in
     val set_of_list : 'a t -> 'a t

So Core.Std.List.t is indeed equal to t, and the compiler see that. The issue is with the sneaky _.

The cause of the error is what's called value restriction. Basically, the typechecker can generalize (pick the most general type) only when a value is bound. In your case, the cullprint is the definition of member.

If you define it this way, the error goes away:

let member x = List.mem ~equal:(=) x

The list is bound to a name, so the typechecker can generalize.

When the compiler can't, it produces a type variable that is "unknown but not polymorphic" (we call them monomorphic) and add _ to the name. The type variable will be specialized at first use. You can try to play with let r = ref None in the toplevel to see it more closely.