FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.68k stars 231 forks source link

Bad type inference when using record disambiguation with monads #3310

Open TWal opened 3 months ago

TWal commented 3 months ago

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 commented 3 months ago

A minimization inspired by guido (https://github.com/FStarLang/FStar/issues/3309#issuecomment-2165639699)

type rec1 = {
  x:int;
}

type rec2 = {
  x:int;
}

val bind : #a:Type -> #b:Type -> a -> (a -> b) -> b
let bind x f = f x

let test (r:rec1): int =
  bind r (fun n ->
    n.x
  )