Lean 4 tc order

Stream: general

[Patrick Massot]

@Daniel Selsam could you comment on https://github.com/leanprover/lean4/pull/130/? I thought the Lean 4 TC system was avoiding every loop problem.

[Mario Carneiro]

It might not be a loop problem. We do that in mathlib to put the fast fail typeclasses before the ones with many instances

[Patrick Massot]

The name of the branch is dselsam:fix-tc-loop...

[Patrick Massot]

And even with Mario's explanation, I kind of hoped that all the tc subtleties without any mathematical content would be gone in Lean 4.

[Daniel Selsam]

@Patrick Massot I have been using the old frontend with the old typeclass resolution procedure. The new frontend is still missing a few necessary features, e.g. an equation compiler. The fix is only relevant for using the old procedure.

[Patrick Massot]

Thanks!