Typeclasses. Bug - Instance over function

[andricicezar]

I do not know how to describe this.

module Poc

open FStar.Tactics.Typeclasses
open FStar.Exn
open FStar.All

class ml (t:Type) = { mldummy : unit }

// Basic ML types
instance ml_int : ml int = { mldummy = () }

instance ml_mlarrow t1 t2 [| ml t1 |] [| ml t2 |] : ml (t1 -> ML t2) = { mldummy = () }

exception Contract_failure

class exportable (t : Type) = { etype : Type; export : t -> etype; ml_etype : ml etype }
class importable (t : Type) = { itype : Type; import : itype -> Ex t; ml_itype : ml itype }

let mk_exportable (#t1 t2 : Type) [|ml t2|] (exp : t1 -> t2) : exportable t1 =
  { etype = t2; export = exp;  ml_etype = solve }
let mk_importable (t1 #t2 : Type) [|ml t1|] (imp : t1 -> Ex t2) : importable t2 =
  { itype = t1; import = imp;  ml_itype = solve }

instance ml_exportable (#t : Type) (d : exportable t) : ml (d.etype) = d.ml_etype
instance ml_importable (#t : Type) (d : importable t) : ml (d.itype) = d.ml_itype

instance exportable_ml t [| ml t |] : exportable t = mk_exportable t (fun x -> x)
instance importable_ml t [| ml t |] : importable t = mk_importable t (fun x -> x)

class checkable (#t:Type) (p : t -> Type0) = { check : (x:t -> b:bool{b ==> p x}) }
instance general_is_checkeable t (p : t -> bool) : checkable (fun x -> p x) = { check = fun x -> p x }

instance exportable_purearrow_spec t1 t2 (pre : t1 -> Type0) (post : t1 -> t2 -> Type0)
  [| d1:importable t1 |] [| d2:exportable t2 |] [| d3:checkable pre |] : exportable ((x:t1) -> Pure t2 (pre x) (post x)) = 
  mk_exportable (d1.itype -> ML d2.etype)
    (fun (f:(x:t1 -> Pure t2 (pre x) (post x))) ->
      (fun (x:d1.itype) ->
        let x : t1 = import x in
        (if check #t1 #pre x then (
          export (f x)
        ) else raise Contract_failure) <: ML d2.etype))

// this works:
let postcond (x:int) (y:int) : Type0 = y = x + 1
let incrs : (x:int) -> Pure int (x > 0) (postcond x) = fun x -> x + 1
let incrs' : int -> ML int = export incrs

// this works too:
let incrs1 : (x:int) -> Pure int (x > 0) (fun y -> y = x + 1) = fun x -> x + 1
let incrs1' : int -> ML int =
  export #_
         #(exportable_purearrow_spec int int (fun x -> b2t (x > 0)) (fun x y -> b2t (y = x + 1)))
         incrs1

// this does not work:
let incrs2 : (x:int) -> Pure int (x > 0) (fun y -> y = x + 1) = fun x -> x + 1
let incrs2' : int -> ML int = export incrs2

error:

(Error) user tactic failed: Typeclass resolution failed: could not solve\
 constraint: Poc.exportable (x: Prims.int -> Prims.Pure Prims.int)

[mtzguido]

So the error Cezar wrote is from an old branch which I need to merge. Current F* fails with a mysterious:

(Error) Type annotation on parameter incompatible with the expected type; The solver found a (partial) counterexample, try to spell your proof in more detail or increase fuel/ifuel

which happens since incrs1' elaborates roughly to

let incrs1 : (x:int) -> Pure int (x > 0) (fun y -> y = x + 1) = fun x -> x + 1

let incrs1' : int -> ML int =
  export #(x:int -> Pure int (x > 0) (fun (y:int{y > x}) -> y = x + 1))
         #(magic ())
         incrs1

(ignore the magic, I added that since that part is not relevant)

For some reason the unifier is infering the type of incrs1 to have a refinement on y in the condition, as shown above. That fails, since we expect a total function there. Not sure where this is coming up. It might be some weird interaction with the fix of #57, but in that case I would expect to see the refinement on y being about x>0, not y>x.

[mtzguido]

I seem to have made a mistake when transcribing it. The refinement is indeed that x > 0 according to the precondition, due to the #57 fix, and this program can be fixed by modifying exportable_purearrow_spec to be fully generic for all Pure functions:

instance exportable_purearrow_spec t1 t2 (pre : t1 -> Type0) (post : (x:t1 -> _:t2{pre x} -> Type0))
  (* ... as before *)

Naming the postcondition as in postcond works since it ascribes the type to int, instead of y:int{x > 0}. This will also work by ascribing the type of y in the postcondition of incrs2:

let incrs2 : (x:int) -> Pure int (x > 0) (fun (y:int) -> y = x + 1) = fun x -> x + 1
let incrs2' : int -> ML int = export incrs2

[mtzguido]

@andricicezar : in the dm4a branch, the second solution (annotating y) seems to work. Not the first one, but not sure why.

Another thing you can do is locally redefine Pure without the trick for #57, so your postconditions do not have any refinement:

effect Pure (a:Type) (pre:Type0) (post: a->Type0) = Prims.Pure a pre post

Personally, I would personally the types, I feel this redefinition might get you in a tough corner at some point.

Closing.

[andricicezar]

I am cool with annotating the types. Thank you very much for looking into this!