You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
structurePairNatwherea: Nat
b: Nat
defforceType (c: PairNat → Prop) := c
deffoo :=
let bar := fun ⟨a, b⟩ => a = b
let ftBefore := forceType bar
let inBarToEq a b: bar ⟨a, b⟩ → a = b := id
let ftAfter := forceType bar
0
Lean is able to infer the type of bar from its usage by the function forceType.
Lean also uses this inferred type to make sense of the pattern matching in the definition
of bar – if the block of three variables is commented out, we get this error:
invalid constructor ⟨...⟩, expected type must be an inductive type
?m.339
Even though the inferred type is used where bar is defined, it is not used where bar is used – if the declaration of ftBefore is commented out, we get the above
error at the definition of inBarToEq (while the definition of bar itself is still error-free).
Strangely, when one hovers the mouse over the bar in the type of inBarToEq,
the type is still displayed correctly:
Also, when the caret is over the usage of bar, the context contains the correct type:
bar: PairNat → Prop := fun x =>
match x with
| { a := a, b := b } => a = b
ab: ?m.416
⊢ Prop
Explicitly typing the variable is an abvious and quick workaround. I realize this is
a very minor issue once one knows what's happening, but from the usage perspective,
it was very confusing before I did 😅
This unfortunately is a consequence of another desirable change, #4096. While we would love to make Lean as independent from elaboration ordering as possible, in practice this is unfortunately not always achievable.
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
In the following code
Lean is able to infer the type of
bar
from its usage by the functionforceType
.Lean also uses this inferred type to make sense of the pattern matching in the definition
of
bar
– if the block of three variables is commented out, we get this error:Even though the inferred type is used where
bar
is defined, it is not used wherebar
is used – if the declaration offtBefore
is commented out, we get the aboveerror at the definition of
inBarToEq
(while the definition ofbar
itself is still error-free).Strangely, when one hovers the mouse over the
bar
in the type ofinBarToEq
,the type is still displayed correctly:
Also, when the caret is over the usage of
bar
, the context contains the correct type:Explicitly typing the variable is an abvious and quick workaround. I realize this is
a very minor issue once one knows what's happening, but from the usage perspective,
it was very confusing before I did 😅
Steps to Reproduce
ftBefore
Expected behavior: There is no error.
Versions
Lean version: 4.11.0-rc2 and 4.12.0-nightly-2024-08-14
OS: Ubuntu 22.04.4 LTS;
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: