-
Notifications
You must be signed in to change notification settings - Fork 231
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
l_to_r
fails when there is subtyping?
#2476
Comments
As we were discussing with @TWal and @R1kM, the bug really seems to come (1) from how type inference happens with Consider the following two top-levels [@@expect_failure]
let foo (x: nat) = assert True by (
let t = quote (x == 3) in
if not (unify (`(`@x == (`#(fresh_uvar None)))) t)
then fail "unification failed"
)
let bar (x: nat) = assert True by (
let t = quote (eq2 #nat x 3) in
if not (unify (`(`@x == (`#(fresh_uvar None)))) t)
then fail "unification failed"
) The thing is that
A (rather painful) workaround is to take care of retyping lemmas correctly before applying them, but it is not reliable and very slow. |
l_to_r
do not work in this case:A workaround works by adding an explicit
<: nat
in the lemma.The text was updated successfully, but these errors were encountered: