Lean not respecting my type ascription?

Stream: new members

[Weiyi Wang]

I have the following code

import Mathlib

instance Additive.instSMul (A : Type*) (α : Type*) [Pow A α] : SMul α (Additive A) where
  smul (n : α) (a : Additive A) := ((a : A) ^ n : A)

(the purpose is to have an ad-hoc translation between additive n • a and multiplicative a ^ n)
However, it gives me error

failed to synthesize
  HPow (Additive A) α ?m.43

which suggests it still tries to use Additive A for ^, despite me specifying doing computation as A. What is going on here?

[Weiyi Wang]

Just after posting, I was able to work it around by

instance Additive.instSMul (A : Type*) (α : Type*) [h : Pow A α] : SMul α (Additive A) where
  smul (n : α) (a : Additive A) := h.pow a n

But I still want to understand why the previous code didn't work

[Sébastien Gouëzel]

a : A does not mean "build an element of Type A using a, it means "if you have difficulty understanding the type of a, you can try to use A". It doesn't force Lean to use A, it's just a hint. If you want to force A, you can use show A from a, like in

import Mathlib

instance Additive.instSMul (A : Type*) (α : Type*) [Pow A α] : SMul α (Additive A) where
  smul (n : α) (a : Additive A) := (show A from a) ^ n

[Sébastien Gouëzel]

But that's called "abusing defeqs", and it's bad practice. It's better to use the explicit functions to and from the additive version.

[Robin Arnez]

so, write:

instance Additive.instSMul (A : Type*) (α : Type*) [Pow A α] : SMul α (Additive A) where
  smul (n : α) (a : Additive A) := ofMul ((toMul a : A) ^ n : A)

[Weiyi Wang]

Thanks for the explanation!