Discrepancy between TC synthesis in Lean 3 and 4

Stream: lean4

[Tomas Skrivan]

I have a piece of code that in Lean 3 fails to synthesize an instance in finite number of steps but in Lean 4 it timeouts. I really do not understands what is going wrong in the Lean 4 code. It gets into very strange infinite loop.

Previously I thought it was a problem with the usage of outParam but I have eliminated it from the code and the problem still persists.

Lean 3 code:

universes u v w

class Vec (X : Type u)

class IsLin {X Y} [Vec X] [Vec Y] (f : X → Y)

structure ℝ :=
  (value : nat)

instance {X : Type u} {Y : Type v} [Vec X] [Vec Y] : Vec (X × Y) := sorry
instance {α : Type u} {X : Type v} [Vec X] : Vec (α → X) := sorry

@[priority std.priority.default+1]
instance : Vec ℝ := sorry

--------------

instance comp_is_lin {X Y Z : Type} [Vec X] [Vec Y] [Vec Z]
  (f : Y → Z) (g : X → Y) [IsLin f] [IsLin g]
  : IsLin (λ x, f (g x)) := sorry

----------------

class Trait (X : Type u) :=
  (R : Type v)

attribute [reducible] Trait.R

class SemiInner (X : Type u) (R : Type v) :=
  (semiInner : X → X → R)

@[reducible] instance instTrait (X) (R : Type u) [SemiInner X R] : Trait X := ⟨R⟩

class SemiHilbert (X) (R : Type u) [Vec R] extends Vec X, SemiInner X R

instance instSemiHilbertForAll (X R) [Trait X] [Vec R] [SemiHilbert X R] (ι : Type v) : SemiHilbert (ι → X) R := sorry
instance instSemiHilbertℝ : SemiHilbert ℝ ℝ := sorry

--------------

def norm {X} [Trait X] [inst : SemiInner X (Trait.R X)] (x : X) : Trait.R X := sorry
def sum' {n} (f : fin n → ℝ) : ℝ := sorry

variables (n m : nat)

-- these all should work
-- oddly enough lean 3 does not require the `reducible` attribute to get these working
example : Trait (fin n → fin m → ℝ) := infer_instance
example : SemiInner ℝ (Trait.R ℝ) := infer_instance
example : SemiHilbert (fin n → ℝ) ℝ := infer_instance
example : SemiHilbert (fin n → ℝ) (Trait.R ℝ) := infer_instance
example : Trait (fin n → fin m → (Trait.R ℝ)) := infer_instance
example : SemiHilbert (Trait.R ℝ) ℝ := infer_instance

-- This fails to synthesize in finite number of steps
example : IsLin  (λ (x : ℝ), sum' (λ i : fin n, norm x)) := infer_instance

Fails with:

failed to synthesize type class instance for
n : ℕ
⊢ IsLin (λ (x : ℝ), sum' (λ (i : fin n), norm x))

On the other hand, the Lean 4 code:

class Vec (X : Type u)

class IsLin {X Y} [Vec X] [Vec Y] (f : X → Y)

structure ℝ where
  value : Float

instance {X : Type u} {Y : Type v} [Vec X] [Vec Y] : Vec (X × Y) := sorry
instance {α : Type u} {X : Type v} [Vec X] : Vec (α → X) := sorry

instance (priority := mid+1) : Vec ℝ := sorry

--------------

instance comp_is_lin {X Y Z : Type} [Vec X] [Vec Y] [Vec Z]
  (f : Y → Z) (g : X → Y) [IsLin f] [IsLin g]
  : IsLin (λ x => f (g x)) := sorry

----------------

class Trait (X : Type u) where
  R : Type v

attribute [reducible] Trait.R

class SemiInner (X : Type u) (R : Type v) where
  semiInner : X → X → R

@[reducible] instance (X) (R : Type u) [SemiInner X R] : Trait X := ⟨R⟩

class SemiHilbert (X) (R : Type u) [Vec R] extends Vec X, SemiInner X R

instance (X R) [Trait X] [Vec R] [SemiHilbert X R] (ι : Type v) : SemiHilbert (ι → X) R := sorry
instance : SemiHilbert ℝ ℝ := sorry

--------------

def norm {X} [Trait X] [inst : SemiInner X (Trait.R X)] (x : X) : Trait.R X := sorry
def sum {n} (f : Fin n → ℝ) : ℝ := sorry

variable (n m : Nat)

-- these all should work
example : Trait (Fin n → Fin m → ℝ) := by infer_instance
example : SemiInner ℝ (Trait.R ℝ) := by infer_instance
example : SemiHilbert (Fin n → ℝ) ℝ := by infer_instance
example : SemiHilbert (Fin n → ℝ) (Trait.R ℝ) := by infer_instance
example : Trait (Fin n → Fin m → (Trait.R ℝ)) := by infer_instance
example : SemiHilbert (Trait.R ℝ) ℝ := by infer_instance

-- set_option synthInstance.maxHeartbeats 50 in
-- set_option pp.explicit true in
-- set_option trace.Meta.synthInstance true in

-- This should not timeout but failt in finite number of steps like in Lean 3
example : IsLin  (λ (x : ℝ) => sum λ i : Fin n => norm x) := by infer_instance

Fails with:

(deterministic) timeout at 'typeclass', maximum number of heartbeats (500) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

I'm expecting the Lean 4 version fail in the same fashion as Lean 3 code.

[Tomas Skrivan]

I forgot to mention versions I'm using:

Lean (version 3.38.0, commit a8cf8a0c9ea1, Release)
Lean (version 4.0.0-nightly-2022-01-25, commit b20ecd02d76d, Release)

[Tomas Skrivan]

One strange thing is that in Lean 3 version you can remove the priority and reducible attributes and the code behaves the same. Not the case in Lean 4.