You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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}
The text was updated successfully, but these errors were encountered:
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...
Suppose I had a file with the following:
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.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:
The text was updated successfully, but these errors were encountered: