Inductive Unit : Set := unit : Unit.

Inductive Ty : Unit -> Set := ty (u : Unit) : Ty u.

Definition f (arg : Ty unit) :=
  match arg with
    | ty unit => unit
    | _ => unit
  end.

Axiom dummy : Ty unit. (* for f's wild_pattern case *)