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

Learning
1

Hello,

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

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

type (_,_) filter =
    | Add : ((int*int),int) 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

2

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

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

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

4

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
5

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

6

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
7

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.