Unification issue involving OfNat

Stream: lean4

[Tomas Skrivan]

I have a typeclass depending on Nat and I'm having some troubles when using constants like 0 or 1. Somehow there is a difference when I write 0 vs Nat.zero or 1 vs Nat.zero.succ.

class Uncurry (n : Nat) (F : Type) where
  {Y : Type} {Xs : Type}
  uncurry : F → Xs → Y

instance (priority := low) uncurry_zero {X : Type} : Uncurry 0 X where
  uncurry := λ (x : X) (_ : Unit) => x

instance uncurry_succ {X Y : Type} [inst : Uncurry n Y] : Uncurry (n+1) (X → Y) where
  Xs := X×inst.Xs
  Y := inst.Y
  uncurry := λ f (x,xs) => Uncurry.uncurry (f x) xs

-- Error:  failed to synthesize instance Uncurry Nat.zero X
example {X : Type} : Uncurry Nat.zero X := by infer_instance  -- error
example {X : Type} : Uncurry Nat.zero X := uncurry_zero -- works

-- This works
example {X Y Z : Type} : Uncurry Nat.zero.succ.succ (X → Y → Z) := by infer_instance
example {X Y Z : Type} : Uncurry Nat.zero.succ.succ (X → Y → Z) := uncurry_succ

What is going on here?

[Gabriel Ebner]

Here is a short version:

class Foo (n : Nat)
instance : Foo 0 where
example : Foo .zero := inferInstance -- fails

The short answer is that Nat.zero and 0 are different functions.

[Gabriel Ebner]

You can tell the discrimination tree index to ignore the function symbol here:

class Foo (n : Nat)
instance : Foo (no_index 0) where
example : Foo .zero := inferInstance -- works

[Gabriel Ebner]

BTW, I would avoid type fields in classes:

class Uncurry (n : Nat) (F : Sort u) (Y : outParam (Sort v)) (Xs : outParam (Sort w)) where
  uncurry : F → Xs → Y

And the (priority := low) has no effect in your snippet.

[Tomas Skrivan]

I see, makes sense.

However, I do not understand what no_index is doing. I see that in core it is used exactly when mixing Nat and and instances. Also somewhere in the code there is a comment that instances are not indexed. But I still do not understand what it is doing.

Thanks for the suggestions, using outParam is a good idea. That way I don't have to mark everything reducible as I had to when I started using this class.

[Jannis Limperg]

no_index X tells the indexing machinery to ignore X. So the instance will be tried on any typeclass problem of the form Foo ?, rather than just on problems of the form Foo 0. At that point, unification can kick in and confirm that 0 = Nat.zero.

[Tomas Skrivan]

Makes perfect sense! Thanks for the explanation.