derive handler for fintype

Stream: general

[Scott Morrison]

@Simon Hudon, I notice that in archive/sensitivity.lean we successfully use a @[derive fintype]. Where is this coming from? I want to use it somewhere else but can't work out what I need to import. I just get a failed to find a derive handler for fintype message.

[Scott Morrison]

Related derive question... It seems there's a problem if you use @[derive decidable_eq] twice in the same file, and there is a broken work-around in place.

[Scott Morrison]

The problem seems to be disambiguating the decidable_eq in the second @[derive decidable_eq] annotation. Does that mean _root_.decidable_eq, or is it just the instance that was defined a moment ago by the first derive handler? (Which has a name ending in decidable_eq!)

[Scott Morrison]

The error message that shows up is failed to find a derive handler for 'choice decidable_eq category_theory.limits.walking_parallel_pair.decidable_eq'

[Simon Hudon]

To find the fintype derive handler, try: run_cmd attribute.get_instances `derive_handler >>= tactic.trace

[Scott Morrison]

And I'm guessing (?) that this choice business is some attempt to work out what we're actually trying to derive, based on what's actually available?

[Simon Hudon]

choice I believe is the Lean macro for name overloading. It defers to the elaborator the choice between the two. But that being said, it's curious that it would affect you there.

[Simon Hudon]

I think I see the problem. This is the parser for the derive attribute: parser := pexpr_list_or_texpr. It has to parse expressions because you could specify something like module real

[Simon Hudon]

If you give a name to the offending decidable_eq instance, that should go away

[Simon Hudon]

(a name different from decidable_eq

[Reid Barton]

which you can't do because it was generated automatically by the derive handler

[Simon Hudon]

Actually, we may be able to make that code a bit more robust

[Scott Morrison]

okay... I have a PR I'm looking at that has @[derive _root_.decidable_eq] to get around this problem. Should I allow that for now, or better to wait on some robustification?

[Simon Hudon]

I think you should keep that PR. The change would go in Lean itself

[Simon Hudon]

There are two ways to fix your particular issue. Either we generate a different name for the instance or we tolerate ambiguities in the name of the classes that we're trying to build an instance for

[Simon Hudon]

The solution for both is very simple. I'm not sure about the ramifications though

[Rob Lewis]

Note that the delta_instance handler (which just unfolds a definition and calls apply_instance) appends something to the name for exactly this reason. https://github.com/leanprover-community/mathlib/blob/master/src/tactic/core.lean#L1511

[Simon Hudon]

If you use it twice in a row and that it generates an instance for the same class, will you have a name clash with that approach?

[Rob Lewis]

The name is based on the type and the instance it's looking for, and it uses get_unused_decl_name, so no, I hope not.

[Simon Hudon]

That might be the right approach then. We could move get_unused_decl_name to core for that

[Rob Lewis]

Huh, I kind of assumed get_unused_decl_name was from core already, guess not.

[Simon Hudon]

Me too. That means that it shouldn't clash too much with its new neighbors

[Simon Hudon]

It would be nice if the meta programming interface allowed us to make protected declarations

[Rob Lewis]

Absolutely, I've wanted that a whole bunch of times.

[Simon Hudon]

Maybe that's a better solution then

[Simon Hudon]

making things protected seem to fix the issue

[Simon Hudon]

https://github.com/leanprover-community/lean/pull/138