Zulip Chat Archive

Stream: general

Topic: instance matching


view this post on Zulip Reid Barton (Sep 23 2019 at 18:06):

Can anyone explain this behavior?

class good (n : ).
instance good_4 : good 4 := good.mk 4

example : good 4 := infer_instance
example : good (2 + 2) := infer_instance  -- other pairs summing to 4 also work
example : good (2 * 2) := infer_instance  -- failed to synthesize type class instance for ⊢ good (2 * 2)

view this post on Zulip Reid Barton (Sep 23 2019 at 18:07):

Oh, good (nat.add 2 2) doesn't work. Some magic then?

view this post on Zulip Reid Barton (Sep 23 2019 at 18:45):

I was originally going to ask what kinds of definitional equivalence instance matching allows, but I realized I could just experiment instead.
My conclusion is that it allows all kinds of definitional equalities except that delta reductions are only permitted for reducible definitions. In other words, it's just usual definitional equality with an appropriate transparency setting.
However, there is a small mystery remaining: why good (2 + 2) works even by default.

view this post on Zulip Floris van Doorn (Sep 23 2019 at 19:03):

This seems to be something hard-coded into type-class inference. I think type-class inference normalizes (addition on) numerals using a mechanism other than definitional equality. Look at this example:

@[priority 100000] instance my_nat_add : has_add  := ⟨λ x y, 1
example : good (2 + 2) := by apply_instance

Note that the tactic apply_instance succeeds, even though 2 + 2 is not definitionally equal to 4 after my instance.

view this post on Zulip Floris van Doorn (Sep 23 2019 at 19:09):

And after apply_instance succeeds, the kernel rejects the found instance.

view this post on Zulip Reid Barton (Sep 26 2019 at 17:30):

I think there's one more special rule about instance matching I didn't notice earlier: as far as I can tell, instances themselves are always treated as reducible, whether or not they are marked as such.

view this post on Zulip Reid Barton (Sep 26 2019 at 17:44):

One "fun fact" here is if you write an instance like

instance : C T := by { delta T, apply_instance }

then the tactic will actually produce id (something), and id is not reducible, so this will behave differently than if you had just written (something) directly, under some circumstances.

view this post on Zulip Mario Carneiro (Sep 26 2019 at 17:45):

You can use clean to fix this

view this post on Zulip Reid Barton (Sep 26 2019 at 17:46):

like by clean by { delta CommRing, apply_instance }?

view this post on Zulip Reid Barton (Sep 26 2019 at 17:47):

It worked but it doesn't look very ... clean


Last updated: May 15 2021 at 23:13 UTC