Serokell’s Work on GHC: Dependent Types, Part 4

“We” seem to be very much still in the minutiae. All I perceive so far is a lot of work going in to supporting putting types in expressions, without taking advantage of the type herald to disambiguate. Then development could get on to what we can do with types in expressions.

On the topic of impenetrability: can I ask why atravers’ whimsical comment got flagged?