    {-|
    Description : type-level proofs involving contexts
    Copyright   : (c) Galois, Inc 2015-2019
    Maintainer  : Joe Hendrix <jhendrix@galois.com>

    This reflects type level proofs involving contexts.
    -}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE TypeOperators #-}
    module Data.Parameterized.Ctx.Proofs
      ( leftId
      , assoc
      ) where

    import Data.Type.Equality

    import Data.Parameterized.Axiom
    import Data.Parameterized.Ctx

    leftId :: p x -> (EmptyCtx <+> x) :~: x
    leftId :: forall {k} (p :: Ctx k -> *) (x :: Ctx k).
    p x -> (EmptyCtx <+> x) :~: x
    leftId p x
    _ = (EmptyCtx <+> x) :~: x
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom

    assoc :: p x -> q y -> r z -> x <+> (y <+> z) :~: (x <+> y) <+> z
    assoc :: forall {k} (p :: Ctx k -> *) (x :: Ctx k) (q :: Ctx k -> *)
           (y :: Ctx k) (r :: Ctx k -> *) (z :: Ctx k).
    p x -> q y -> r z -> (x <+> (y <+> z)) :~: ((x <+> y) <+> z)
    assoc p x
    _ q y
    _ r z
    _ = (x <+> (y <+> z)) :~: ((x <+> y) <+> z)
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom