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.