@jespercockx, are you fine with this change?

I am not sure if I understand the need for this flag, is it just out of principle because we do not (yet) understand it that well or do you have a concrete example of something that goes wrong? In the former case, I think it would be more in line with the Agda philosophy to have the option be enabled by default.

I am not sure if I understand the need for this flag, is it just out of principle because we do not (yet) understand it that well or do you have a concrete example of something that goes wrong?

Mainly because this kind of pattern matching seems to be less well understood. For instance, I have sketched a proof of the statement "[]-cong cannot be defined in a certain type theory", but the proof does not work if single-constructor matching is allowed. The theoretical development in the current draft of "Compiling Programs with Erased Univalence" also does not cover this kind of matching. Mishra-Linger uses the term "token type target erasure" for something similar in his PhD thesis. He argues against it, because it can lead to non-termination (if it is allowed for the equality type and code is compiled in a certain way), and I think that most of his thesis concerns a theory without it.

In the former case, I think it would be more in line with the Agda philosophy to have the option be enabled by default.

The option is enabled by default, because it is implied by --with-K. However, it is not enabled by default if you use --without-K. The --without-K variant of Agda is intended to be compatible with many things (if --safe is used), so I think it makes sense for the default to be "off" when --without-K is used.

Furthermore I went through some of my code, and only a small part of it depends on this feature. I'd rather not add --no-single-constructor-matching to hundreds of files.

I'm still confused, I was under the impression that the semantics of erasure is "it is possible to erase this argument during compilation without changing its results at run-time". If there is no example of a program that violates this principle, then I do not see a reason to disable it. But it seems you have a different semantics in mind of what you mean by "erasure", so we are not talking about the same thing. Perhaps we should make a clear design choice on what kind of erasure we exactly want to have in Agda, so we do not run in this kind of misunderstanding again in the future.

Furthermore I went through some of my code, and only a small part of it depends on this feature. I'd rather not add --no-single-constructor-matching to hundreds of files.

I don't think this is a strong argument anymore since you can add the flag to your agda-lib file. Of course, so can I, so the question is mainly what is less surprising to a "casual" user of Agda who does not necessarily know how to set up an agda-lib file.

I'm still confused, I was under the impression that the semantics of erasure is "it is possible to erase this argument during compilation without changing its results at run-time". If there is no example of a program that violates this principle, then I do not see a reason to disable it.

We have not proved that there is no such example.

But it seems you have a different semantics in mind of what you mean by "erasure"

I'm not sure what you have in mind. However, note that "it is possible to erase this argument during compilation without changing its results at run-time" is rather imprecise. For instance, do you only care about evaluation of closed terms, or also about evaluation of open terms? To take another example, Agda currently does not actually remove all erased arguments (#4193), and this does not work in strict backends. Instead erased arguments are replaced by dummy arguments. If the rules for erasure were set up differently, then one could perhaps fully erase everything. (In Mishra-Linger's theory erased arguments are removed entirely, and he proves that the erasure of a well-typed term is strongly normalising if you start with a PTS with strong normalisation.)

I don't think this is a strong argument anymore since you can add the flag to your agda-lib file. Of course, so can I, so the question is mainly what is less surprising to a "casual" user of Agda who does not necessarily know how to set up an agda-lib file.

I have a library in which I want to distinguish code that uses single-constructor matching from code which doesn't, so I can't use --single-constructor-matching in that library's .agda-lib file. People who don't care about this distinction can use --single-constructor-matching in their .agda-lib files.

I agree that it can be inconvenient to edit .agda-lib files, but if we also add --erasure, then it is not much extra work to add --single-constructor-matching when --erasure is added.

I also fail to see why erased single-constructor-matching for non-indexed data/record types should be problematic in non-cubical/non-univalent type theories, given K or not K.

1. One argument brought forward in this discussion is strictness. But if you match on something that is erased, you should not expect to be strict in it, naturally.
2. One question raised was what about open terms? Well, we don't run open terms, only closed terms.
3. I don't think that we should take Mishra-Linger's PhD thesis as foundation, as imo he does not distinguish properly irrelevance and erasure. A more solid bases is the PhD thesis of Pierre Letouzey, at least for what "erasure" as a translation from type theory to standard functional PLs should be. He does not have an erasure modality, but whatever the erasure modality is, should be compatible with this translation semantics.
4. Oskar Eriksson has formalized the erasure modality for MLTT and its soundness wrt. program extraction to an untyped language in his Master thesis. The semantics there is that closed terms of first-order base type get the same canonical form in MLTT with reduction and the untyped language with standard evaluation. The extraction does not "fully erase" but keeps dummy terms, to not run into strictness issues.
5. If erased single-constructor-matching on non-indexed data/record types is a problem in Cubical Agda, (please link to a test case that demonstrates the problem), then maybe the flag would make sense in context of --cubical-compatible (rather than --without-K).

