Lack of bidirectionality with records

[mtzguido]

noeq
type inj (t1 t2 : Type) = {
  f : t1 -> t2;
}

let double (x:nat) : inj nat nat = {
  f = (fun x -> x+1);
}

This fails with

- Subtyping check failed
- Expected type inj nat nat got type inj int int

The annotation on double should force the right instantiation for the implicits of the record constructor. Note this also fails even if we annotate that x is a nat:

- Subtyping check failed
- Expected type inj nat nat got type inj nat int

[mtzguido]

Smaller repro, this is caused due to not accumulating guards / subtyping constraints across abstractions.

let f : nat -> nat = let r = fun x -> x + 1 in r

- Subtyping check failed
- Expected type _: nat -> nat got type x: int -> int
- The SMT solver could not prove the query. Use --query_stats for more details.

[nikswamy]

This is another example of lack of bidirectionality with records, though perhaps not the same as the original issue (given that it doesn't involve propagating guards across abstractions). Thanks to @amosr-msft

module BugRecordPoly

type record_ab 'a 'b = { a: 'a; b: 'b }
type record_ac 'a 'b = { a: 'a; b: 'b }

type record_r1 'rab = { r1_ab: 'rab }
type record_r2 'rab = { r2_ab: 'rab }

assume val rec1: record_r1 (record_ab string int)

let rec2_ok = { rec1.r1_ab with a = "AA" }

let rec2: record_r2 (record_ab string int) = {
    r2_ab =
      { rec1.r1_ab with a = "AA" }
      //<: record_ab string int // concrete type on result lets it go through
}