{-|
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 Unsafe.Coerce

import Data.Parameterized.Ctx

leftId :: p x -> (EmptyCtx <+> x) :~: x
leftId :: p x -> (EmptyCtx <+> x) :~: x
leftId p x
_ = (Any :~: Any) -> (EmptyCtx <+> x) :~: x
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl

assoc :: 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)
assoc p x
_ q y
_ r z
_ = (Any :~: Any) -> (x <+> (y <+> z)) :~: ((x <+> y) <+> z)
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl