class abbrev set-up not seeing through other abbrevs

Stream: lean4

[Isak Colboubrani]

The following fails with unknown constant 'IntegrallyClosedDomain₂.mk' and 'IsIntegrallyClosed' is not a structure.

import Mathlib
class abbrev IntegrallyClosedDomain₂ (P : Type*) := CommRing P, IsDomain P, IsIntegrallyClosed P

In contrast the following works:

import Mathlib
class abbrev IntegrallyClosedDomain₁ (P : Type*) := CommRing P, IsDomain P, IsIntegralClosure P P (FractionRing P)

Also, trying to solve the first issue using the following does not work:

import Mathlib
def IsIntegrallyClosed.mk (R : Type*) [CommRing R] := IsIntegralClosure.mk (A := R) (R := R) (B := FractionRing R)
class abbrev IntegrallyClosedDomain₃ (P : Type*) := CommRing P, IsDomain P, IsIntegrallyClosed P

Note that  the referenced IsIntegralClosure is implemented as an abbrev.

It seems like the class abbrev set-up was not seeing through other abbrevs.

Is this intended behaviour?

[Isak Colboubrani]

#mwe showing the issue:

import Mathlib
class abbrev A (B : Type*) := CommRing B, IsIntegrallyClosed B

[Kevin Buzzard]

Can you give an import-free #mwe ?

[Damiano Testa]

Is this highlighting the same issue?

class Z0 where
abbrev Z1 := Z0

-- works
class abbrev Z0' := Z0

-- `Z1` is not a structure
class abbrev Z1' := Z1

[Daniel Weber]

The problem is not with class abbrev, it's with extends:

structure Z0 where

abbrev Z1 := Z0

-- works
structure Z0' extends Z0

-- `Z1` is not a structure
structure Z1' extends Z1

[Isak Colboubrani]

Update #mwe. Note that the only difference between the working and non-working examples is class abbrev vs bare abbrev :

class OK₁
class abbrev OK₂ := OK₁
class OK₃ extends OK₂

class FAIL₁
abbrev FAIL₂ := FAIL₁
class FAIL₃ extends FAIL₂

---

structure OKAY₁
class abbrev OKAY₂ := OKAY₁
structure OKAY₃ extends OKAY₂

structure FAILURE₁
abbrev FAILURE₂ := FAILURE₁
structure FAILURE₃ extends FAILURE₂

[Mac Malone]

That's because a class abbrev is not an abbrev but a structure.

[Isak Colboubrani]

@Mac Malone I apologize if this is a basic question, but does that mean that everything is working as expected here from both a Lean and Mathlib perspective?

From the perspective of a a novice undergraduate user, this is the code I naïvely assumed would work:

import Mathlib
class abbrev IntegrallyClosedDomain₂ (P : Type*) := CommRing P, IsDomain P, IsIntegrallyClosed P

I'm trying to pinpoint exactly where my reasoning went wrong here, and what I can do to fix it :)

[Kyle Miller]

Daniel Weber said:

-- `Z1` is not a structure
structure Z1' extends Z1

This looks like it's worth reporting as a bug.

[Mac Malone]

@Isak Colboubrani As Kyle noted, the problem here is that a structure does not see through abbreviations. As you experienced, this is unintuitive and would be nice to fix.

[Kyle Miller]

Thanks for reporting it (lean4#5417)