Can't see the type of some holes in a where block

[yacinehmito]

Given this snippet:

five : Int
five = two + three where
  two : Int
  two = ?two_rhs
  three : Int
  three = 3

This type-checks fine but I can't query the type of ?two_rhs using vim interactive editing (<Leader> + t) by default. When loading in the REPL, :t two_rhs works fine too.

The error:

"Main.idr" 16L, 224C written                                                                              
/home/gpyh/idris-sandbox/Main.idr:10:3: error: not                                                        
    end of block, expected: ")",                                                                          
    "->", ";", "in",                                                                                      
    ambiguous use of a left-associative operator,                                                         
    ambiguous use of a non-associative operator,                                                          
    ambiguous use of a right-associative operator,                                                        
    declaration, end of input,                                                                            
    matching application expression,                                                                      
    where block                                                                                           
  three : Int                                                                                             
  ^                                                                                                       
/home/gpyh/idris-sandbox/Main.idr:10:3: error: not                                                        
    end of block, expected: ")",                                                                          
    "->", ";", "in",                                                                                      
    ambiguous use of a left-associative operator,                                                         
    ambiguous use of a non-associative operator,                                                          
    ambiguous use of a right-associative operator,                                                        
    declaration, end of input,                                                                            
    matching application expression,                                                                      
    where block                                                                                           
  three : Int                                                                                             
  ^                                                                                                       

However, querying the type of ?three_rhs in this snippet works fine:

five : Int
five = two + three where
  two : Int
  two = 2
  three : Int
  three = ?three_rhs

[yacinehmito]

The bug seems to be introduced by the d9f312d76afb7c009f0eea163df01146c71bc8dd commit. See my comment

Apparently vim doesn't send the whole file to the REPL and some important bits in the where clause seems needed in order to type-check. I can't debug further.

[artemohanjanyan]

Using IdrisReload instead of IdrisReloadToLine seems to work just fine. https://github.com/artemohanjanyan/idris-vim/commit/86c544bc88e69d057cf0021c98addf38a230320f

[artemohanjanyan]

Close?

[yacinehmito]

It's been eight years. I am closing if you don't mind.