Idris2: Nested WITH clause

Question

My Code

My piece of code, i.e.:

equal_suffix: Eq a => List a -> List a -> List a
equal_suffix u v with (snocList u)
    equal_suffix _ _ | Empty = []
    equal_suffix _ v | (Snoc x xs snx) with (snocList v)
        equal_suffix _ _ | (Snoc x xs snx) | Empty = []
        equal_suffix _ _ | (Snoc x xs snx) | (Snoc y ys sny) = case x == y of
            False => []
            True => (equal_suffix xs ys | snx | sny) ++ [x]

does not type check, with compile yelling:

Error: With clause does not match parent

Hello:857:25--857:38
 853 | 
 854 | equal_suffix: Eq a => List a -> List a -> List a
 855 | equal_suffix u v with (snocList u)
 856 |     equal_suffix _ _ | Empty = []
 857 |     equal_suffix _ v | (Snoc x xs snx) with (snocList v)
                               ^^^^^^^^^^^^^

My Question(s)

My first question is:

What does parent mean for a with clause in the context of Idris (Idris2 to be specific)? (Edit1: Thanks to @joel I now understand)

And if the first question can't help me understand this:

What is the problem with my code? (Edit1: Original Final Question)

What is the correct syntax of using nested with clause in Idris(2)? (Edit1: A More Focused Question thanks to the reminder from the comment @Vega)

(Excuse my snake-cased Pythonic mind for the naming of the variables :D)

Edit1 (2022-05-09): The question was closed because the original last question is not focused enough. I adjust my question hopefully to reopen this as I am still in trouble with the with clause still.

What I have tried

To add more details, I did try the @joel version myself independently, i.e., to only case-split after specifying all with statement:

func: input_type -> output_type
func input with (view1 input)
    func input | input_in_view1 with (view2 input)
        func input | input_in_view1 | input_in_view2 = ...

I also tried to make a tuple of the two views, i.e.,

func: input_type -> output_type
func input with (view1 input, view2 input)
    func input | (input_in_view1, input_in_view2) = ...

However, these two do not seem to work (the first leads to an unsolved hole error and the second non-covering error or non terminating type checking depending on how I case-split) .

Example from TDD by Edwin

This equal_suffix exercise is from TDD by Edwin. I was still stuck and stopped at exactly this exercise.

Here is an example in the book which I copy as follows:

isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (snocList input1)
    isSuffix [] input2 | Empty = True
    isSuffix (xs ++ [x]) input2 | (Snoc rec) with (snocList input2)
        isSuffix (xs ++ [x]) [] | (Snoc rec) | Empty = False
        isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc rec) | (Snoc z) 
            = if x == y then isSuffix xs ys | xsrec | ysrec
                else False

where snocList is redefined in the book for educational purpose and rec might be just a typo of xsrec and ysrec respectively.

Recursing on with clause directly for the totality.

I did manage to make it work when changing the recursive call equal_suffix xs ys | snx | sny to equal_suffix xs ys

However, according to the book P275, to make a totally defined function, we need to recurse on the with clause directly to tell compiler about the relation between the recursive calls, so I want the function to be defined by directly calling the with clause recursively.

Answer 1

Simplest fix: remove | sny in your final line. Apparently it's not needed.

"Parent" presumably means parent function call in the recursive loop.

Now as to why it doesn't compile with | sny ... my guess is your second view is only present in one branch of your pattern match, whereas it needs to be present in both if you're going to pass sny recursively in equal_suffix xs ys | snx | sny.

You might be able to get something like this to work

equal_suffix: Eq a => List a -> List a -> List a
equal_suffix u v with (snocList u)
  equal_suffix u v | su with (snocList v)
    equal_suffix [] _ | Empty | _ = []
    equal_suffix _ [] | _ | Empty = []
    equal_suffix (xs ++ [x]) (ys ++ [y]) | (Snoc x xs snx) | (Snoc y ys sny) =
      case x == y of
        False => []
        True => (equal_suffix xs ys | snx | sny) ++ [x]

but this particular example fails to compile with unsolved holes.