elaboration of ^ shouldn't try to put the arguments in the same type #2220
Description
Description
The macro for the ^ notation for exponentiation is defined as
macro_rules | `($x ^ $y) => `(binop% HPow.hPow $x $y)However, the binop% elaborator tries to make the type of x and y the same, which is not desired for exponentiation.
MWE
class NatCast (R : Type u) where
natCast : Nat → R
instance [NatCast R] : CoeTail Nat R where coe := NatCast.natCast
instance [NatCast R] : CoeHTCT Nat R where coe := NatCast.natCast
axiom Real : Type
notation "ℝ" => Real
instance (n : Nat) : OfNat ℝ n := sorry
variable (a : ℝ)
instance natCast : NatCast ℝ where natCast n := sorry
instance : HPow ℝ Nat ℝ := sorry
set_option pp.all true
#check a ^ 4
-- @HPow.hPow.{0, 0, 0} Real Nat Real instHPowRealNat a (@OfNat.ofNat.{0} Nat 4 (instOfNatNat 4)) : Real
instance : HPow ℝ ℝ ℝ := sorry
#check a ^ 4
-- @HPow.hPow.{0, 0, 0} Real Real Real instHPowReal a (@OfNat.ofNat.{0} Real 4 (instOfNatReal 4)) : Real
#check a ^ (4 : Nat)
-- @HPow.hPow.{0, 0, 0} Real Real Real instHPowReal a (@NatCast.natCast.{0} Real natCast (@OfNat.ofNat.{0} Nat 4 (instOfNatNat 4))) : RealThe desired result is that all checks use the instHPowRealNat instance, i.e. that 4 is interpreted as a Nat.
Additional Notes
Just removing binop% and replacing the macro with the following fixes the current issue, but it causes problems in other elaboration problems.
macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)With this macro an example like the following fails.
example (n : Nat) := ∃ k, n = 2 ^ k -- fails to find any instance, needs to know the type of `k`