I was investigating down the path suggested by Ahmad and Edwin in issue #4279. After a few tries, it looks like Superclass default implementation behaviour is weird when you use parametric types:

# Steps to reproduce

Try to compile the following file:

```Idris
module Main

import Data.Vect

interface Enumerated (t : Type) (len : Nat) | t where
toFin : t -> Fin len

data FooBar = Foo

implementation Enumerated FooBar 1 where
toFin Foo = FZ

interface (Eq t, Ord t) => EnumeratedDerivation t (len : Nat) | t where
implementation Eq t where
x == y = myFin x == myFin y
implementation Ord t where
compare x y = compare (myFin x) (myFin y)
x > y = (myFin x) > (myFin y)
x < y = (myFin x) < (myFin y)
x >= y = (myFin x) >= (myFin y)
x <= y = (myFin x) <= (myFin y)

myFin : t -> Fin len

{- This one works:
implementation EnumeratedDerivation FooBar 1 where
myFin = toFin
-}

-- This one fails
implementation Enumerated t len => EnumeratedDerivation t len where
myFin = toFin
```

# Observed behavior

```
34 | implementation Enumerated t len => EnumeratedDerivation t len where
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of Main.t, len implementation of Main.EnumeratedDerivation with expected type
EnumeratedDerivation t len

Can't find implementation for Ord t
```

# Expected behavior

I think it should compile, but anyhow, it shouldn't claim that the superinterface implementation can't be found while we can provide a default implementation.