Jesper Cockx

Actually, Agda does modality-check meta solutions before instantiating them (see https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/MetaVars/Occurs.hs#L166 and https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/MetaVars/Occurs.hs#L196 and https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/MetaVars/Occurs.hs#L231) so calling `unify` in erased mode should also not be a problem. That just leaves...

Actually, after thinking about `unquoteTC` a bit more I don't believe that anything bad could really happen here: the only thing that `unquoteTC` would allow you to do (if it...

I've tried the approach I outlined before, adding `applyQuantityToContext zeroQuantity` to the appropriate places in the execution of TC operations. However, I've run into one more snag: with this change...

Coming back to the original issue, I guess I still don't really understand why it is not allowed to freely use the argument of an erased function type in its...

Actually apparently I made this change before and it was undone by @Saizan : https://github.com/agda/agda/commit/78b956beb5045480326a906a5949c185c5e781ab I don't really understand why it was considered to be "ad hoc" though, it feels...

> I received an answer from @Saizan via some other channel. He noted that the typing rules for erasure have been designed to ensure that definitional equality preserves erasure, and...

> I don't know if this type is fine or not, and I don't think we should allow it without some kind of supporting theory. (I imagine that the type...

> I'm not sure exactly what "definitional equality preserves erasure" (which is not a direct quote from what @Saizan wrote) refers to You are the one who used that phrasing...

After going through the paper by @Saizan @nad and @andreasabel I got convinced that in the context of cubical type theory it is indeed not desirable to allow the type...

> I think the reflection interface should allow the user to change the quantity annotation on the right, by analogy to `inContext` and `extendContext`. Ah yes, that would only require...