CoeHTCT synthesis timing out with default args and coercions

Stream: lean4

[Yakov Pechersky]

As part of the mathlib4 port (mathlib4#549), I'm running into an CoeHTCT synthesis timeout. I've minimized away from any mathlib4 import. There seems to a complicated contribution to the timeout, where commenting out some of the instances, or remove default terms/proofs in some of the class definitions, prevents the timeout.

universe u

class One (α : Type u) where
  one : α

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

variable {G : Type _}

class Inv (α : Type u) where
  inv : α → α

postfix:max "⁻¹" => Inv.inv

class Semigroup (G : Type u) extends Mul G where
  mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

class CommSemigroup (G : Type u) extends Semigroup G where
  mul_comm : ∀ a b : G, a * b = b * a

class MulOneClass (M : Type u) extends One M, Mul M where
  one_mul : ∀ a : M, 1 * a = a
  mul_one : ∀ a : M, a * 1 = a

section

variable {M : Type u}

def npowRec [One M] [Mul M] : Nat → M → M
  | 0, _ => 1
  | n + 1, a => a * npowRec n a

end

class Monoid (M : Type u) extends Semigroup M, MulOneClass M where
  npow : Nat → M → M := npowRec
  npow_zero' : ∀ x, npow 0 x = 1 := by intros; rfl -- can comment this out to not timeout

@[default_instance high] instance Monoid.Pow {M : Type _} [Monoid M] : Pow M Nat :=
  ⟨fun x n => Monoid.npow n x⟩

class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M

class DivInvMonoid (G : Type u) extends Monoid G, Inv G, Div G where
  div a b := a * b⁻¹ -- or remove this and the `extends Div G` to not timeout

class Group (G : Type u) extends DivInvMonoid G where
  mul_left_inv : ∀ a : G, a⁻¹ * a = 1

class CommGroup (G : Type u) extends Group G, CommMonoid G

structure Units (α : Type u) [Monoid α] where
  val : α

-- comment out any of the instances below to have `mul_pow'` not time out
instance (priority := low) [Monoid α] : Coe (Units α) α :=
  ⟨Units.val⟩

instance [Monoid α] : Group (Units α) where
  one := ⟨One.one⟩
  mul u₁ u₂ := ⟨u₁.val * u₂.val⟩
  inv := fun u => ⟨u.1⟩
  one_mul u := sorry
  mul_one u := sorry
  mul_left_inv := sorry
  mul_assoc := sorry

instance {α} [CommMonoid α] : CommGroup (Units α) where
  one := ⟨One.one⟩
  mul u₁ u₂ := ⟨u₁.val * u₂.val⟩
  inv := fun u => ⟨u.1⟩
  one_mul u := sorry
  mul_one u := sorry
  mul_left_inv := sorry
  mul_assoc := sorry
  mul_comm := sorry

variable {M : Type _}

theorem mul_pow' [CommMonoid M] (a b : M) (n : Nat) : (a * b) ^ n = a ^ n * b ^ n := sorry -- this times out
theorem mul_pow'' [CommMonoid M] (a b : M) (n : Nat) : HPow.hPow (a * b) n = HPow.hPow a n * HPow.hPow b n := sorry -- this doesn't time out

[Gabriel Ebner]

Coe (Units α) α must not be an instance.

[Gabriel Ebner]

This leads to nontermination, see also https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Gory.20details.20of.20.60coe.60/near/311183132

[Gabriel Ebner]

It could be CoeHead or CoeTail.

[Yakov Pechersky]

Makes sense -- why does commenting out the npow proof fix it?

[Kevin Buzzard]

I don't get this at all. We can't have a coercion from the units of a monoid to the monoid? How am I supposed to know if this is a head or a tail?

[Mario Carneiro]

we used to have a convention that coes of the form Coe (T A) A should be head coes and Coe A (T A) should be tail coes, or was it vice versa?

[Mario Carneiro]

I'm guessing we want it to be a head coe

[Mario Carneiro]

It won't really matter for most purposes unless you start chaining coercions, like if you have an element in {x : Units Nat // p x} and you want an Int

[Kevin Buzzard]

Right! I don't see why I shouldn't want that in general. How would one do that example in lean 4?

[Mario Carneiro]

You wouldn't

[Mario Carneiro]

I don't think it's possible with the current setup of coercions, since there is at most one CoeHead or CoeTail

[Mario Carneiro]

you would need something like CoeHead? CoeOut* CoeIn* CoeTail? where CoeOut : A -> outParam B and CoeIn : outParam A -> B

[Mario Carneiro]

currently we only have CoeIn (that's Coe)

[Mario Carneiro]

You would need CoeOut as well in order to chain coes like the Units one

[Mario Carneiro]

but also, chained coercions were a big headache in lean 3 and I would not be surprised if we essentially only use chained coercions in a very limited way in mathlib because of this

[Mario Carneiro]

note that you can always insert type ascriptions to force multiple coercion in case lean won't do it in one go

[Kevin Buzzard]

Ok so if multiple type ascriptions still work this is fine