{-|
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
_ = 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
_ = forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom