FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Bad type inference when using record disambiguation with monads

Open TWal opened this issue 8 months ago • 1 comments

Similar to #3309, but using record disambiguation to bamboozle the type inference of F*:

// Two monads, with returns and binds
assume val m1: Type0 -> Type0
assume val m2: Type0 -> Type0

assume val return1: #a:Type0 -> a -> m1 a
assume val return2: #a:Type0 -> a -> m2 a

assume val (let?): #a:Type0 -> #b:Type0 -> m2 a -> (a -> m2 b) -> m2 b
assume val (let*?): #a:Type0 -> #b:Type0 -> m1 (m2 a) -> (a -> m1 (m2 b)) -> m1 (m2 b)

type rec1 = {
  x:int;
}

type rec2 = {
  x:int;
}

assume val f: unit -> m2 (rec1)

val g: unit -> m1 (m2 int)

[@@ expect_failure]
let g () =
  let*? x = return1 (f ()) in
  return1 (return2 x.x)

// The workaround
let g () =
  let*? x = return1 #(m2 rec1) (f ()) in
  return1 (return2 x.x)

Note that this time this is not using fancy dependent types, it's something we could write in any functional programming language (with record field name disambiguation)

TWal avatar Jun 07 '24 12:06 TWal