type class inference with parameters

Stream: general

[Floris van Doorn]

Is there a way to tell type class inference to "use the current parameter"? In the following code, the apply_instance fails, because the argument of type decidable_eq A is a metavariable, and I want Lean to use the parameter.

section
parameters {A : Type} {h : decidable_eq A}
def X := A ⊕ A
def decidable_eq_X : decidable_eq X := @sum.decidable_eq _ h _ h
local attribute [instance] decidable_eq_X
set_option trace.class_instances true
def foo : decidable_eq X := by apply_instance
end

(note: it is unacceptable in my actual application to let X depend on h)

[Simon Hudon]

What if you use [ ] around the declaration of h?

[Floris van Doorn]

That works, but in my actual example h is not a type class parameter, but just some extra data to construct a setoid.

[Simon Hudon]

You could do something like by haveI := h; apply_instance, replacing h with whatever you need it to be.

[Simon Hudon]

(you need mathlib for haveI by the way, and to import tactic)

[Floris van Doorn]

this is a more faithful representation of my actual scenario:

constant some_data (α : Type) : Type
definition foo {α : Type} (h : some_data α) : setoid (α ⊕ α) := sorry
section
parameters {α : Type} (h : some_data α)
def X := α ⊕ α
def setoid_X : setoid X := foo h
local attribute [instance] setoid_X
set_option trace.class_instances true
def foo : setoid X := by apply_instance
end

[Floris van Doorn]

yes, that works, but is still a little annoying.

[Floris van Doorn]

I only have a problem with quotient.mk, so currently I just have something like def my_quotient.mk := @quotient.mk _ setoid_X, which is also a little annoying.

[Simon Hudon]

There's been a couple of back-and-forth on the subject. Leo doesn't like to allow instances to be created on the fly but he still granted us a way to do it.

[Simon Hudon]

Does it work if you replace @quotient.mk _ setoid_X with by haveI := setoid_X; apply quotient.mk?

[Floris van Doorn]

There's been a couple of back-and-forth on the subject. Leo doesn't like to allow instances to be created on the fly but he still granted us a way to do it.

Yeah, I know, but I don't want to add instances on the fly, I just want that in that section I have an instance of type setoid X.

[Simon Hudon]

I see. I mistook your issue. I think the problem is that your instance depend on stuff that can't be inferred. You may have to make some_data a class locally.