Not a splittable variable

[andreasabel]

data S : Set where
  c : S

module _ (A : Set) where
  test : S
  test with c
  ... | q = {!q!}

reports

Not a (splittable) variable: q
when checking that the expression ? has type q

The reported type looks also fishy. De Bruijn mess with module parameters?

Works fine with agda-2.5.1.1.

[andreasabel]

In the debug output I get

Coverage checking Bug-Splittable._.with-14
  tel  = (w : S) (A : Set)

Thus, the with-variable preceeds the module parameters. The calculation which variables are interactively splittable (because not module parameters) should be more complicated now, as the module parameters can be shuffled arbitrarily into the argument vector by the with-abstraction.

[andreasabel]

@UlfNorell: where does a function store which of its arguments are module parameters?
I pass this to you...

[UlfNorell]

Hm, that didn't quite do it:

module _ (n : Nat) where

  foo : (m : Nat) → n ≡ m → Nat
  foo m refl = {!m!} -- not a splittable var: m

In this case the value of the module parameter is m so my fix gets confused.

[UlfNorell]

Actually, that's not the problem. The problem is that the m has been refined to a dot pattern and so is not available for splitting. This is no longer a regression wrt to 2.5.1 so I'll remove that label.

[UlfNorell]

Fixing this would require a bit of work. I'll close this issue and add a fresh one for this feature.