Switch on GADT expecting all branches to have same type

1

The following rescript code is not accepted:

type foo<'a>

type rec var<'a> = Basic: var<unit> | Nested: var<foo<unit>> 

let process: 'a. var<'a> => () = var => {
  switch var {
    | Basic => ()
    | Nested => () // error
  }
}

let res = process(Basic)

The error message is:

This pattern matches values of type var<foo<unit>>
but a pattern was expected which matches values of type var<unit>

The incompatible parts:
  foo<unit> vs unit

It appears that a switch over a GADT does not work where the branches may have different types.

What I believe to be the equivalent OCaml code is accepted:

type _ foo

type _ var =
  | Basic : unit var
  | Nested: unit foo var

let process: type a. a var -> unit = function
  | Basic -> ()
  | Nested -> ()
  
let res = process Basic

It appears that OCaml does not expect the branches to have the same type.

Is there some way to use a switch on a GADT in rescript where the branches may have different types?

2

You can express the same type signature in rescript:

let process: type a. var<a> => () = var => {
  switch var {
    | Basic => ()
    | Nested => ()
  }
}

Or, if you don’t need the universal quantification and don’t want to annotate the whole function type, you can do:

let process = (type a, var: var<a>) => {
  switch var {
    | Basic => ()
    | Nested => ()
  }
}

Also, function ... in OCaml is just syntax sugar for fun x -> match x with ... (which translated to rescript is x => switch x { ... })

7 Likes
3

@glennsl Thank you! I was missing that 'a. and type a. are different.

4

Yep, they certainly are. type a is called a locally abstract type, which is essentially a proper abstract type definition that is scoped to a function. This allows it to be a bit schizophrenic, assuming different identities depending on where you look at it from. At least that’s the way I view it. From the outside it will look like an ordinary type variable, and from inside the branches of a pattern matched GADT it will take on the identity of (i.e. be refined to) the type assigned to it by the GADT constructor used in the pattern.

And the reason it fails even when there’s no payload using that type is that the type could also occur elsewhere and therefore still needs to be refined.

This, for example, is also perfectly valid:

type rec var<'a> = Unit: var<unit> | Int: var<int>

let process  = (type a, var: var<a>, x: a) => {
 switch var {
   | Unit => 42 // Here `x` would have type `unit`
   | Int => x // While here it has type `int`
 }
}

let res = process(Int, 26)
6 Likes