instance matching

Stream: general

[Reid Barton]

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)

[Reid Barton]

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

[Reid Barton]

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.

[Floris van Doorn]

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.

[Floris van Doorn]

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

[Reid Barton]

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.

[Reid Barton]

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.

[Mario Carneiro]

You can use clean to fix this

[Reid Barton]

like by clean by { delta CommRing, apply_instance }?

[Reid Barton]

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