FStar
FStar copied to clipboard
Bad type inference when using record disambiguation with monads
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)