Gadts

Stream: lean4

[Joseph O]

What does this error mean and how do i fix it?
image.png

[Edward Ayers]

What is Boolbn?

[Edward Ayers]

Also it looks like you are mixing α and a

[Edward Ayers]

The problem that the error is talking about is that you need to increase the universe level of the output type of GADT

inductive GADT : Type → Type → Type → Type 1 where
| C1 : α → β → GADT α β Bool
| C2 : α → GADT α α α
| C3 : β → γ → GADT γ β Int

[Joseph O]

Huh thats weird. Ok, let me try to apply the fixes

[Kevin Buzzard]

@Joseph O have you considered upgrading from constantly posting screenshots to posting code in triple backticks? It's much easier to read on mobile and also mush easier to write!

[Arthur Paulino]

You can copy/past the error message as a Lean commentary in the code block

[Joseph O]

I just find it more convenient to include the error message as well in place

[Joseph O]

But I will put it in code blocks from now on

[Arthur Paulino]

If we think it's hard to understand where the error is coming from (because we can't see the the red underlines), at least we can copy your code and see it for ourselves.
Also, some troubles require tweaking the code so we can understand what's happening

[Edward Ayers]

It does seem a bit weird though. Does anyone know why the following errors if I uncomment the second line?

inductive G : Type  → Type → Type  where
| C1 : α → β → G α β
-- | C2 : α → G α α

[Edward Ayers]

Another example

inductive G : Type → Type  where
| C1 : α → G Int

[Arthur Paulino]

This works:

inductive G {α : Type} : Type → Type  where
| C1 : α → G Int

But I don't understand why (given that the code above failed)

[Mario Carneiro]

This looks like https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Regression.20in.20implicit.20argument.20inference

[Edward Ayers]

@Arthur Paulino your example is ok because α is now a parameter

[Mario Carneiro]

I haven't checked the last few nightlies, but if @Edward Ayers you are on the most recent version and leo implemented the index inference algorithm he mentioned at the end, then I would guess that your first example is comparing

inductive G {α β} : Type  → Type → Type  where
| C1 : α → β → G α β
-- | C2 : α → G α α

to

inductive G {α} : ∀ {β}, Type  → Type → Type  where
| C1 : α → β → G α β
| C2 : α → G α α

[Edward Ayers]

I think my second example fails correctly right?

[Mario Carneiro]

well, it's also possible to rewrite all these examples so that they live in Type

[Mario Carneiro]

but not with the obvious encoding

[Mario Carneiro]

For the second example you would write

inductive G (α : Type) : Type where
| C1 : α = Int → G α

[Mario Carneiro]

and yes that's an equality of types

[Arthur Paulino]

Edward Ayers said:

Arthur Paulino your example is ok because α is now a parameter

Ah, I thought Lean was able to create implicit parameters for me as it usually does with theorems

[Mario Carneiro]

The bug report I linked was because the inference algorithm changed to prefer them as indices

[Edward Ayers]

Please correct me if I've messed this up. You get the "is too big for the corresponding inductive datatype" error if the constructor's type is (p₁ : π₁) → ... → (pₘ : πₘ) → (x₁ : α₁) → (x₂ : α₂) ... → (xₙ : αₙ) → G .. where the pᵢ are the parameters and one of the αᵢ : Type u where u is greater than or equal to the universe that the inductive type lives in.

So, the examples here (including OP example) fail because the inference system is not setting (not necessarily erroneously) α, β to be parameters of G?