If indices to types come from a different syntactic category than programs, there are a few things you cannot do.\xa0 Some initial thoughts on how to work around these.