Converting typed term representations: from HOAS to de Bruijn.
Given a GADT representation of a typed higher-order term language using higher-order abstract syntax (HOAS), it is more difficult to convert to an alternative GADT representation using de Bruijn indices for bound variables than I at first expected. Here is a solution using explicit type representations (with Data.Typeable).
