yeslogic/fathom

Incorrect elaboration of record literals?

Kmeakin opened this issue · 0 comments

Kmeakin commented 
// synthesises type `fun (A: Type) (B : Type) -> {x: A, y: B}`
def good_id = fun (A: Type) (B: Type) (p: {x: A, y: B}) =>
    ({x = p.x, y = p.y} : {x : A, y : B});

// synthesises type `fun (A: Type) (B : Type) -> {x: A, y: p}`!
def bad_id = fun (A: Type) (B: Type) (p: {x: A, y: B}) =>
    {x = p.x, y = p.y};