Negation and Floats (Is `Neg.neg` biased towards `Int`?)

Stream: lean4

[Andrew Kent]

I just noticed that it's a bit tricky to write down a negated Float value in nested arithmetic expressions. E.g.:

#eval (Neg.neg 42.0)
-- ^ produces the error `failed to synthesize instance OfScientific Int`
-- pointing at `42.0`
#eval (1.0 * -42.0)
-- ^ produces the error `failed to synthesize instance OfScientific Int`
-- pointing again at `42.0`
#eval (1.0 * -(42.0 : Float))
-- ^ works fine

Is there an inference bias towards Int for Neg.neg usages or similar? (I tried to grep for such a bias in the lean4 repo and nothing jumped out at me...)

[Leonardo de Moura]

Thanks for reporting this issue. I will submit a fix. The issue is due to the priorities of default instances.

[Leonardo de Moura]

Pushed https://github.com/leanprover/lean4/commit/d408c835d20b6a2f1eee09804222316b755b2ae2