{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fno-warn-missing-methods #-}
module Language.Symantic.Helper.Data.Type.Equality where

-- | Like (:~:) but prove also that the kinds are equal.
data (:~~:) (a::ka) (b::kb) where
	KRefl :: a :~~: a