Type escape error in mutually recursive functions on GADT and phantom types

Learning
1

Hello,

I’m trying to write an interpreter using GADTs and phantom types to encode AST variants with state and exceptions. I’m now combining the state and exception variants and I have two mutually recursive functions.

Here’s a minimal example that reproduces the type error:

type 'a has_state_m = 'a constraint 'a = [< `HasState ]
type 'a has_exception_m = 'a constraint 'a = [< `HasException ]

type _ t =
  | HasState : 'a t -> 'a has_state_m t
  | HasException : 'a t -> 'a has_exception_m t
  | Core : 'a t -> 'a t
  | End : 'a t

let rec print : type a. a t -> unit =
  fun mode ->
    match mode with
    | HasState inner ->
        print_endline "Has State";
        do_something_for_state (HasState inner)
    | HasException inner ->
        print_endline "Has Exception";
        print inner
    | Core inner ->
        print_endline "Core";
        print inner
    | End -> print_endline "End of modes"; ()

and do_something_for_state : 'a -> unit = function
  | HasState inner ->
      print_endline "doing something for Has State";
      print inner
  | _ -> failwith "Not applicable"

Error: The value inner has type [< `HasState ] t
       but an expression was expected of type [< `HasState ] t
       The type constructor $0 would escape its scope

I cannot remove the mutual recursion because it reflects the semantics of my interpreter. Does anyone know a way to structure this code so that it typechecks?

2

You should essentially never mix unification variables (an 'a appearing unbound in an annotation) with GADTs (and recursion). Using the correct annotation fixes the surface issue:

let rec print : type a. a t -> unit = ...
and do_something_for_state : type a. a t -> unit = function
  | HasState inner ->
      print_endline "doing something for Has State";
      print inner
  | _ -> failwith "Not applicable"

However, the next issue is probably that your phantom type represents the wrong semantics: currently you can only have state xor exceptions. Moreover, the interaction of polymorphic variants and GADTs is complex and brittle. Thus I tend to advise to start with the simpler object type encoding:

type yes = Yes
type no = No

type _ t =
  | HasState : <has_exception:'e; .. > -> <has_state:yes; has_exception:'e>  t
  | HasException : <has_state:'s; .. > t -> <has_exception:yes; has_state:'s> t
  | Core : 'a t -> 'a t
  | End : 'a t
3

Thank you so much! This solved my problem.