Applications of the function are parsed in the body of the interface

[spcfox]

Steps to Reproduce

interface Iface where
  foo x y

Expected Behavior

Parsing error

Observed Behavior

This code produces empty interface:

Main> :doc Iface
interface Main.Iface : Type

[buzden]

foo x y may be parsed as a forward declaration of an implementation of an interface foo:

interface foo (0 a, b : Type) where

foo x y

works.

But it still seems to not to make sense in interface declarations.

Interestingly, we can have data forward declaration in interfaces, but they behave as a usual functions:

interface X (0 x, y : Type) where
  %inline
  foo x y -- ignored
  data Y : Type

X Nat Nat where
  Y = Nat

If we try to add a data declaration according to the forward declaration in the interface, we get a strange error:

failing "Missing methods in X: Y"
  X String String where
    data Y : Type where
      MkY : Y

But if we add another declaration for Y, we can see that "missing methods" checks earlier than "can only contain definitions":

failing "Implementation body can only contain definitions"
  X String String where
    Y = Nat
    data Y : Type where
      MkY : Y