[Agda] Rewriting rules in parametrized modules

[Andrej Tokarčík]

Hello,

I've got the following situation involving a rewrite rule in a
parametrized module

  module N (i : I) where
    postulate
      [_] : I → Set
      rw : [ i ] ≡ Nat
    {-# REWRITE rw #-}

    f : [ i ] → Set
    f p = {! !}

Even though a (normalized) view of the hole's context shows p to be of
type Nat, an attempt to case-split on the variable p results in
"Cannot split on argument of non-datatype [ i₁ ]". Further, if I
replace the module parameter with a postulate or variable declaration
of `i : I` inside the module, the case-splitting works, see the
attached file.

Is this expected behavior? I know there's already been some discussion
regarding the interaction of rewriting rules and parametrized rules as
evidenced by the test files Issue1563-6.agda and
RewritingRuleInParametrizedModule.agda. These however seem to deal
with rewrite rules on the level of "ground values" where this kind of
error cannot occur. I'd be therefore very grateful for any hints in
this particular direction.

I've observed this using custom builds of Agda 2.6.2-4108da6 and 2.6.1-36b9448.

Kind regards,
Andrej
-------------- next part --------------
A non-text attachment was scrubbed...
Name: rewrite-module2.agda
Type: application/octet-stream
Size: 353 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200602/734a35ea/attachment.obj>