Project: https://github.com/AndrasKovacs/elaboration-zoo
This repo includes a series of Haskell implementations for elaborating dependently typed languages, where packages add progressively more power and functionality. Currently, packages focus on basics of unification, inference and implicit argument handling, and we don't have any inductive types or modules (yet).