Multiplicative mul and pow are wrong

Stream: mathlib4

[Yongyi Chen]

Minimal working example:

import Mathlib

/-
instHMul
-/
#synth HMul (Multiplicative (ZMod 10)) (Multiplicative (ZMod 10)) (Multiplicative (ZMod 10))
/-
Multiplicative.mul
-/
#synth Mul (Multiplicative (ZMod 10))
/-
instHPow
-/
#synth HPow (Multiplicative (ZMod 10)) ℤ (Multiplicative (ZMod 10))
/-
DivInvMonoid.Pow
-/
#synth Pow (Multiplicative (ZMod 10)) ℤ

/-
6
-/
#eval ((2 : ZMod 10) : Multiplicative (ZMod 10)) * ((3 : ZMod 10) : Multiplicative (ZMod 10))
/-
8
-/
#eval ((2 : ZMod 10) : Multiplicative (ZMod 10)) ^ 3

The evals should output 5 and 6 respectively, not 6 and 8. This is despite that#synth shows the right thing for Mul (and no idea if DivInvMonoid is the right thing for Pow)...

[Kyle Miller]

What if you change those to show Multiplicative (ZMod 10) from (2 : ZMod 10) for example? (I think I got the right syntax). Type ascriptions don't cause terms to have a type hint, they just do a defeq check, so it can be surprising to learn that you're still in ZMod 10. Try seeing the output of #check ((2 : ZMod 10) : Multiplicative (ZMod 10)).

[Kyle Miller]

Here's a trick to register a type hint: #check (id (2 : ZMod 10) : Multiplicative (ZMod 10))

[Yongyi Chen]

Ah you're right. Changing them to Multiplicative.ofAdd (2 : ZMod 10) and Multiplicative.ofAdd (3 : ZMod 10) gives expected output. However, this actually arose out of me trying to prove something to the effect of Multiplicative.ofAdd (1 : ZMod N) ^ m = Multiplicative.ofAdd (m : ZMod N) and me being suspicious about whether there was a bug related to that.

[Eric Wieser]

Using letI is another way to specify the type, without inserting an id into the term:

#eval ((2 : ZMod 10) : Multiplicative (ZMod 10)) ^ 3 -- 8
#eval (letI : Multiplicative (ZMod 10) := (2 : ZMod 10); this) ^ 3 -- 6

[Eric Wieser]

by exact works too; which is what I've used in #8086

[Yongyi Chen]

These tricks are way too folklore, haha.