Hi Cafe I am currently experimenting with the excellent bound library. I want to implement the simply typed lambda calc from TAPL (no type inference yet). When moving under a binder I want to extend my context and then look up bound terms by their indices using list indexing. I would have thought I could use something like foldMapScope to recover the bound variables, then write some function to calculate the depth of the "listy" type value returned and thus recover the index. However! The type returned is non-regular and I cannot for the life of me figure out anything that doesn't involve GHC complaining about infinite types. Any pointers on how this can be accomplished? For the record, this is what I have that works at the moment. http://lpaste.net/101279