I was making a heterogenous list (hlist) in the line of what's mentioned in here.

```
Inductive hlist (A : Type) (B : A -> Type) : list A -> Type :=
| hnil : hlist A B []
| hcons : forall (x : A) (ls : list A),
(B x) -> hlist A B ls -> hlist A B (x::ls).
Arguments hnil {A B}.
Arguments hcons {A B x ls}.
```

This type checked all right.

And I was able to make hlists as well.

```
Example hls1 : hlist Set (fun x => x) [nat; bool] :=
hcons 3 (hcons true hnil).
```

Then I tried making a function to index into the element of hlists and made an `hidx`

function.

But that gave error.

```
Fixpoint hidx_helper {A : Type} (ls : list A) (idx : nat) : Type :=
match idx, ls with
| _, []%list => unit
| O, (x::xs)%list => A
| S n', (x::xs)%list => hidx_helper xs n'
end.
Fixpoint hidx {A: Type} {B: A -> Type} {ls: list A}
(idx : nat) (hls : hlist A B ls)
: hidx_helper ls idx :=
match idx, hls with
| _, hnil _ _ => tt (* --------ERROR here--------- *)
| O, hcons _ _ _ _ x xs => x
| S n', hcons _ _ _ _ x xs => hidx n' xs
end.
(*
In environment
hidx : forall (A : Type) (B : A -> Type) (ls : list A) (idx : nat),
hlist A B ls -> hidx_helper ls idx
A : Type
B : A -> Type
ls : list A
idx : nat
hls : hlist A B ls
The term "tt" has type "unit" while it is expected to have type
"hidx_helper ?l@{l0:=[]} ?n@{i0:=0}".
*)
```

I guess the problem is that I can't let Coq know that `hidx_helper [] 0`

evaluates to `unit`

?

```
Compute hidx_helper []%list 0.
(* = unit : Type *)
```

How can I set this right?

And could there be a way where the `hidx_helper`

needn't have been separately defined?

As it's used just to find the type of `hidx`

?

I guess the problem is that I can't let Coq know that hidx_helper [] 0 evaluates to unit?

no, the problem is that it hasn't figured out that the return type is `hidx_helper [] 0`

so it can't evaluate it

try `match idx , hls in hlist _ _ ls return hidx_helper ls idx with`

Thanks. That fixed the first branch of that match.

But the second is also having trouble that I couldn't figure out.

It says:

```
In environment
hidx : forall (A : Type) (B : A -> Type) (ls : list A) (idx : nat),
hlist A B ls -> hidx_helper ls idx
A : Type
B : A -> Type
ls : list A
idx : nat
hls : hlist A B ls
a : A
l : list A
x : B a
xs : hlist A B l
The term "x" has type "B a" while it is expected to have type
"hidx_helper (a :: l) 0".
```

Could this be a similar problem?

the definition of the helper looks wrong to me, it uses only the length of the list but not its contents

Yeah, I hadn't realized it.

I changed it to:

```
Fixpoint hidx_helper (A : Type) (lslen idx : nat) : Type :=
match idx, lslen with
| _, O => unit
| O, _ => A
| S n', S lslen' => hidx_helper A lslen' n'
(*| S n', (x::xs)%list => hidx_helper xs n' *)
end.
Fixpoint hidx {A: Type} {B: A -> Type} {ls: list A}
(idx : nat) (hls : hlist A B ls)
: hidx_helper A (length ls) idx :=
match idx, hls in (hlist _ _ ls) return
(hidx_helper A (length ls) idx) with
| _, hnil _ _ => tt
| O, hcons _ _ _ _ x xs => x (* Error here! *)
| S n', hcons _ _ _ _ x xs => hidx n' xs
end.
```

But got a similar error:

```
In environment
hidx : forall (A : Type) (B : A -> Type) (ls : list A) (idx : nat),
hlist A B ls -> hidx_helper A (length ls) idx
A : Type
B : A -> Type
ls : list A
idx : nat
hls : hlist A B ls
a : A
l : list A
x : B a
xs : hlist A B l
The term "x" has type "B a" while it is expected to have type
"hidx_helper A (length (a :: l)) 0".
```

it should be something like

```
Fixpoint hidx_helper {A : Type} (B:A->Type) (ls : list A) (idx : nat) {struct ls} : Type :=
match idx, ls with
| _, []%list => unit
| O, (x::xs)%list => B x
| S n', (x::xs)%list => hidx_helper B xs n'
end.
```

I used this helper like:

```
Fixpoint hidx {A: Type} {B: A -> Type} {ls: list A}
(idx : nat) (hls : hlist A B ls)
: hidx_helper (fun x=>Type) ls idx :=
match idx, hls in (hlist _ _ ls) return
(hidx_helper (fun x=>Type) ls idx) with
| _, @hnil _ _ => tt
| O, @hcons _ _ _ _ x xs => x
| S n', @hcons _ _ _ _ x xs => hidx n' xs
end.
```

But got error:

```
In environment
hidx : forall (A : Type) (B : A -> Type) (ls : list A) (idx : nat),
hlist A B ls -> hidx_helper (fun _ : A => Type) ls idx
A : Type
B : A -> Type
ls : list A
idx : nat
hls : hlist A B ls
a : A
l : list A
x : B a
xs : hlist A B l
The term "x" has type "B a" while it is expected to have type
"hidx_helper (fun _ : A => Type) (a :: l) 0".
```

I guess I'm using it wrong. How should it be used?

use B not fun x=>Type

Thanks a lot. That works. Now let me spend some time understanding it. :smiley:

Julin S has marked this topic as resolved.

Last updated: Oct 03 2023 at 21:01 UTC