fact package:gdp
A Fact p is an implicit proof of p, propagated by
Haskell's constraint solver. Facts can be used to implicitly
introduce or propagate proofs. However, there is a small run-time cost
associated with using Facts: typeclass dictionaries for
Facts are still passed around. In many cases they will be
optimized away, but this is not guaranteed.