[Agda] Impossible proofs about where blocks?

[Daniel Peebles]

Let's say I'm writing a proof with a goal type of:

Goal: (fromℕ
       (peanoInduction (λ {x'} _ → ℕ) 0 (λ {.x} {.m} → Nsuc)
        (toPeano (x ∷ xs)))
       | (.Data.Digit._.helper 0
          (peanoInduction (λ {x'} _ → ℕ) 0 (λ {.x} {.m} → Nsuc)
           (toPeano (x ∷ xs)))
          (peanoInduction (λ {x'} _ → ℕ) 0 (λ {.x} {.m} → Nsuc)
           (toPeano (x ∷ xs)))
  ...

Note that it will not proceed in normalizing the goal type unless I can
match on the result of the expression after the pipe. Unfortunately, said
expression lives within a where block in a module that's out of my control,
so I can't see it at all, to proceed on the proof. As far as I can
understand, assuming there aren't completely different approaches to the
proof, this makes my proof actually impossible. Am I correct?

Now, the ._.helper notation looks like the helper is secretly living inside
an anonymous module that the where block created. Given the recent change
that made datatypes into modules, would it be worthwhile or problematic to
make all value declarations with where blocks into explicit modules as well,
so that we can open them and prove things about whatever happened inside?
Would this cause problems in other ways?

Even if my suggestion isn't valid, it seems like it'd be good to have a good
answer for this kind of situation. Or is there already some solution that
I'm missing?

Thanks,
Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110615/5b8c7de4/attachment.html