agda
agda copied to clipboard
agda
Denial of case split in the presence of known values
- Agda version: 2.7.0.1
- Emacs verion: GNU Emacs 30.1
Reproduction:
data Bool : Set where
true false : Bool
data Dep : Bool → Set where
t : Dep true
f : Dep false
rep : (b : Bool) → Dep b → Bool
rep b t = {!!}
rep b f = {!!}
Performing a case split on b in either hole (C-c C-c b RET) produces the following error:
Cannot split on variable b, because it is bound to true
when checking that the expression ? has type Bool
It seems logical that if the value is known, this split should be performable.
Internally for Agda, the case split has "already happened" so there is no variable in the context anymore to case split on. Basically, Agda treats the variable b as a let-bound variable, and you wouldn't expect to be able to case split on those either.
However, it should be possible in theory to add a special case to the case split command so it simply inlines the value of a variable in case it's already instantiated. In that case we should check whether the value is a constructor or a variable (which can be inlined as-is) or anything else (which should be turned into a dot pattern).
Didn't the UI use to do that automatically? I seem to remember it did. [I mean when a variable is let bound, it got automatically changed into that value, as a dot pattern]. That was nice.
Didn't the UI use to do that automatically? I seem to remember it did. [I mean when a variable is let bound, it got automatically changed into that value, as a dot pattern]. That was nice.
That is because of the --keep-pattern-variables option which is now enabled by default (since https://github.com/agda/agda/commit/3a26f073df0f9ce69ac0a88b15a8a181c52d2f4f). The reasoning being that nowadays you can see the values of instantiated variables in the context, and dot patterns appearing by themselves were often considered confusing by newcomers. You can revert to the old behavior with --no-keep-pattern-variables.
Ah thanks. I'll definitely use --no-keep-pattern-variables when live coding PLFA. Having to do this "by hand" was a major pain.
Thank you, that reasoning makes sense. I agree that that special case would be quite useful - in fact, I initially noted this working through some programming language formalisation, where there would arise a binding like f = lam body.
If one needed to explicitly reference body for some reason, you'd have to go modify the case for f manually, as body isn't in scope, but case splitting did nothing. Thanks!
Found the "cannot split" error too. Thanks for the --no-keep-pattern-variables hint.
(On the other hand, --keep-pattern-variables does seem like a better default option because dot pattern does not represent constructor arguments well.)
@jake-87 wrote:
Performing a case split on
bin either hole (C-c C-c b RET) produces the following error...
Wouldn't a better behavior be that you get the dot pattern in this case?
You are asking Agda for the possible forms of b, so Agda should comply and show it, even if there is only one and it does not change the split tree.
@jake-87 wrote:
Performing a case split on
bin either hole (C-c C-c b RET) produces the following error...Wouldn't a better behavior be that you get the dot pattern in this case? You are asking Agda for the possible forms of
b, so Agda should comply and show it, even if there is only one and it does not change the split tree.
Apologies for the slightly bad wording; that is indeed what I would consider the desired behaviour.