-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Data.Type.Equality compat package
--   
--   This library defines a propositional equality data type, shims
--   @Data.Type.Equality" as well as possible for older GHCs (< 7.8).
--   
--   <pre>
--   data a :~: b where
--       Refl :: a :~: a
--   </pre>
--   
--   The module <tt>Data.Type.Equality.Hetero</tt> shims <tt>:~~:</tt>
--   equality, for compilers with <tt>PolyKinds</tt>
@package type-equality
@version 1


-- | This module shims kind heterogeneous propositional equality.
--   
--   Note: some instances: <a>Read</a>, <a>Enum</a>, <a>Bounded</a> and
--   <tt>Data</tt> would be available only since GHC-8.0 as we need
--   <tt>~~</tt> constraint. Also GH-7.10.3 is nitpicky <i>data constructor
--   ‘HRefl’ cannot be GADT-like in its *kind* arguments</i>, thus this
--   module is available only with GHC &gt;= 8.0
module Data.Type.Equality.Hetero

-- | Kind heterogeneous propositional equality. Like <a>:~:</a>, <tt>a :~~:
--   b</tt> is inhabited by a terminating value if and only if <tt>a</tt>
--   is the same type as <tt>b</tt>.
data (:~~:) (a :: k1) (b :: k2) :: forall k1 k2. () => k1 -> k2 -> Type
[HRefl] :: forall k1 k2 (a :: k1) (b :: k2). () => a :~~: a
infix 4 :~~: