Skip to content

Instantly share code, notes, and snippets.

@infinity0
Last active October 13, 2021 19:49
Show Gist options
  • Save infinity0/ea064ba358ea44e4f4919789f12d8d7e to your computer and use it in GitHub Desktop.
Save infinity0/ea064ba358ea44e4f4919789f12d8d7e to your computer and use it in GitHub Desktop.
OCaml GADTs and avoiding "type constructor would escape its scope" errors
(* GADT list that exposes the type of the head element *)
type _ hlist =
| Nil: 'a hlist
| Cons: ('a * 'b hlist) -> 'a hlist
(* let rec len = function *)
(* let rec len (type a) (l: a hlist): int = match l with *)
(* both of the above result in a "type constructor would escape its scope" error *)
(* correct version: *)
let rec len : type a. a hlist -> int = function
(* also correct: *)
(* let rec len : 'a. 'a hlist -> int = function *)
| Nil -> 0
| Cons (h, t) -> 1 + len t
(* NB: this only works if you don't extract your elements.
if you need to extract the elements then the error is real, and you either need to redesign your code
so that the inner types (to be extracted) are contained in the outer type param *)
@ebresafegaga
Copy link

What's the difference between (type n) and type n.

Aren't they both locally abstract types?

@infinity0
Copy link
Author

@ebresafegaga It's been a few years, but I think the difference is that in the incorrect version a refers to a unification variable that needs to be unified with the other types in the program; whereas in the correct version a is used in the context of an implicit forall a quantifier over the type, which is self-contained and does not need to be unified with the other types in the program.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment