Zulip Chat Archive

Stream: lean4

Topic: Gadts


Joseph O (Mar 15 2022 at 23:02):

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

Edward Ayers (Mar 15 2022 at 23:03):

What is Boolbn?

Edward Ayers (Mar 15 2022 at 23:04):

Also it looks like you are mixing α and a

Edward Ayers (Mar 15 2022 at 23:10):

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 (Mar 15 2022 at 23:10):

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

Kevin Buzzard (Mar 15 2022 at 23:11):

@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 (Mar 15 2022 at 23:13):

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

Joseph O (Mar 15 2022 at 23:13):

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

Joseph O (Mar 15 2022 at 23:13):

But I will put it in code blocks from now on

Arthur Paulino (Mar 15 2022 at 23:17):

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 (Mar 15 2022 at 23:26):

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 (Mar 15 2022 at 23:26):

Another example

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

Arthur Paulino (Mar 15 2022 at 23:30):

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 (Mar 15 2022 at 23:33):

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

Edward Ayers (Mar 15 2022 at 23:35):

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

Mario Carneiro (Mar 15 2022 at 23:36):

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 (Mar 15 2022 at 23:36):

I think my second example fails correctly right?

Mario Carneiro (Mar 15 2022 at 23:36):

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

Mario Carneiro (Mar 15 2022 at 23:37):

but not with the obvious encoding

Mario Carneiro (Mar 15 2022 at 23:38):

For the second example you would write

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

Mario Carneiro (Mar 15 2022 at 23:38):

and yes that's an equality of types

Arthur Paulino (Mar 15 2022 at 23:38):

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 (Mar 15 2022 at 23:39):

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

Edward Ayers (Mar 15 2022 at 23:56):

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?


Last updated: Dec 20 2023 at 11:08 UTC