    ------------------------------------------------------------------------
    -- |
    -- Module           : Data.Parameterized.All
    -- Copyright        : (c) Galois, Inc 2019
    -- Maintainer       : Langston Barrett <langston@galois.com>
    -- 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):
    --
    -- @
    --   {-# LANGUAGE FlexibleInstances #-}
    --   {-# LANGUAGE GADTs #-}
    --
    --   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/
    ------------------------------------------------------------------------

    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}

    module Data.Parameterized.All
      ( All(..)
      , allConst
      ) where

    import Data.Functor.Const (Const(..))
    import Data.Kind

    import Data.Parameterized.Classes
    import Data.Parameterized.TraversableF

    newtype All (f :: k -> Type) = All { forall k (f :: k -> *). All f -> forall (x :: k). f x
    getAll :: forall x. f x }

    instance FunctorF All where
      fmapF :: forall (f :: k -> *) (g :: k -> *).
    (forall (x :: k). f x -> g x) -> All f -> All g
    fmapF forall (x :: k). f x -> g x
    f (All forall (x :: k). f x
    a) = (forall (x :: k). g x) -> All g
    forall k (f :: k -> *). (forall (x :: k). f x) -> All f
    All (f x -> g x
    forall (x :: k). f x -> g x
    f f x
    forall (x :: k). f x
    a)

    instance FoldableF All where
      foldMapF :: forall m (e :: k -> *).
    Monoid m =>
    (forall (s :: k). e s -> m) -> All e -> m
    foldMapF forall (s :: k). e s -> m
    toMonoid (All forall (x :: k). e x
    x) = e (ZonkAny 2) -> m
    forall (s :: k). e s -> m
    toMonoid e (ZonkAny 2)
    forall (x :: k). e x
    x

    instance ShowF f => Show (All f) where
      show :: All f -> String
    show (All forall (x :: k). f x
    fa) = f (ZonkAny 1) -> String
    forall (tp :: k). f tp -> String
    forall k (f :: k -> *) (tp :: k). ShowF f => f tp -> String
    showF f (ZonkAny 1)
    forall (x :: k). f x
    fa

    instance EqF f => Eq (All f) where
      (All forall (x :: k). f x
    x) == :: All f -> All f -> Bool
    == (All forall (x :: k). f x
    y) = f (ZonkAny 0) -> f (ZonkAny 0) -> Bool
    forall (a :: k). f a -> f a -> Bool
    forall k (f :: k -> *) (a :: k). EqF f => f a -> f a -> Bool
    eqF f (ZonkAny 0)
    forall (x :: k). f x
    x f (ZonkAny 0)
    forall (x :: k). f x
    y

    allConst :: a -> All (Const a)
    allConst :: forall {k} a. a -> All (Const a)
    allConst a
    a = (forall (x :: k). Const a x) -> All (Const a)
    forall k (f :: k -> *). (forall (x :: k). f x) -> All f
    All (a -> Const a x
    forall {k} a (b :: k). a -> Const a b
    Const a
    a)