Agda considers module parameters to be flexible for interactive case splitting

[jespercockx]

Minimal example:

open import Common.Equality
module _ (A : Set₁) where
  foo : A ≡ Set → Set
  foo e = {!e!}

When case splitting on e, Agda produces foo refl = ?, which is an error. Either module parameters shouldn't be flexible, or there should be some mechanism supporting specialization of module parameters (could maybe be useful sometimes).

[andreasabel]

I notice that TC.Coverage.computeNeighbourhood gets a different "telescope before split point" delta1, depending on whether we are interactive (A : Set1 is included) or not (it is not there). So it seems we have to put interactive splitting into the right module context (it is in top context, seemingly).

[andreasabel]

The original problem is easily fixed by stripping the module parameters from the split clause:

-  (casectxt, f, clause@(Clause{ clauseTel = tel, clausePerm = perm, namedClausePats = ps })) <- findClause meta
+  (casectxt, f, cl) <- findClause meta
+  vs <- take <$> (getModuleFreeVars =<< currentModule) <*> getContextArgs
+  let clause@(Clause{ clauseTel = tel, clausePerm = perm, namedClausePats = ps }) = cl `apply` vs

However, then case splitting for extended lambda does not work anymore (too many patterns are dropped during printing). Extended Lambda has some magic which I do not really understand.
Giving up.