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.

[Filippo A. E. Nuccio]

I have just noticed that the use of outParam in HMul makes the following example typecheck

import Mathlib.Data.Nat.Defs

instance : HMul ℝ ℝ ℕ := ⟨fun _ _ ↦ 0⟩

example (x y : ℝ) : HMul.hMul x y = (0 : ℕ) := by rfl

but not the following

import Mathlib.Data.Nat.Defs

instance : HMul ℝ ℝ ℕ := ⟨fun _ _ ↦ 0⟩

instance : HMul ℝ ℝ Bool := ⟨fun _ _ ↦ false⟩

example (x y : ℝ) : HMul.hMul x y = (0 : ℕ) := by rfl--type mismatch
example (x y : ℝ) : HMul.hMul x y = false := by rfl -- it works

because due to the second instance, the outParam is set to Bool instead of ℕ. I understand that this is to be expected, according to the explanation in the manual, in particular when it says

When a class parameter is an output parameter, instance synthesis will not require that it be known; in fact, any existing value is ignored completely. The first instance that matches the input parameters is selected, and that instance's assignment of the output parameter becomes its value. If there was a pre-existing value, then it is compared with the assignment after synthesis is complete, and it is an error if they do not match.

My questions:

1. In the above quotation, what is a "pre-existing value"? If TC is launched, it might or not find the instance it is looking for, but I do not understand what is meant by "pre-existing".
2. By "first instance" do we mean the latest that has been defined?
3. Overall, are the above features (forgetting pre-existing values and picking the first instance) sought for, or are they forced upon us by the implementation of the outParam class, but in principle not needed? I still cannot understand why one cannot hope for a outParam behaviour that allows for treating parameters as outputs, and yet in my example compares the final term 0 : Nat with the two instances it has HMul ℝ ℝ Bool and HMul ℝ ℝ ℕ and realizes by unification that it is after the second, not the first.

PS: Of course changing outParam to a normal parameter (or even a semiOutParam) solves this issue, but not the "true" one for which outParam was chosen in HMul in the first place, so these are not viable options.

[Floris van Doorn]

1. If Lean knows it's looking for HMul ℝ ℝ Bool then Bool is the pre-existing value for the argument (and thus, is ignored when searching for an instance).

[Floris van Doorn]

2. It means the one with the highest priority. So if you don't specify priorities, it is indeed the last one that has been defined (or imported).

[Floris van Doorn]

3. is above my pay-grade. Probably has something to do with making the elaborator more reliable. I think the heuristic for outParam should be that there is (up to defeq) at most one instance matching a pattern, ignoring the outParams. If you want a binary operation on a type that takes different types depending on the context, maybe don't use * but a binary operation you define yourself.

[Filippo A. E. Nuccio]

Thanks ! 1. and 2. are crystal clear :crystal: , as usual :smile:

[Filippo A. E. Nuccio]

For 3, I was not looking to define a binary operator, I stumbled upon this example and ended up in the rabbit hole :rabbit: .

[Filippo A. E. Nuccio]

At any rate I take home the message "for outParam we expect a unique instance".