Can't figure out parse error

[Kim Stebel]

To get my feet wet with Idris, I translated a simple queue implementation from Haskell to Idris. I thought the changes should be minimal, but Idris version 0.9.2.1 tells me there is a "parse error at column 9" in line 10 of this:

module Queue

data Queue a = mkQueue [a] [a]
 
enqueue : Queue a -> a -> Queue a
enqueue (mkQueue front back) element = mkQueue (element :: front) back

dequeue : Queue a -> (Queue a, a)
dequeue (mkQueue front (b :: back)) = (mkQueue front back, b)
dequeue (mkQueue front []) = (mkQueue [] revFrontTail, revFrontHead) where -- this is where the parse error occurs
  (revFrontHead :: revFrontTail) = reverse front

More helpfull error messages would really be great.

[Cezar Ionescu]

This has tripped me too. "where" clauses don't work like in Haskell,
they require a type declaration (page 7 of the tutorial) and you don't
get pattern matching assignments. Use a "let binding" instead (page 14
of the tutorial), i.e.

dequeue (mkQueue front Nil) =
let (revFrontHead :: revFrontTail) = reverse front in
(mkQueue Nil revFrontTail, revFrontHead)

Best,
Cezar.