type good
type bad
type okay

type ('a, 'b) incl =
  | Incl_good_r : (good, good) incl
  | Incl_good : (good, okay) incl
  | Incl_bad_r : (bad, bad) incl
  | Incl_bad  : (bad, okay) incl
  | Incl_okay_r : (okay, okay) incl

type _ tree =
  | Node  : 'a tree * 'b tree * ('a, 'c) incl * ('b, 'c) incl -> 'c tree
  | Leaf  : good tree
  | Stump : bad tree

let exclude_bad : type a b. (a, b) incl -> bool =
  function
  | Incl_good -> true
  | Incl_good_r -> true
  | _ -> false

(* This doesn't seem to work, though:

type ('a, 'b) incl =
  | Incl_refl : ('a, 'a) incl
  | Incl_good : (good, okay) incl
  | Incl_bad  : (bad, okay) incl

let exclude_bad : type a b. (a, b) incl -> bool =
  function
  | Incl_good -> true
  | Incl_refl : (good, good) incl -> true
  | _ -> false
*)

let rec fix_tree_type : 'a. 'a tree -> good tree =
  fun (type t) (tr : t tree) ->
    match tr with
    | Leaf -> Leaf
    | Stump -> failwith "Not a good tree"
    | Node (l, r, pf1, pf2) -> begin
        if exclude_bad pf1 && exclude_bad pf2 then
          Node (fix_tree_type l, fix_tree_type r, Incl_good_r, Incl_good_r)
        else
          failwith "This node stinks"
      end