How to write a simple list-based quicksort in Idris?

Question

I'm just trying to do the bare minimum to translate the following Haskell to Idris (I'm not looking for efficiency or proofs of correctness):

quicksort  []           =  []
quicksort (x:xs)        =  quicksort [y | y <- xs, y<x ]
                        ++ [x]
                        ++ quicksort [y | y <- xs, y>=x]

Here's the Idris code I have, which is essentially unchanged from the Haskell except for needing to tell Idris that we are dealing with Ordered types:

quicksort: List (Ord b) -> List (Ord b)
quicksort  []           =  []
quicksort (x::xs)       =  quicksort [y | y <- xs, y<x ]
                        ++ [x]
                        ++ quicksort [y | y <- xs, y>=x]

However, I'm apparently doing this wrong. I see there is an answer in the question at Quicksort in Idris , but the form is a bit different - I'd like to understand what is wrong with the current approach. My above code gives the error:

40 | quicksort (x::xs)       =  quicksort [y | y <- xs, y<x ]
   |                            ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
When checking right hand side of quicksort with expected type
        List b

When checking an application of function Prelude.Applicative.guard:
        Can't find implementation for Ord (Ord b)

Answer 1

The problem is that Prelude.Applicative.guard (function which is used for guards in list comprehensions) can't find implementation for Ord typeclass.

That tells us, that we haven't added (or added incorrectly) typeclass constraint. If we change your code to this one, it should work:

quicksort: Ord b => List b -> List  b
quicksort  []           =  []
quicksort (x::xs)       =  quicksort [y | y <- xs, y < x ]
                        ++ [x]
                        ++ quicksort [y | y <- xs, y >= x]