Parent instance arguments in auto_param / opt_param

Stream: general

[Eric Wieser]

This proof was a really weird one to get working (verbatim from #5645):

/-- A linearly ordered commutative monoid with a zero element. -/
class linear_ordered_comm_monoid_with_zero (α : Type*)
  extends linear_order α, comm_monoid_with_zero α, ordered_comm_monoid α :=
(zero_le_one : (0:α) ≤ 1)
(lt_of_mul_lt_mul_left := λ x y z, by {
  -- type-class inference uses a meaningless `linear_order` without this!
  set l : linear_order α := {
    le := le,
    lt := lt,
    le_refl := ‹_›,
    le_trans := ‹_›,
    lt_iff_le_not_le := ‹_›,
    le_antisymm := ‹_›,
    le_total := ‹_›,
    decidable_le := ‹_›,
    decidable_eq := ‹_›,
    decidable_lt := ‹_› },
  apply imp_of_not_imp_not,
  intro h,
  apply not_lt_of_le,
  apply mul_le_mul_left,
  exact @le_of_not_lt _ l _ _ h })

If I don't construct my own l, it uses the a : linear_order α object (is there a new "a" bug hiding here waiting to be found?) from the context, and then flops because it doesn't have any knowledge that a contains the other local hypotheses as its fields.

Is there a trick I'm missing here? Would there be any value to a tactic that constructs these "correct" instances automatically, discarding the bad ones?

[Gabriel Ebner]

This is probably related to lean#282. I think the cleanest workaround is just to extract the default argument into a lemma.