[Agda] lists/vectors

[Amr Sabry]

Hi all,

Probably a fairly basic question...

Say I have an Agda module that works with things of type 

  Vector Bool 32

How does one write a complete program, i.e., an external Haskell
wrapper, that interacts with this module? I am thinking of a Haskell
wrapper that reads an arbitrary string, checks that the string length is
32, and if so calls the Agda code. This approach requires some
function:

  (xs : List Bool) -> Vector Bool 32

where *we* know that the length of xs is actually 32 but Agda doesn't,
i.e., this will require an unsafe cast at the interface between Haskell
and Agda.

First, my approach above seems like the "natural" way to interface
between trusted Agda code and untrusted external code, right? If not,
what is the right idiom? 

Even if this is not the right idiom, what's the right incantation to
get Agda to trust me and allow the cast above? 

Thanks. --Amr