Structural Recursion Failed

Stream: general

[Ellis Kesterton]

I'm trying to prove something about two mutually defined propositions inductively. Because the induction tactic does not work with mutual, I used "cases" and made recursive calls manually. However I get the following error:

fail to show termination for
  completeness
with errors
structural recursion failed, produced type incorrect term

Could anyone give me any insight to what this error means? I've stripped my definition down to a single recursive call which is trivially structurally recursive. My real code is a little involved so difficult to post a complete example.

[Ellis Kesterton]

This is the most minimal example I can come up with:

axiom P : Nat → Prop
axiom R : Nat → List Nat → Prop


mutual
  inductive Tree : Nat → Prop where
    | leaf : P n → Tree n
    | node : R n ns → Forest ns ns.length → Tree n

  inductive Forest : List Nat → Nat → Prop where
    | nil : Forest ns zero
    | cons : Tree n → Forest ns k → Forest ns (Nat.succ k)
end


axiom Qs : List Nat → Prop


theorem q (forest : Forest ns k) : Qs ns := by
  cases forest
  case nil =>
    sorry
  case cons t ts =>

    have qs' := q ts
    sorry

[Ellis Kesterton]

My understanding is that 'ts' should be smaller than 'forest', and implicitly the 'k' passed will be smaller too.