Why does guard need the Ord typeclass in Idris?

Question

In another question (How to write a simple list-based quicksort in Idris?), I was left trying to understand why Prelude.Applicative.guard requires an Ord typeclass.

Guard is defined like this:

guard : Alternative f => Bool -> f ()
guard a = if a then pure () else empty

Looking at the Alternative interface docs (I don't actually understand how it is defined in the code yet, but I'm not very far along in learning Idris), I don't see how it requires Ord either.

Answer 1

guard alone does not need the Ord constraint, but rather (<) in your previous question. I gave there an answer to distingush between List (Ord b) and Ord b => List b.

To see why guard complains about the missing constraint, see how monad comprehensions are de-sugared.

[y | y <- xs, y < x] becomes do {y <- xs; guard (y < x); pure y}.