to_dual and structure projections

Stream: metaprogramming / tactics

[Jovan Gerbscheid]

Here's an (unrelated) problematic interaction with the module system:

import Mathlib

structure MySup

@[to_dual]
structure MyInf

structure MyLattice extends MySup, MyInf

attribute [to_dual] MyLattice.toMySup
/-
trying to realize `_private.Lean.Environment.0.Lean.Environment.RealizeConstKey` value but `enableRealizationsForConst` must be called for 'MyLattice.toMyInf' first
-/

[Jovan Gerbscheid]

It can be fixed locally by following the instructions from the error, by calling

run_meta Lean.enableRealizationsForConst ``MyLattice.toMyInf

Though I don't really understand what is going on.

[Joachim Breitner]

This is unrelated to the module system, there is no module :-)

[Notification Bot]

3 messages were moved here from #metaprogramming / tactics > to_additive and module system by Joachim Breitner.

[Joachim Breitner]

Looks like to_dual is trying to use realizeConst MyLattice.toMyInf. That function can only be used on declarations after Lean.enableRealizationsForConst has run on them, which Lean core does on for most, but all declarations.

A fix would be to find the place in Lean core where toMyInf is declared and add a call to enableRealizationsForConstafter and near the addDecl call.

[Joachim Breitner]

Do you want to report an issue and give fixing it a shot?

[Jovan Gerbscheid]

Here's a to_dual-free version:

import Lean

structure MySup
structure MyInf
structure MyLattice extends MyInf, MySup

run_meta do -- error
  _ ← Lean.Meta.getEqnsFor? ``MyLattice.toMySup

[Jovan Gerbscheid]

Ok, I've implemented a fix in the to_dual implementation, since it turns out we don't actually want to look at the equation lemmas for MyLattice.MySup. #32396

If you are still insterested in fixing this in core, I think that the filter here is responsible for the trouble.