A blog post of lexi-lambda's recently put me onto Matt Noonan's technique "Ghosts of Departed Proofs" [1], which appeared in the 2018 Haskell Symposium. One example that intrigued me was a safe `Map`, which uses the type system to guarantee that lookup does not fail. Maps are used pretty extensively in Cmm-land; for example, I recently have been using them to get information like the dominator set or the reverse postorder number of every node in a `CmmGraph`. In these maps, every `Label` that appears in the `CmmGraph` is expected to have an entry. For the moment, I am just using the standard lookup function; if an entry should be missing, my code calls `panic`. The idea of eliminating these calls and getting compile-time type safety is intriguing, but I'm not sure the game is worth the candle. What do other GHC devs think? Norman [1] https://iohk.io/en/research/library/papers/ghosts-of-departed-proofsfunction...