elaboration failure in algebra.order.group.units

Stream: mathlib4

[Heather Macbeth]

Here is a version without imports of an issue I encountered in the port:

variable {α : Type}

structure Units (α : Type) [Mul α] where
  val : α

instance [Mul α] : CoeHead (Units α) α := ⟨Units.val⟩

instance [Mul α] : Mul (Units α) where
  mul u₁ u₂ := ⟨u₁.val * u₂.val⟩

instance [Mul α] [LE α] : LE (Units α) where
  le u₁ u₂ := u₁.val ≤ u₂.val

class OrderedCommMonoid (α : Type) extends Mul α, LE α

class CovariantClass (α : Type) [Mul α] [LE α] : Prop

instance OrderedCommMonoid.to_CovariantClass_left (α : Type) [OrderedCommMonoid α] :
    CovariantClass α :=
  sorry

theorem mul_le_mul_left [Mul α] [LE α] [CovariantClass α] {b c : α} (bc : b ≤ c) (a : α) :
    a * b ≤ a * c :=
  sorry

variable [OrderedCommMonoid α]

example (a b c : Units α) (h : a ≤ b) : c * a ≤ c * b :=
@mul_le_mul_left α _ _ _ _ _ h _ -- works

example (a b c : Units α) (h : a ≤ b) : c * a ≤ c * b :=
(mul_le_mul_left (h : (a : α) ≤ b) _ : (c : α) * a ≤ c * b)
-- failed to synthesize instance CovariantClass (Units α)

It seems to work in Lean 3:

variable {α : Type}

structure Units (α : Type*) [has_mul α] :=
( val : α )

instance Units.coe [has_mul α] : has_coe (Units α) α := ⟨Units.val⟩

instance [has_mul α] : has_mul (Units α) :=
{ mul := λ u₁ u₂, ⟨u₁.val * u₂.val⟩ }

instance [has_mul α] [has_le α] : has_le (Units α) :=
{ le := λ u₁ u₂, u₁.val ≤ u₂.val }

class OrderedCommMonoid (α : Type) extends has_mul α, has_le α

class CovariantClass (α : Type) [has_mul α] [has_le α] : Prop

instance OrderedCommMonoid.to_CovariantClass_left (α : Type) [OrderedCommMonoid α] :
  CovariantClass α :=
sorry

theorem mul_le_mul_left [has_mul α] [has_le α] [CovariantClass α] {b c : α} (bc : b ≤ c) (a : α) :
  a * b ≤ a * c :=
sorry

variable [OrderedCommMonoid α]

example (a b c : Units α) (h : a ≤ b) : c * a ≤ c * b :=
@mul_le_mul_left α _ _ _ _ _ h _

example (a b c : Units α) (h : a ≤ b) : c * a ≤ c * b :=
(mul_le_mul_left (h : (a : α) ≤ b) _ : (c : α) * a ≤ c * b)

[Heather Macbeth]

Somehow the type annotation (... : (c : α) * a ≤ c * b) is more powerful in Lean 3 than in Lean 4.

[Heather Macbeth]

I cross-posted to #lean4.