anoma / juvix

A language for intent-centric and declarative decentralised applications
https://docs.juvix.org
GNU General Public License v3.0
449 stars 54 forks source link

Mutually recursive blocks are sometimes wrong #3071

Open janmasrovira opened 3 days ago

janmasrovira commented 3 days ago

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 commented 9 hours ago

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.