Stupid assumptions tactic

Stream: general

[Patrick Massot]

It would be nice to have a tactic detecting bad type class assumptions in the current context. I just wasted ten minutes because my bad variables management got me topological_space E and normed_group E in the same context and then Lean was super confused. The tactic would inspect all type class assumptions and somehow hunt for conflicting ones. This is a vague specification, but I feel like @Alex J. Best could enjoy that challenge.

[Yury G. Kudryashov]

Something like fails_quickly?

[Yury G. Kudryashov]

I mean, try to remove all instances but one (and all those depending on it) and try to deduce it from what's left.

[Mario Carneiro]

I think it would be more like two assumptions with a common parent, for example group R and ring R both have a has_mul R parent

[Mario Carneiro]

I think that it should be restricted to parents in the extends sense rather than arbitrary typeclass diamonds, which would be a lot more expensive to determine

[Yaël Dillies]

Best would be to detect the Type-valued typeclasses which add fields, maybe by tagging them.