-
Notifications
You must be signed in to change notification settings - Fork 58
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
Cycle detected in solution of metavariable: #68
Comments
Here is a self-contained example:
The error is the same:
|
I'll take a closer look. At best, this is a bad error message because it hasn't said what the internal name refers to, and because it hasn't said what the cyclic definition is. This message should indicate a problem with the program, but it's the first time I've seen it other than in contrived circumstances so I'll need to have a proper look first. |
I don't know if this will help me be organised, but I've added a label that I hope will remind me to investigate! |
I am not sure how to reproduce this in a small, self-contained example but you should be able to download https://gitlab.pik-potsdam.de/botta/Idris2Libs and then do:
in the root directory of Idris2Libs. This should work fine. However, doing
should yield
This is strange because the type of
s1
inFiniteAsInterface.Properties.toVectComplete
is the same as the type ofs1
inFiniteAsSigmaType.Properties.toVectComplete
.If you think it's worth, I can try to build a self-contained example of this behavior.
The text was updated successfully, but these errors were encountered: