`idris.caseSplit` and `idris.proofSearch` don't work after an `idris.addClause`

[ruippeixotog]

I don't know the exact steps that cause this, but I can reproduce this consistently by:

1. Creating and saving a new test.idr file with the following content:

   
   import Data.Vect

vectZip : Vect n a -> Vect n b -> Vect n (a, b)

2. Using `idris.addClause` on `vectZip`, generating a clause `vectZip xs ys = ?vectZip_rhs`;
3. Trying to run `idris.caseSplit` on `xs` or `ys` or trying to run `idris.proofSearch` on `?vectZip_rhs`.

When I try to case-split, I get the message "xs cannot be case-split.", even though it obviously can. Saving, closing and reopening the file makes case splitting work as expected.

From step 3, when I try a proof-search I see a message "Solving for ?vectZip_rhs..." followed by a notification "Cannot call write after a stream was destroyed". After this no other command works and reopening the file doesn't help - a VS Code restart is needed.

[ruippeixotog]

I believe the problem might be that the extension is not handling well unsaved files. If I save the file after each command I run, everything works as expected. However, commands seem to run against the version on disk rather than the one in the buffer. Here's some evidence - if I have the following saved file:

import Data.Vect

vectZip : Vect n a -> Vect n b -> Vect n (a, b)
vectZip xs ys = ?vectZip_rhs

And I try to case-split on xs, it works as expected:

import Data.Vect

vectZip : Vect n a -> Vect n b -> Vect n (a, b)
vectZip [] ys = ?vectZip_rhs_1
vectZip (x :: xs) ys = ?vectZip_rhs_2

If I try to case-split on ys in the first clause without saving first, the following occurs:

import Data.Vect

vectZip : Vect n a -> Vect n b -> Vect n (a, b)
vectZip xs [] = ?vectZip_rhs_1
vectZip xs (x :: ys) = ?vectZip_rhs_2
vectZip (x :: xs) ys = ?vectZip_rhs_2

The expectation was for ys to be simply replaced with [], but instead some strange things happened here: [] was replaced by xs in the first clause and a duplicate ?vectZip_rhs_2 was created and the last clause was left untouched.

[meraymond2]

Hey, did this turn out to be a duplicate of https://github.com/meraymond2/idris-vscode/issues/24? and if so, can I close it?

[ruippeixotog]

Yes, it did. Thanks once again @meraymond2!