<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <div class="moz-cite-prefix">Here is one way to do it.</div>
    <div class="moz-cite-prefix"><br>
    </div>
    <div class="moz-cite-prefix">module HAL where<br>
      <br>
      open import Data.List<br>
      open import Level<br>
      <br>
      data HAL {ll lx : Level} {Label : Set ll} : List Label -> Set
      (ll ⊔ suc lx) where<br>
        hnil  : HAL []<br>
        hcons : {ls : List Label} {X : Set lx}<br>
          -> (l : Label)<br>
          -> (x : X)<br>
          -> (h : HAL {ll} {lx} ls)<br>
          -> HAL (l ∷ ls)</div>
    <div class="moz-cite-prefix"><br>
    </div>
    <div class="moz-cite-prefix">If you want to be level-free, then you
      can set ll and lx to 0, and get</div>
    <div class="moz-cite-prefix"><br>
    </div>
    <div class="moz-cite-prefix">data HAL0 {Label : Set} : List Label
      -> Set (suc zero) where<br>
        hnil  : HAL0 []<br>
        hcons : {ls : List Label} {X : Set}<br>
          -> (l : Label)<br>
          -> (x : X)<br>
          -> (h : HAL0 ls)<br>
          -> HAL0 (l ∷ ls)<br>
    </div>
    <div class="moz-cite-prefix"><br>
    </div>
    <div class="moz-cite-prefix">You need to go up a level because hcons
      contains a whole Set (of Level 0).</div>
    <div class="moz-cite-prefix"><br>
    </div>
    <div class="moz-cite-prefix">Jacques</div>
    <div class="moz-cite-prefix"><br>
    </div>
    <div class="moz-cite-prefix">On 2020-Apr.-18 09:17 , Nicolas Osborne
      wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:f334a3d5-cee0-39d4-c4d5-0a9d380b1728@univ-lille.fr">
      <pre class="moz-quote-pre" wrap="">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

</pre>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <p><br>
    </p>
  </body>
</html>