edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

type inference on record update in let doesn't work based on RHS #327

Open shmish111 opened 4 years ago

shmish111 commented 4 years ago

Steps to Reproduce

Check

f : A -> A
f a =
    let x = record { fieldA = 1 } a
    in ?x

Expected Behavior

Checks successfully

Observed Behavior

Errors (1)
Test.idr:203:13
While processing right hand side of f at Test.idr:202:1--205:1:
Can't infer type for this record update

However if I replace ?x with x it will type check.

edwinb commented 4 years ago

I can't reproduce this because you haven't included the full example.

shmish111 commented 4 years ago

Ooops:

record A where
    constructor MkR
    fieldA : Int

f : A -> A
f a =
    let x = record { fieldA = 1 } a
    in ?x