section, universe, namespace deadly interaction

Stream: general

[Yaël Dillies]

I think we've just uncovered one of the "corner-cases" @Gabriel Ebner was talking on this PR (and the linked issue).

section sec

universe u

structure equipartition (V : Type u) :=
(parts : V)

namespace equipartition
variables {V : Type u}

protected def stuff (P : equipartition V) : ℕ := 0

end equipartition

variables {V : Type u}

protected def equipartition.stuff' (P : equipartition V) : ℕ := 0

variable (P : equipartition V)

#printprefix equipartition
#check P.stuff              -- works
#check P.stuff'             -- works
#check equipartition.stuff  -- doesn't work
#check equipartition.stuff' -- works

end sec

The bug seems to result from a very peculiar arrangement of section, universe and namespace. If you

• replace universe by universes, it doesn't work
• replace universe by universe variable it does work
• replace Type u by Type* it does work
• delete section, it does work
• move universe u above section it does work

[Gabriel Ebner]

move universe u above section it does work

I think this is what you should do.

[Kevin Buzzard]

#check equipartition.stuff  -- doesn't work
#check @equipartition.stuff  -- works

shrug