Understanding outParam

Stream: lean4

[Tomas Skrivan]

I'm really confused on what outParam is actually doing. To my limited understanding, you can use it to prevent for example an instance to be polymorphic in certain argument.

I would like to understand the following code that runs into an infinite loop exactly because of outParam.

class Vec (X : Type u)

structure ℝ where
  value : Float

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

class SemiHilbert (X) (R : outParam $ Type u) [outParam $ Vec R] extends Vec X

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

set_option synthInstance.maxHeartbeats 15 in
set_option trace.Meta.synthInstance true in
example : SemiHilbert (Fin n → ℝ) ℝ := by infer_instance

It works fine if you change (R : outParam $ Type u) to (R : Type u) in the definition of SemiHilbert class.

What I do not understand is why the last subgoal

[Meta.synthInstance.newSubgoal] Vec _tc.0

causes TC to going into an insane infinite loop producing longer and longer instances of Vec (ℝ × ... × ℝ).

[Chris B]

I don't mean this to sound flippant ("read the manual"), but there is a small section in there which is the best description I've found of what it actually does (adjusts the starting point for TC synthesis). https://leanprover.github.io/lean4/doc/typeclass.html?highlight=outParam#output-parameters.

[Tomas Skrivan]

Yes to that extent as described there I understand it, but I'm utterly confused what is Lean trying to do in the code I have posted.