parallelism induces weird errors on variable explicitness

Stream: lean4

[Jakob von Raumer]

The screencast below shows the problem, though it's on 4.22.0-rc3, so not sure if it's been resolved since then. Somehow something further down in the file causes Lean to think that EnrichedOrdinaryCategory only expects one explicit argument. Interrupting the processing of the rest of the file removes the error somehow?

simplescreenrecorder-2025-07-22_13.11.42.mkv

[Sebastian Ullrich]

It has always been the case in Lean 4 that elaboration of variables can have different results depending on the declaration (and its context) they are elaborated for, and the original variable command is arguably one of the least bad places to show this error (especially as such divergence is possible but rare in practice). I can't say what difference contexts may cause your specific issue.

[Jakob von Raumer]

Hm, I don't think there should be any error at all? EnrichedOrdinaryCategory should two explicit arguments. It's not overloaded, it's not in any other way amiguous?

[Jakob von Raumer]

I'll try to recreate this in a more minimal example.

[Jakob von Raumer]

Okay, it is overloaded with a bad instance name. Case closed :sweat_smile: