Extending interfaces with dependent types

[YanaTes]

Steps to Reproduce

import Data.Vect

interface MyInterface (t : {n : Nat} ->  Vect n Nat -> Type) where
  myFunction : {n : Nat} -> {k : Nat} -> {v1 : Vect n Nat} -> {v2 : Vect k Nat} ->
               t v1 -> t v2 -> t (v1 ++ v2)

interface MyInterface t => MyExtendedInterface (t : {n : Nat} -> Vect n Nat -> Type) where
  myId : {n : Nat} -> {v1 : Vect n Nat} -> t v1 -> t v1

Expected Behavior

Extending the interface.

Observed Behavior

Error: While processing type of Constraint (MyInterface t). 
Can't solve constraint between: ?type_of_t [no locals in scope] and Vect n Nat -> Type.

ExtendInterface.idr:8:1--8:91
   |
 8 | interface MyInterface t => MyExtendedInterface (t : {n : Nat} -> Vect n Nat -> Type) where
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[ohad]

Nice find!

I think it's an issue with implicit arguments rather than dependent types, since the following type-checks fine:

import Data.Vect

interface MyInterface (t : (n : Nat) ->  Vect n Nat -> Type) where
  myFunction : {n : Nat} -> {k : Nat} -> {v1 : Vect n Nat} -> {v2 : Vect k Nat} ->
               t n v1 -> t k v2 -> t (n + k) (v1 ++ v2)

interface MyInterface t => MyExtendedInterface (t : (n : Nat) -> Vect n Nat -> Type) where
  myId : {n : Nat} -> {v1 : Vect n Nat} -> t n v1 -> t n v1

It looks like implicit arguments don't play nice with interfaces at the moment, for example:

interface MyInterface (0 t : {n : Nat} -> Type) where
  myConstant : t {n = Z} 

gives:

Errors (1)
 `-- line 2 col 2:
     While processing left hand side of myConstant. Can't solve constraint between: ?t and ?_.

[gallais]

I believe @ohad is correct and it's the same issue as #660, albeit in a slightly different context (interface declarations get elaborated to datatype declarations).