Zulip Chat Archive

Stream: general

Topic: type class inference with parameters


view this post on Zulip Floris van Doorn (Nov 07 2018 at 16:43):

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)

view this post on Zulip Simon Hudon (Nov 07 2018 at 16:47):

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

view this post on Zulip Floris van Doorn (Nov 07 2018 at 16:56):

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

view this post on Zulip Simon Hudon (Nov 07 2018 at 16:57):

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

view this post on Zulip Simon Hudon (Nov 07 2018 at 16:59):

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

view this post on Zulip Floris van Doorn (Nov 07 2018 at 17:00):

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

view this post on Zulip Floris van Doorn (Nov 07 2018 at 17:01):

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

view this post on Zulip Floris van Doorn (Nov 07 2018 at 17:02):

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.

view this post on Zulip Simon Hudon (Nov 07 2018 at 17:03):

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.

view this post on Zulip Simon Hudon (Nov 07 2018 at 17:06):

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

view this post on Zulip Floris van Doorn (Nov 07 2018 at 17:08):

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.

view this post on Zulip Simon Hudon (Nov 07 2018 at 17:10):

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.


Last updated: May 11 2021 at 00:31 UTC