# GADT question (it would escape the scope of its equation)

Hello,

I don’t understand why the following does not typecheck:

``````type com = Seq of com*com | Skip
type state

type (_,_) filter =
| Eq : ((int*int),bool) filter

and _ cont = Sst : (com * state cont) -> state cont
| Filter : ('a,'b) filter * 'b cont -> 'a cont

let apply_filter : type a b. (a,b) filter -> a -> b =
fun f a -> match f with
| Add -> let (x,y) = a in x + y
| Eq  -> let (x,y) = a in x = y

let rec apply : type a. a -> a cont -> 'b =
fun arg k -> match k with
| Filter (f,k) -> apply (apply_filter f arg) k
| Sst (c,k) -> eval_com_cont arg c k

and eval_com_cont (st:state) c cont = match c with
| Seq(c1,c2) -> eval_com_cont st c1 (Sst (c2,cont))
| Skip -> apply st cont
``````

In the second branch of apply, the type `a` is `state`, but for some reason ocaml says:

``````This expression has type state but an expression was expected of type
'a
This instance of state is ambiguous:
it would escape the scope of its equation
``````

What does it mean, and is there a way to fix it?

Thanks,

Alan

Moving the type annotation on the whole `eval_com_cont` function solves this issue:

``````and eval_com_cont: state -> com -> state cont -> 'never = ...
``````

Thanks! I’ll know to try this next time.

Here, by the scope of its equation, the compiler actually means the scope of the `Sst` branch, where the type of `arg` could be either `'a` or `state`. Normally, the compiler uses heuristics to resolve such ambiguities, so it is sufficient to annotate on the function level. However, in a general case, as your example shows, you have to annotate even more, that means that you have to refine your locally abstract types on the branch level (the refinement will only extend to the scope of the branch), e.g.,

``````
let rec apply : type a. a -> a cont -> 'b =
fun arg k -> match k with
| Filter (f,k) -> apply (apply_filter f arg) k
| Sst (c,k) -> eval_com_cont (arg : state) c k (* <--- refine here *)

and eval_com_cont st c cont = match c with
| Seq(c1,c2) -> eval_com_cont st c1 (Sst (c2,cont))
| Skip -> apply st cont
``````

Interestingly, by rearranging your functions, (and thus changing the flow of type inference), you can enable the heuristic to work again, (since now the compiler will be able to refine `'a` automatically). e.g.,

``````let rec eval_com_cont = fun st c cont -> match c with
| Seq(c1,c2) -> eval_com_cont st c1 (Sst (c2,cont))
| Skip -> apply st cont

and apply : type a. a -> a cont -> _ =
fun arg k -> match k with
| Filter (f,k) -> apply (apply_filter f arg) k
| Sst (c,k) -> eval_com_cont arg c k
``````

Alternatively, you can inline the body of `eval_com_cont` into the `Sst` branch, that will give the compiler enough context to refine `a` to state:

``````let rec apply : type a. a -> a cont -> _ = fun arg k -> match k with
| Filter (f,k) -> apply (apply_filter f arg) k
| Sst (c,k) -> match c with
| Seq(c1,c2) -> eval_com_cont arg c1 (Sst (c2,k))
| Skip -> apply arg k
``````
1 Like

Thanks for the detailed explanation. I think the most elegant (yet fragile) solution is changing the order of the functions.

Note: I’m going to use the error messages which will be printed by the next version of the compiler, because the formatting is much nicer (courtesy of @Armael), but the error message itself is unchanged since at least 4.03, so the version of OCaml doesn’t really matter here.

So, first: I think we all agree that the following error message is terrible (and hopefully we’ll improve it some day):

``````19 |     | Sst (c,k) -> eval_com_cont arg c k
^^^
Error: This expression has type state but an expression was expected of type
'a
This instance of state is ambiguous:
it would escape the scope of its equation
``````

Funnily enough, if we invoke the compiler with `-short-paths` (which is what dune does I believe), the error message becomes:

``````19 |     | Sst (c,k) -> eval_com_cont arg c k
^^^
Error: This expression has type a but an expression was expected of type 'a
This instance of a is ambiguous:
it would escape the scope of its equation
``````

And that actually gives some hint about what the error actually is: `arg` at this point has type `a ≈ state` (which we call an ambivalent type), but that type only exists in the scope of the branch (where the equality is introduced by matching on `Sst`). If you want to pass `arg` to another function, a choice needs be made regarding which side of the equation you want to use as the type for `arg`, and in the code you gave in your first message, the compiler doesn’t have enough information to make that choice: it is ambiguous.

The first solution given by @ivg resolves that ambiguity by telling the compiler "choose the type `state`", and of his two proposed solutions, that one is indeed the more robust, and in my opinion, the one you should use.

The reason why his second proposition (the reordering) has any effect (that is: solves your problem), is the same reason explaining why @octachron’s proposition also solves the problem, and is sort of an implementation detail: when you have a group of mutually recursive functions, the compiler will start by approximating their type, before actually typing them (because when you start typing `apply` and you encounter the use of `eval_com_cont` you need to have a guess at what its type actually is).
So, assuming you had something like

``````let rec apply arg k = ...
and eval_com_cont st c cont = ...
``````

the compiler would assign the type `'a -> 'b -> 'c` to `apply` and `'d -> 'e -> 'f -> 'g` to `eval_com_cont` before typing `apply`, and after that, when it starts typing `eval_com_cont` it will use the proper type of `apply` that it has just computed, but will still use the “approximation” of the type of `eval_com_cont`.

That is why the reordering has an impact, if you reorder then when you type `apply`, you already know that `eval_com_cont` has type `state -> com -> state cont -> 'b`, and you can without a doubt choose to use `state` as the type for `arg`.

Now, the reason why @octachron’s solution works, i.e. having `eval_com_cont : state -> _ -> _ -> _ = fun st c cont -> ...` (that is enough btw, you don’t need to expand any more), is that in this particular case, the compiler will look at the type annotation when approximating the type of the function, whereas it doesn’t when you write `eval_com_cont (st : state) c cont = ...`.
That is a bit disappointing, and we could probably look into making it better.

I think that’s the full explanation. If you want to know more about ambivalent types, this paper from Garrigue and Rémy contains all there is to know (and if, you omit the formal development, is very accessible).

8 Likes

Thanks a lot, this is very clear now. I understand the best option to help the compiler is to specify the type in the branch. I’ll do that next time I have an issue.