safe maps within GHC?

[Norman Ramsey]

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-proofsfunctional-pearls/