Description : Universal quantification, in a datatype

This module provides All, a GADT that encodes universal quantification/parametricity over a type variable.

The following is an example of a situation in which it might be necessary to use All (though it is a bit contrived):

  {--}
  {--}

  data F (x :: Bool) where
    FTrue :: F 'True
    FFalse :: F 'False
    FIndeterminate :: F b

  data Value =
    VAllF (All F)

  class Valuable a where
    valuation :: a -> Value

  instance Valuable (All F) where
    valuation = VAllF

  val1 :: Value
  val1 = valuation (All FIndeterminate)

For a less contrived but more complex example, see this blog post: http://comonad.com/reader/2008/rotten-bananas/