diff --git a/Type/Eq.hs b/Type/Eq.hs
--- a/Type/Eq.hs
+++ b/Type/Eq.hs
@@ -34,7 +34,7 @@
 -- | Evidence that type @a@ is the same as type @b@.
 -- 
 --   The @'Functor'@, @'Applicative'@, and @'Monad'@ instances of @Maybe@
---   are extremely useful for working with values of type @Maybe (a :~: b)@.
+--   are very useful for working with values of type @Maybe (a :~: b)@.
 data a :~: b where
     Eq :: (a ~ b) => a :~: b
 
@@ -45,7 +45,7 @@
 
 -- | Unpack equality evidence and use it.
 -- 
---   This function compiles with GHC 6.10, but doesn't work. Beware!
+--   This function compiles with GHC 6.10, but doesn't work.
 withEq :: (a ~ b => r) -> (a :~: b) -> r
 withEq x Eq = x
 -- This doesn't seem to work in 6.10, so for compatibility, we're not going to use it
@@ -99,13 +99,13 @@
 
 -- | Unpack partial equality evidence and use it.
 --
---   This function compiles with GHC 6.10, but doesn't work. Beware!
+--   This function compiles with GHC 6.10, but doesn't work.
 withOuterEq :: (forall i. f i ~ a => r) -> OuterEq f a -> r
 withOuterEq x OuterEq = x
 
 -- | Unpack partial equality evidence and use it.
 --
---   This function compiles with GHC 6.10, but doesn't work. Beware!
+--   This function compiles with GHC 6.10, but doesn't work.
 withInnerEq :: (forall f. f i ~ a => r) -> InnerEq i a -> r
 withInnerEq x InnerEq = x
 
@@ -138,7 +138,9 @@
 --       - @(\<~>)@, or
 -- 
 --       - both @(~>)@ and @(<~)@.
-class TypeEq t where
+-- 
+--   Due to <http://hackage.haskell.org/trac/ghc/ticket/5591> you may have to use 'unsafeOuterEq' and/or 'unsafeInnerEq' to define some of these.
+class TypeCompare t where
     maybeEq,          (~~)  :: t a     -> t b -> Maybe (a :~: b)
     maybeOuterEq,     (~>)  :: t (f i) -> t a -> Maybe (OuterEq f a)
     maybeInnerEq,     (<~)  :: t (f i) -> t a -> Maybe (InnerEq i a)
@@ -153,21 +155,17 @@
     (<~)  = maybeInnerEq
     (<~>) = piecewiseMaybeEq
 
-instance TypeEq ((:~:) a) where
+instance TypeCompare ((:~:) a) where
     maybeEq      Eq Eq = Just Eq
     maybeOuterEq Eq Eq = Just OuterEq
     maybeInnerEq Eq Eq = Just InnerEq
 
-instance TypeEq (InnerEq i) where
+instance TypeCompare (InnerEq i) where
     maybeEq      _ _ = Nothing
     maybeOuterEq _ _ = Nothing
     maybeInnerEq InnerEq InnerEq = Just BUG_5591(InnerEq)
 
-instance TypeEq (OuterEq f) where
+instance TypeCompare (OuterEq f) where
     maybeEq      _ _ = Nothing
     maybeOuterEq OuterEq OuterEq = Just BUG_5591(OuterEq)
     maybeInnerEq _ _ = Nothing
-
--- TODO
--- fixities
--- other compilers
diff --git a/Type/Eq.hs-boot b/Type/Eq.hs-boot
--- a/Type/Eq.hs-boot
+++ b/Type/Eq.hs-boot
@@ -9,3 +9,9 @@
 
 data a :~: b where
     Eq :: (a ~ b) => a :~: b
+
+data OuterEq f a where
+    OuterEq :: f i ~ a => OuterEq f a
+
+data InnerEq i a where
+    InnerEq :: f i ~ a => InnerEq i a
diff --git a/Type/Eq/Higher.hs-boot b/Type/Eq/Higher.hs-boot
--- a/Type/Eq/Higher.hs-boot
+++ b/Type/Eq/Higher.hs-boot
@@ -11,3 +11,9 @@
 
 data (m :: * -> * -> *) :::~::: (n :: * -> * -> *) where
     Eq2 :: (m ~ n) => m :::~::: n
