[Agda] Pie in the sky

[Benja Fallenstein]

Hi all,

I wrote:

> Hmm, I never thought about it precisely this way, but are Haskell type
> classes without undecidable instances = Horn clauses with a simple
> termination checker?

No, of course not, silly me. Haskell ensures that it will find only
one instance; Horn clauses don't ensure that there can be only one
derivation of a proposition, of course. I.e., there is nothing wrong
with writing,

uncle(X,Z) :- father(X,Y), brother(Y,Z).
uncle(X,Z) :- mother(X,Y), brother(Y,Z).

But Haskell without extensions wouldn't accept

instance Monad m => MyClass (Foo m) where
instance Functor f => MyClass (Foo f) where

Something like the latter behavior seems like a more reasonable
starting point for Agda, perhaps, so that it's easy to ensure not more
than one instance can be found...

- Benja