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

**URL:** <https://discuss.ocaml.org/t/using-failwith-does-not-type-check-when-the-concrete-return-type-is-a-ref-why/9894>\
**Category:** Learning\
**Tags:** type-system\
**Created:** [May 21, 2022, 5:23pm UTC](https://discuss.ocaml.org/t/using-failwith-does-not-type-check-when-the-concrete-return-type-is-a-ref-why/9894 "2022-05-21T17:23:18Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![acorello](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/acorello/32/3747_2.png) [@acorello](https://discuss.ocaml.org/u/acorello)\
**Post date:** [May 21, 2022, 5:23pm UTC](https://discuss.ocaml.org/t/using-failwith-does-not-type-check-when-the-concrete-return-type-is-a-ref-why/9894/1 "2022-05-21T17:23:18Z")

</div>

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

This is the failing code:

```ocaml
(* .mli *)
type 'a t

val create : unit -> 'a t

```

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

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

```

The error:

```auto
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._

---

<div class="post-metadata">

**Author:** ![nojb](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/nojb/32/519_2.png) [@nojb](https://discuss.ocaml.org/u/nojb)\
**Post date:** [May 21, 2022, 5:55pm UTC](https://discuss.ocaml.org/t/using-failwith-does-not-type-check-when-the-concrete-return-type-is-a-ref-why/9894/2 "2022-05-21T17:55:32Z")

</div>

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

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

```

which should typecheck just fine.

Cheers,  
Nicolas

---

<div class="post-metadata">

**Author:** ![amongonz](https://avatars.discourse-cdn.com/v4/letter/a/a88e4f/32.png) [@amongonz](https://discuss.ocaml.org/u/amongonz)\
**Post date:** [May 21, 2022, 6:11pm UTC](https://discuss.ocaml.org/t/using-failwith-does-not-type-check-when-the-concrete-return-type-is-a-ref-why/9894/3 "2022-05-21T18:11:16Z")

</div>

The OCaml manual [has a chapter about this](https://v2.ocaml.org/manual/polymorphism.html); 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:

```ocaml
let create () : 'a t = failwith "..."

```

---

<div class="post-metadata">

**Author:** ![acorello](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/acorello/32/3747_2.png) [@acorello](https://discuss.ocaml.org/u/acorello)\
**Post date:** [May 21, 2022, 6:16pm UTC](https://discuss.ocaml.org/t/using-failwith-does-not-type-check-when-the-concrete-return-type-is-a-ref-why/9894/4 "2022-05-21T18:16:34Z")

</div>

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.

@amongonz 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!