Error with semiOutParam

Stream: lean4

[Gareth Ma]

Hi, the following code should explain pretty well:

import Mathlib.Tactic

variable (α : Type*) [DecidableEq α] [LinearOrder α] [Coe α ℚ] [Fintype α]

def MyProp : Prop := ∀ a : α, (0 : ℚ) < a

instance : Decidable (MyProp α) := inferInstanceAs (Decidable (∀ _, _))

def S : Finset ℚ := {0, 2, 4, 6, 8}

/- Works -/
instance : Coe S ℚ where
  coe := fun x => x

/- Error: instance does not provide concrete values for (semi-)out-params -/
instance ApparentlyICanNameThis {T : Finset ℚ} : Coe T ℚ where
  coe := fun x => x

#check ApparentlyICanNameThis             -- Also exists

#eval MyProp S                            -- False
#eval MyProp ({1, 2, 3, 4, 5} : Finset ℚ) -- Funny enough, this evaluates (to True)

A few questions:

1. Why does it error? (at ApparentlyICanNameThis)
2. Why does it work? (at ApparentlyICanNameThis)
3. Why are the questions above contradictory?
4. Is this (ApparentlyICanNameThis existing) a bug?

[Timo Carlin-Burns]

The semi-out-param error goes away if I change it to CoeOut T ℚ. I think this makes sense given the explanation here in the Coe docs

[Jireh Loreaux]

I think that actually this behavior makes sense. a semi-out-param is an argument to the type class which should be solved for first (or, earlier than other things) during unification. It's basically a marker which says, "hey, Lean, if you're stuck trying to unify the type, try unifying this thing first." That's good as long as there is some way to do it. For example, Mathlib uses this for docs#IsROrC because there's only two (i.e., ℝ and ℂ) instances of that type, and so it should be easy for Lean to figure out which one it is. Now, if you fix S : Finset ℚ, and create the Coe instance, that's not a problem because you're essentially only adding the single type S(it gets coerced from Finset to a type) to the list of things Lean needs to look for. But in your ApparentlyICanNameThis declaration, you are adding all of Finset Q to the list of list of things Lean needs to try, which will make it a bad semi-out-param. Therefore, Lean errors (as it should because otherwise this is a massive footgun), but it doesn't actually prevent the instance being added to the environment.

[Jireh Loreaux]

The CoeOut direction should be fine.

[Timo Carlin-Burns]

After changing it to CoeOut, the remaining error is because MyProp explicitly requires [Coe α ℚ], not [CoeOut α ℚ]. This can be fixed by changing the requirement. I don't know what would be suitable.. Maybe [CoeHTCT α ℚ]?

[Jireh Loreaux]

Why not make it [CoeOut α ℚ]? It's a bit hard to say because I'm not entirely sure what you're trying to do overall.

[Gareth Ma]

Sorry for the late reply. Thanks, CoeOut works, I will read the docs.

[Gareth Ma]

It's a bit hard to say because I'm not entirely sure what you're trying to do overall.

I just want to express the instance / property "\alpha is a type that is Coe'able to \Q"

[Ruben Van de Velde]

Do you want this coercion to have any particular properties?

[Gareth Ma]

Not right now, I just wanted my MyProp to pass type check, my focus was on the Decidable part (and making it computable) haha
But I need more properties later I will ask again? :)

[Gareth Ma]

In particular, this works for my purpose!

import Mathlib.Tactic
import Mathlib.Combinatorics.Additive.Behrend
variable (α : Type*) [DecidableEq α] [LinearOrder α] [CoeOut α ℚ] [Fintype α]
def MyProp : Prop := ∀ a : α, (0 : ℚ) < a
instance : Decidable (MyProp α) := inferInstanceAs (Decidable (∀ _, _))
def S : Finset ℚ := {0, 2, 4, 6, 8}
instance ApparentlyICanNameThis {T : Finset ℚ} : CoeOut T ℚ where coe := fun x => x
#check ApparentlyICanNameThis

#eval MyProp S
#eval MyProp ({1, 2, 3, 4, 5} : Finset ℚ)