Pow type coercion broken
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 9.2k
- Forks
- 990
- Avg merge
- 1d 17h
- Merged PRs (30d)
- 175
Description
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: https://github.com/leanprover/lean4/pull/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.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Run the minimal reproduction on the Lean nightly release and compare Pow's behavior with Sub's coercion behavior. Read pull request #2778 for related context. Done means mixed Float/TestType exponentiation evaluates to TestType.a 4.000000 instead of failing to synthesize HPow TestType Float.
Written by the indexing model from the issue text.
Assessment
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Clearly specified
- Newbie friendliness
- 48/100