typeclass instance resolution implicit params

Stream: new members

[Klaus Gy]

Why is terminalFoo failing but terminalBar not? Is this simply due to too many implicit params?

import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq

universe u v

namespace CategoryTheory

open Category Limits Functor IsPullback

variable (C : Type u) [Category.{v} C]

structure Foo (c : C) where
  t : ∀ Y : C, Unique (Y ⟶ c)

variable {c : C}

instance {f : Foo C c} : ∀ Y : C, Unique (Y ⟶ c) := f.t

def terminalFoo {f : Foo C c} : IsTerminal c := IsTerminal.ofUnique c

structure Bar where
  c : C
  t : ∀ Y : C, Unique (Y ⟶ c)

instance {b : Bar C} : ∀ Y : C, Unique (Y ⟶ b.c) := b.t

def terminalBar {b : Bar C} : IsTerminal b.c := IsTerminal.ofUnique b.c

[Robin Arnez]

Because it has a way to find b using unification. It won't search in the local context unless it is an instance implicit.

[Robin Arnez]

In other words, since the goal doesn't contain f : Foo C c, it won't find it. Since the goal contains b : Bar C it can find it.

[Klaus Gy]

thanks a lot, it starts to make sense :)

[Robin Arnez]

class Foo (c : C) where
  t : ∀ Y : C, Unique (Y ⟶ c)

variable {c : C}

instance [f : Foo C c] : ∀ Y : C, Unique (Y ⟶ c) := f.t

would also work because it is an instance implicit

[Klaus Gy]

hmm, yes, but I think in my case a structure is more natural than a class. will think about it!

[Kyle Miller]

Maybe Robin's using "goal" loosely here and I'm misunderstanding, but in particular the instance isn't able to ever apply because the argument f doesn't appear in the resulting type.

CategoryTheory.instUniqueHomOfFoo.{u, v} (C : Type u) [Category.{v, u} C] {c : C} {f : Foo C c} (Y : C) : Unique (Y ⟶ c)

Typeclass inference needs all the arguments to appear in Unique (Y ⟶ c), but f doesn't.

The difference is that the Bar instance has b in the resulting type.

(I thought there was a linter that checked for this. Maybe it only flags the case when there are other instance arguments that aren't determined by the resulting type.)

[Klaus Gy]

Thank you Kyle! I now just brought the instance inside the definition of terminalFoo.