Default interface resolution with parametric types is odd

[berewt]

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:

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.