Checking exports blows up with abstract inductive and private predicate that matches on the inductive

[aseemr]

This code gives an error:

module Test

abstract type t (a:Type0) (n:nat) =
  | C: #m:nat -> x:nat{x > m} -> t a n

private let pred (#a:Type0) (#n:nat) (x:t a n) :Type0
  = let C y = x in
    True

aseemr@aseemr-dt1 ~/FStar
$ fstar.exe Test.fst
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Failure("Not a datacon: C")

The error happens only on the command line (or when this module is checked as a dependency of other modules). Which leads me to believe that it has something to do with exports checking.

Also. changing private to abstract in the definition of pred makes it work. But also note that I am specifically marking the type of pred to Type0, so C should not have escaped in the return type.

I remember one similar issue that I raised before, need to look if this is a duplicate or not. Just noting it down for record.

[aseemr]

I guess this is expected. private is only an access qualifier. A private definition in module A is still encoded to the solver, when A is a dependency of B. But abstract definitions in A are not. So, this code does leak abstraction. Marking pred as abstract makes it go away, since the defn. of pred is also hidden from the solver in that case.

[catalin-hritcu]

Unexpected error should never be expected behavior though, at the very least this should fail more graciously.

[nikswamy]

This is related to #1123

Overall, the bugs in this area suggest that checking exports needs to be revised significantly.

Currently, it only checks the signatures of non-private functions. This is insufficient. It should really typecheck the entire module again, while removing the definitions of all abstract symbols.

This would also bring it closer to matching the semantics of modules with interfaces.

However, this revision is non-trivial since:

1. It is related to idempotence of type-checking Typechecker is not idempotent #1307 (and two-phases)
2. It is potentially quite expensive to type-check the module twice

[nikswamy]

Oh, i think this is more than just an error message issue

[catalin-hritcu]

This now also appears in miTLS.

[aseemr]

Exports checking behavior is now significantly revised in master (see https://github.com/FStarLang/FStar/wiki/Revised-checking-of-a-module's-interface).

The new behavior is currently under the flag --use_extracted_interfaces, which I hope some day can become a default. The flag is enabled in ulib/Makefile, so ulib/ verification happens with this new behavior (of course, I found a lot abstraction violations in ulib/, many of them in the code that I wrote!).

Consider the following example:

A.fst:

module A

abstract type t =
  | C: t

private let foo :t = C

B.fst:

module B

open A

The invocation fstar.exe --use_extracted_interfaces B.fst gives an error:

A.fst(6,21-6,22): (Error 133) Name "A.C" not found

The reason is that, in the invocation above, F* tries to verify B against an extracted interface for A. In the extracted interface, the type t is abstract but the definition of A.foo leaks the constructor C, and hence the error.

There is another flag --check_interface that verifies the extracted interface of the file on the command line:

$ fstar.exe A.fst --check_interface
A.fst(6,21-6,22): (Error 133) Name "A.C" not found
1 error was reported (see above)

[nikswamy]

This is great, Aseem! Thanks!

Some questions:

Does it with with cache_checked_modules already?

Is the interface extracted after type checking the implementation? E.g., can we make use of inferred types in the interface?

Aside from finding and fixing abstraction violations, are you aware of any other gotchas that prevent us from turning this feature on in other developments?

[aseemr]

Hi Nik:

-- Yes, it works with cache_checked_modules already and is also integrated into dependency analysis. fstar.exe --use_extracted_interfaces --dep full ... generates dependencies on .fsti.checked. The flag is enabled in ulib where all these are used via the existing makefiles.

-- No, sorry, it is currently extracted before type checking. As we discussed once, this has a 2-phase flavor, may be I can try that some time.

-- The scheme requires annotations for abstract definitions. Since interfaces are extracted before type checking, for abstract let bindings it needs the comp annotation (at least), and for abstract inductives, it's better to be precise about universes (else there are unnecessary generalized universes that can create problems). The idea of extraction post type checking will get around both these, however, would require two invocations, unless we roll back the type environment.