5. If erased single-constructor-matching on non-indexed data/record types is a problem in Cubical Agda, (please link to a test case that demonstrates the problem), then maybe the flag would make sense in context of --cubical-compatible (rather than --without-K).

I don't think "no one has found a problem with this yet" is sufficient evidence for the soundness of a feature, and I think that any restrictions that apply when --cubical is used should apply also when --without-K is used (unless we actively decide to decouple these options). Furthermore I want to be able to say with confidence that some code does not use this feature, and that is easier (and easier to trust) if Agda checks this for me. @martinescardo has raised similar points in the past.

In this case I suspect that the addition of this flag would be rather undisruptive, because I suspect that most of the Agda code that uses erasure is written by me or people using agda2hs together with --without-K (perhaps that is only @jespercockx). I found few uses of single-constructor matching in my --without-K code. Basically all examples used W-types or the accessibility predicate. @jespercockx, does any of your code fail if this flag is added?

A concrete benefit of having this flag, and turning the feature off by default, is that you do not need to mention the feature at all when writing a paper about code that does not use the feature. If the feature is on by default, then an author might feel compelled to mention explicitly in a paper that the feature was turned off.

I don't think "no one has found a problem with this yet" is sufficient evidence for the soundness of a feature,

If we go by this argument, we should disable Agda's induction-recursion as well, because no one has proven it sound.
Most of Agda's features are extrapolation from theory, and we allow their use by default as long as have not found any inconsistency (and often, plus a way to fix it).
We have flags that limit Agda's capabilities, e.g. --no-pattern-matching, and I think it is fine to add more of them (e.g., I think --no-induction-recursion would be good to have) but I would not want to turn them on my default.
Why is it not good enough to be able to opt out of a feature you are suspicious of? In a paper, couldn't you list such flags in the fine-print, with links to the documentation?

In this case I suspect that the addition of this flag would be rather undisruptive, because I suspect that most of the Agda code that uses erasure is written by me or people using agda2hs together with --without-K (perhaps that is only @jespercockx). I found few uses of single-constructor matching in my --without-K code. Basically all examples used W-types or the accessibility predicate. @jespercockx, does any of your code fail if this flag is added?

I believe I do make use of the single-constructor matching feature in my experiments, but that's really all they are (experiments) and I would not mind much to roll back the addition of --erased-cubical if it turns out the theory is not yet sufficiently well understood. The main reason for me to want --erased-cubical in the first place was so that I could use the interval and path type to prove equality of streams.

I believe I do make use of the single-constructor matching feature in my experiments, but that's really all they are (experiments) and I would not mind much to roll back the addition of --erased-cubical if it turns out the theory is not yet sufficiently well understood. The main reason for me to want --erased-cubical in the first place was so that I could use the interval and path type to prove equality of streams.

"Compiling Programs with Erased Univalence" contains sketched proofs suggesting that a simplified type theory that is based on what you get with --erased-cubical "works". However, that type theory does not include single-constructor matching. If it had included it, then I would not have made this pull request.

If we go by this argument, we should disable Agda's induction-recursion as well, because no one has proven it sound.

I think it would be a good idea to make it possible to turn off induction-recursion, as well as other things. However, turning off induction-recursion would break a lot of code, so the default should perhaps be "on". Turning off single-constructor matching would presumably not break a lot of code, so then the default could be "off". Note also that if you do make use of single-constructor matching without having turned on the feature, then you get an error message like the following one:

Cannot branch on erased argument of datatype Unit because the
option --single-constructor-matching is not activated

Thus the option is easy to discover.

If a feature like this is on by default, then I suspect that it will typically be used even in developments that do not depend on the feature. In this case I did not need to update the standard library, which does not use the feature. However, if the feature had been on by default, then I would have had to turn it off in the standard library. I think we should make it easy to make reusable code, so the defaults for new features should be "off", if possible.

One other consideration: perhaps the flag should use erasure in its name to make clear that it is about matching on erased arguments.

Nisse persuaded me that this flag makes sense, since it distinguishes between different intepretations of the @0 modality.

