[Agda] complex indices

[Ramana Kumar]

Hi Brandon

I'm sorry to say my only motivation was to see what kinds of declaration
are possible and whether it matches what people generally have in mind
should be.

For example, this works
  bar : ℕ → Set1
  bar n  = ℕ → Set
  data foo (x : ℕ) : (n : ℕ) → bar n where
    baz : foo x x (suc x)

But I wonder if it's only accidental that it works, since if I were to make
the definition of bar any more complicated (even if it was ultimately just
a constant function) I'd run into similar problems. That is, with
  bar zero  = ℕ → Set
  bar (suc _) = ℕ → Set
I get the error
  bar x != Set of type Set₁
  when checking the definition of foo

On Wed, Feb 22, 2012 at 8:59 PM, Brandon Moore <brandon_m_moore at yahoo.com>wrote:

> Hello Ramana
>
> Could you motivate your definition a bit more?
> I don't have much idea what it should mean.
> It seems very similar to a this definition,
> which I am not surprised to see rejected
>
> data foo : (y : Bool) -> Bool where
> -- no constructors
>
> If the idea is to have an inductive family where some indices
> live at different levels, you might compare to this definition:
>
> data foo : (y : Bool) → Set (if y then zero else suc zero) where
>   bar : foo true
>
> which produces a more straightforward error message
>
> home/brandon/test/test.agda:5,6-9
> The sort of foo cannot depend on its indices in the type (y : Bool)
> → Set (if y then zero else suc zero)
> when checking the definition of foo
>
> Brandon
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120222/ec879ad0/attachment-0001.html