fstarlang/fstar

A Proof-oriented Programming Language

fstar's Issues

Replace "=>" with "->" everywhere in our syntax

Change the front-end to drop the '=>' notation altogether and use only '->' throughout, at all levels: fun, types, kinds, match. Nik thinks it should still possible to still disambiguate everything and that the different kinds of arrows are just a pain to explain. I often mixed them up.

Do we really need FSharp.Core.dll to be checked in?

My build keeps clobbering it with a different version, depending on which machine I'm working. Would be nice to not have it checked it, if we don't really need it. But, perhaps we do need it for mono or something? Not sure.

Type-checking error in triple pattern match

After last night's changes we're getting a new spurious typing error in stlc.fst. I minimized it to this:

val typing : option int
let typing =
  match 41, 42, Some 43 with
  | 41, 42, Some 43 -> None
  | _, _, _         -> None
  end

The error message is:

Problem:
<prob>
Failed because: head mismatch (t-1)
Incompatible types ('c0 int int 'U539 _7875)
and (option 'U540)
stlc-bugnew.fst(8,4-8,19) : Error
Expected type "(option 'U540)";
got type "('c0 int int 'U539 _7875)"
Exception of type 'Microsoft.FStar.Absyn.Syntax+Error' was thrown.
  at Microsoft.FStar.Tc.Rel.subtype (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 t1, Microsoft.FStar.Absyn.syntax`2 t2) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Util.weaken_result_typ (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FStar.Absyn.syntax`2 c, Microsoft.FStar.Absyn.syntax`2 t) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.comp_check_expected_typ (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FStar.Absyn.syntax`2 c) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_exp (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_args@641-3 (Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FStar.Tc.env env, Boolean head_is_atom, Microsoft.FStar.Absyn.syntax`2 f, Microsoft.FStar.Absyn.syntax`2 cf, Microsoft.FStar.Absyn.syntax`2 tf, Microsoft.FSharp.Collections.FSharpList`1 vars, Microsoft.FSharp.Collections.FSharpList`1 tvars, Microsoft.FSharp.Collections.FSharpList`1 subst, Microsoft.FSharp.Collections.FSharpList`1 outargs, Microsoft.FSharp.Collections.FSharpList`1 arg_rets, Microsoft.FSharp.Collections.FSharpList`1 comps, Microsoft.FStar.Tc.guard_t g, System.Tuple`2 fvs, Microsoft.FSharp.Collections.FSharpList`1 bs, Microsoft.FStar.Absyn.syntax`2 cres, Microsoft.FSharp.Collections.FSharpList`1 args) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.check_function_app@615 (Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FSharp.Collections.FSharpList`1 args, Microsoft.FStar.Tc.env env, Boolean head_is_atom, Microsoft.FStar.Absyn.syntax`2 f, Microsoft.FStar.Absyn.syntax`2 cf, Boolean norm, Microsoft.FStar.Absyn.syntax`2 tf) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_exp (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_total_exp (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.discriminate@973[syntax`2] (Microsoft.FStar.Tc.env scrutinee_env, Microsoft.FStar.Absyn.syntax`2 scrutinee, Microsoft.FStar.Absyn.withinfo_t`2 f) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.mk_guard@979 (Microsoft.FStar.Tc.env env, Microsoft.FStar.Tc.env scrutinee_env, Microsoft.FStar.Absyn.syntax`2 scrutinee, Microsoft.FStar.Absyn.syntax`2 pat_exp) [0x00000] in <filename unknown>:0 
  at [email protected] (Int32 i, System.Tuple`2 arg) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Primitives.Basics.List.mapiToFreshConsTail[FSharpList`1,Tuple`2] (Microsoft.FSharp.Collections.FSharpList`1 cons, Microsoft.FSharp.Core.FSharpFunc`3 f, Microsoft.FSharp.Collections.FSharpList`1 x, Int32 i) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Primitives.Basics.List.mapi[Tuple`2,FSharpList`1] (Microsoft.FSharp.Core.FSharpFunc`2 f, Microsoft.FSharp.Collections.FSharpList`1 x) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.MapIndexed[Tuple`2,FSharpList`1] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.mk_guard@979 (Microsoft.FStar.Tc.env env, Microsoft.FStar.Tc.env scrutinee_env, Microsoft.FStar.Absyn.syntax`2 scrutinee, Microsoft.FStar.Absyn.syntax`2 pat_exp) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Invoke@3000[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]].Invoke (Microsoft.FStar.Absyn.syntax`2 u) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Primitives.Basics.List.map[syntax`2,syntax`2] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 x) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Map[syntax`2,syntax`2] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_eqn (Microsoft.FStar.Absyn.bvdef`1 scrutinee_x, Microsoft.FStar.Absyn.syntax`2 pat_t, Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.pat pattern, Microsoft.FSharp.Core.FSharpOption`1 when_clause, Microsoft.FStar.Absyn.syntax`2 branch) [0x00000] in <filename unknown>:0 
  at [email protected] (System.Tuple`3 tupledArg) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Primitives.Basics.List.map[Tuple`3,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 x) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Map[Tuple`3,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_exp (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_exp (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_decl (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>:0 
  at [email protected] (Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3006[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+sigelt],Microsoft.FStar.Tc.Env+env],Microsoft.FStar.Absyn.Syntax+sigelt,System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+sigelt],Microsoft.FStar.Tc.Env+env]].Invoke (System.Tuple`2 , Microsoft.FStar.Absyn.sigelt ) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.loop@144-20[sigelt,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`2 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Fold[sigelt,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_decls (Microsoft.FStar.Tc.env env, Microsoft.FSharp.Collections.FSharpList`1 ses) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_modul (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.modul modul) [0x00000] in <filename unknown>:0 
  at [email protected] (Microsoft.FStar.Absyn.modul m) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3006[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+modul],Microsoft.FStar.Tc.Env+env],Microsoft.FStar.Absyn.Syntax+modul,System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+modul],Microsoft.FStar.Tc.Env+env]].Invoke (System.Tuple`2 , Microsoft.FStar.Absyn.modul ) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.loop@144-20[modul,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`2 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Fold[modul,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.check_modules (Microsoft.FStar.Tc.solver_t s, Microsoft.FSharp.Collections.FSharpList`1 mods) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.FStar.go$cont@52 (Microsoft.FSharp.Collections.FSharpList`1 filenames, Microsoft.FSharp.Core.Unit unitVar) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.FStar.go[Unit] (Microsoft.FSharp.Core.Unit _arg1) [0x00000] in <filename unknown>:0 
  at <StartupCode$FStar>.$Microsoft.FStar.FStar.main@ () [0x00000] in <filename unknown>:0 

Exp_fvar `ctor` marker invalid

For example, [None|Some _] are not marked.

F* has different behaviors in different contexts

The following code perfectly type-checks in an empty context:

val test2 : int * unit
let test2 = (3, ())

but not if we put some unrelated code before:

type foo 'a : Type => Type =
| Foo : 'b:Type => 'a -> 'b -> foo 'a 'b

let f x =
  match x with
  | Foo (_, y) -> y

val test2 : int * unit
let test2 = (3, ())

in which case I get the error:

Problem:
<prob>
Failed because: head mismatch (t-1)
examples/unit-tests/polymorphism.fst(10,9-10,10) : Error
Expected expression of type "(foo 'U531 'U532)";
got expression "_7883" of type "(_:'U529 -> PURE ((foo (Tuple2 'U523 'U530) 'U529)))"

This example can be found in examples/unit-tests/polymorphism.fst.

Unification failure: arrow mismatch, incompatible types

The following works (see sf-poly.fst):

val ftrue : 'b -> Tot bool
let ftrue _ = true

But the following equivalent definition doesn't

val constfun : 'a -> 'b -> Tot 'a
let constfun x _ = x
val ftrue : 'b -> Tot bool
let ftrue = constfun true

It causes the following error:

Problem:
<prob>
Failed because: arrow mismatch
Incompatible types (_:'U1265 -> Tot bool)
and ('b:Type -> _:'b -> Tot bool)
examples\unit-tests\sf-poly.fst(345,12-345,25) : Error
Expected type "('b:Type -> _:'b -> Tot bool)";
got type "(_:'U1265 -> Tot bool)"

Too weak logic encoding for pure functions

I would expect that the body of a pure function like:

val next_weekday : day -> Tot day
let next_weekday d =
  match d with
  | Monday    -> Tuesday
  | Tuesday   -> Wednesday
  | Wednesday -> Thursday
  | Thursday  -> Friday
  | Friday    -> Monday
  | Saturday  -> Monday
  | Sunday    -> Monday

would be passed in its entirety to the solver. However, this doesn't seem the case now, so no wonder the solver is not able to prove even trivial facts like:

(= (Basic.next_weekday (Basic.next_weekday Basic.Saturday__395))
 Basic.Tuesday__387)

My impression is that this could be the cause for all the 12 unsolved VCs in sf-basic.fst, I'm just surprised that some non-trivial VCs in sf-basic.fst are solved even with the current encoding (like test_mult1, plus_O_n, plus_id_example, and mult_0_plus). Same for append_mem in listlemmas.fst.

Shouldn't require that all types have trivial well-formedness conditions

The following code should succeed:

assume val factorial : n:nat -> Tot nat
assume val bar:n:int{n > 1} -> Tot (y:int{y==factorial n})

but it fails with the following error message:

Type "(n:n:int{n > 1} -> Tot y:int{y == (factorial n)})" has an unexpected non-trivial pre-condition 2: (forall n:n:int{n > 1} y:int. (Meta (labeled This term may not terminate (well-formedness.fst(10,55-10,56))) (l_and (Meta (labeled Subtyping check failed; expected type nat; got type n:int{n > 1} (well-formedness.fst(10,55-10,56))) (GTE n 0)) True)) /\ (forall x:i:int{i >= 0}. True))

Made F* blow up

This works (it seems, I was surprised too):

val minus : nat -> nat -> Tot nat
let rec minus (n : nat) (m : nat) : nat =
  match n, m with
  | O   , _    -> O
  | S _ , O    -> n
  | S n', S m' -> minus n' m'

But the following blows up (I've just removed the spurious annotations on the arguments):

val minus : nat -> nat -> Tot nat
let rec minus n m =
  match n, m with
  | O   , _    -> O
  | S _ , O    -> n
  | S n', S m' -> minus n' m'

Here is the output

[hritcu@detained unit-tests]$ ../../bin/fstar.exe --prims ../../lib/prims.fst --verify sf-basic.fst --trace_error
<tar.exe --prims ../../lib/prims.fst --verify sf-basic.fst --trace_error
Bound term variable not found: n'
  at Microsoft.FStar.ToSMT.Encode.lookup_term_var[syntax`2,syntax`2] (Microsoft.FStar.ToSMT.env_t env, Microsoft.FStar.Absyn.withinfo_t`2 a) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_exp (Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at [email protected] (System.Tuple`2 tupledArg) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3042[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Util+either`2[Microsoft.FStar.ToSMT.Term+term,Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]]],System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean],System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Util+either`2[Microsoft.FStar.ToSMT.Term+term,Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]]]].Invoke (System.Tuple`2 , System.Tuple`2 ) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.loop@151-20[Tuple`2,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`2 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Fold[Tuple`2,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_args (Microsoft.FSharp.Collections.FSharpList`1 l, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_exp (Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_equation@946 (Microsoft.FStar.ToSMT.term ftok, System.String f, Microsoft.FSharp.Collections.FSharpList`1 xs, Microsoft.FStar.Absyn.syntax`2 scrutinee, Microsoft.FStar.Absyn.pat p, Microsoft.FSharp.Core.FSharpOption`1 w, Microsoft.FStar.Absyn.syntax`2 br, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.aux@994-7 (Microsoft.FStar.ToSMT.term ftok, System.String f, Microsoft.FStar.ToSMT.env_t env, Microsoft.FSharp.Collections.FSharpList`1 xs, Microsoft.FStar.Absyn.syntax`2 scrutinee, Microsoft.FSharp.Collections.FSharpList`1 out, Microsoft.FSharp.Collections.FSharpList`1 _arg6) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_sigelt' (Microsoft.FStar.ToSMT.env_t env, Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_sigelt (Microsoft.FStar.ToSMT.env_t env, Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_sig (Microsoft.FStar.Tc.env tcenv, Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>:0 
  at [email protected] (Microsoft.FStar.Tc.env tcenv, Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FStar.Tc.Env+env,Microsoft.FStar.Absyn.Syntax+sigelt].InvokeFast[Unit] (Microsoft.FSharp.Core.FSharpFunc`2 func, Microsoft.FStar.Tc.env arg1, Microsoft.FStar.Absyn.sigelt arg2) [0x00000] in <filename unknown>:0 
  at [email protected] (Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3042[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+sigelt],Microsoft.FStar.Tc.Env+env],Microsoft.FStar.Absyn.Syntax+sigelt,System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+sigelt],Microsoft.FStar.Tc.Env+env]].Invoke (System.Tuple`2 , Microsoft.FStar.Absyn.sigelt ) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.loop@151-20[sigelt,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`2 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Fold[sigelt,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_decls (Microsoft.FStar.Tc.env env, Microsoft.FSharp.Collections.FSharpList`1 ses) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_modul (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.modul modul) [0x00000] in <filename unknown>:0 
  at [email protected] (Microsoft.FStar.Absyn.modul m) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3042[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+modul],Microsoft.FStar.Tc.Env+env],Microsoft.FStar.Absyn.Syntax+modul,System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+modul],Microsoft.FStar.Tc.Env+env]].Invoke (System.Tuple`2 , Microsoft.FStar.Absyn.modul ) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.loop@151-20[modul,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`2 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Fold[modul,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.check_modules (Microsoft.FStar.Tc.solver_t s, Microsoft.FSharp.Collections.FSharpList`1 mods) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.FStar.go$cont@52 (Microsoft.FSharp.Collections.FSharpList`1 filenames, Microsoft.FSharp.Core.Unit unitVar) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.FStar.go[Unit] (Microsoft.FSharp.Core.Unit _arg1) [0x00000] in <filename unknown>:0 
  at <StartupCode$fstar>.$Microsoft.FStar.FStar.main@ () [0x00000] in <filename unknown>:0 

These patterns are clearly not incomplete

It seems that F* now reports that patterns are incomplete when other errors are around, even when that's completely bogus. Here is an example:

val lemma : n:nat -> Fact unit (ensures 0 < 42)
let lemma n =
  match n with
  | O -> admit()
  | S n -> assert(False); admit()

The error:

Error bug44.fst(8,0-12,0): The following problems were found:
    assertion failed (call at bug44.fst(11,12-11,26)) (call at bug44.fst(11,12-11,26))
    Patterns are incomplete (bug44.fst(9,2-12,0))

Yes, the assert is false, but that doesn't mean that F* should report any other errors besides that.

Support more than one SMT solver (Z3)

Hi,

Is it possible to Open Source Z3 under ASL 2.0 so the whole F* stack is under ASL 2.0?

Suminda

"flex-rigid case failed all backtracking attempts" to prove "assert false" in an impossible case due to dependent types

The following code:

val head: n:(n:nat{n > 0}) -> vector 'a n -> 'a
let head n v =
  match v with
    | VNil -> assert false; failwith "Dead code"
    | VCons x n xs -> x

raises the following error during pre-typing (without the --verify flag):

Failed because: flex-rigid case failed all backtracking attempts
examples/unit-tests/vectors.fst(29,0-33,0) : Error
Expected type "('U525 'a)";
got type "(vector 'a n)"

This example can be found in examples/unit-tests/vectors.fst.

Passing lemma to SMT in local scope of extrinsic proof (using)

Chantal suggested that we could have a construct that feeds a given lemma (or set of lemmas?) to the SMT solver in the local scope. I can imagine syntaxes like using typable_empty_closed, or using typable_empty_closed [VPat (appears_free_in x e)] or using [typable_empty_closed [VPat (appears_free_in x e)], sometime_other_lemma [some_other_pattern]] or using list_lemmas where list lemmas is a "lemma database" for lists containing lemma-pattern pairs.

See which type was infered by F*

fstar.exe could have an option that prints the types infered by F*, when none is given by the user (this option is -i for ocaml)

Output diffs for unit tests

We discussed that we want to check for any output changes in the unit tests, and report any inconsistencies with respect to previously saved and audited logs.

Implement the 'private' qualifier on type/val/let declarations and filter those declarations from the module’s export list

The "function" keyword

The "function" keyword is currently not working. For instance:

let rec length l = match l with
| [] -> 0
| x::xs -> 1 + (length xs)

works well whereas

let rec length = function
| [] -> 0
| x::xs -> 1 + (length xs)

raises the error:

Unexpected term
let rec length=(fun _682 -> match _682 with [] -> 0 | (Cons x xs) -> +(1, (...

Parser support for infix/mix fix operators

Better logging/tracing

original title: An error reporting and diagnostics logging framework, with tunable levels

CH: we could take some inspiration from the F5 type derivation viewer, some screenshots here:
http://www.infsec.cs.uni-saarland.de/projects/F5 Generally, I think a tree view is much better suited for displaying this kind of data than a huge sequential log.

NS: Doing something like those screenshots would be terrific! It sounds like a BIG effort though and is likely to take a while, including some invasive work on the type-checker to make sure that such contexts are made available. I'd prefer to do that after we stabilize the checker for the school (and would be happy to make this kind of visualization a priority thereafter).

NS: in the short term, I was just thinking that it would be good to clean up the way in which we're reporting errors. For example, assign unique error codes to all of them; classify some as errors, others as warnings; provide flags to disable certain warnings; etc. On the diagnostic side, the code is littered with (if debug env Options.Low/Med/High then printf "...") ... which is really ugly. Can we adopt some more principled logging framework?

CH: I'll have a look at the existing logging frameworks for OCaml and F# [..] and then report back. I've started a Google Doc about this here: https://docs.google.com/document/d/16Y_kl9yx505siu8BWh7Hc7xDR0UeX-OLX9ZS4HemH0Q/edit?usp=sharing
Please let me know if you want edit access to it.

Problem with recursive function taking function as argument

This recursive function (a simplified variant of a lemma in stlc.fst):

type env = int -> Tot (option nat)

assume val f : e:nat -> Tot bool

val free_in_context : e:nat -> g:env -> Pure unit
      (requires True)
      (ensures \r -> (is_Some (g 42)))
let rec free_in_context e g =
  match e with
  | S n' -> free_in_context n' g

Causes the following bogus error:

mono ../../bin/fstar.exe --fstar_home ../.. bug43.fst --verify --logQueries
bug43.fst(11,31-11,32) : Error
Expected a function;
got an expression of type "_7894:(_:int -> Tot (option nat)){(Precedes #lex_t #lex_t (LexPair #nat #lex_t e (LexPair #(_:int -> Tot (option nat)) #lex_t _7894 LexTop)) (LexPair #nat #lex_t e (LexPair #(_:int -> Tot (option nat)) #lex_t g LexTop)))}"

Apparently no support for Z3 4.3.2

It seems that currently F* requires Z3 4.3.1, which is a not the newest version and for which there are no Linux binaries available. So on Linux one has to build Z3 from source to use F*.

On Z3 4.3.2, the latest version and for which Linux binaries exist, I'm getting the following error:

[hritcu@detained pub]$ z3.exe --version
Z3 version 4.3.2
[hritcu@detained pub]$ mono bin/fstar.exe --prims lib/prims.fst examples/unit-tests/utils.fst 
Parsed, desugared, and pre-typed module: Prims
Parsed, desugared, and pre-typed module: List
WARNING: input file was already specified.
ERROR: the parameter 'mbqi' was renamed to 'smt.mbqi', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:smt.mbqi' for the full description of the parameter

Type-checker stumbles upon type abbreviation

This works (taken from stlc.fs):

val extend : env -> int -> ty -> int -> Tot (option ty)
let extend g x t  = (fun x' -> if x = x' then Some t else g x')

But this equivalent variant fails type-checking:

type env = int -> Tot (option ty)
val extend : env -> int -> ty -> Tot env
let extend g x t  = (fun x' -> if x = x' then Some t else g x')

The error message is:

Expected a term of type "(_:env -> _:int -> _:ty -> Tot env)";
got a function "(fun g:<UNKNOWN> x:<UNKNOWN> t:<UNKNOWN> x':<UNKNOWN> -> (match (op_Equality x x') with true  -> (Some t)
    false  -> (g x')))"

Extension to the parser, allowing type variables to begin without a prime

Bound term variable not found during SMT encoding for some pattern matches

An error similar to the one in #16 occurs for with some (but clearly not all) pattern matches. There are two simultaneous pattern matches from sf-basic.fst. For instance:

val beq_nat : nat -> nat -> Tot mbool
let rec beq_nat n m =
  match n, m with
  | O   , O    -> MTrue
  | S n', S m' -> beq_nat n' m'
  | _   , _    -> MFalse

Causes

Bound term variable not found: n'
   at Microsoft.FStar.ToSMT.Encode.lookup_term_var[a,b](env_t env, withinfo_t`2
a) in E:\Projects\fstar\pub\src\tosmt\encode.fs:line 141
   at Microsoft.FStar.ToSMT.Encode.encode_exp(syntax`2 e, env_t env) in E:\Proje
cts\fstar\pub\src\tosmt\encode.fs:line 421
   at [email protected](Tuple`2 tupledArg) i
n E:\Projects\fstar\pub\src\tosmt\encode.fs:line 585
   at Microsoft.FSharp.Collections.ListModule.loop@142-20[T,TState](FSharpFunc`3
 f, TState s, FSharpList`1 xs)
   at Microsoft.FSharp.Collections.ListModule.Fold[T,TState](FSharpFunc`2 folder
, TState state, FSharpList`1 list)
   at Microsoft.FStar.ToSMT.Encode.encode_args(FSharpList`1 l, env_t env) in E:\
Projects\fstar\pub\src\tosmt\encode.fs:line 583
   at Microsoft.FStar.ToSMT.Encode.encode_exp(syntax`2 e, env_t env) in E:\Proje
cts\fstar\pub\src\tosmt\encode.fs:line 419
   at Microsoft.FStar.ToSMT.Encode.encode_equation@1031(term ftok, String f, FSh
arpList`1 xs, syntax`2 scrutinee, pat p, FSharpOption`1 w, syntax`2 br, env_t en
v) in E:\Projects\fstar\pub\src\tosmt\encode.fs:line 1081
   at Microsoft.FStar.ToSMT.Encode.aux@1086-7(term ftok, String f, env_t env, FS
harpList`1 xs, syntax`2 scrutinee, FSharpList`1 out, FSharpList`1 _arg6) in E:\P
rojects\fstar\pub\src\tosmt\encode.fs:line 1089
   at Microsoft.FStar.ToSMT.Encode.encode_sigelt'(env_t env, sigelt se) in E:\Pr
ojects\fstar\pub\src\tosmt\encode.fs:line 1084
   at Microsoft.FStar.ToSMT.Encode.encode_sigelt(env_t env, sigelt se) in E:\Pro
jects\fstar\pub\src\tosmt\encode.fs:line 770
   at Microsoft.FStar.ToSMT.Encode.encode_sig(env tcenv, sigelt se) in E:\Projec
ts\fstar\pub\src\tosmt\encode.fs:line 1233
   at [email protected](env tcenv, sigelt se) in
 E:\Projects\fstar\pub\src\tosmt\encode.fs:line 1270
   at [email protected](sigelt se) in E:\Projects\fst
ar\pub\src\tc\tc.fs:line 1285
   at Microsoft.FSharp.Collections.ListModule.loop@142-20[T,TState](FSharpFunc`3
 f, TState s, FSharpList`1 xs)
   at Microsoft.FSharp.Collections.ListModule.Fold[T,TState](FSharpFunc`2 folder
, TState state, FSharpList`1 list)
   at Microsoft.FStar.Tc.Tc.tc_decls(env env, FSharpList`1 ses) in E:\Projects\f
star\pub\src\tc\tc.fs:line 1279
   at Microsoft.FStar.Tc.Tc.tc_modul(env env, modul modul) in E:\Projects\fstar\
pub\src\tc\tc.fs:line 1300
   at [email protected](modul m) in E:\Projects\
fstar\pub\src\tc\tc.fs:line 1313
   at Microsoft.FSharp.Collections.ListModule.loop@142-20[T,TState](FSharpFunc`3
 f, TState s, FSharpList`1 xs)
   at Microsoft.FSharp.Collections.ListModule.Fold[T,TState](FSharpFunc`2 folder
, TState state, FSharpList`1 list)
   at Microsoft.FStar.Tc.Tc.check_modules(solver_t s, FSharpList`1 mods) in E:\P
rojects\fstar\pub\src\tc\tc.fs:line 1308
   at Microsoft.FStar.FStar.go$cont@52(FSharpList`1 filenames, Unit unitVar) in
E:\Projects\fstar\pub\src\fstar.fs:line 52
   at <StartupCode$FStar>.$Microsoft.FStar.FStar.main@() in E:\Projects\fstar\pu
b\src\fstar.fs:line 89

Replacing the simultaneous pattern match with a nested one works around the problem in sf-basic.fst.

IDE Support | Wizards

Another area you might be able to improve on.

Incompatible types (list i:int{i >= 0}) and (list nat)

The following code in sf-poly.fst (now commented out):

val test_filter1 : unit -> Fact unit
      (ensures (filter evenb [1;2;3;4] == [2;4]))

Causes the following error:

Problem:
<prob>
Failed because: refinement subtyping is not applicable
Incompatible types (list i:int{i >= 0})
and (list nat)
examples\unit-tests\sf-poly.fst(232,29-232,38) : Error
Expected type "(list nat)";
got type "(list i:int{i >= 0})"

Error compiling "Hello World" in Ubuntu 14.04

I managed to get fstar to compile fine in Ubuntu 14.04. I then downloaded Z3 at http://z3.codeplex.com/releases/view/101911 and added the bin directories of fstar and Z3 to the path. I also made the environment variable FSTAR_HOME pointing to the directory of the fstar download. However when I try to compile :

module HelloWorld
let _ = print "Hello world!"

via fstar.exe hello.fst I get the error message :

unknown(0,0-0,0) : Error : Identifier not found: [Prims.print] 
WARNING: input file was already specified.
ERROR: the parameter 'mbqi' was renamed to 'smt.mbqi', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:smt.mbqi' for the full description of the parameter

Better pretty printer

NS: better printing of terms would improve the readability of error messages immediately (and would also be useful groundwork for better visualizations in the future)

NS: About debug level low: It's not designed to be robust right now. Hence one of my tasks on the list I sent last night. It's using a very naive normalizer to print types. That thing blows up on anything but the smallest types.

Spurious/subsumed termination problems

I've noticed recently that now many of our errors also report termination problems that seem spurious, implied by the the failure of type-checking. For instance

assume val factorial : n:nat -> Tot nat
assume val foo: n:int -> Tot (y:int{y==factorial n})

complains not just about not respecting factorial's precondition, but also about the obvious fact that not respecting any pure function's preconditions can lead to non-termination?

Error well-formedness-bug26.fst(12,0-13,0): The following problems were found:
    This term may not terminate (well-formedness-bug26.fst(12,49-12,50))
    Subtyping check failed; expected type nat; got type int (well-formedness-bug26.fst(12,49-12,50))

In this case, the termination error is reported before the real cause of the problem, which I think can make it harder to understand the problem.

Did not manage to prove properties about higher-order functions

F* does not manage to prove (--verify) this:

val f3 : g:('a -> Tot 'b) -> h:(a:'a -> Tot (b:'b{b == g a})) -> 'a -> r:('b * 'b){fst r == snd r}
let f3 g h x = (g x, h x)

The error message is:

Error higherorder.fst(27,0-27,25): The following problems were found:
    Subtyping check failed; expected type r:(Tuple2 'b 'b){(fst #'b #'b r) == (snd #'b #'b r)}; got type (Tuple2 'b 'b) (higherorder.fst(27,15-27,25))

My first try was actually this:

val f2 : g:('a -> Tot 'b) -> h:('a -> Tot 'b){forall (a:'a). g a == h a} -> 'a -> r:('b * 'b){fst r == snd r}
let f2 g h x = (g x, h x)

but then F* complains:

Error
Expected a function;
got an expression of type "h:(_:'a -> Tot 'b){(forall a:'a. (g a) == (h a))}"

All this can be found in examples/unit-tests/higherorder.fst.

Installation failure on Ubuntu 14.04

Hi, I have installed mono and fsharp. However when I perform make -C src/ on Ubuntu 14.04 I get the error message :

mono .nuget/NuGet.exe restore FStar.sln
WARNING: The initialization function tries to access Value on this instance
WARNING: Error getting response stream (Write: The authentication or decryption has failed.): SendFailure
Unable to find version '6.0.3' of package 'FsLexYacc'.
Unable to find version '6.0.2' of package 'FsLexYacc.Runtime'.
make[1]: *** [install-packages] Error 1

Thanks.

F* loops when Z3 times out or gets killed

System.Threading.Monitor.Wait in ask_process in utils.fs gets stuck forever when Z3 times out or gets killed. Could this be some sort of deadlock?

Lambda bound variable not found during SMT encoding

For instance the following code from sf-poly.fst works fine:

val plus3 : int -> Tot int
let plus3 n = n + 3
val test_map1 : unit -> Fact unit
      (ensures (map plus3 [2;0;2] == [5;3;5]))

Replacing plus3 with (fun n -> n + 3) (just inlining) makes F* blow up though:

Bound term variable not found: n
   at Microsoft.FStar.ToSMT.Encode.lookup_term_var[a,b](env_t env, withinfo_t`2
a) in E:\Projects\fstar\pub\src\tosmt\encode.fs:line 141
   at Microsoft.FStar.ToSMT.Encode.encode_exp(syntax`2 e, env_t env) in E:\Proje
cts\fstar\pub\src\tosmt\encode.fs:line 421
   at [email protected](Tuple`2 tupledArg) i
n E:\Projects\fstar\pub\src\tosmt\encode.fs:line 585
   at Microsoft.FSharp.Collections.ListModule.loop@142-20[T,TState](FSharpFunc`3
 f, TState s, FSharpList`1 xs)
   at Microsoft.FSharp.Collections.ListModule.Fold[T,TState](FSharpFunc`2 folder
, TState state, FSharpList`1 list)
   at Microsoft.FStar.ToSMT.Encode.encode_args(FSharpList`1 l, env_t env) in E:\
Projects\fstar\pub\src\tosmt\encode.fs:line 583
   at Microsoft.FStar.ToSMT.Encode.encode_exp(syntax`2 e, env_t env) in E:\Proje
cts\fstar\pub\src\tosmt\encode.fs:line 419
   at Microsoft.FStar.ToSMT.Encode.encode_exp(syntax`2 e, env_t env) in E:\Proje
cts\fstar\pub\src\tosmt\encode.fs:line 448
   at [email protected](Tuple`2 tupledArg) i
n E:\Projects\fstar\pub\src\tosmt\encode.fs:line 585
   at Microsoft.FSharp.Collections.ListModule.loop@142-20[T,TState](FSharpFunc`3
 f, TState s, FSharpList`1 xs)
   at Microsoft.FSharp.Collections.ListModule.Fold[T,TState](FSharpFunc`2 folder
, TState state, FSharpList`1 list)
   at Microsoft.FStar.ToSMT.Encode.encode_args(FSharpList`1 l, env_t env) in E:\
Projects\fstar\pub\src\tosmt\encode.fs:line 583
   at Microsoft.FStar.ToSMT.Encode.encode_exp(syntax`2 e, env_t env) in E:\Proje
cts\fstar\pub\src\tosmt\encode.fs:line 419
   at [email protected](Tuple`2 tupledArg) in
E:\Projects\fstar\pub\src\tosmt\encode.fs:line 598
   at Microsoft.FSharp.Collections.ListModule.loop@142-20[T,TState](FSharpFunc`3
 f, TState s, FSharpList`1 xs)
   at Microsoft.FSharp.Collections.ListModule.Fold[T,TState](FSharpFunc`2 folder
, TState state, FSharpList`1 list)
   at Microsoft.FStar.ToSMT.Encode.encode_fe@595[a](FSharpList`1 l, env_t env) i
n E:\Projects\fstar\pub\src\tosmt\encode.fs:line 596
   at [email protected](FSharpList`1 l) in E:\Projec
ts\fstar\pub\src\tosmt\encode.fs:line 601
   at Microsoft.FStar.ToSMT.Encode.fallback@631(env_t env, syntax`2 phi) in E:\P
rojects\fstar\pub\src\tosmt\encode.fs:line 633
   at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels(syntax`2 phi, env_
t env) in E:\Projects\fstar\pub\src\tosmt\encode.fs:line 661
   at [email protected](Tuple`2 tupledArg) in
E:\Projects\fstar\pub\src\tosmt\encode.fs:line 597
   at Microsoft.FSharp.Collections.ListModule.loop@142-20[T,TState](FSharpFunc`3
 f, TState s, FSharpList`1 xs)
   at Microsoft.FSharp.Collections.ListModule.Fold[T,TState](FSharpFunc`2 folder
, TState state, FSharpList`1 list)
   at Microsoft.FStar.ToSMT.Encode.encode_fe@595[a](FSharpList`1 l, env_t env) i
n E:\Projects\fstar\pub\src\tosmt\encode.fs:line 596
   at [email protected](FSharpList`1 l) in E:\Projec
ts\fstar\pub\src\tosmt\encode.fs:line 601
   at Microsoft.FStar.ToSMT.Encode.encode_q_body@643(env_t env, FSharpList`1 bs,
 FSharpList`1 ps, syntax`2 body) in E:\Projects\fstar\pub\src\tosmt\encode.fs:li
ne 649
   at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels(syntax`2 phi, env_
t env) in E:\Projects\fstar\pub\src\tosmt\encode.fs:line 672
   at [email protected](Tuple`2 tupledArg) in
E:\Projects\fstar\pub\src\tosmt\encode.fs:line 597
   at Microsoft.FSharp.Collections.ListModule.loop@142-20[T,TState](FSharpFunc`3
 f, TState s, FSharpList`1 xs)
   at Microsoft.FSharp.Collections.ListModule.Fold[T,TState](FSharpFunc`2 folder
, TState state, FSharpList`1 list)
   at Microsoft.FStar.ToSMT.Encode.encode_fe@595[a](FSharpList`1 l, env_t env) i
n E:\Projects\fstar\pub\src\tosmt\encode.fs:line 596
   at [email protected](FSharpList`1 l) in E:\Projec
ts\fstar\pub\src\tosmt\encode.fs:line 601
   at [email protected](Tuple`2 tupledArg) in
E:\Projects\fstar\pub\src\tosmt\encode.fs:line 597
   at Microsoft.FSharp.Collections.ListModule.loop@142-20[T,TState](FSharpFunc`3
 f, TState s, FSharpList`1 xs)
   at Microsoft.FSharp.Collections.ListModule.Fold[T,TState](FSharpFunc`2 folder
, TState state, FSharpList`1 list)
   at Microsoft.FStar.ToSMT.Encode.encode_fe@595[a](FSharpList`1 l, env_t env) i
n E:\Projects\fstar\pub\src\tosmt\encode.fs:line 596
   at [email protected](FSharpList`1 l) in E:\Projec
ts\fstar\pub\src\tosmt\encode.fs:line 601
   at Microsoft.FStar.ToSMT.Encode.encode_q_body@643(env_t env, FSharpList`1 bs,
 FSharpList`1 ps, syntax`2 body) in E:\Projects\fstar\pub\src\tosmt\encode.fs:li
ne 649
   at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels(syntax`2 phi, env_
t env) in E:\Projects\fstar\pub\src\tosmt\encode.fs:line 672
   at Microsoft.FStar.ToSMT.Encode.solve(env tcenv, syntax`2 q) in E:\Projects\f
star\pub\src\tosmt\encode.fs:line 1246
   at [email protected](env tcenv, syntax`2 q) i
n E:\Projects\fstar\pub\src\tosmt\encode.fs:line 1272
   at Microsoft.FStar.Tc.Util.solve(env env, syntax`2 f) in E:\Projects\fstar\pu
b\src\tc\tcutil.fs:line 564
   at Microsoft.FStar.Tc.Util.discharge_guard(env env, guard_t g) in E:\Projects
\fstar\pub\src\tc\tcutil.fs:line 578
   at Microsoft.FStar.Tc.Tc.tc_value(env env, syntax`2 e) in E:\Projects\fstar\p
ub\src\tc\tc.fs:line 486
   at Microsoft.FStar.Tc.Tc.tc_exp(env env, syntax`2 e) in E:\Projects\fstar\pub
\src\tc\tc.fs:line 514
   at Microsoft.FStar.Tc.Tc.tc_exp(env env, syntax`2 e) in E:\Projects\fstar\pub
\src\tc\tc.fs:line 800
   at Microsoft.FStar.Tc.Tc.tc_decl(env env, sigelt se) in E:\Projects\fstar\pub
\src\tc\tc.fs:line 1228
   at [email protected](sigelt se) in E:\Projects\fst
ar\pub\src\tc\tc.fs:line 1282
   at Microsoft.FSharp.Collections.ListModule.loop@142-20[T,TState](FSharpFunc`3
 f, TState s, FSharpList`1 xs)
   at Microsoft.FSharp.Collections.ListModule.Fold[T,TState](FSharpFunc`2 folder
, TState state, FSharpList`1 list)
   at Microsoft.FStar.Tc.Tc.tc_decls(env env, FSharpList`1 ses) in E:\Projects\f
star\pub\src\tc\tc.fs:line 1279
   at Microsoft.FStar.Tc.Tc.tc_modul(env env, modul modul) in E:\Projects\fstar\
pub\src\tc\tc.fs:line 1300
   at [email protected](modul m) in E:\Projects\
fstar\pub\src\tc\tc.fs:line 1313
   at Microsoft.FSharp.Collections.ListModule.loop@142-20[T,TState](FSharpFunc`3
 f, TState s, FSharpList`1 xs)
   at Microsoft.FSharp.Collections.ListModule.Fold[T,TState](FSharpFunc`2 folder
, TState state, FSharpList`1 list)
   at Microsoft.FStar.Tc.Tc.check_modules(solver_t s, FSharpList`1 mods) in E:\P
rojects\fstar\pub\src\tc\tc.fs:line 1308
   at Microsoft.FStar.FStar.go$cont@52(FSharpList`1 filenames, Unit unitVar) in
E:\Projects\fstar\pub\src\fstar.fs:line 52
   at <StartupCode$FStar>.$Microsoft.FStar.FStar.main@() in E:\Projects\fstar\pu
b\src\fstar.fs:line 89

Made logical encoding blow up

The following code (simplified from stlc.fst):

(* having this type abbreviation seems crucial for reproducing this *)
type env = int -> Tot (option int)

val empty : env
let empty _ = None

assume val xxx : g:env -> Fact unit (ensures (is_Some (g 45)))

val yyy : unit -> Tot unit
let yyy () =
 match 42 with
 _ -> xxx empty

causes encode_exp to blow up:

(bug46.fst(10,54-10,60)) term is (empty 45); head type is (option int)
  at Microsoft.FStar.ToSMT.Encode.encode_exp (Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at [email protected] (System.Tuple`2 tupledArg) [0x00000] in <filename unknown>:0 
......

Type "(unit -> Fact (unit))" has unexpected non-trivial pre-condition

If this type doesn't have a trivial pre-condition than which one does?
See commented out code in sf-poly.fst.

Better notation for passing implicit parameters

I'm not sure what Nik had in mind, but we could consider taking some inspiration from Coq, where prefixing an identifier name with @ allows+requires one to pass in all its implicit arguments. If I understood correctly from Nik's code walk-though, if one passes in one implict with #, one needs to pass all of them, so I don't see why mark each argument passed in explictly and not the function.

Sharing annotations among arguments

It would be nice if one could write

let rec mult (n m : nat) : nat = ...

instead of

let rec mult (n : nat) (m : nat) : nat = ...

Automatic instantiation of induction hypothesis in extrinsic proofs

This would be optional, triggered by some syntax like autoind() or autoind(pattern).

F* does not generalize inner lets

When defining the following example:

val test : int * unit
let test = let g x = x in (g 3, g ())

F* complains:

Problem:
<prob>
Failed because: head mismatch (t-1)
examples/unit-tests/polymorphism.fst(4,34-4,36) : Error
Expected expression of type "int";
got expression "()" of type "unit"

This example can be found in examples/unit-test/polymorphism.fst.

Z3 models not minimal leads to bad error messages: e.g. admitted post-condition shouldn't fail

F* sometimes reports failing post-condition when other things failed, but the post-condition does hold (e.g, we've admited it). For instance:

val xxx : unit -> Fact unit (ensures (False))
let xxx _ = assert(False); admit()

Causes the following errors:

Error bug45.fst(5,0-6,0): The following problems were found:
    assertion failed (call at bug45.fst(5,12-5,26)) (call at bug45.fst(5,12-5,26))
    post-condition at bug45.fst(4,37-4,42)

Yes, the assertion is wrong, but the post-condition is not, and having anything about it in the error message is extremely confusing. When removing the wrong assert, the whole thing succeeds, as it should.

Name not found (failwith), ToSMT.Encode.lookup_term_var in tosmt\encode.fs:line 141

The following code:

val impossible : u : unit { False } -> Tot 'a
let impossible = failwith "this won't happen"

causes this exception

../../bin/fstar.exe --fstar_home ../.. sf-poly.fst --verify --logQueries --trace_error
Opening file queries.smt2
Name not found: failwith
  at Microsoft.FStar.ToSMT.Encode.lookup_lid (Microsoft.FStar.ToSMT.env_t env, Microsoft.FStar.Absyn.LongIdent a) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.lookup_free_var_name[syntax`2] (Microsoft.FStar.ToSMT.env_t env, Microsoft.FStar.Absyn.withinfo_t`2 a) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_full_app@515[syntax`2] (Microsoft.FStar.ToSMT.env_t env, Microsoft.FSharp.Collections.FSharpList`1 vars, Microsoft.FSharp.Collections.FSharpList`1 args, Microsoft.FStar.Absyn.withinfo_t`2 fv) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_exp (Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_sigelt' (Microsoft.FStar.ToSMT.env_t env, Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_sigelt (Microsoft.FStar.ToSMT.env_t env, Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_sig (Microsoft.FStar.Tc.env tcenv, Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>:0 
  at [email protected] (Microsoft.FStar.Tc.env tcenv, Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FStar.Tc.Env+env,Microsoft.FStar.Absyn.Syntax+sigelt].InvokeFast[Unit] (Microsoft.FSharp.Core.FSharpFunc`2 func, Microsoft.FStar.Tc.env arg1, Microsoft.FStar.Absyn.sigelt arg2) [0x00000] in <filename unknown>:0 
  at [email protected] (Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3042[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+sigelt],Microsoft.FStar.Tc.Env+env],Microsoft.FStar.Absyn.Syntax+sigelt,System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+sigelt],Microsoft.FStar.Tc.Env+env]].Invoke (System.Tuple`2 , Microsoft.FStar.Absyn.sigelt ) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.loop@151-20[sigelt,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`2 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Fold[sigelt,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_decls (Microsoft.FStar.Tc.env env, Microsoft.FSharp.Collections.FSharpList`1 ses) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_modul (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.modul modul) [0x00000] in <filename unknown>:0 
  at [email protected] (Microsoft.FStar.Absyn.modul m) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3042[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+modul],Microsoft.FStar.Tc.Env+env],Microsoft.FStar.Absyn.Syntax+modul,System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+modul],Microsoft.FStar.Tc.Env+env]].Invoke (System.Tuple`2 , Microsoft.FStar.Absyn.modul ) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.loop@151-20[modul,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`2 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Fold[modul,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.check_modules (Microsoft.FStar.Tc.solver_t s, Microsoft.FSharp.Collections.FSharpList`1 mods) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.FStar.go$cont@52 (Microsoft.FSharp.Collections.FSharpList`1 filenames, Microsoft.FSharp.Core.Unit unitVar) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.FStar.go[Unit] (Microsoft.FSharp.Core.Unit _arg1) [0x00000] in <filename unknown>:0 
  at <StartupCode$fstar>.$Microsoft.FStar.FStar.main@ () [0x00000] in <filename unknown>:0 

I was expecting this to succeed (failwith is defined in prims) or to produce a more gracious failure.

Length-indexed lists cannot take a nat as its argument

The following type definition works:

type vector 'a : int => Type =
  | VNil : vector 'a 0
  | VCons : 'a -> n:nat -> vector 'a n -> vector 'a (n+1)

but it does not if we restrict the length to be a natural number:

type vector2 'a : nat => Type =
  | VNil2 : vector2 'a 0
  | VCons2 : 'a -> n:nat -> vector2 'a n -> vector2 'a (n+1)

We get the error:

Type "('a:Type -> Tot (vector2 'a 0))" has an unexpected non-trivial pre-condition 2: (forall 'a:Type. 0 >= 0)

This example can be found in examples/unit-test/vectors.fst.

Returning function fails pre-type-checking

A frequent pattern in proofs is to only introduce some of the arguments after inducting/recursing over others. I've tried to reproduce this pattern in F*, but so far without much success. For instance:

val foo2 : n : int -> m : int -> l : ilist -> Pure unit
      (requires (repeat n m == l))
      (ensures \r => length l == m)
let rec foo2 n m =
  match m with
  | 0 -> (fun l => foo1 n l)
  | _ -> (fun l => foo2 n (m-1) (repeat n (m-1)))

Produces the following error:

../../bin/fstar.exe --fstar_home ../.. sf-lists.fst --verify
[snip]
sf-lists.fst(128,0-138,3) : Error
Expected a term of type "(n:int -> m:int -> l:ilist -> Pure (unit))";
got a function "(fun n:<UNKNOWN> m:<UNKNOWN> -> (match m with 0  -> (fun l:<UNKNOWN> -> (foo1 n l))
    _  -> (fun l:<UNKNOWN> -> (foo2 n (op_Subtraction m 1) (repeat n (op_Subtraction m 1))))))"

Adding typing annotations doesn't seem to help:

val foo2 : n : int -> m : int -> l : ilist -> Pure unit
      (requires (repeat n m == l))
      (ensures \r => length l == m)
let rec foo2 (n : int) (m : int) : (l : ilist -> Pure unit
      (requires (repeat n m == l))
      (ensures \r => length l == m)) =
  match m with
  | 0 -> (fun l => foo1 n l)
  | _ -> (fun l => foo2 n (m-1) (repeat n (m-1)))

also fails with this error message:

sf-lists.fst(128,0-140,3) : Error
Expected a term of type "(n:int -> m:int -> l:ilist -> Pure (unit))";
got a function "(fun n:int m:int -> (match m with 0  -> (fun l:<UNKNOWN> -> (foo1 n l))
    _  -> (fun l:<UNKNOWN> -> (foo2 n (op_Subtraction m 1) (repeat n (op_Subtraction m 1))))))"

