Re: [Agda] Level ω

[David Leduc]

Andreas wrote:
> Can't you do
>
> data T (max : Level) : Stream (BoundedLevel max) -> Set (suc max) where
>  makeT : (ls : Stream (BoundedLevel max)) -> Set max -> T max (tail ls)
>
> and then define a smart constructor
>
>  makeT' : (ls : Stream (BoundedLevel max)) -> Set (Carrier (head ls)) ->
>   T max (tail ls)
>
> that does the necessary liftings?

Assuming that I have proved

  max-is-max : (max : Level)(ls : Stream (BoundedLevel max)) ->
    max ⊔ Carrier (head ls) ≡ max

I cannot use it in the definition of makeT' because when I try do destruct p in

  makeT' max ls s with (max-is-max max ls)
  makeT' max ls s | p = {!!}

Agda raises an error

  Cannot pattern match on constructor refl, since the inferred
  indices [max' ⊔ Carrier (head ls')] cannot be unified with the
  expected indices [max'] for some ls', max'
  when checking that the expression ? has type T max (tail ls)

Is it my mistake, or a limitation of Agda?