The paper in question: An Implementation of a Dependently Typed Lambda Calculus by Andres Löh, Conor McBride and Wouter Swierstra.
I'm wondering whether it's correct in what's it is doing. Precisely on page 7. In type checker. It's got these evaluations with empty environments. Eg.
let v = eval↓ t . Precisely when these are evaluated, could it crash to the
d !! i in the Figure 4?
Dependently typed languages are related to implementation of proof assistants.