Idris function to construct empty `List a` where `a` is bound to an instance of `Ord`?

Question

I've only read the standard tutorial and fumbled around a bit, so I may be missing something simple.

If this isn't possible in Idris, please explain why. Furthermore, if can be done in another language please provide a code sample and explain what's different about that language's type system that makes it possible.

Here's my approach. Problems first arise in the third section.

Create an empty list of a known type

 v : List Nat
 v = []

This compiles and manifests in the REPL as [] : List Nat. Excellent.

Generalize to any provided type

 emptyList : (t : Type) -> List t
 emptyList t = []

 v' : List Nat
 v' = emptyList Nat

Unsurprisingly, this works and v' == v.

Constrain type to instances of Ord class

emptyListOfOrds : Ord t => (t : Type) -> List t
emptyListOfOrds t = []

v'' : List Nat
v'' = emptyListOfOrds Nat     -- !!! typecheck failure

The last line fails with this error:

When elaborating right hand side of v'':
Can't resolve type class Ord t

Nat is an instance of Ord, so what's the problem? I tried replacing the Nats in v'' with Bool (not an instance of Ord), but there was no change in the error.

Another angle...

Does making Ord t an explicit parameter satisfy the type checker? Apparently not, but even if it did requiring the caller to pass redundant information isn't ideal.

 emptyListOfOrds' : Ord t -> (t : Type) -> List t
 emptyListOfOrds' a b = []

 v''' : List Nat
 v''' = emptyListOfOrds (Ord Nat) Nat     -- !!! typecheck failure

The error is more elaborate this time:

 When elaborating right hand side of v''':
 When elaborating an application of function stackoverflow.emptyListOfOrds':
         Can't unify
                 Type
         with
                 Ord t

         Specifically:
                 Can't unify
                         Type
                 with
                         Ord t

I'm probably missing some key insights about how values are checked against type declarations.

Answer 1

As other answers have explained, this is about how and where the variable t is bound. That is, when you write:

emptyListOfOrds : Ord t => (t : Type) -> List t

The elaborator will see that 't' is unbound at the point it is used in Ord t and so bind it implicitly:

emptyListOfOrds : {t : Type} -> Ord t => (t : Type) -> List t

So what you'd really like to say is something a bit like:

emptyListOfOrds : (t : Type) -> Ord t => List t

Which would bind the t before the type class constraint, and therefore it's in scope when Ord t appears. Unfortunately, this syntax isn't supported. I see no reason why this syntax shouldn't be supported but, currently, it isn't.

You can still implement what you want, but it's ugly, I'm afraid:

Since classes are first class, you can give them as ordinary arguments:

emptyListOfOrds : (t : type) -> Ord t -> List t

Then you can use the special syntax %instance to search for the default instance when you call emptyListOfOrds:

v'' = emptyListOfOrds Nat %instance

Of course, you don't really want to do this at every call site, so you can use a default implicit argument to invoke the search procedure for you:

emptyListOfOrds : (t : Type) -> {default %instance x : Ord t} -> List t
v'' = emptyListOfOrds Nat

The default val x : T syntax will fill in the implicit argument x with the default value val if no other value is explicitly given. Giving %instance as the default then is pretty much identical to what happens with class constraints, and actually we could probably change the implementation of the Foo x => syntax to do exactly this... I think the only reason I didn't is that default arguments didn't exist yet when I implemented type classes at first.