it's funny to see it written as "basic" dependent typing, considering it's an extremely complex type system to implement.