Incorrect type inference leads to type-incorrect OCaml code

[cpitclaudel]

This code:

#light "off"
module Mini

open FStar
open FStar.All
module BU = FStar.Util

type btree<'a> =
| StrEmpty
| StrBranch of string * 'a * (btree<'a>) * (btree<'a>)

type name_collection<'a> =
| Names of btree<'a>
| ImportedNames of string * names<'a>
and names<'a> = list<name_collection<'a>>

let rec aux (fn: btree<'a> -> 'b) (acc: list<(list<string> * 'b)>)
            (imports: list<string>) (name_collections: names<'a>)
       =
  List.fold_left (fun acc -> function
      | Names bt -> (imports, fn bt) :: acc
      | ImportedNames (nm, name_collections) ->
        aux fn acc (nm :: imports) name_collections)
    acc name_collections

…extracts with a bunch of Obj.magic. They go away if I add an explicit type on aux (list<(list<string> * 'b)>).

Investigating reveals that F* infers this type:

  fn:(uu___639771:Mini.btree 'a -> FStar.All.ML 'b) ->
  acc:Prims.list (Prims.list Prims.string * 'b) ->
  imports:Prims.list Prims.string ->
  name_collections:Mini.names 'a -> FStar.All.ML (Prims.list (Prims.list Prims.string * 'a))

This looks wrong to me. That 'a in the end should be a 'b. This leads to an inconsistency (not in Tot, though):

let absurd : False =
  snd (List.hd (aux (fun x -> ()) [] [] [Names (StrEmpty)]))

To extract I used ../../bin/fstar.exe "--eager_inference" "--lax" "--MLish" "--include" "../../ulib" "--include" "../u_boot_fsts" "--include" "../boot_fstis" --codegen OCaml mini.fst

[cpitclaudel]

Note that requires --lax to fail; otherwise you do get an error message:

Subtyping check failed; expected type Prims.list (Prims.list Prims.string * 'a); got type Prims.list (Prims.list Prims.string * 'b)

[aseemr]

I think this is expected, the lax mode drops the VC, so the constraint a == b might just have been dropped.

[cpitclaudel]

I think this is expected

Which part? Isn't producing incorrectly-typed OCaml code an issue?

[aseemr]

Not in the lax mode, as far as I know (trying to find a similar issue).

[aseemr]

Oh, may be I misunderstood what you mean, do you mean F* should have inserted enough magic to make it compile (but running that program could crash at run time)?

[aseemr]

ok, i see it now, the inference indeed looks strange.

[cpitclaudel]

Oh, may be I misunderstood what you mean, do you mean F* should have inserted enough magic to make it compile (but running that program could crash at run time)?

No, I think you understood me right :) I think it's an issue that a program that typechecks and extracts with --mlish --lax can fail to compile or crash. I was under the vague impression that with --mlish, --lax was sound. Otherwise, why do we compile the compiler in --lax mode?

[aseemr]

lax is not sound, independent of --MLish, you can do strange things with it: let foo (a:Type) (x:option a) :a = x.

But I still don't see why is F* inferring the return type of aux to be Prims.list (Prims.list Prims.string * 'a).

[catalin-hritcu]

Right, --lax doesn't ensure that the code is typable in ML is not sound [edited]. For instance, all the 3 examples we had in #1055 (comment) are lax well-typed. Scary enough 2 of them are even well-typed without the lax. Scared by what they will extract to ... will try now and report back.

[catalin-hritcu]

It's actually not that bad, F* inserts enough Obj.magics so that the code from #1055 (comment) does extract to well-typed OCaml code:

let write: 'Aa . 'Aa FStar_ST.ref -> Prims.unit =
  fun r  -> FStar_ST.op_Colon_Equals r (Obj.magic (Prims.parse_int "42"))
let append_to1: 'Aa . 'Aa Prims.list -> 'Aa Prims.list =
  fun xs  -> (Obj.magic (Prims.parse_int "2")) :: xs
let append_to2: 'Auu____193 'Aa . 'Aa Prims.list -> 'Aa Prims.list =
  fun xs  ->
    (let uu____214 = FStar_ST.alloc (Prims.parse_int "5") in ());
    (Obj.magic (Prims.parse_int "2")) :: xs

So I'm actually not sure whether --lax is supposed to guarantee that things will type-check in OCaml or not, but it's clearly type unsound. For instance it can definitely lead to segmentation faults in OCaml. Just got one right now for the extraction of this lax valid code (for the write above):

let r = alloc "some string" in write r; ignore(!r ^ !r)

[catalin-hritcu]

A small variant of Aseem's example (which also lax-typechecks)

let foo (#a:Type) (x:a) : Tot (option a) = x
let bar = Some?.v (foo 1)

also causes a segmentation fault by basically converting an integer to a pointer and then dereferencing it. Funny enough, if I call foo 0 instead, I just get assertion failure because foo 0 returns 0 which is the binary representation of None, and Some?.v is implemented like this

let __proj__Some__item__v = function Some x -> x | _ -> assert false

[nikswamy]

Came across this issue with @aseemr today.

It seems there are two parts to it:

1. --lax is intentionally unsound (it doesn't build VCs). We shouldn't expect --lax --mlish to give you anything more than --lax.

2. The second issue is that type inference seems to require an unnecessary annotation. So, here's the remaining issue:

module Bug1158
open FStar
open FStar.All
module BU = FStar.Util
module L = FStar.List

type btree 'a =
| StrEmpty
| StrBranch of string * 'a * btree 'a * btree 'a

type name_collection 'a =
| Names of btree 'a
| ImportedNames of string * names 'a
and names 'a = list (name_collection 'a)

let rec aux (fn: btree 'a -> 'b) (acc: list (list string * 'b))
            (imports: list string) (name_collections: names 'a)
      : ML _ (* rightfully need this, otherwise we try to prove it Tot *)
       =
  List.fold_left (fun acc //<-- Type inference bug: without this annotation, type inference fails :(list (list string * 'b)))
  -> function
      | Names bt -> (imports, fn bt) :: acc
      | ImportedNames (nm, name_collections) ->
        aux fn acc (nm :: imports) name_collections)
    acc name_collections

[nikswamy]

Here's another occurrence of it:

//OK
let map_rev (f : 'a -> 'b) (l : list 'a) : list 'b =
  let rec aux (l:list 'a) acc = // (acc:list 'b) = // (l:list 'a) acc = //(acc:list 'b) = //NS: weird, this needs an annotation to type-check 
    match l with
    | [] -> acc
    | x :: xs -> aux xs (f x :: acc)
  in  aux l []

//OK
let map_rev2 (f : 'a -> 'b) (l : list 'a) : list 'b =
  let rec aux l (acc:list 'b) =
    match l with
    | [] -> acc
    | x :: xs -> aux xs (f x :: acc)
  in  aux l []

//FAILS
let map_rev3 (f : 'a -> 'b) (l : list 'a) : list 'b =
  let rec aux l acc =
    match l with
    | [] -> acc
    | x :: xs -> aux xs (f x :: acc)
  in  aux l []