FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.68k stars 231 forks source link

An interfaced module that references itself wrongly cause a dependency cycle #3311

Open TWal opened 3 months ago

TWal commented 3 months ago

Test.fsti:

module Test

Test.fst:

module Test

let x:int = 0

let y:int = Test.x
$ fstar.exe Test.fst
* Error 117:
  - You may have a cyclic dependence on module test: use --dep full to confirm. Alternatively, invoking fstar with Test.fst on the command line breaks the abstraction imposed by its interface Test.fsti; if you really want this behavior add the option '--expose_interfaces'

1 error was reported (see above)