Help tracking down a Lean bug

Stream: lean4

[Sebastian Reichelt]

I've run into a specific Lean 4 bug a few times but so far failed to minimize it, in fact the locations where the bug appears have always been places where I build concrete instances of complex dependent types, so it sort of resists minimization. Therefore I'm posting here in the hope that someone could either offer some guidance on how to minimize it, or look at my code directly. (Sorry, it's really not small.)

The symptom is that definitions fail to compile with "(kernel) function expected". The (expected) function that is displayed in the message is actually an object with a CoeFun instance, i.e. there is some situation where Lean forgets to use this instance and outputs a raw function application instead. Unfortunately, the failure is always quite a few layers of abstraction away from the code where the function application (via CoeFun) actually happens.

It seems that at least two ingredients are required for the bug to occur:

• The code where the function application happens is used as part of a parameter x of a dependent type T (x : ...). The definition where the failure occurs receives an instance of T x and then uses the value of x as part of the definition.
• Apparently, the bug only occurs if x involves sufficiently complex structures/classes. I find this part especially hard to pinpoint, but now at least I have a single commit that triggers the bug at a specific location, and the change that triggered it was essentially just a refactoring that moves fields between structures and classes.

Anyway, I have committed the broken state to master in my repo at https://github.com/SReichelt/universe-abstractions. The failing definitions are https://github.com/SReichelt/universe-abstractions/blob/3f7bae7fee593af6f571a87a053b632980e60860/UniverseAbstractions/Instances/HomUniverses/Type.lean#L125 and a few following ones. Any help would be appreciated, thanks!

[Sebastian Reichelt]

I've managed to reduce it to 1150 self-contained lines: https://gist.github.com/SReichelt/70a75eb4a7e8b899294d8b1a72c1833a
Some further simplifications made the bug disappear, but I feel that I could reduce it a lot further if I had a better handle on the cause of this bug. Any ideas?

[Sebastian Reichelt]

Oh, I found a workaround: https://gist.github.com/SReichelt/70a75eb4a7e8b899294d8b1a72c1833a#file-kernelfunctionexpected-lean-L705
I suppose that could give a hint about the nature of the bug as well.