Zulip Chat Archive

Stream: general

Topic: type classes in an inductive type

Floris van Doorn (Jul 22 2020 at 22:28):

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 (Jul 23 2020 at 09:37):

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 (Jul 23 2020 at 15:40):

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 (Jul 23 2020 at 15:46):

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.

Last updated: Aug 03 2023 at 10:10 UTC