Case in do block produces bad code

[dunhamsteve]

On discord, a user reported a case where the compiler was producing scheme code that wouldn't compile. I've reduced the test case below. It appears that an internal pattern variable pat0:0 is being referenced.

Steps to Reproduce

Attempt to compile this with the scheme backend:

import Data.Vect
foo : Maybe Int
foo = do
    y <- pure 0
    if y == 0 then do
        [x] : Vect _ Int <- sequence [pure 0]
        Just x
      else Nothing   
main : IO ()
main = printLn foo

Expected Behavior

Compilation succeeds

Observed Behavior

Exception: attempt to reference unbound identifier pat0C-58-0 at line 664, char 1948 of /Users/dunham/prj/idris/scratch/build/exec/mini_app/mini.ss
Error: INTERNAL ERROR: Chez exited with return code 255

The scheme code and the case tree contain a reference to a pat0::0 variable, which is not in scope. This should be e:2. If a 1 is filled in for the _, then correct code is generated. In that case, the only change in the case tree is {e:2} in place of `({pat0::0} [])

import Data.Vect
foo : Maybe Int
foo = do
    y <- pure 0
    if y == 0 then do
        [x] : Vect 1 Int <- sequence [pure 0]
        Just x
      else Nothing   
main : IO ()
main = printLn foo

Correct code is also generated if the outer if then else is removed.

[dunhamsteve]

This seems to reproduce it too:

import Data.Vect
foo : Maybe Int
foo = let xx = [0] in
      case the (Vect _ Int) xx of [x] => Just x   
main : IO ()
main = printLn foo

[dunhamsteve]

I think whats going on is that we've got a Guess on the left hand side, with a pattern variable buried inside of it:

broken:

LOG compile.casetree:5: simpleCase: Clauses:
  (Main.case block in foo [__]@{pat0::1} ?Main.{postpone:4542}_[]) = (Prelude.Types.Just Int {pat0::0})

vs working:

LOG compile.casetree:5: simpleCase: Clauses:
  (Main.case block in foo [__]@{pat0::1} (Data.Vect.(::) Prelude.Types.Z Int {pat0::0} (Data.Vect.Nil Int))) = (Prelude.Types.Just Int {pat0::0})

So x becomes pat0::0 on both sides in the working case, but the x in the LHS is hiding in a postpone in the broken case. Eventually the thing we want on the left gets dotted.