arg #n of func contains invalid occurrence. Which arg is it?

Stream: general

[nrs]

I have a sort of complicated function and I'm getting (kernel) arg #3 of 'RecursionSchemes.WType.sup' contains a non valid occurrence of the datatypes being declared. This isn't the first time I've encountered this error, in this specific case since there's a single occurrence of the datatype the position is obvious, but I was wondering: when this error occurs, is there a way to trace what number is getting assigned to the arguments of a definition that fails to compile?

namespace RecursionSchemes
structure Functor where
  actionOnType : Type -> Type
  actionOnMorphism {α β : Type} : (α -> β) -> actionOnType α -> actionOnType β

inductive Container : Type 1
  | mk : (shape : Type) -> (shape -> Type) -> Container

def functorOf : Container -> Functor
  | ⟨shape, positions⟩ => {
    actionOnType := fun (α : Type) => (s : shape) × (positions s -> α)
    actionOnMorphism := fun (m : _) => fun | ⟨s, f⟩ => ⟨s, m ∘ f⟩
    }

inductive WType (shape : Type) (positions : shape -> Type) : Type
  | sup : (functorOf ⟨shape, positions⟩).actionOnType (WType shape positions) -> WType shape positions

edit: wrt actually fixing the problem, if someone has a similar issue: you have to use an inductive type instead of a def for functorOf

[Kyle Miller]

It's argument number 3 like it says, but you have to keep in mind that the inductive type's parameters are the first arguments.

[nrs]

Kyle Miller said:

It's argument number 3 like it says, but you have to keep in mind that the inductive type's parameters are the first arguments.

ah this was what wasn't adding up, thanks!