    {-|
    Description : Classes for working with type of kind @k -> *@
    Copyright   : (c) Galois, Inc 2014-2019
    Maintainer  : Joe Hendrix <jhendrix@galois.com>

    This module declares classes for working with types with the kind
    @k -> *@ for any kind @k@.  These are generalizations of the
    "Data.Functor.Classes" types as they work with any kind @k@, and are
    not restricted to '*'.
    -}
    {-# LANGUAGE AllowAmbiguousTypes #-}
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DefaultSignatures #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE Safe #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    module Data.Parameterized.Classes
      ( -- * Equality exports
        Equality.TestEquality(..)
      , (Equality.:~:)(..)
      , EqF(..)
      , PolyEq(..)
        -- * Ordering generalization
      , OrdF(..)
      , lexCompareF
      , OrderingF(..)
      , joinOrderingF
      , orderingF_refl
      , toOrdering
      , fromOrdering
      , ordFCompose
        -- * Typeclass generalizations
      , ShowF(..)
      , showsF
      , HashableF(..)
      , CoercibleF(..)
        -- * Type function application constructor
      , TypeAp(..)
        -- * Optics generalizations
      , IndexF
      , IxValueF
      , IxedF(..)
      , IxedF'(..)
      , AtF(..)
        -- * KnownRepr
      , KnownRepr(..)
        -- * Re-exports
      , Data.Hashable.Hashable(..)
      , Data.Maybe.isJust
      ) where

    import Data.Functor.Const
    import Data.Functor.Compose (Compose(..))
    import Data.Kind
    import Data.Hashable
    import Data.Maybe (isJust)
    import Data.Proxy
    import Data.Type.Equality as Equality

    import Data.Parameterized.Compose ()

    -- We define these type alias here to avoid importing Control.Lens
    -- modules, as this apparently causes problems with the safe Hasekll
    -- checking.
    type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
    type Traversal' s a = forall f. Applicative f => (a -> f a) -> s -> f s

    ------------------------------------------------------------------------
    -- CoercibleF

    -- | An instance of 'CoercibleF' gives a way to coerce between
    --   all the types of a family.  We generally use this to witness
    --   the fact that the type parameter to @rtp@ is a phantom type
    --   by giving an implementation in terms of Data.Coerce.coerce.
    class CoercibleF (rtp :: k -> Type) where
      coerceF :: rtp a -> rtp b

    instance CoercibleF (Const x) where
      coerceF :: forall (a :: k) (b :: k). Const x a -> Const x b
    coerceF (Const x
    x) = x -> Const x b
    forall {k} a (b :: k). a -> Const a b
    Const x
    x

    ------------------------------------------------------------------------
    -- EqF

    -- | @EqF@ provides a method @eqF@ for testing whether two parameterized
    -- types are equal.
    --
    -- Unlike 'TestEquality', this only works when the type arguments are
    -- the same, and does not provide a proof that the types have the same
    -- type when they are equal. Thus this can be implemented over
    -- parameterized types that are unable to provide evidence that their
    -- type arguments are equal.
    class EqF (f :: k -> Type) where
      eqF :: f a -> f a -> Bool

    instance Eq a => EqF (Const a) where
      eqF :: forall (a :: k). Const a a -> Const a a -> Bool
    eqF (Const a
    x) (Const a
    y) = a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    y

    instance EqF Proxy where
      eqF :: forall (a :: k). Proxy a -> Proxy a -> Bool
    eqF Proxy a
    _ Proxy a
    _ = Bool
    True

    ------------------------------------------------------------------------
    -- PolyEq

    -- | A polymorphic equality operator that generalizes 'TestEquality'.
    class PolyEq u v where
      polyEqF :: u -> v -> Maybe (u :~: v)

      polyEq :: u -> v -> Bool
      polyEq u
    x v
    y = Maybe (u :~: v) -> Bool
    forall a. Maybe a -> Bool
    isJust (u -> v -> Maybe (u :~: v)
    forall u v. PolyEq u v => u -> v -> Maybe (u :~: v)
    polyEqF u
    x v
    y)

    ------------------------------------------------------------------------
    -- Ordering

    -- | Ordering over two distinct types with a proof they are equal.
    data OrderingF x y where
      LTF :: OrderingF x y
      EQF :: OrderingF x x
      GTF :: OrderingF x y

    orderingF_refl :: OrderingF x y -> Maybe (x :~: y)
    orderingF_refl :: forall {k} (x :: k) (y :: k). OrderingF x y -> Maybe (x :~: y)
    orderingF_refl OrderingF x y
    o =
      case OrderingF x y
    o of
        OrderingF x y
    LTF -> Maybe (x :~: y)
    forall a. Maybe a
    Nothing
        OrderingF x y
    EQF -> (x :~: y) -> Maybe (x :~: y)
    forall a. a -> Maybe a
    Just x :~: x
    x :~: y
    forall {k} (a :: k). a :~: a
    Refl
        OrderingF x y
    GTF -> Maybe (x :~: y)
    forall a. Maybe a
    Nothing

    -- | Convert 'OrderingF' to standard ordering.
    toOrdering :: OrderingF x y -> Ordering
    toOrdering :: forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
    toOrdering OrderingF x y
    LTF = Ordering
    LT
    toOrdering OrderingF x y
    EQF = Ordering
    EQ
    toOrdering OrderingF x y
    GTF = Ordering
    GT

    -- | Convert standard ordering to 'OrderingF'.
    fromOrdering :: Ordering -> OrderingF x x
    fromOrdering :: forall {k} (x :: k). Ordering -> OrderingF x x
    fromOrdering Ordering
    LT = OrderingF x x
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
    fromOrdering Ordering
    EQ = OrderingF x x
    forall {k} (x :: k). OrderingF x x
    EQF
    fromOrdering Ordering
    GT = OrderingF x x
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF

    -- | @joinOrderingF x y@ first compares on @x@, returning an
    -- equivalent value if it is not `EQF`.  If it is `EQF`, it returns @y@.
    joinOrderingF :: forall j k (a :: j) (b :: j) (c :: k) (d :: k)
                  .  OrderingF a b
                  -> (a ~ b => OrderingF c d)
                  -> OrderingF c d
    joinOrderingF :: forall j k (a :: j) (b :: j) (c :: k) (d :: k).
    OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
    joinOrderingF OrderingF a b
    EQF (a ~ b) => OrderingF c d
    y = OrderingF c d
    (a ~ b) => OrderingF c d
    y
    joinOrderingF OrderingF a b
    LTF (a ~ b) => OrderingF c d
    _ = OrderingF c d
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
    joinOrderingF OrderingF a b
    GTF (a ~ b) => OrderingF c d
    _ = OrderingF c d
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF

    ------------------------------------------------------------------------
    -- OrdF

    -- | The `OrdF` class is a total ordering over parameterized types so
    -- that types with different parameters can be compared.
    --
    -- Instances of `OrdF` are expected to satisfy the following laws:
    --
    -- [__Transitivity__]: if @leqF x y && leqF y z@ = 'True', then @leqF x = z@ = @True@
    -- [__Reflexivity__]: @leqF x x@ = @True@
    -- [__Antisymmetry__]: if @leqF x y && leqF y x@ = 'True', then @testEquality x y@ = @Just Refl@
    --
    -- Note that the following operator interactions are expected to hold:
    --
    -- * @geqF x y@ iff @leqF y x@
    -- * @ltF  x y@ iff @leqF x y && testEquality x y = Nothing@
    -- * @gtF  x y@ iff @ltF y x@
    -- * @ltF  x y@ iff @compareF x y == LTF@
    -- * @gtF  x y@ iff @compareF x y == GTF@
    -- * @isJust (testEquality x y)@ iff @compareF x y == EQF@
    --
    -- Furthermore, when @x@ and @y@ both have type @(k tp)@, we expect:
    --
    -- * @toOrdering (compareF x y)@ equals @compare x y@ when @Ord (k tp)@ has an instance.
    -- * @isJust (testEquality x y)@ equals @x == y@ when @Eq (k tp)@ has an instance.
    --
    -- Minimal complete definition: either 'compareF' or 'leqF'.
    -- Using 'compareF' can be more efficient for complex types.
    class TestEquality ktp => OrdF (ktp :: k -> Type) where
      {-# MINIMAL compareF | leqF #-}

      compareF :: ktp x -> ktp y -> OrderingF x y
      compareF ktp x
    x ktp y
    y =
        case ktp x -> ktp y -> Maybe (x :~: y)
    forall (a :: k) (b :: k). ktp a -> ktp b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality ktp x
    x ktp y
    y of
          Just x :~: y
    Refl -> OrderingF x x
    OrderingF x y
    forall {k} (x :: k). OrderingF x x
    EQF
          Maybe (x :~: y)
    Nothing | ktp x -> ktp y -> Bool
    forall (x :: k) (y :: k). ktp x -> ktp y -> Bool
    forall k (ktp :: k -> *) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> Bool
    leqF ktp x
    x ktp y
    y -> OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
                  | Bool
    otherwise -> OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF

      leqF :: ktp x -> ktp y -> Bool
      leqF ktp x
    x ktp y
    y =
        case ktp x -> ktp y -> OrderingF x y
    forall (x :: k) (y :: k). ktp x -> ktp y -> OrderingF x y
    forall k (ktp :: k -> *) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    compareF ktp x
    x ktp y
    y of
          OrderingF x y
    LTF -> Bool
    True
          OrderingF x y
    EQF -> Bool
    True
          OrderingF x y
    GTF -> Bool
    False

      ltF :: ktp x -> ktp y -> Bool
      ltF ktp x
    x ktp y
    y =
        case ktp x -> ktp y -> OrderingF x y
    forall (x :: k) (y :: k). ktp x -> ktp y -> OrderingF x y
    forall k (ktp :: k -> *) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    compareF ktp x
    x ktp y
    y of
          OrderingF x y
    LTF -> Bool
    True
          OrderingF x y
    EQF -> Bool
    False
          OrderingF x y
    GTF -> Bool
    False

      geqF :: ktp x -> ktp y -> Bool
      geqF ktp x
    x ktp y
    y =
        case ktp x -> ktp y -> OrderingF x y
    forall (x :: k) (y :: k). ktp x -> ktp y -> OrderingF x y
    forall k (ktp :: k -> *) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    compareF ktp x
    x ktp y
    y of
          OrderingF x y
    LTF -> Bool
    False
          OrderingF x y
    EQF -> Bool
    True
          OrderingF x y
    GTF -> Bool
    True

      gtF :: ktp x -> ktp y -> Bool
      gtF ktp x
    x ktp y
    y =
        case ktp x -> ktp y -> OrderingF x y
    forall (x :: k) (y :: k). ktp x -> ktp y -> OrderingF x y
    forall k (ktp :: k -> *) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    compareF ktp x
    x ktp y
    y of
          OrderingF x y
    LTF -> Bool
    False
          OrderingF x y
    EQF -> Bool
    False
          OrderingF x y
    GTF -> Bool
    True

    -- | Compare two values, and if they are equal compare the next values,
    -- otherwise return LTF or GTF
    lexCompareF :: forall j k (f :: j -> Type) (a :: j) (b :: j) (c :: k) (d :: k)
                 .  OrdF f
                => f a
                -> f b
                -> (a ~ b => OrderingF c d)
                -> OrderingF c d
    lexCompareF :: forall j k (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k).
    OrdF f =>
    f a -> f b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
    lexCompareF f a
    x f b
    y = OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
    OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
    joinOrderingF (f a -> f b -> OrderingF a b
    forall (x :: j) (y :: j). f x -> f y -> OrderingF x y
    forall k (ktp :: k -> *) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    compareF f a
    x f b
    y)

    -- | If the \"outer\" functor has an 'OrdF' instance, then one can be generated
    -- for the \"inner\" functor. The type-level evidence of equality is deduced
    -- via generativity of @g@, e.g. the inference @g x ~ g y@ implies @x ~ y@.
    ordFCompose :: forall k l (f :: k -> Type) (g :: l -> k) x y.
                    (forall w z. f w -> f z -> OrderingF w z)
                -> Compose f g x
                -> Compose f g y
                -> OrderingF x y
    ordFCompose :: forall k l (f :: k -> *) (g :: l -> k) (x :: l) (y :: l).
    (forall (w :: k) (z :: k). f w -> f z -> OrderingF w z)
    -> Compose f g x -> Compose f g y -> OrderingF x y
    ordFCompose forall (w :: k) (z :: k). f w -> f z -> OrderingF w z
    ordF_ (Compose f (g x)
    x) (Compose f (g y)
    y) =
      case f (g x) -> f (g y) -> OrderingF (g x) (g y)
    forall (w :: k) (z :: k). f w -> f z -> OrderingF w z
    ordF_ f (g x)
    x f (g y)
    y of
        OrderingF (g x) (g y)
    LTF -> OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
        OrderingF (g x) (g y)
    GTF -> OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF
        OrderingF (g x) (g y)
    EQF -> OrderingF x x
    OrderingF x y
    forall {k} (x :: k). OrderingF x x
    EQF

    instance OrdF f => OrdF (Compose f g) where
      compareF :: forall (x :: k) (y :: k).
    Compose f g x -> Compose f g y -> OrderingF x y
    compareF Compose f g x
    x Compose f g y
    y = (forall (w :: k) (z :: k). f w -> f z -> OrderingF w z)
    -> Compose f g x -> Compose f g y -> OrderingF x y
    forall k l (f :: k -> *) (g :: l -> k) (x :: l) (y :: l).
    (forall (w :: k) (z :: k). f w -> f z -> OrderingF w z)
    -> Compose f g x -> Compose f g y -> OrderingF x y
    ordFCompose f w -> f z -> OrderingF w z
    forall (w :: k) (z :: k). f w -> f z -> OrderingF w z
    forall k (ktp :: k -> *) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    compareF Compose f g x
    x Compose f g y
    y

    ------------------------------------------------------------------------
    -- ShowF

    -- | A parameterized type that can be shown on all instances.
    --
    -- To implement @'ShowF' g@, one should implement an instance @'Show'
    -- (g tp)@ for all argument types @tp@, then write an empty instance
    -- @instance 'ShowF' g@.
    class ShowF (f :: k -> Type) where
      -- | Provides a show instance for each type.
      withShow :: p f -> q tp -> (Show (f tp) => a) -> a

      default withShow :: Show (f tp) => p f -> q tp -> (Show (f tp) => a) -> a
      withShow p f
    _ q tp
    _ Show (f tp) => a
    x = a
    Show (f tp) => a
    x

      showF :: forall tp . f tp -> String
      showF f tp
    x = Proxy f -> Proxy tp -> (Show (f tp) => String) -> String
    forall k (f :: k -> *) (p :: (k -> *) -> *) (q :: k -> *) (tp :: k)
           a.
    ShowF f =>
    p f -> q tp -> (Show (f tp) => a) -> a
    forall (p :: (k -> *) -> *) (q :: k -> *) (tp :: k) a.
    p f -> q tp -> (Show (f tp) => a) -> a
    withShow (Proxy f
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy f) (Proxy tp
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy tp) (f tp -> String
    forall a. Show a => a -> String
    show f tp
    x)

      -- | Like 'showsPrec', the precedence argument is /one more/ than the
      -- precedence of the enclosing context.
      showsPrecF :: forall tp. Int -> f tp -> String -> String
      showsPrecF Int
    p f tp
    x = Proxy f
    -> Proxy tp
    -> (Show (f tp) => String -> String)
    -> String
    -> String
    forall k (f :: k -> *) (p :: (k -> *) -> *) (q :: k -> *) (tp :: k)
           a.
    ShowF f =>
    p f -> q tp -> (Show (f tp) => a) -> a
    forall (p :: (k -> *) -> *) (q :: k -> *) (tp :: k) a.
    p f -> q tp -> (Show (f tp) => a) -> a
    withShow (Proxy f
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy f) (Proxy tp
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy tp) (Int -> f tp -> String -> String
    forall a. Show a => Int -> a -> String -> String
    showsPrec Int
    p f tp
    x)

    showsF :: ShowF f => f tp -> String -> String
    showsF :: forall {k} (f :: k -> *) (tp :: k).
    ShowF f =>
    f tp -> String -> String
    showsF f tp
    x = Int -> f tp -> String -> String
    forall (tp :: k). Int -> f tp -> String -> String
    forall k (f :: k -> *) (tp :: k).
    ShowF f =>
    Int -> f tp -> String -> String
    showsPrecF Int
    0 f tp
    x

    instance Show x => ShowF (Const x)

    instance ShowF Proxy

    ------------------------------------------------------------------------
    -- IxedF

    type family IndexF       (m :: Type) :: k -> Type
    type family IxValueF     (m :: Type) :: k -> Type

    -- | Parameterized generalization of the lens @Ixed@ class.
    class IxedF k m where
      -- | Given an index into a container, build a traversal that visits
      --   the given element in the container, if it exists.
      ixF :: forall (x :: k). IndexF m x -> Traversal' m (IxValueF m x)

    -- | Parameterized generalization of the lens @Ixed@ class,
    --   but with the guarantee that indexes exist in the container.
    class IxedF k m => IxedF' k m where
      -- | Given an index into a container, build a lens that
      --   points into the given element in the container.
      ixF' :: forall (x :: k). IndexF m x -> Lens' m (IxValueF m x)

    ------------------------------------------------------------------------
    -- AtF

    -- | Parameterized generalization of the lens @At@ class.
    class IxedF k m => AtF k m where
      -- | Given an index into a container, build a lens that points into
      --   the given position in the container, whether or not it currently
      --   exists.  Setting values of @atF@ to a @Just@ value will insert
      --   the value if it does not already exist.
      atF :: forall (x :: k). IndexF m x -> Lens' m (Maybe (IxValueF m x))

    ------------------------------------------------------------------------
    -- HashableF

    -- | A default salt used in the implementation of 'hash'.
    defaultSalt :: Int
    #if WORD_SIZE_IN_BITS == 64
    defaultSalt = 0xdc36d1615b7400a4
    #else
    defaultSalt :: Int
    defaultSalt = Int
    0x087fc72c
    #endif
    {-# INLINE defaultSalt #-}

    -- | A parameterized type that is hashable on all instances.
    class HashableF (f :: k -> Type) where
      hashWithSaltF :: Int -> f tp -> Int

      -- | Hash with default salt.
      hashF :: f tp -> Int
      hashF = Int -> f tp -> Int
    forall (tp :: k). Int -> f tp -> Int
    forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
    hashWithSaltF Int
    defaultSalt

    instance Hashable a => HashableF (Const a) where
      hashWithSaltF :: forall (tp :: k). Int -> Const a tp -> Int
    hashWithSaltF Int
    s (Const a
    x) = Int -> a -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    s a
    x

    ------------------------------------------------------------------------
    -- TypeAp

    -- | Captures the value obtained from applying a type to a function so
    -- that we can use parameterized class instance to provide unparameterized
    -- instances for specific types.
    --
    -- This is the same as `Ap` from @Control.Applicative@, but we introduce
    -- our own new type to avoid orphan instances.
    newtype TypeAp (f :: k -> Type) (tp :: k) = TypeAp (f tp)

    instance TestEquality f => Eq (TypeAp f tp) where
      TypeAp f tp
    x == :: TypeAp f tp -> TypeAp f tp -> Bool
    == TypeAp f tp
    y = Maybe (tp :~: tp) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (tp :~: tp) -> Bool) -> Maybe (tp :~: tp) -> Bool
    forall a b. (a -> b) -> a -> b
    $ f tp -> f tp -> Maybe (tp :~: tp)
    forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality f tp
    x f tp
    y

    instance OrdF f => Ord (TypeAp f tp) where
      compare :: TypeAp f tp -> TypeAp f tp -> Ordering
    compare (TypeAp f tp
    x) (TypeAp f tp
    y) = OrderingF tp tp -> Ordering
    forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
    toOrdering (f tp -> f tp -> OrderingF tp tp
    forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    forall k (ktp :: k -> *) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    compareF f tp
    x f tp
    y)

    instance ShowF f => Show (TypeAp f tp) where
      showsPrec :: Int -> TypeAp f tp -> String -> String
    showsPrec Int
    p (TypeAp f tp
    x) = Int -> f tp -> String -> String
    forall (tp :: k). Int -> f tp -> String -> String
    forall k (f :: k -> *) (tp :: k).
    ShowF f =>
    Int -> f tp -> String -> String
    showsPrecF Int
    p f tp
    x

    instance (HashableF f, TestEquality f) => Hashable (TypeAp f tp) where
      hashWithSalt :: Int -> TypeAp f tp -> Int
    hashWithSalt Int
    s (TypeAp f tp
    x) = Int -> f tp -> Int
    forall (tp :: k). Int -> f tp -> Int
    forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
    hashWithSaltF Int
    s f tp
    x

    ------------------------------------------------------------------------
    -- KnownRepr

    -- | This class is parameterized by a kind @k@ (typically a data
    -- kind), a type constructor @f@ of kind @k -> *@ (typically a GADT of
    -- singleton types indexed by @k@), and an index parameter @ctx@ of
    -- kind @k@.
    class KnownRepr (f :: k -> Type) (ctx :: k) where
      knownRepr :: f ctx

    instance KnownRepr Proxy ctx where
      knownRepr :: Proxy ctx
    knownRepr = Proxy ctx
    forall {k} (t :: k). Proxy t
    Proxy