Can't apply erased arguments to kinds imported from parametrized module

[ionathanch]

Suppose I had a file with the following:

module P (T: ★) {t: T}.
U : ★ = T.
𝒌 = ★.

In a different file where I import this, I can't apply a second argument to 𝒌. If I try to make it erased, there's a parse error, and if I don't mark it as erased (which I think is the correct option), there's a "Mismatched argument erasure" error.

import P.
module Q (T: ★) (t: T).
U' : ★ = U ·T t. -- works fine
𝒌' = 𝒌 ·T -t     -- doesn't work
𝒌'' = 𝒌 ·T t     -- doesn't work either

I know I can import a module applied to arguments after the file's module declaration to avoid this error, but my current use-case looks something more like this:

import P.
module Q (T: ★) {t: T} (R: 𝒌 ·T t) {u: U ·T t}

[ionathanch]

Out of curiosity I went to find where the error was coming from and it looks like it's here: https://github.com/cedille/cedille/blob/master/src/classify.agda#L736 I think since types effectively ignore whether an erased parameter argument is applied as erased or not (well, you can't apply erased arguments to types at all I suppose), so should kinds...