instead of

items : (store : DataStore) -> Vect (size store) (schema store)

I think it should be

items : (store : DataStore) -> Vect (size store) (SchemaType (schema store))

due to the type in the DataStore being defined as

(items : Vect size (SchemaType schema))

in listing 5.6

I do believe you're right. Thanks! It'll be fixed in the next version.

These things are more likely to creep in for things which don't end up in the final example code so I'll take another pass through in case I spot any others (hopefully there aren't any others like this...)