But I also propose a name change for the flag. It should definitely refer to erasure. How about --match-on-erased?

I plan to add --erasure as well, perhaps we could use --erasure- as a prefix for this flag, to make the names more uniform. What about --erasure-single-constructor-matching? Is that name too long? The name --erasure-matching is shorter, but less precise, because even without this flag we allow "matching" when no constructors match.

I plan to add --erasure as well, perhaps we could use --erasure- as a prefix for this flag, to make the names more uniform.

In that case, should --erasure- be a prefix also of the flag currently called --erase-record-parameters? (I don't like the name --erasure-erase-record-parameters.)

I implemented --erasure.

What about --erasure-single-constructor-matching?

Language wise, --erased-single-constructor-matching would be clearer, I think.
Maybe your idea of a general --erasure prefix can be relaxed to include variants like --erase and --erased?

Otherwise, I could imagine the format --erasure:XYZ, e.g. --erasure:single-constructor-matching and --erasure:no-singleton-constructor-matching. But it is still a bit less clear with --erasure:record-parameters (because this just pins a topic, not a specific action like --erase-record-parameteres).

Maybe your idea of a general --erasure prefix can be relaxed to include variants like --erase and --erased?

Yes, we also have --erased-cubical.

Language wise, --erased-single-constructor-matching would be clearer, I think.

I don't agree: the flag does not enable matching on erased constructors, but on erased arguments. Is --erased-matching-for-single-constructor-types too long? :)

@nad can this be merged now? I've been convinced that it's probably a good idea to add the flag.

@nad can this be merged now?

I implemented this before we reverted (a698313) the change that made parameters non-erased in the types of constructors and projections (for some types). When --erasure is used the parameters should be erased (for some types).

We should also decide what the single-constructor matching flag should be called.

I implemented this before we reverted (a698313) the change that made parameters non-erased in the types of constructors and projections (for some types). When --erasure is used the parameters should be erased (for some types).

I tried to fix this.

If this pull request is merged in its current state, then --erase-record-parameters implies --erasure. However, I realised that there is also a flag --no-erase-record-parameters (which is not documented in the user manual). It seems as if --erase-record-parameters --no-erase-record-parameters is equivalent to --erasure, and I don't find this intuitive.

What is the purpose of --no-erase-record-parameters? Could this option be removed? An alternative:

• Keep (and document) --no-erase-record-parameters.
• Change --erase-record-parameters so that it no longer implies --erasure.
• Complain if --erase-record-parameters is used without --erasure.

What do you think?

There's no real purpose, I just thought it was good practice to always have a negation for each flag.

There's no real purpose, I just thought it was good practice to always have a negation for each flag.

Do you think it should be possible to turn on --erase-record-parameters in a .agda-lib file, but turn off the option in a specific Agda file using --no-erase-record-parameters? In that case we can take the alternative approach that I suggested above. I've tried to implement it (but I did not add any documentation for --no-erase-record-parameters, and I did not fix the incorrect --help text).

Language wise, --erased-single-constructor-matching would be clearer, I think.

I don't agree: the flag does not enable matching on erased constructors, but on erased arguments. Is --erased-matching-for-single-constructor-types too long? :)

The current implementation uses --erasure-single-constructor-matching. I think this name is too long. (The longest of the other options are --show-identity-substitutions and --injective-type-constructors, which have the same length as --single-constructor-matching, without the erasure- prefix.)

What about --erasure-single-constructor-matching? Is that name too long? The name --erasure-matching is shorter, but less precise, because even without this flag we allow "matching" when no constructors match.

Perhaps --erased-matches is good enough: if someone later wants to add a flag for matching on nothing in an erased position, then that flag could be called something like --erased-absurd-eliminations. I'll switch to this name.

A concrete use case for (something like) --erased-matches: Building on the work of others @andreasabel, @oskeri and I have formalised a family of type theories with support for erasure and optional support for erased matches (for Σ without η-equality, a unit type without η-equality, and an identity type). If erased matches are not allowed, then canonicity for ℕ holds for open terms in non-erased contexts, as long as all the free variables are marked as erasable and the context is consistent. However, this form of canonicity does not necessarily hold if erased matches are allowed. Here is one example:

{-# OPTIONS --safe --without-K --erasure --erased-matches #-}

open import Agda.Builtin.Nat

data Unit : Set where
  unit : Unit

block : {A : Set} → @0 Unit → A → A
block unit x = x

module _ (@0 x : Unit) where

  stuck : Nat
  stuck = block x 12