"Linearity checking failed (`Type` not a function type)" due to a `data` declaration being tagged as linear

[elkcl]

Trying to compile this code:

module LinearBug
%default total

data X : (() -> Type) -> Type where
  MkX : f () -> X f

data Y : X f -> Type where
  MkY : () -> Y (MkX a)

fails with the following error:

Error: While processing constructor MkY. Linearity checking failed on {f:849}[0] (Type not a function type)

Inspecting the types in the REPL shows that Y gets tagged as linear for some reason:

1 LinearBug.Y : {0 f : () -> Type} -> X f -> Type

The issue disappears if f is passed explicitly in the return type:

MkY : () -> Y {f} (MkX a)

Also, both MkY and f taking some kind of argument seems to be important for triggering the bug. If you define MkY as just:

MkY : Y (MkX a)

or define X as:

data X : Type -> Type where
  MkX : f -> X f

then the bug goes away too.

Tested on Idris version 0.8.0-37d29157a