Agda: Implicit arguments hard to find in interface

[GavinMendelGleason]

Sometimes during pattern matching with a number of constructors, it becomes very difficult to know the source of a given implicit variable in order to make it explicit so that it can be referred to.

Currently if it is possible to pattern match on the variable, one can use C-c C-c to case split and then manually unsplit to use the variable, but if it is not possible there appears to be no way to find the source other than guessing based on Agda's algorithm for changing variable names which is time consuming.

Would it be possible to introduce a command that would take an implicit argument in the hole and introduce it explicitly on the lhs?

[andreasabel]

Thanks for reporting! Can you please add a concrete case with

• a short example and
• the envisioned behavior of the new command for this example.

Thanks!

[GavinMendelGleason]

A completely contrived example which hopefully conveys the underlying feature request:

module FeatureExample where

infix 30 _≡_ 
data _≡_ {A : Set} : A → A → Set where
  refl : {x : A} → x ≡ x

data List (A : Set) : Set where
  [] : List A
  ∷ : {x : A} → {xs : List A} → List A

_++_ : ∀ {A : Set} → List A → List A → List A
[] ++ ys = ys
_++_ {A} (∷ {x} {xs}) ys = ∷ {A} {x} {xs ++ ys}

++-comm : ∀ {A : Set} (xs ys zs : List A) → (xs ++ (ys ++ zs)) ≡ ((xs ++ ys) ++ zs)
++-comm [] ys zs = refl
++-comm ∷ [] zs = {!!}
++-comm ∷ ∷ [] = {!!}
++-comm ∷ ∷ ∷ = {! .x₂ !}  

In the final hole we have the following goal:

Goal: ∷ ≡ ∷
—————————————————————————
.xs₂ : List .A
.x₂  : .A
.xs₁ : List .A
.x₁  : .A
.xs  : List .A
.x   : .A
.A   : Set

It's not so clear which constructor to augment to make a given implicit parameter, explicit, in order to refer to it.

Some Key sequence (C-c C-j ?) could potentially take the implicit parameter in the hole and transform it to:

++-comm : ∀ {A : Set} (xs ys zs : List A) → (xs ++ (ys ++ zs)) ≡ ((xs ++ ys) ++ zs)
++-comm [] ys zs = refl
++-comm ∷ [] zs = {!!}
++-comm ∷ ∷ [] = {!!}
++-comm ∷ ∷ (∷ {_} {x₂}) = {! !} 

[andreasabel]

Thanks. A possibility would be to modify the case split command C-c C-c to not split on a hidden variable, but to bring it into scope. Then, one can split on it on a second invokation of C-c C-c. Seems more economic: the user has to remember less commands.

[andreasabel]

Thanks to @jespercockx 5e71c3d6bb10cfa43d464ca21e58523645f17e96, this was straightforward to implement.
@GavinMendelGleason , does this suit your needs?