Auto-force not working properly in with blocks

[nmccarty]

Using a nested with block to inspect the next step of a lazy recursive view, such as String's AsList, does not currently compile without manually forcing the value

Steps to Reproduce

Consider the following function that inspects two characters from a string at a time

doubleLetter : String -> Bool
doubleLetter str with (asList str)
  doubleLetter "" | [] = False
  doubleLetter (strCons c str) | (c :: x) with (x)
    doubleLetter (strCons c "") | (c :: x) | [] = False
    doubleLetter (strCons c (strCons d str)) | (c :: x) | (d :: y) = 
      if c == d
        then True
        else doubleLetter (strCons d str) | x

Expected Behavior

This function should either compile and work, or at least fail with a less confusing error message.

Observed Behavior

This function fails to compile, unless you replace the (x) in the inner with block with (force x), with the following error message:

 -- src/Years/Y2015/Day5.md line 72 col 14:
     While processing right hand side of with block in with block in doubleLetter. d is not accessible in
     this context.
     
     Years.Y2015.Day5:72:15--72:16
      68 |   doubleLetter "" | [] = False
      69 |   doubleLetter (strCons c str) | (c :: x) with (x)
      70 |     doubleLetter (strCons c "") | (c :: x) | [] = False
      71 |     doubleLetter (strCons c (strCons d str)) | (c :: x) | (d :: y) = 
      72 |       if c == d

[buzden]

Is this problem the same as #557?

I think I'm wrong in mentioning the other issue.

Minimised current example:

import Data.String

doubleLetter : String -> Bool
doubleLetter str with (asList str)
  doubleLetter "" | [] = False
  doubleLetter _  | (c :: []) = False
  doubleLetter _  | (c :: cs@(d :: _)) =
    if c == d
      then True
      else doubleLetter _ | cs

If we define out alternative AsList without laziness, we don't have this issue:

import Data.String

data AsList' : String -> Type where
  Nil  : AsList' ""
  (::) : (c : Char) -> {str : String} -> AsList' str -> AsList' (strCons c str)

asList' : (str : String) -> AsList' str
asList' str with (strM str)
  asList' "" | StrNil = []
  asList' str@(strCons x xs) | StrCons _ _ = x :: asList' (assert_smaller str xs)

doubleLetter : String -> Bool
doubleLetter str with (asList' str)
  doubleLetter "" | [] = False
  doubleLetter _  | (c :: []) = False
  doubleLetter _  | (c :: cs@(d :: _)) =
    if c == d
      then True
      else doubleLetter _ | cs

[buzden]

At the same time, the original code snippet may show some troubles with the termination checker, since if you try to use strCons instead of _ on the LHS of with-clauses, compiler starts to complain as if the function is non-covering