[Agda] Questions regarding non-constructor indexed datatypes

[Nils Anders Danielsson]

On Sun, Oct 12, 2008 at 18:19, Shin-Cheng Mu <scm at iis.sinica.edu.tw> wrote:
>
> Question 1: I guess the problem is that Agda tries to unify
>  i + j with suc k.

Yes, this unification problem does not have a unique solution (unless
more is known about i).

> Question 2: What is the suggested approach to resolve the
>  problem above?

We had a similar discussion recently. See "basic question about
induction/recursion & pattern-matching"
(http://thread.gmane.org/gmane.comp.lang.agda/406).

>  However, if I mention an implicit argument:
>
> [...]
>
>  The typecheck fails with a message similar to the one above:
>
> [...]
>
>  Why does simply mentioning the argument make a difference?

Because you changed the order in which the pattern matching was
performed. Previously the hidden argument was dotted.

Agda requires that the pattern matching in a function definition can
be broken down into a "case tree", where every case node performs
pattern matching on the top-level constructor of a single pattern
variable. In such a case tree every individual case node has to be
type correct. As far as I know the order of the case nodes is
implicitly defined by the textual order of the patterns, with
sub-patterns coming after their parent patterns (naturally).

-- 
/NAD