!4#2046 to_additive trouble

Stream: mathlib4

[Eric Wieser]

to_additive doesn't seem to like the use of the equation compiler in !4#2046 (a forward-port). Is this a problem we already know about?

[Eric Wieser]

The error there is on these lines, and is

./././Mathlib/Algebra/GroupPower/Order.lean:168:2: error: application type mismatch
  motive 0 x✝
argument has type
  1 ≠ 0
but function has type
  0 ≠ 0 → Prop

[Eric Wieser]

Replacing 1 in the match with Nat.succ 0 seems to fix it

[Eric Wieser]

mwe:

import Mathlib.Algebra.Group.Basic

-- fails
@[to_additive]
def mul_foo {α} [Monoid α] (a : α) : ℕ → α
| 0 => 1
| 1 => 1
| (n + 2) => a

-- ok
@[to_additive]
def mul_bar {α} [Monoid α] (a : α) : ℕ → α
| 0 => 1
| (Nat.succ 0) => 1
| (n + 2) => a

[Floris van Doorn]

This one is indeed new.

The problem is that the elaborated term contains motive 1, where 1 is a pure natural number literal, not within a ofNat application (which the elaborator inserts in all other cases we've encountered so far).
This means we do not know what type this literal is supposed to be in.
I'll try to add the rule that a variable applied to a literal should never be changed. Hopefully that will not break other cases.

[Eric Wieser]

Could this be an elaboration bug?

[Floris van Doorn]

I expect this is intended behavior. But the fix is easy !4#2153 and seems to have no bad side-effects