An example of how to use dependent types to write custom notations.

Tree.v

Inductive tree (X : Type) : Type :=
  | t_a : X -> tree X
  | t_m : tree X -> tree X -> tree X.

Arguments t_a {X} _.
Arguments t_m {X} _ _.

CoInductive tree_builder X : nat -> Type :=
| TbDone : tree X -> tree_builder X 0
| TbRead : forall n, (forall o : option X, tree_builder X match o with
                                                          | Some x => n
                                                          | None => S (S n)
                                                          end) ->
                     tree_builder X (S n).

Arguments TbDone {X} _.
Arguments TbRead {X} _ _.

(* Destructors for tree_builder *)

Definition case0 {X} (x : tree_builder X 0) : tree X :=
  match x with
  | TbDone t => t
  end.

Definition caseS {X n} (x : tree_builder X (S n)) :
  forall o : option X, tree_builder X match o with
                                      | Some x => n
                                      | None => S (S n)
                                      end :=
  match x with
  | TbRead _ f => f
  end.

Definition tb X n := tree_builder X (S n).

(* force is what does the magic here: it takes a tb and coerces it to a
   function that may produce another tb, depending on what it is applied to. *)

Definition force X n (x : tb X n) : forall o : option X,
                                      match o with
                                      | Some x =>
                                        match n with
                                        | 0 => tree X
                                        | S n' => tb X n'
                                         end
                                      | None =>
                                        tb X (S n)
                                      end :=
  fun o =>
    match o return tree_builder X match o with
                                  | Some x => n
                                  | None => S (S n)
                                  end ->
                   match o with
                   | Some x => match n with
                               | 0 => tree X
                               | S n' => tb X n'
                               end
                   | None => tb X (S n)
                   end
    with
    | Some x => match n return tree_builder X n -> match n with
                                                   | 0 => tree X
                                                   | S n' => tb X n'
                                                   end
                with
                | 0 => fun t => case0 t
                | S _ => fun t => t
                end
    | None => fun t => t
    end (caseS x o).

Coercion force : tb >-> Funclass.

Fixpoint parser_cont_type X (n : nat) : Type :=
  match n with
  | 0 => tree X
  | S n' => tree X -> parser_cont_type X n'
  end.

CoFixpoint parser X n : parser_cont_type X n -> tree_builder X n :=
  match n with
  | 0 => fun k => TbDone k
  | S n' => fun k : tree X -> parser_cont_type X n' =>
              TbRead n' (fun o => match o return tree_builder X match o with
                                                                | Some _ => n'
                                                                | None => S (S n')
                                                                end
                               with
                               | Some x => parser X n' (k (t_a x))
                               | None => parser X (S (S n')) (fun (t1 t2 : tree X) => k (t_m t1 t2))
                               end)
  end.

Definition parser' X : tb X 0 :=
  parser X 1 (fun t => t).

Notation "[ x ]" := (Some x) (at level 0).
Notation "''" := None (at level 0).
Notation "!" := (parser' _) (at level 20).

Definition my_tree : tree nat := Eval hnf in ! '' [1] '' '' [2] [3] [4].