[Agda] Possible bug

[Chris Eidhof]

Hey everyone,

This morning, we were experimenting with Agda, and we think we might  
have found a possible bug. Hopefully this is not a bug, but then I am  
very interested in the explanation of this behavior. This is our  
program:

> module Test where
>
> open import Data.String
> open import Data.Bool
> open import Data.List
>
> test : String -> Bool
> test xs with toList xs
> ... | [] = false
> ... | ys = true

If we now evaluate 'test ""' it return false, but 'test "hi"' also  
returns false. I would expect the last case to return true. If we  
replace the ys by (y ∷ ys) it does work.

Thanks!

-chris