What's the problem with just returning a function?

Cannot pre-typecheck the definition of vectors

examples/unit-tests/vectors.fst does not pass pre-typechecking with the following error:

examples/unit-tests/vectors.fst(21,4-21,8) : Error
Expected expression of type "(vector )";
got expression "_718" of type "(vector )"

F* should return non-zero exit code when something failed

Currently fstar --verify succeeds even if Z3 fails to discharge some of the obligations, which is really bad for automatic testing. Yes, sometimes we expect things to fail, in which case just add a minus sign in front of the command in the Makefile, but we shouldn't be ignoring errors all the time.

Clearly complete pattern match on polymorphic datatype marked as incomplete

The following, clearly complete triple pattern match taken from stlc.fst, is currently rejected as incomplete:

      match typing e1 g, typing e2 g, typing e3 g with
      | Some TBool, Some t2, Some t3 -> if t2 = t3 then Some t2 else None
      | _         , _      , _       -> None

Different binary names and flags for Z3 on UNIX systems

First, the Z3 binary is not called "z3.exe" on UNIX systems, but simply "z3". This can be easily fixed with a symbolic link:

$ ln -s z3 z3.exe

Second, Z3 4.3.1 (the only version that seems to work with F* currently #6) takes flags in a slightly different format on UNIX systems than on Windows. At the moment the workaround is to (re)compile F* on UNIX after changing line 27 in src/tosmt/z3.fs with (i.e. "-" instead of "/" for options):

format1 "-smt2 -in %s \

While these workarounds seem to work, we need a solution for such cross-platform differences that doesn't involve users creating symlinks and editing our source files.

Internals: Meta_desugared (_, Data_app) is never set

I'm currently relying on the type case to infer if a symbol is a constructor or not.

Infinite loop after "unconstrained unification variables" error

The following code (in bug34.fst):

assume val g : 'a -> Tot 'b
assume val h : 'a:Type -> 'b:Type -> a:'a -> Tot (b:'b{b == g a})

first prints

Error bug34.fst(5,0-6,0): Unconstrained unification variables; please add an annotation

and then (apparently) goes into an infinite loop.

Failed admits

I'm encountering cases in which F* fails to type-check admitted cases in proofs:

val foo2' : n : int -> m : int -> l : ilist -> Pure unit
      (requires (repeat n m == l))
      (ensures \r => length l == m)
let foo2' n m l = admit()

or

val foo4 : n : int -> l1 : ilist -> l2 : ilist -> Pure unit
      (requires (snoc l1 n == l2))
      (ensures \r => 0 < (length l2))
let foo4 n l1 l2 = admit()

I thought that False implies everything, but F* seems to sometimes disagree.