Trying to use linear name in non-linear context.

[po-stulate]

Steps to Reproduce

Forward declarations for Foo and Bar.

module A

namespace Foo
  public export data Foo : (a : Type) -> Type
namespace Bar
  public export data Bar : (a : Type) -> Type

Define Foo and Bar.

module A.Foo

import public A

public export
interface Foo (a : Type) where
  constructor MkFoo

module A.Bar

import public A

public export
interface Bar (a : Type) where
  constructor MkBar

This gives error:

module B

import public A.Foo
import public A.Bar

f : Type -> ()
f (Foo _) = ()
f (Bar _) = ()
f _       = ()

Expected Behavior

typecheck

Observed Behavior

In module B:

While processing left hand side of f. Trying to use linear name A.Bar.Bar in non-linear context.

Test/src/B.idr:8:4--8:9
   |
 8 | f (Bar _) = ()
   |    ^^^^^

Same error for data and record (instead of interface).

However, it typechecks if: Foo and Bar were in a same module or function f was defined in any submodule of A

Interestingly, if f was in module B.A, Bar is fine and Foo gives error, while if f is in module B (like the above example), Foo is fine and Bar gives error instead.

[po-stulate]

For people who also have this problem, at the moment import forward declarations instead of import public do the trick for me.