Open
Description
Consider the following snippet.
data U : Set where
u : U
test : U
test = let X = U
a : X
a = u
in {!helper a!} -- C-c C-hCurrently, the signature of helper function is helper : U → U, but it would be better to print helper : (let X = U) → X → U