fix: handle flattened inheritance in wrapInstance#13302
fix: handle flattened inheritance in wrapInstance#13302Kha merged 5 commits intoleanprover:masterfrom
wrapInstance#13302Conversation
github-actions
bot
added
the
toolchain-available
github-actions
bot
added
the
mathlib4-nightly-available
leanprover-bot
added
the
builds-manual
|
Reference manual CI status:
|
mathlib-lean-pr-testing
bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
| try | ||
| if let .some new ← trySynthInstance argExpectedType then | ||
| trace[Meta.wrapInstance] "using existing instance {new}" | ||
| mvarId.assign new |
There was a problem hiding this comment.
I think there ought to be a check that new is defeq to arg, since it's possible for a class argument to be non-canonical, and in any case you'd want to be sure the existing instance is defeq at the correct transparency, right?
I know that sometimes there are explicit fields in structures that are instances, but not instance implicit, and we wouldn't want to replace those.
There was a problem hiding this comment.
We should assume new and arg are not defeq at instances transparency because their types aren't - if they were defeq, we wouldn't have to replace anything in the first place, no? But maybe you mean we should test if they are equal at least at the default level and if that's not the case just skip this case and continue with the ones below?
There was a problem hiding this comment.
Yeah, I'd hope they're defeq at default transparency, as a consistency check.
Rather than skipping, it might even be worth a "synthesized instance is not definitionally equal to provided instance" error — not sure!
| return ← getFieldOrigin parent.structName field | ||
| let some fi := getFieldInfo? env structName field | ||
| | throwError "no such field {field} in {structName}" | ||
| return (structName, fi) |
There was a problem hiding this comment.
getFieldOrigin was meant to be a #print heuristic, and I'm not sure about using it for this purpose. There can be multiple paths to a field, and not every parent needs to be a class. At least it appears to give the parent that mkProjection would pass through.
To copy the behavior of StructInst, what you'd do instead is take getAllParentStructures structName, filter by those that are classes, and then filter by those that have field as a field. Then you take the first that has a synthesizable instance (comments about that below).
|
Mathlib CI status (docs):
|
Kha
changed the title
wrapInstancewrapInstance
Kha
added
the
fast-ci
|
Mathlib CI status (docs):
|
Kha
changed the title
wrapInstance
Kha
added
changelog-no
Instead of unconditionally wrapping value of fields that were copied from flattened parent structures, try finding an existing instance and projecting it first. (cherry picked from commit 031bfa5)
3 participants
Instead of unconditionally wrapping value of fields that were copied from flattened parent structures, try finding an existing instance and projecting it first.