OCaml polymorphic variants in pattern matching

Question

I'm growing a small programming language by means of AST transforms. That is, starting from the VM and slowly adding layers that help the programmer.

Since each layer knows how to transform its new types, I've done something like this:

module AST0 = struct

  type t = [
    | `Halt
    | `In
    | `Out
    | `Add of (int * int * int)
    | `Sub of (int * int * int)
  ]

  let lower (ast : t list) = ast
end

module AST1 = struct
  type t = [
    AST0.t

    | `Inc of int
    | `Dec of int 
    | `Cmp of (int * int * int)
  ]

  let lower (ast : t list) =
    let lower_one = function
      | `Inc a -> [`Add (a, a, `Imm 1)]
      | `Dec a -> [`Sub (a, a, `Imm 1)]
      | `Cmp (a, b) -> [`Sub (13, a, b)]
      | (x : AST0.t) -> AST0.lower [x]      (* <--- problem line *)
    in
    List.concat @@ List.map lower_one ast
end

Unfortunately I get the error:

File "stackoverflow.ml", line 28, characters 8-20:
Error: This pattern matches values of type AST0.t
       but a pattern was expected which matches values of type
         [? `Cmp of 'a * 'b | `Dec of 'c | `Inc of 'd ]
       The first variant type does not allow tag(s) `Cmp, `Dec, `Inc

I thought since the compiler is smart enough to notice that I haven't handled X Y and Z variants in an arbitrary match case that it could tell that x in AST1.lower will never actually be one of Cmp or Inc or Dec. This doesn't seem to be the case.

Have I misunderstood OCaml's type system? Am I missing something obvious? Is this a dumb approach?

Answer 1

You cannot locally constrain the type of a case pattern. The type constraint : AST0.t enforces the other patterns' type to AST0.t too. That is why your code does not type check; `Inc is not included in AST0.t.

However, there is a neat feature in OCaml exactly for what you want to do. Use #AST0.t pattern alias, instead of the type constraint. See https://caml.inria.fr/pub/docs/manual-ocaml/lablexamples.html#sec46 for details:

  (* I fixed several other trivial typing problems *)
  let lower (ast : t list) =
    let lower_one = function
      | `Inc a -> [`Add (a, a, 1)]
      | `Dec a -> [`Sub (a, a, 1)]
      | `Cmp (a, b, c) -> [`Sub (13, a, b)]
      | #AST0.t as x -> AST0.lower [x]     (* <--- problem line *)
    in
    List.concat @@ List.map lower_one ast

#AST0.t as x is not only an abbreviation of (`Halt | `In | `Out | `And _ | `Sub _ as x) but also changes the type of x in the right hand side of -> from [> AST1.t] to [> AST0.t]. You can use it as AST0.t there.