FunLike for subtype of FunLike

Stream: Is there code for X?

[Matthew Ballard]

Do we not have this? Is it a bad idea?

import Mathlib

variable {α β : Sort*} {γ : β → Sort*} (p : α → Prop) [DFunLike α β γ]

set_option trace.Meta.synthInstance true in
#synth DFunLike {f : α // p f} β γ

#synth CoeFun {f : α // p f} fun _ => (b : β) → γ b

instance instDFunLikeSubtype : DFunLike {f : α // p f} β γ where
  coe := fun f b => f.val b
  coe_injective' := fun _ _ h => Subtype.coe_injective <| DFunLike.coe_injective' h

[Yaël Dillies]

Yes, see my closed PR

[Yaël Dillies]

#10631

[Kyle Miller]

There's a closed PR with a message that says "it does seem like a bad idea", but what was the reason you decided it was a bad idea?

[Eric Wieser]

FunLike is a bad idea (because it introduces a second canonical spelling and confluence issues), but CoeFun should be harmless and probably convenient.

[Matthew Ballard]

I was going through the helper instances in mathlib to see what ones might suffer for discrimination tree issues. docs#Submodule.instFunLikeSubtypeDualMemDualAnnihilator doesn't but seems like a prime motivator for such a thing

[Matthew Ballard]

@Eric Wieser what is the other spelling here? The confluence issues are what made it a bad idea I imagine (or at least de-motivated).

[Eric Wieser]

Subtype.val vs DFunlike.coe

[Yaël Dillies]

Kyle Miller said:

There's a closed PR with a message that says "it does seem like a bad idea", but what was the reason you decided it was a bad idea?

Checkout the branch and check out the CI errors

[Kyle Miller]

@Yaël Dillies It'd be useful to document the results of your experiment so that when this question comes up we don't have to re-evaluate build results. It's fine if you don't want to summarize your findings, but that just means that the PR isn't showing anything on its own.