Pow type coercion broken

[alexkireeff]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Pow doesn't do type coercion whereas Sub does.

Context

Could be related to this pull request: #2778

Steps to Reproduce

inductive TestType
  | a (value : Float)
  deriving Repr

instance : Coe Float TestType where
  coe x := TestType.a x

instance : Coe TestType Float where
  coe x := 
    let (TestType.a value) := x
    value

instance : HomogeneousPow TestType where
  pow :=
      let pow x y := 
      let (TestType.a value1) := x
      let (TestType.a value2) := y
      TestType.a (value1 ^ value2)
    pow

#eval ((2. : Float) : TestType) ^ ((2. : Float) : TestType) -- `TestType.a 4.000000`
#eval ((2. : Float) : TestType) ^ ((2. : Float)) -- failed to synthesize HPow TestType Float
#eval ((2. : Float)) ^ ((2. : Float) : TestType) -- failed to synthesize HPow TestType Float

Expected behavior:

#eval ((2. : Float) : TestType) ^ ((2. : Float)) -- should return `TestType.a 4.000000`

Actual behavior:

#eval ((2. : Float) : TestType) ^ ((2. : Float)) -- failed to synthesize HPow TestType Float

Versions

using live.lean-lang.org, lean version 4.10.0-rc1

Additional Information

None

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.