Jean Abou Samra (new account) on Nostr: nprofile1q…9ktlj Great project! My pet peeve is the error message for ill-typed ...

nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpq3p50dwg48ec85vc22dr2u3xj5knm5jpn0p8kvvffcxvxl2djkgqqc9ktlj (nprofile…ktlj) Great project! My pet peeve is the error message for ill-typed with-abstractions. It tells me that the type of some internally generated function is ill-typed and displays that big type. I'd really like it to pinpoint to a specific subterm that's ill-typed (as if I had written that function myself). Here's a toy example from some code I happened to be working on: https://gitlab.com/-/snippets/4922467