Can't find implementation of Ord a

[williamdemeo]

I am new to Idris, so forgive me if this a dumb question.

When doing Exercise 5 on page 101 of the TypeDD book, my solution (which is the same as the suggested solution in this repository) exhibits the following behavior when I launch idris ex_4_1.idr:

Type checking ./ex_4_1.idr
*ex_4_1> maxMaybe Nothing Nothing
Can't find implementation for Ord a

According to the definition of maxMaybe (included below for reference), it seems the answer should be Nothing. Is this an error? Do I not have Idris set up correctly?

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing Nothing = Nothing
maxMaybe Nothing (Just y) = Just y
maxMaybe (Just x) Nothing = Just x
maxMaybe (Just x) (Just y) = Just (max x y)

[edwinb]

This is because at the REPL Idris doesn't know what type the 'Maybe' contains, since you haven't explicitly specified. It won't, in general, infer a type - in programs you have to give top level types - but it does make a best effort at the REPL.

(Sorry to be slow, I haven't been paying attention to this repo... probably a better place to ask for a quicker response is the idris mailing list)