Hi.

I wanted to construct a heterogeneous list like

```
[[true; false]%vector;
[true]%vector]%list
```

`[Vector.t bool 2, Vector.t bool 3]`

I was trying to follow Adam Chlipala’s CPDT book and defined an hlist as:

```
Inductive hlist {A : Type} {B : A -> Type} : list A -> Type :=
| HNil : hlist nil
| HCons : forall (x : A) (ls : list A), A -> hlist ls -> hlist (x :: ls).
```

The definition was executed without error.

But I couldn’t figure out how to construct the hlist.

I tried making an hlist like

```
(* Wanted to get [Vector.t bool 2; Vector.t bool 3] *)
Compute (HCons nat (fun (n:nat) => Vector.t bool n) [2;3]).
(*
The type of this term is a product while it is expected to be (list Set).
*)
```

but ran into the error.

In fact, I couldn’t even figure out how to make the example given in the CPDT book work.

```
Example someValues : hlist (fun T : Set => T ) someTypes :=
HCons 5 (HCons true HNil).
(*
The type of this term is a product while it is expected to be (list ?A).
*)
```

I got error in the part of the anonymous function.

Couldn’t understand why `someTypes`

is even needed here.

Is it that the elements of the hlist must belong to one of the types in `someTypes`

?

Can’t we just make an hlist out of `HCons`

with something like

```
Compute (HCons 5 (HCons true HNil)).
```

without resorting to use the `Example`

command? Or is it to provide the value of `B`

function?

What I thought was `A`

is like a universal type for the elements in the list and `B`

is a function which can be used to get the exact type for each of the elements in the hlist. Isn’t that so?

Any idea what I’m missing or not understanding here?