type _ weirdtree =
| Leaf : int -> int weirdtree
| Node : ('a weirdtree * 'a weirdtree) -> 'a weirdtree weirdtree
Suppose I want to convert the tree into a list:
let rec list_of_weirdtree : 'a . 'a weirdtree -> int list = fun w ->
match w with
| Leaf n -> [n]
| Node (l, r) -> (list_of_weirdtree l) @ (list_of_weirdtree r)
This results in the following error, with Node (l, r) underlined:
Error: This pattern matches values of type $0 weirdtree weirdtree
but a pattern was expected which matches values of type int weirdtree
The type constructor $0 would escape its scope
Which mostly makes sense to me. But is there a way to get this sort of function to typecheck? Most of the online results I get for the “type constructor would escape its scope” error seem to be solved by using an explicit polymorphic type annotation, but that doesn’t seem to do the trick here.
You need both an explicit polymorphic annotation, for polymorphic recursion, and a locally abstract type (type a) for GADT matching. You can neatly combine both using let rec list_of_weirdtree : type a. a weirdtree -> int list = fun ....
In fact, it is commonly advised to always use the type a. syntax when writing polymorphic type annotations, even if you don’t actually need the locally abstract type.
What would you expect the type of list_of_weirdtree to be ? 'a weirdtree -> 'a list is probably wrong, as you want the content of the leaves, which is not of type 'a if your tree has at least one node. 'a weirdtree -> 'b list is wrong too, as you can’t produce a list of any type from any weirdtree. Even trying to existentially quantify over 'b (instead of universally) wouldn’t work, as you wouldn’t be able to type the recursive call.
The usual solution is to add a type parameter to weirdtree, for instance ('elt, 'height) weirdtree, where 'elt is the type of things stored in leaves and 'height the one that encodes the height of the tree. Then list_of_weirdtree would have type type elt height . (elt, height) weirdtree -> elt list.