Mapping GADT AST node to list of it's children not allowed by compiler?

Learning
, , ,
1

I have a GADT type for representing an AST and would like to have a function that gives me a list of a nodes children wrapped in polyvariant

let take_next : type a. a t -> [`Expr of expr t | `Stmt of stmt t | `Decl of decl t] list =
    let module Opt = struct
        open Option
        let expr = map (fun x -> `Expr x)
        let stmt = map (fun x -> `Stmt x)
        let decl = map (fun x -> `Decl x)
    end in
    function
    | CompoundStmt lst -> lst |> List.map (fun stmt -> `Stmt stmt)
    | DeclStmt decl -> [`Decl decl]
    | CastExpr {expr; _}
    | UpdateExpr {expr; _} 
    | UnaryExpr {expr; _}
    | FieldExpr {expr; _}
    | RetStmt expr
    | ExprStmt expr -> [`Expr expr]
    | IfStmt {cond; if_true; if_false} -> cons_opts' [Some (`Expr cond); Some (`Stmt if_true); Opt.stmt if_false]
    | ForStmt {init; cond; update; body} -> cons_opts' [Opt.stmt init; Opt.expr cond; Opt.expr update; Some (`Stmt body)]
    | SwitchStmt {cond; body}
    | WhileStmt {cond; body}
    | DoStmt {cond; body} -> [`Expr cond; `Stmt body]
    | LabeledStmt {body; _} -> [`Stmt body]
    | CaseStmt {body; _} -> [`Stmt body] (* Ignore cond for now *)
    | FuncDecl {args; body; _} -> (`Stmt body)::(args |> List.map (fun arg -> `Decl arg))
    | VarDecl {init; _} -> cons_opts' [Opt.expr init]
    | IndexExpr {expr; index} -> [`Expr expr; `Expr index]
    | CommaExpr (lhs, rhs)
    | BinExpr {lhs; rhs; _} -> [`Expr lhs; `Expr rhs]
    | CallExpr {args; _} -> args |> List.map (fun arg -> `Expr arg)
    | CondExpr {cond; if_true; if_false} -> [`Expr cond; `Expr if_true; `Expr if_false]
    | _ -> []

Unfortunately I get this message which means just about nothing to me. And for that matter I don’t think what I’m asking for is unreasonable, just a function from GADT type to list of fixed types.

Error: This definition has type
         'a t -> [ `Decl of decl t | `Expr of expr t | `Stmt of stmt t ] list
       which is less general than
         'a0.
           'a0 t ->
           [ `Decl of decl t | `Expr of expr t | `Stmt of stmt t ] list

I’ve found these posts when searching for my issue but again don’t see how they’d be relevant as no permutation of proposed type annotations would make the compiler shut up which leads me to believe that it’s just not possible for some hand wavy reason

2

Have you tried adding a locally abstract type annotation to your function?

let take_next (type a) (x : a t) = ...

See https://discuss.ocaml.org/t/locally-abstract-type-polymorphism-and-function-signature for a longer discussion of this.

Cheers,
Nicolas

3

The issue is unrelated to GADTs: this is the value restriction at work.
The definition of the Opt module computes some value, and thus makes the function take_next a non-syntactic function.

let module Opt = struct
        open Option
        let expr = map (fun x -> `Expr x)
        let stmt = map (fun x -> `Stmt x)
        let decl = map (fun x -> `Decl x)
    end in
   function

The solution is to η-expand those functions in the Opt module

    let module Opt = struct
        open Option
        let expr  x = map (fun x -> `Expr x) x
        let stmt x = map (fun x -> `Stmt x) x
        let decl x  = map (fun x -> `Decl x) x
    end in

PS: take_next: type a. a t -> ... is already using a locally abstract type, and this is the right form to use for GADTs function in general since it doesn’t require to be able to distinguish polymorphic recursion from ordinary recursion.

1 Like
4

Wow, very impressed that you got that right, I’ve moved the module outside of the function and that worked, although I’m not happy with it polluting the module namespace
edit: moved it back into the function and that also works