Using `failwith` does not type-check when the concrete return type is a `ref`. Why?

Learning
1

I’d appreciate some help/pointers to understand the following type-error.

This is the failing code:

(* .mli *)
type 'a t

val create : unit -> 'a t

(* .ml *)
type 'a t = 'a ref (* this `ref` causes the error *)

let create : unit -> 'a t = failwith "Not Implemented"

The error:

The implementation lib/MyModule.ml
  does not match the interface lib/.Project.objs/byte/project__MyModule.cmi:
  Values do not match:
    val create : unit -> '_a t
  is not included in
    val create : unit -> 'a t
  The type unit -> '_a t is not compatible with the type unit -> 'b t
  Type '_a is not compatible with type 'b 
  File "lib/MyModule.mli", line 6, characters 0-25:
    Expected declaration
  File "lib/MyModule.ml", line 11, characters 4-10:
    Actual declaration

If I change the .ml to use type 'a t = 'a list (or option instead of list) then it type-checks.

If you’re wondering why on earth I’m doing this: I’m using failwith "Not Implemented" as a temporary implementation just to have a compiling project; I started implementing a bigger .mli and I wanted to get rid of all the type-errors due in the incomplete .ml file by entering all the expected items.

1 Like
2

There are a couple of different issues here, but I believe that what you want is

let create : unit -> 'a t = fun () -> failwith "Not implemented"

which should typecheck just fine.

Cheers,
Nicolas

2 Likes
3

The OCaml manual has a chapter about this; in short, you’re meeting the value restriction because the 'a in 'a ref is an invariant type variable, so it becomes a weak type variable '_a when trying to “return” a unit -> 'a ref from failwith. This doesn’t happen with the 'a in 'a list because it’s covariant, which have relaxed restrictions.

This restriction exists to prevent you from using a global instance of 'a ref as both int ref and string ref at the same time, for example. Your function will work if you use failwith inside it, however:

let create () : 'a t = failwith "..."
5 Likes
4

Hi @nojb,
and thank you, that indeed type-checks.

But I’m still unable to explain why the polymorphic type of failwith is rejected in case the expected type is (I guess) a function type returning a polymorphic ref: _ -> 'a t where type 'a t = 'a ref. In other words, I don’t understand why the code compiles when, for example, type 'a t = 'a option without wrapping failwith in an anonymous function.

@debugnik explains what rules I have bumped into, I’ll pick his answer as a solution as I wanted to understand rather than just fix.

Cheers!