+
+data OuterEq1 (m :: * -> * -> *) (f :: * -> *) where
+    OuterEq1 :: m a ~ f => OuterEq1 m f
+
+data InnerEq1 (a :: *) (f :: * -> *) where
+    InnerEq1 :: m a ~ f => InnerEq1 a f
diff --git a/Type/Eq/Higher/Unsafe.hs b/Type/Eq/Higher/Unsafe.hs
--- a/Type/Eq/Higher/Unsafe.hs
+++ b/Type/Eq/Higher/Unsafe.hs
@@ -17,3 +17,11 @@
 -- | Very unsafe! The same rules apply as for 'unsafeCoerce'.
 unsafeCoercion2 :: m :::~::: n
 unsafeCoercion2 = unsafeCoerce Eq2
+
+-- | Very unsafe!
+unsafeOuterEq1 :: OuterEq1 m f
+unsafeOuterEq1 = unsafeCoerce OuterEq1
+
+-- | Very unsafe!
+unsafeInnerEq1 :: InnerEq1 a f
+unsafeInnerEq1 = unsafeCoerce InnerEq1
diff --git a/Type/Eq/Poly.hs b/Type/Eq/Poly.hs
new file mode 100644
--- /dev/null
+++ b/Type/Eq/Poly.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE GADTs, TypeOperators, PolyKinds, RankNTypes, CPP #-}
+
+#include "macros.h"
+
+LANGUAGE_TRUSTWORTHY
+
+{-# OPTIONS_GHC -fno-warn-unused-imports -fno-warn-orphans #-}
+
+-- | Kind-polymorphic combinators for manipulating type equality evidence.
+-- 
+--   This module is available only if @PolyKinds@ are available (GHC 7.6+).
+
+module Type.Eq.Poly (module Type.Eq, module Type.Eq.Poly) where
+
+import Control.Applicative ((<$>))
+import Control.Category ((.)) -- for haddock
+import Data.Typeable hiding (cast)
+import Type.Eq
+import Type.Eq.Higher ((::~::)(..), (:::~:::)(..), OuterEq1(..), InnerEq1(..))
+import Type.Eq.Unsafe
+import Prelude hiding ((.))
+import Unsafe.Coerce
+
+{-
+INSTANCE_TYPEABLE(1,:~:,f,g,"Type.Eq",":~:",())
+INSTANCE_TYPEABLE(2,:~:,m,n,"Type.Eq",":~:",() ())
+INSTANCE_TYPEABLE(3,:~:,x,y,"Type.Eq",":~:",() () ())
+INSTANCE_TYPEABLE(4,:~:,x,y,"Type.Eq",":~:",() () () ())
+INSTANCE_TYPEABLE(5,:~:,x,y,"Type.Eq",":~:",() () () () ())
+INSTANCE_TYPEABLE(6,:~:,x,y,"Type.Eq",":~:",() () () () () ())
+INSTANCE_TYPEABLE(7,:~:,x,y,"Type.Eq",":~:",() () () () () () ())
+-}
+
+-- | Synonym for @'composeEq'@. Kind-polymorphic, unlike @('.')@.
+(|.|) :: b :~: c -> a :~: b -> a :~: c
+(|.|) = composeEq
+
+-- | Congruence?
+applyEq, (|$|) :: f :~: g -> a :~: b -> f a :~: g b
+applyEq = withEq (withEq Eq)
+(|$|) = applyEq
+
+-- | Type constructors are generative
+constructorEq :: f a :~: g b -> f :~: g
+constructorEq = withEq BUG_5591(Eq)
+
+DYNAMIC_EQ(1,,:~:,f,g,())
+DYNAMIC_EQ(2,,:~:,n,m,() ())
+DYNAMIC_EQ(3,,:~:,x,y,() () ())
+DYNAMIC_EQ(4,,:~:,x,y,() () () ())
+DYNAMIC_EQ(5,,:~:,x,y,() () () () ())
+DYNAMIC_EQ(6,,:~:,x,y,() () () () () ())
+DYNAMIC_EQ(7,,:~:,x,y,() () () () () () ())
+
+sameOuterEq :: OuterEq f a -> OuterEq g a -> f :~: g
+sameOuterEq OuterEq OuterEq = BUG_5591(Eq)
+
+-- * Compatibility with Type.Eq.Higher
+
+fromEq1 :: f ::~:: g -> f :~: g
+fromEq1 Eq1 = Eq
+
+toEq1 :: f :~: g -> f ::~:: g
+toEq1 Eq = Eq1
+
+fromEq2 :: n :::~::: m -> n :~: m
+fromEq2 Eq2 = Eq
+
+toEq2 :: n :~: m -> n :::~::: m
+toEq2 Eq = Eq2
+
+fromOuterEq1 :: OuterEq1 m f -> OuterEq m f
+fromOuterEq1 OuterEq1 = BUG_5591(OuterEq)
+
+toOuterEq1 :: OuterEq m f -> OuterEq1 m f
+toOuterEq1 OuterEq = OuterEq1
+
+fromInnerEq1 :: InnerEq1 a f -> InnerEq a f
+fromInnerEq1 InnerEq1 = BUG_5591(InnerEq)
+
+toInnerEq1 :: InnerEq a f -> InnerEq1 a f
+toInnerEq1 InnerEq = InnerEq1
diff --git a/Type/Eq/Unsafe.hs b/Type/Eq/Unsafe.hs
--- a/Type/Eq/Unsafe.hs
+++ b/Type/Eq/Unsafe.hs
@@ -15,3 +15,11 @@
 -- | Very unsafe! The same rules apply as for 'unsafeCoerce'.
 unsafeCoercion :: a :~: b
 unsafeCoercion = unsafeCoerce Eq
+
+-- | Very unsafe!
+unsafeOuterEq :: OuterEq f a
+unsafeOuterEq = unsafeCoerce OuterEq
+
+-- | Very unsafe!
+unsafeInnerEq :: InnerEq i a
+unsafeInnerEq = unsafeCoerce InnerEq
diff --git a/macros.h b/macros.h
--- a/macros.h
+++ b/macros.h
@@ -38,7 +38,7 @@
 #endif
 
 -- http://hackage.haskell.org/trac/ghc/ticket/5591
-#if (__GLASGOW_HASKELL__ >= 702) && (__GLASGOW_HASKELL__ <= 704)
+#if (__GLASGOW_HASKELL__ >= 702) && (__GLASGOW_HASKELL__ <= 706)
 #   define BUG_5591(X) (unsafeCoerce X)
 #else
 #   define BUG_5591(X) X
diff --git a/type-eq.cabal b/type-eq.cabal
--- a/type-eq.cabal
+++ b/type-eq.cabal
@@ -1,6 +1,6 @@
 name:          type-eq
 category:      Type System
-version:       0.1.2
+version:       0.2
 author:        Gábor Lehel
 maintainer:    Gábor Lehel <illissius@gmail.com>
 homepage:      http://github.com/glehel/type-eq
@@ -14,15 +14,13 @@
 description:
     This package provides types and combinators to store and manipulate evidence of equality between types.
     .
-    To take advantage of kind-polymorphism when it is available but not require it, it is split into the following primary modules:
+    To take advantage of kind polymorphism when it is available but not require it, it is split into the following primary modules:
     .
         - @/Type.Eq/@: Types and combinators which can be kind-polymorphic if @PolyKinds@ are available, but are specific to kind @*@ otherwise.
     .
         - @/Type.Eq.Higher/@: Kind-monomorphic types and combinators of higher kind, up to @* -> * -> *@.
     .
-        - @/Type.Eq.Poly/@: Combinators that require kind-polymorphism. This module is only available if @PolyKinds@ are available.
-    .
-    Support for kind-polymorphism first appeared with GHC 7.4, but because it is too buggy to be practical, it will only be enabled with GHC 7.6.
+        - @/Type.Eq.Poly/@: Combinators that require kind polymorphism. This module is only available if @PolyKinds@ are available.
     .
     Major required extensions: @GADTs@, @TypeFamilies@ (for @~@), @Rank2Types@, @TypeOperators@
     .
@@ -62,7 +60,7 @@
         FlexibleContexts
 
     build-depends:
-        base >= 3.0 && < 4.6
+        base >= 3.0 && < 4.7
 
     exposed-modules:
         Type.Eq
@@ -80,17 +78,17 @@
         cpp-options: -DHAVE_DEPENDENCIES
         build-depends:
 -- Semigroupoid
-            semigroupoids >= 1.0 && < 1.4,
+            semigroupoids >= 1.0 && < 3.1,
 -- Groupoid
-            groupoids     >= 0.1 && < 0.3
+            groupoids     >= 0.1 && < 3.1
 -- Tensor
 --            data-lens     >= 2.9 && < 2.11
 
     if impl(ghc >= 7.2)
         other-extensions: Trustworthy
 
---    if impl(ghc >= 7.6)
---        exposed-modules:  Type.Eq.Poly
+    if impl(ghc >= 7.6)
+        exposed-modules:  Type.Eq.Poly
 --        other-extensions: PolyKinds, Unsafe
 
     include-dirs: .