even if you start with an
nwith some proofp, you often need to then proveq. Haskell just can’t do this at the moment.
Ghosts of Departed Proofs is a step in this direction. It requires a little contortion at both the value and type levels, but it’s quite general (for example, it’s the approach underlying justified-containers). The author, Matt Noonan, positions it as an alternative to partial functions and failure conditions (Maybe/ Either wrapping).
OP, I don’t necessarily recommend GDP for everyday use, but I do recommend reading the paper for a fascinating glimpse at just how much information you can pack into a type.