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 : type maybe. maybe expr -> no expr = function
  | X -> X
  | Y -> X (* Error: This pattern matches values of type yes expr
       but a pattern was expected which matches values of type no expr
       Type yes is not compatible with type no *)
  | F1 (x, y) -> F1 (f x, f y)
  | F2 (x, y) -> F1 (f x, f y)
  | F3 (x, y) -> F1 (f x, f y);;