Case-split on a datatype defined in a parametrised module produces needlessly-prefixed patterns

[gallais]

When case-splitting on x in B.agda, we get the pattern (;A.A⁺.a x) which is a parse error rather the completely valid (a x).

A.agda:

open import Level

module A {l : Level} (A : Set l) where

data A⁺ : Set l where a : A → A⁺

B.agda:

module B where

open import Agda.Builtin.Nat
open import A Nat

swap : A⁺ → A⁺
swap x = {!!}

Note that if we inline A.agda as a parametrised module defined in B.agda then everything is fine!

[gallais]

Here is my current understanding of the situation:

• A⁺ is B._.A⁺ Nat internally
• B._.A⁺ gets reverse-looked up to A.A⁺ internally
• case splitting works on A.A⁺
• it generates the potential pattern A.A⁺.a
• inverse lookup of A.A⁺.a fails to find a (or even A⁺.a) because they are not actually equivalent
• Agda gives up and returns the out of scope identifier

[jespercockx]

After the fix of #4037 (https://github.com/agda/agda/commit/3d0dc0b2c3a7933a2e4986d9a073fbde385c2ecd) you now get an error message:

Cannot split because Issue3209a.A⁺.a is not in scope
when checking that the expression ? has type A⁺

Not much better than before...

[gallais]

It's actually worse than before: with a simple search and replace it was possible to drop the prefix & get code that works. Now the interactive machinery will not even split on the value, forcing you to guess what the cover actually is!

[jespercockx]

That's true :/ I took a look at this issue but I have no idea how to fix it. If it remains unfixed for the release perhaps it's better to revert the fix of #4037 for now.

[gallais]

modified example:

{-# OPTIONS -vscope.inverse:100 #-}

module B where

open import Agda.Builtin.Nat
open import A Nat as ANat

swap : A⁺ → A⁺
swap x = ? -- C-c C-c x RET

inverse looking up abstract name A.A⁺.a yields []

suggests to me that we ought to add inverse scope lookups from old.a to new.a when we trigger a copyScope old new.

[EdNutting]

This has been causing me headaches for a while. Most of my modules are parameterised - I thought I'd been using the case split incorrectly somehow.

Would much appreciate a fix as stripping the prefixes from big case splits can take a lot of time and really confuse me (especially if implicit record parameters get and deconstructed, with a zillion long prefixes to remove).

[gallais]

stripping the prefixes from big case splits can take a lot of time

With search & replace it's not too bad. But it would indeed be nice to get a fix.

[EdNutting]

Does this also affect "Helper function" (C-c C-h)? It can be even more frustrating to try to figure out what's happened to the helper function definition as all the module parameters can get in the way of a simple find-replace (edit: especially as sometimes it puts in _ for module parameters and sometimes it fills them out in-full - meaning there can be dozens of different cases to find-replace!)

[lclem]

I also stumbled into this and it is quite frustrating

[xekoukou]

Maybe related.

module test where

module QBree (A : Set) where

  data Bree : Set where
    _∪_ : Bree → Bree → Bree

  data S : Bree → Bree → Set where
    assoc   : (x y z : Bree) → S (x ∪ (y ∪ z)) ((x ∪ y) ∪ z)

module _ W Q where

  module WMB = QBree W
  module QMB = QBree Q

  l12 : (a b : WMB.Bree) → WMB.S a b → Set
  l12 a b r = {!!} -- C-c C-c r Ret

[andreasabel]

Since this issue has been open for >5 years and may not be fixed, maybe we could instead change the interaction for case-splitting:

1. When you case split C-c C-c, you get in a buffer the candidate text for the new clause(s) displayed.
2. You can edit around in this buffer, and then press C-c C-c again to commit the text, which then replaces the old clause in your main window and triggers a reload.

The advantage here would be that if Agda produces an ugly result, you may decide to abort the split, and not lose your proof state (no reload needed). And, even if you want to finally commit to the case split, by editing it first there is only a single reload, not two reloads (one failing one before editing the produced clauses, one after).