Scope error with locally abstract type when GADT constructor contains multiple type variables

Question

Given this GADT

type _ t = 
  | A : (string -> 'ok) * (string -> 'err) -> ('ok, 'err) result t

Why is it that this fails with a "type constructor would escape its scope" error

let f (type a) (gadt: a t): a Future.t =
  Future.bind (fetch ()) (fun response ->
      match gadt with
      | A (ok, _) -> Ok (ok response))

Error: This expression has type $0 but an expression was expected of type 'a
       The type constructor $0 would escape its scope

while this, which just extracts the pattern match into a separate function, works?

let parse (type a) (gadt: a t) (response: string): a = 
  match gadt with
  | A (ok, _) -> Ok (ok response)
                     
let f (type a) (gadt: a t): a Future.t = 
  Future.bind (fetch ()) (parse gadt) 

The first example also works with a simpler GADT such as

type _ t =
  | B : (string -> 'a) -> 'a t

suggesting there is some weird interaction between GADT constructors with multiple type variables, locally abstract types and closures.

This has been tested on several OCaml versions from 4.06 to 4.14 with identical results, so it seems unlikely to be a bug at least.

Complete example

module Future = struct
  type 'a t

  let bind : 'a t -> ('a -> 'b) -> 'b t = Obj.magic
end
  
let fetch : unit -> 'a Future.t = Obj.magic

type _ t = 
  | A : (string -> 'ok) * (string -> 'err) -> ('ok, 'err) result t

let parse (type a) (gadt: a t) (response: string): a = 
  match gadt with
  | A (ok, _) -> Ok (ok response)
                     
let f_works (type a) (gadt: a t): a Future.t = 
  Future.bind (fetch ()) (parse gadt) 

let f_fails (type a) (gadt: a t): a Future.t =
  Future.bind (fetch ()) (fun response ->
      match gadt with
      | A (ok, _) -> Ok (ok response))

Edit: Extended example

The above example is a bit over-simplified, in that while it does illustrate the underlying problem well, it doesn't show that I actually do need the whole ('ok, 'err) result type to be abstracted, because there are other constructors with other shapes, here illustrated by the additional B constructor:

type _ t = 
  | A : (string -> 'ok) * (string -> 'err) -> ('ok, 'err) result t
  | B : (string -> 'a) -> 'a t

let f (type a) (gadt: a t): a Future.t =
  Future.bind (fetch ()) (fun response ->
      match gadt with
       | A (ok, _) -> Ok (ok response)
       | B f -> f response)

Answer 1

Another way to see the issue in this case is that

let f (type a) (gadt: a t): a Future.t =
  Future.bind (fetch ()) (fun response ->
      match gadt with
      | A (ok, _) -> Ok (ok response)
  )

is expecting that the type constraint a Future.t is propagated to the argument of the bind function at exactly the right time to be used to repack the type ($0,$1) result into a.

This doesn't work out. The smallest fix is to add the annotation when leaving the pattern matching:

let f (type a) (gadt: a t) =
  Future.bind (fetch ()) (fun response ->
      match gadt with
      | A (ok, _) -> (Ok (ok response): a)
  )

With this annotation, we are using the local equation ($0,$1) result=a to make sure that the local types $0 and $1 do not escape their branch of the pattern matching.

Answer 2

You have to create a locally abstract type for each type variable to extend its scope, e.g., the following typechecks,

let f (type ok err) (gadt: (ok,err) result t): (ok,err) result Future.t =
  Future.bind (fetch ()) (fun response ->
      match gadt with
      | A (ok, _) -> Ok (ok response))

In your example, you bind a with ('ok,'err) result and it would be a little bit far-fetching for a compiler to assume that if a locally abstract, then 'ok and 'err are as well abstract. In other words, you can't abstract two variables with a single variable.

In addition, irrelevant to the scope issue, when you abstract 'a in 'a t to a, and then unify it with _ result by using Ok (ok response) you break the abstraction of a.

let f (type a) (gadt: a t): a Future.t =
  Future.bind (fetch ()) (fun response ->
      match gadt with
      | A (ok, err) ->
        Ok (ok response))

This is indicated by the error message that you decided to ignore,

Type ('a, 'b) result is not compatible with type a

The type variable of 'a t is shared across all branches of GADT and the fact that is constrained in the branch A to ('ok,'error) result doesn't mean that all instances of 'a t constrained to it, even though your type definition has only one branch at this time.

For what it's worth, although it is possible that your example is just a minimization to highlight the problem, but the same behavior could be achieved without any GADT and scope issues using a simple ADT, e.g.,

  type 'a t = {
    ok : string -> 'ok;
    err : string -> 'err;
  } constraint 'a = ('ok,'err) result

  let f {ok; err} =
    Future.bind (fetch ()) (fun response ->
        Ok (ok response))