Data.Type.Equality

equality.hs

{-# LANGUAGE TypeOperators, ConstraintKinds, TypeFamilies #-}

import Data.Type.Equality

-- if  we have two functions
--   a -> b
--   a' -> b'
-- and a proof that the function types are the same
-- then b must equal b' 
proof1 ::
	( f ~ (a -> b)
	, g ~ (a' -> b')
	, fgEqual ~ (f :~: g) -- try commenting this out
	, bEqual ~ (b :~: b'))
	=> fgEqual -> bEqual
proof1 Refl -- or removing the pattern match 
	= Refl

slightlyMoreInteresting ::
	-- given:
	((b -> c) -> a :~: b) -> -- a function that proves b = a when given a function b->c
	((b -> c) -> c :~: a) -> -- a function that proves c = a when given a function b->c
	(b -> c) -> -- a function b->c
	(a -> a) -- i can give you a function a->a
slightlyMoreInteresting a b f =
	case (a f, b f) of
	(Refl, Refl) -> f -- we've proven (b -> c = a -> a) so we can use f