In agda-mode there is C-c C-d command to infer a type of expression. This is especially needed when we arrive at a type error! But exactly then this command doesn't work. I would guess that this is because the feature wants to evaluate the expression type in the context of the working file. Rightfully so - but is there a way to bypass it and for example find the expression type in the context of the longest typechecking prefix of a file?

I'm using agda-mode for vs-code but emacs tips are appreciated as well as they hopefully translate.

Also did I miss some feature to infer the type of expression at cursor? The way I use C-c C-d (infer type) is after this command I input the expression of interest manually (or paste it). Would be nice to get a type of the word the cursor points to.