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

Mutually recursive blocks are sometimes wrong #3071

Open
janmasrovira opened this issue Sep 28, 2024 · 1 comment
Open

Mutually recursive blocks are sometimes wrong #3071

janmasrovira opened this issue Sep 28, 2024 · 1 comment

Comments

@janmasrovira
Copy link
Collaborator

E.g.

module Example;

type Fun := mkFun (T -> T);

type T := mkT;

is incorrectly translated (with juvix dev internal pretty Example.juvix) to

module MutualIssue;

mutual {
  type Fun =
    mkFun : (T → T) → Fun

  type T =
    mkT : T
}

If we put the definition of T before Fun, then the output is correct.

@lukaszcz
Copy link
Collaborator

lukaszcz commented Oct 1, 2024

I think the reason for this is that textually later definitions implicitly depend on textually earlier ones, so T implicitly depends on Fun.

These implicit dependencies are necessary for instance declarations to work correctly. Perhaps we could re-think this and find some less restrictive solution (with fewer implicit dependencies), but in general this is necessary.

lukaszcz pushed a commit that referenced this issue Oct 1, 2024
- Fixes #3048
- Fixes #3058

Due to #3071 I had to change the order of two lines in
tests/Compilation/positive/test079.juvix.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants