## Stream: general

### Topic: derive handler for fintype

#### Scott Morrison (Mar 04 2020 at 20:05):

@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 (Mar 04 2020 at 20:08):

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 (Mar 04 2020 at 20:09):

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 (Mar 04 2020 at 20:10):

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 (Mar 04 2020 at 20:10):

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

#### Scott Morrison (Mar 04 2020 at 20:10):

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 (Mar 04 2020 at 20:12):

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 (Mar 04 2020 at 20:16):

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 (Mar 04 2020 at 20:17):

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

#### Simon Hudon (Mar 04 2020 at 20:17):

(a name different from decidable_eq

#### Reid Barton (Mar 04 2020 at 20:19):

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

#### Simon Hudon (Mar 04 2020 at 20:19):

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

#### Scott Morrison (Mar 04 2020 at 20:29):

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 (Mar 04 2020 at 20:34):

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

#### Simon Hudon (Mar 04 2020 at 20:45):

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 (Mar 04 2020 at 20:47):

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

#### Rob Lewis (Mar 04 2020 at 20:48):

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 (Mar 04 2020 at 20:52):

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 (Mar 04 2020 at 20:53):

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 (Mar 04 2020 at 21:04):

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

#### Rob Lewis (Mar 04 2020 at 21:06):

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

#### Simon Hudon (Mar 04 2020 at 21:16):

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

#### Simon Hudon (Mar 04 2020 at 21:22):

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

#### Rob Lewis (Mar 04 2020 at 21:22):

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

#### Simon Hudon (Mar 04 2020 at 21:23):

Maybe that's a better solution then

#### Simon Hudon (Mar 04 2020 at 21:56):

making things protected seem to fix the issue

#### Simon Hudon (Mar 04 2020 at 22:05):

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

Last updated: May 06 2021 at 22:13 UTC