Skip to content
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

Typechecking issue ? Wrong type generated in Coq. #3

Open
pessaux-f opened this issue May 22, 2023 · 2 comments
Open

Typechecking issue ? Wrong type generated in Coq. #3

pessaux-f opened this issue May 22, 2023 · 2 comments

Comments

@pessaux-f
Copy link
Owner

The same abstracted method from a collection parameter does not have the same type in very similar situations.
In some, it looks wrong, causing the lookup in the collection carriers mapping to fail. Hence, the type is considered as coming from an external top-level collection.

File "./bug.v", line 180, characters 6-45:
Error: The reference conversionFunctions.Super.me_as_carrier was not found
in the current environment.

See the attached file (to rename .fcl). Instructions to reproduce the bug are in comment in the file.
Tester with version 0.9.5, OCaml 5.0.0, Coq 8.17.0.
bug.txt

@pessaux-f
Copy link
Owner Author

pessaux-f commented May 22, 2023

There is something wrong during the dependencies calculus (focalize/focalizec/src/typing/abstrs.ml)
Rules _PRM and _DIDOU seem to introduce the method with the wrong type. The rule _TYPE is ok.

Don't know yet why by the way :/

@pessaux-f
Copy link
Owner Author

pessaux-f commented May 24, 2023

Possibly related to issue #4.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant