disable TC by some sigil

Stream: general

[Johan Commelin]

I know that Lean 4 is around the corner, so hacking on Lean 3 is of limited use. But I'm wondering, how hard would it be to add the following feature:
If foobar is some name, then @foobar makes all arguments explicit, but it still runs TC on the typeclass arguments.
Can we have something like @!foobar to disable TC (roughly by replacing all the TC arguments with (id _))?
This would be extremely useful when TC is for some reason unhelpful and you want type inference to do the job instead.

[Johan Commelin]

I'm mainly wondering: is this a < 20-line patch to Lean 3. Or more like a 2500-line patch?

[Gabriel Ebner]

It's about a 100-line change, but spread over several modules. You need to add the @! token, you need to add macro annotation to store it in the pre-expression, and finally you need to add support to the elaborator. I would start by searching for @@ and using the copy-and-paste development methodology.

[Gabriel Ebner]

But why can't you just use id _?

[Johan Commelin]

Because then I need to figure out whether it's underscore 7 and 12 or 6 and 11

[Gabriel Ebner]

I've always found that to be the easy part (just move over the underscores and check which one is a type class). The part that I dread is figuring out whether you need 12 or 13 underscores and if they come before or after the explicit arguments..

[Johan Commelin]

Right, and it it's all just underscores, then rw [@!foobar] is a lot easier and faster to write.

[Johan Commelin]

Because then you can omit 13 underscores to begin with

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid/blob/master/src/breen_deligne/suitable.lean#L699-L715
It's more like 7 or 8 underscores, but you get the point.

[Gabriel Ebner]

Johan Commelin said:

Right, and it it's all just underscores, then rw [@!foobar] is a lot easier and faster to write.

Hmm, this doesn't work because @foobar and @!foobar elaborate to the same expression. (The difference only kicks in for @foobar _ _ _ _ _ _ _ and @!foobar _ _ _ _ _ _ _.)

[Johan Commelin]

Aha, so it would be a 2500-line patch to the elaborator?

[Gabriel Ebner]

It's more a question of "I don't know what you want it to do".

[Johan Commelin]

Well, I guess the elaborator could notice "hey, I see @!, let's insert (id _) for all TC arguments"

[Gabriel Ebner]

Can you be more concrete? What should #check @!add_comm output?

[Gabriel Ebner]

I believe in Lean 2 there was a sigil which turned all arguments implicit. Maybe that's what you're after (with disabling TC inference).

[Johan Commelin]

Aha, I see what you mean. Does the following make sense:

#check @add_comm
-- add_comm : ∀ {G : Type u_2} [_inst_1 : add_comm_semigroup G] (a b : G), a + b = b + a

#check @!add_comm
-- add_comm : ∀ {G : Type u_2} {_inst_1 : add_comm_semigroup G} (a b : G), a + b = b + a

[Gabriel Ebner]

That's hard. It would have to return something like id (∀ {G : Type u_2} {_inst_1 : add_comm_semigroup G} (a b : G), a+b=b+a) @add_comm

[Johan Commelin]

Hmm, I see.

[Eric Wieser]

Would this be easier with a tactic, by no_tc @lemma_name?

[Jannis Limperg]

I just hacked a tactic like this together on the notc branch: https://github.com/leanprover-community/mathlib/blob/notc/src/tactic/no_typeclasses.lean

Johan, would the test case at the bottom of that file work for you?

[Jannis Limperg]

Ping @Johan Commelin

[Johan Commelin]

@Jannis Limperg wow, I somehow missed your previous message. Thanks for the ping!

[Johan Commelin]

Let me look at that file

[Jannis Limperg]

No worries, I figured. :)

[Johan Commelin]

Can I now rw [by no_typeclasses @test]?

[Johan Commelin]

I guess that would just work, right?

[Johan Commelin]

(Assuming test is a bit more interesting)

[Johan Commelin]

I guess this could be combined with the machinery in https://github.com/leanprover-community/lean-liquid/blob/master/src/hacks_and_tricks/by_exactI_hack.lean to turn it into a sigil.

[Jannis Limperg]

It seems like the rw works. You get subgoals for α, testclass α and a : α if type inference doesn't figure them out.

[Jannis Limperg]

I can try to make this a user_notation as well (but probably not today).