Open packages "leak" via #check

Stream: lean4

[Robert Maxton]

Consider the following MWE:

import Mathlib.CategoryTheory.Category.Basic

open CategoryTheory

universe v v₁ u u₁ u₂
variable {C : Type u} [Category.{v, u} C]


section «notation»
--  open Lean Macro Parser Syntax Tactic PrettyPrinter Qq Elab.Term in
--  #check ℕ
end «notation»

As written, all is well. But if the two commented lines are uncommented, Lean reports an error under my use of Category: too many explicit universe levels for 'Lean.Parser.Category'. Even though the open package occurs after the line, within its own section, and in fact within an open in declaration so it should only apply to the next line, apparently none of that stops Lean from "backporting" my open declaration so that it confuses it the line before.

Am I missing a reason this is intended behavior, or is this just a bug?

[Kim Morrison]

This is not great, but not too surprising. The variable statements unfortunately can't be processed once and for all, but need to be re-elaborated, and this opens the door to bad situations like this.

It is going to need to be addressed in intra-file parallelism, so we will get there eventually, but it's unlikely there'll be a fast fix for this one, unfortunately. (It is "just" a bug!)

I guess in the meantime my suggestion is to keep your category theory code and meta code separate, and avoid opening both Categorys at once! :-)

[Robert Maxton]

Alright, just wanted to make sure I wasn't going mad :p. Thanks!