Consider this example:
Inductive T :=
| foo : T
| bar : nat -> T -> T.
Fixpoint evalT (t:T) {struct t} : nat :=
match t with
| foo => 1
| bar n x => evalBar x n
end
with evalBar (x:T) (n:nat) {struct n} : nat :=
match n with
| O => 0
| S n' => (evalT x) + (evalBar x n')
end.
Coq rejects it with an error: Recursive call to evalBar has principal argument equal to "n" instead of "x".
I understand that termination checker got confused by two unrelated inductive types (T and nat). However, it looks like the function I am trying to define will indeed terminate. How can I make Coq accept it?