instance for both DFunLike and (fun i => b i)

Stream: Is there code for X?

[Edward van de Meent]

i have defined a bundled structure Metric X, which bundels a metric on the space X. i'd like to define hammingDist' ... : Metric X in such a way that T with [DFunLike T ι β] and the appropriate assumptions on ι and β, hammingDist' : Metric T succeeds, while hammingDist : Metric (∀ i, β i) does too. is there some way to do this?

my guess would be to have hammingDist' take {X:Type*} and [DFunLike T ι β], and define an instance : DFunLike (∀ i, β i) ι β, but that seems like such a straightforward idea that i suspect it doesn't exist because it would result in some kind of synthesis/diamond/etc. problem...

is there some other way around this?