type yes
type no

type _ expr =
  | X : no expr
  | Y : yes expr
  | F1 : no expr * no expr -> no expr
  | F2 : _ expr * yes expr -> yes expr
  | F3 : yes expr * _ expr -> yes expr

let rec f : 'maybe expr -> no expr = function
  | Y -> X
  | F1 (x, y)
  | F2 (x, y)
  | F3 (x, y) -> F1 (f x, f y)