Early stumbling blocks, FAQ

Table of Contents

• Confusing error message
• Which editor should I use?
• Include non-standard libraries when using fstar-mode
• Error message: two types differ but the same in the error message?
• Error message: complaining about projectee's.
• Error message: inconsistent OCaml object files?
• My pattern-match on a pair won't type-check!
• Subtyping check failed
• Inconsistent implicit argument annotation on argument x
• What do these symbols mean?

FStar gives me a confusing error message. What can I do?

This will happen quite often. Don't PANIC. Often making sure that you re-compiled fstar after a pull will help.

Here is a, not necessarily representative example:

$ fstar <some-fst-file>
E:\FStar\bin\..\ulib\prims.fst(628,14-628,14) : Error
Syntax error: Failure("unexpected char")

See also other Error message: ... in table of content.

Which editor should I use?

It is up to you, see Editor-support-for-F*, but currently fstar-mode is the most actively developed.

How can I include non-standard libraries when using fstar-mode?

Add the following line to your .emacs.

(setq fstar-subp-prover-args '("--include" "<your-path>"))

See fstar-mode for more information.

fstar-mode gives error message "F*: subprocess exited". What shall I do?

The first thing to try is to look in your *Messages* buffer in emacs for error messages.

You might also try running fstar <file-name> in a terminal to see whether you get a more meaningful error message.

How to debug an error message complaining about two types being different that look the same in the error message?

E.g. Expected type "(Prims.list entry)"; got type "(Prims.list entry)"

Use --print_universes and --print_implicits options to see hidden differences.

I get an error complaining about projectee's. What should I do?

This is a temporary workaround. Please remove this QaA entry once it is no longer needed.

Expected expression of type "(Module.entry (Module.property(Module.Entry.elem1 projectee)))";
got expression "elem2" of type "(Module.entry (Module.property elem1))"

You can use " --__temp_no_proj Module" to disable the creation of projectee's.

What to do about inconsistent OCaml object files?

Sometimes OCaml files are inconsistent and need to be deleted, here is an example with its specific solution:

Error: Files FStar_Mul.cmx and ./prims.cmx
       make inconsistent assumptions over interface Prims

run make -C ulib/ml clean in the F* main directory.

My pattern-match on a pair won't type-check!

This doesn't work because of a bug (#682)

val map2:
  n:nat ->
  f:('a -> 'b -> Tot 'c) ->
  l1:vec 'a n ->
  l2:vec 'b n ->
  Tot (vec 'c n)
let rec map2 n f l1 l2 =
  match l1, l2 with
  | Cons hd1 n1 tl1, Cons hd2 n2 tl2 ->
      Cons (f hd1 hd2) n2 (map2 n2 f tl1 tl2)
  | Nil, Nil ->
      Nil

Instead, do:

val map2:
  n:nat ->
  f:('a -> 'b -> Tot 'c) ->
  l1:vec 'a n ->
  l2:vec 'b n ->
  Tot (vec 'c n)
let rec map2 n f l1 l2 =
  match l1 with
  | Cons hd1 n1 tl1 ->
      begin match l2 with
      | Cons hd2 n2 tl2 ->
          Cons (f hd1 hd2) n2 (map2 n2 f tl1 tl2)
      end
  | Nil ->
      begin match l2 with
      | Nil ->
          Nil
      end

Subtyping check failed

As an example, let us say you wrote this code:

let foo (x : (nat * int)) : (int * int) = x

As of now, this will not type check, but instead fail with:

Subtyping check failed; expected type int * int; got type nat * int

Shouldn't (nat * int) be a subtype of (int * int)?!

This is related to a long standing open issue (see https://github.com/FStarLang/FStar/issues/65). In short, subtyping for product types (i.e., tuples) and other inductive types, is a slippery slope for dependent type theories in general.

However, there usually exist simple and easy workarounds for this. For example, an easy workaround for our specific example here is:

let foo (x : (nat * int)) : (int * int) = (fst x, snd x)

Inconsistent implicit argument annotation on argument x

Mixing OCaml-style type variables ('a) and implicit arguments is brittle. The best is to avoid mixing them, unless source compatibility with OCaml is required.

Results vary and are not very predictable. For instance, this doesn't type check

val f: #u:unit -> x:'a -> Tot unit
let f #u x = ()

whereas it type checks swapping the order of arguments

val f: x:'a -> #u:unit -> Tot unit
let f x #u = ()

What do these symbols mean?

While the F* symbols reference is incomplete, for most commonly used symbols, a short description exists there.