(eli5) Unexpected constructor resulting type

Stream: new members

[McCoy R. Becker]

Can anyone take a shot at explaining what the error "Unexpected constructor resulting type" means?

Context, if useful: I'm attempting to define a hierarchy of types, and write a type judgement relation. So I have:

inductive GType
| Unit : GType
| Bool : GType
| Str : GType
| Trace : GType
| Prod : GType → GType → GType

inductive TType
| GType : GType → TType
| Arrow : TType → TType → TType
| Prod : TType → TType → TType
| DMonad : GType → TType
| MMonad : TType → TType

But then, a relation rule like:

inductive TypeJudgment : TypingContext → Term → TType → Prop
| Type_NonEmptyTrace {Γ : TypingContext} (t1 : Term) (t2 : Term) (τ_1 τ_2 : TType) :
    TypeJudgment Γ t1 τ_1 ->
    TypeJudgement Γ t2 τ_2 ->
    TypeJudgement Γ (Term.TraceAppend t1 t2) (TType.GType GType.Trace)

throws this error. I can't quite tell -- if I'm messing up by having these two type universes, and how to fix it.

[Mario Carneiro]

What is TypingContext and Term? #mwe

[Mario Carneiro]

I'm pretty sure the issue is that you typo'd TypeJudgment as TypeJudgement - lean will report this error if the constructor is not an arrow resulting in the type being defined

[McCoy R. Becker]

This was exactly the issue -- what a dumb mistake, thank you for catching

[Kevin Buzzard]

set_option autoImplicit false to avoid this footgun