type classes in an inductive type

Stream: general

[Floris van Doorn]

Does anyone know why the elaborator fails on one of these two inductive types, but fails on the other?

def nat.incl {n : ℕ} (i : ℕ) [hi : fact (i < n)] : fin n := ⟨i, hi⟩
def my_predicate (n : ℕ) (i : fin n) : Type := bool

inductive failing : Prop -- failed to synthesize type class instance `fact (i < n)`
| mk : ∀ (i n : ℕ) [fact (i < n)], my_predicate n i.incl → failing

inductive succeeding : Prop
| mk : ∀ (i n : ℕ) [fact (i < n)], my_predicate n (i.incl : fin _) → succeeding

(side note: the usual by exactI trick doesn't work for inductive types, because tactic mode doesn't know how to deal with the name of the inductive type.)

[Gabriel Ebner]

Here is your explanation:

failed to synthesize type class instance for
i n : nat,
_inst_1 : fact (@has_lt.lt.{0} nat ?m_1 i n)
⊢ fact (@has_lt.lt.{0} nat nat.has_lt i n)

And here is the by exact trick that works:

inductive not_failing : Prop
| mk : ∀ (i n : ℕ) [fact (i < n)], (by exact my_predicate n i.incl) → failing

[Floris van Doorn]

Oh, that's interesting. Is this a side-effect of trying to solve type-class inference problems from right-to-left?

Thanks for investigating! Knowing the problem will make it a lot easier to work around the problem.

[Gabriel Ebner]

This is a bug in the elaborator in the case that the local instances are not frozen. It thinks that an instance is ready to be synthesized if it does not contain metavariables. And indeed, fact (i < n) doesn't contain metavariables so it is synthesized and fails.