[Ur] MY_ORD = resolving eq class instance / functor?

[Adam Chlipala]

Marc Weber wrote:
> structure My_Ord : MY_ORD = struct
>    class strict_less a = a ->  a ->  bool
>    fun lt [a] (f: strict_less a) (x:a) (y:a) = f x y
>    (* causing Can't resolve type class instance
>       Class constraint:  Basis.eq a
>    *)
>    fun le [a] (f: strict_less a) (x:a) (y:a) = f x y || x = y
> end
>
> The le implementation does not know which eq implementation to use ?
>    

Perhaps it would be useful for you to review the concept of type classes 
in Haskell.  They are very similar in Ur.

In your code above, nowhere have you declared that type [a] belongs to 
class [eq], so of course you are not allowed to use [=] on [a] values.

Two solutions that come to mind:
1) Add an [eq a] argument to [le].
2) Extend the definition of [strict_less a] to contain an [eq a], too.  
(Though this seems to create some dissonance with the words "strict less"!)