Invalid type universe level

Stream: new members

[Shubham Kumar 🦀 (he/him)]

The following code errors with a message - The Type universes are in u + 2 instead of u + 1 which is how inductive types must be smaller than or equal to universe level 1

inductive DecodingErr : Type where
| JErr : JSONErr → DecodingErr
| JParseErr : Prod FileContext ParseErr → DecodingErr
deriving Repr

error:

error: invalid universe level in constructor 'DecodingErr.JParseErr', parameter 'ParseErr' has type
  Type ?u.13626
at universe level
  ?u.13626+2
it must be smaller than or equal to the inductive datatype universe level
  1

Can anyone point me to a direction where I can correct this error?
The implementations of the other data types are

structure Bounds where
  startLine: Int
  startCol: Int
  endLine: Int
  endCol: Int
deriving Repr

and

structure FileContext where
  file : String
  range : Bounds
deriving Repr

[Timo Carlin-Burns]

JSONErr and ParseErr are autoimplicits in this code. Did you intend to refer to some pre-existing types?

[Timo Carlin-Burns]

If I make them explicit, perhaps the error is clearer

set_option autoImplicit false

structure Bounds where
  startLine: Int
  startCol: Int
  endLine: Int
  endCol: Int
deriving Repr

structure FileContext where
  file : String
  range : Bounds
deriving Repr

inductive DecodingErr : Type where
| JErr {JSONErr : Type} : JSONErr → DecodingErr
| JParseErr {ParseErr : Type} : Prod FileContext ParseErr → DecodingErr
deriving Repr

[Timo Carlin-Burns]

Here the JErr constructor takes two parameters, one of which is a Type. Since DecodingError can store types in Type, it might be in at least Type 1

[Shubham Kumar 🦀 (he/him)]

yeah the JSONErr is

def JSONErr : Type := Prod JSONPath String

and ParseErr is something that I haven't define yet so maybe using explict option might be the better first step.
I always forget to add this to every project.
Thanks for reminding me!

[Shubham Kumar 🦀 (he/him)]

unknown identifier 'ParseErr'

better