Dangerous instance vs elaboration problems

Stream: new members

[Frédéric Dupuis]

In #4057 (which defines inner products based on is_R_or_C), the main outstanding issue is that the linter reports a dangerous instance in the definition:

class inner_product_space (𝕜 : Type*) (α : Type*)
  [nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜] [is_R_or_C 𝕜]
  extends normed_group α, normed_space 𝕜 α, has_inner 𝕜 α := sorry

which presumably comes from the fact that normed_group α doesn't have 𝕜 as a parameter. I gather that the usual way to fix this is to move normed_group α into the assumptions, as in

class inner_product_space (𝕜 : Type*) (α : Type*)
  [nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜] [is_R_or_C 𝕜]  [normed_group α]
  extends normed_space 𝕜 α, has_inner 𝕜 α := sorry

However, when I do that, I run into some very annoying elaboration issues where I have to constantly spoonfeed it 𝕜 and/or α in lemmas that rewrite norms in terms of inner products, even though the relevant instance is directly present in the context.

So: just how dangerous is an instance like this? Would it still send the search algorithm into a wild goose chase, even though the only possibilities for 𝕜 should always remain only ℂ and ℝ?

[Heather Macbeth]

I think you could have asked this in #maths! :) @Yury G. Kudryashov @Sebastien Gouezel ?