Goblint GADT query attempt

queries.ml

type _ t =
  | Query1: int t
  | Query2: bool t 

type result = unit (* for now *) 
    
    
type ctx = {
  ask: 'a. 'a t -> result
}

module type S =
sig
  val query: ctx -> 'a t -> result
end


module MCP: S =
struct
  let rec query (ctx: ctx) (type a) (q: a t): result =
    let ctx' = {
      ask = (fun (type b) (q: b t) -> query ctx q)          
      (* on q above: *)
      (* Error: This expression has type b t
         but an expression was expected of type 'a
         The type constructor b would escape its scope *) 
      (* why expected ['a] not ['a t]? *)
    }
    in
    failwith "TODO"
end