b'
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.