[Agda] Universe level in heterogeneous association list

[Nicolas Osborne]

Hello,

I am trying to implement the heterogeneous association list from McBride
and McKinna's View From the Left, and universe polymorphism is giving me
a hard time.

The version without any level information is:

```agda
module HAL where

open import Data.List
open import Level

data HAL {Label : Set} : List Label -> Set where
  hnil  : HAL []
  hcons : {ls : List Label}{X : Set}
    -> (l : Label)
    -> (x : X)
    -> (h : HAL ls)
    -> HAL (l ∷ ls)
```

The `hcons` constructor raises an error. I believe that the Universe
level should be the max between the level of the Label and the level of
X, a list of Label being at the same level as Label. (But, am I right in
believing so ?)

Here is what Agda said:

Set₁ is not less or equal than Set
when checking that the type
{ls : List Label} {X : Set} (l : Label) → X → HAL ls → HAL (l ∷ ls)
of the constructor hcons fits in the sort Set of the datatype.


So far, in the few Universe polymorphism I have done, the level
information was in the type signature. But I don't want to put X in the
type signature, the point being that we should be able to change the X
at each hcons (also, Agda does not accept this definition neither).

Anybody has a suggestion ?


Nicolas Osborne

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200418/90595634/attachment.sig>