If this issue has already been opened before, please forgive me. I have not found any while searching through the issues here.
I have been reading quite a lot through the docs of Agda (version 2.6.2.2), up until irrelevance.
As far as I understand, there are 2 kinds of irrelevance:
@0 or @erased modalities.Run-time irrelevance means that data will not actually be part of the generated source code (it has been erased during compilation).
However, compile-time irrelevance isn't really clear whether it is supposed to be erased or not. From the docs, I gathered that this is not the case: a dotted value will be typechecked but not normalised by the typechecker, as stated multiple times throughout the docs:
The general rule is that anything prepended by a dot (.) is marked irrelevant, which means that it will only be typechecked but never evaluated.
However, while playing with the FFI, I actually discovered that compile-time irrelevant constructor arguments are in fact erased.
See this short Agda file:
open import Agda.Builtin.Unit
{-# FOREIGN GHC data X = X () () #-}
data X : Set where
X′ : ⊤ → .⊤ → X
{-# COMPILE GHC X = data X (X) #-}
Upon compiling with the GHC backend, I get the following Haskell code:
data X = X () ()
-- Test.X
d_X_2 = ()
type T_X_2 = X
pattern C_X'8242'_4 a0 = X a0
check_X'8242'_4 ::
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 -> T_X_2
check_X'8242'_4 = X
cover_X_2 :: X -> ()
cover_X_2 x
= case x of
X _ -> ()
which will fail to compile due to a missing unit argument in the type of check_X'8242'_4 as well as a missing wildcard in the pattern matching for cover_X_2 (which is the compile-time irrelevant one).
Are compile-time irrelevant constructor arguments meant to be erased (as if they were run-time irrelevant)? Is it also true when the corresponding data type has a COMPILE pragma?
If yes, maybe Agda could yield either a warning or an error for this case?
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4