Class inductive non positive occurence

Stream: lean4

[Anders Christiansen Sørby]

Trying to port Rust trait code using class inductive leads to this

class inductive Circuit (Scalar: Type u)  (CS: Type v) [ConstraintSystem CS Scalar]
    -- Synthesize the circuit into a rank-1 quadratic constraint system.
| circuit : (synthesize : (self : Circuit Scalar CS) → (cs: CS) → (Result CS SynthesisError)) -> Circuit
Scalar CS

Which produces this error:

arg #4 of 'zkSNARK.ConstraintSystem.Circuit.circuit' has a non positive occurrence of the datatypes being declared

Why does this happen?

[Jannis Limperg]

Inductives in Lean must be strictly positive. This means that in an inductive I with constructor C : T1 -> T2 -> ... -> I, I may not occur to the left of an arrow in any of the Ti. In your case, the occurrence of Circuit in the type of the constructor argument synthesize is to blame.

The strict positivity restriction is required for consistency. You can disable it with unsafe; if you don't want to do that, you'll have to change your data representation.

[Marc Huisinga]

I found this helpful as well: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/non-positive.20occurrence.20of.20datatype.20being.20declared.3F/near/221433415