diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
diff --git a/graphted.cabal b/graphted.cabal
--- a/graphted.cabal
+++ b/graphted.cabal
@@ -1,5 +1,5 @@
 name:                graphted
-version:             0.1.5.0
+version:             0.2.5.1
 synopsis:    Graph indexed monads.
 -- description: TODO
 homepage:            https://github.com/aaronfriel/graphted#readme
@@ -26,8 +26,10 @@
                      , Data.Functor.Graph
                      , Data.Pointed.Graph
                      , Data.GWrapped
+                     , Data.GWrappedIx
                      , Prelude.Graphted
   build-depends:       base >= 4.8 && < 5
+                     , indexed
   default-language:    Haskell2010
   ghc-options:         -fno-warn-partial-type-signatures
 
diff --git a/src/Control/Applicative/Graph.hs b/src/Control/Applicative/Graph.hs
--- a/src/Control/Applicative/Graph.hs
+++ b/src/Control/Applicative/Graph.hs
@@ -15,6 +15,9 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ImpredicativeTypes          #-}
+{-# LANGUAGE AllowAmbiguousTypes          #-}
 
 -- For the default Apply, Then, and But instances.
 {-# LANGUAGE UndecidableInstances  #-}
@@ -35,27 +38,45 @@
     type family Apply f (i :: p) (j :: p) :: p
     type instance Apply f i j = Combine f i j
 
+    -- | An invariant on the indexes of 'Apply'.
+    --
+    -- Default instance: @ApplyInv m i j = 'Inv' m i j@
+    type family ApplyInv f (i :: p) (j :: p) :: Constraint
+    type instance ApplyInv f i j = Inv f i j
+
     -- | The then operation ('*>') on the graph index.
     --
     -- Default instance: @'Then' f i j = 'Apply' f ('Fconst' f i) j@ 
     type family Then f (i :: p) (j :: p) :: p
     type instance Then f i j = Apply f (Fconst f i) j
 
+    -- | An invariant on the indexes of 'Then'.
+    --
+    -- Default instance: @ThenInv m i j = 'ApplyInv' m i j@
+    type family ThenInv f (i :: p) (j :: p) :: Constraint
+    type instance ThenInv f i j = ApplyInv f i j
+
     -- | The but operation ('<*') on the graph index.
     --
     -- Default instance: @But f i j = 'Apply' f ('Apply' f ('Pure' f) i) j@ 
     type family But f (i :: p) (j :: p) :: p
     type instance But f i j = Apply f (Apply f (Pure f) i) j
 
+    -- | An invariant on the indexes of 'But'.
+    --
+    -- Default instance: @ButInv m i j = 'ApplyInv' m i j@
+    type family ButInv f (i :: p) (j :: p) :: Constraint
+    type instance ButInv f i j = ApplyInv f i j
+
     -- | Sequential application ('<*>').
-    gap :: Inv f i j => f i (a -> b) -> f j a -> f (Apply f i j) b
+    gap :: ApplyInv f i j => f i (a -> b) -> f j a -> f (Apply f i j) b
 
     -- | Sequence actions, discarding the value of the first argument ('*>').
     --
     -- Default implementation requires the default instance of 'Then'.
     {-# INLINE gthen #-}
-    gthen :: Inv f i j => f i a -> f j b -> f (Then f i j) b
-    default gthen :: (Apply f (Fconst f i) j ~ Then f i j, Inv f (Fconst f i) j)
+    gthen :: ThenInv f i j => f i a -> f j b -> f (Then f i j) b
+    default gthen :: (Apply f (Fconst f i) j ~ Then f i j, ApplyInv f (Fconst f i) j, ThenInv f (Fconst f i) j)
                   => f i a -> f j b -> f (Then f i j) b
     gthen a b = (id `gconst` a) `gap` b
 
@@ -63,9 +84,12 @@
     --
     -- Default implementation requires the default instance of 'But'.
     {-# INLINE gbut #-}
-    gbut :: Inv f i j => f i a -> f j b -> f (But f i j) a
-    default gbut :: (Apply f (Apply f (Pure f) i) j ~ But f i j, Inv f (Pure f) i, Inv f (Apply f (Pure f) i) j)
+    gbut :: ButInv f i j => f i a -> f j b -> f (But f i j) a
+    default gbut :: (Apply f (Apply f (Pure f) i) j ~ But f i j, 
+                    ApplyInv f (Pure f) i, 
+                    ApplyInv f (Apply f (Pure f) i) j,
+                    ButInv f (Apply f (Pure f) i) j)
                  => f i a -> f j b -> f (But f i j) a
-    gbut a b = gpoint const `gap` a `gap` b
+    gbut a b = gpure const `gap` a `gap` b
 
     {-# MINIMAL gap #-}
diff --git a/src/Control/Graphted/Class.hs b/src/Control/Graphted/Class.hs
--- a/src/Control/Graphted/Class.hs
+++ b/src/Control/Graphted/Class.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP             #-}
+
 {- |
 Module      :  Control.Graph.Base
 Description :  Base type class for graph indexed types.
@@ -10,15 +12,13 @@
 
 -}
 
-{-# LANGUAGE CPP #-}
-
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE PolyKinds       #-}
 {-# LANGUAGE TypeFamilies    #-}
 
-module Control.Graphted.Class where
+module Control.Graphted.Class (Graphted (..), Constraint) where
 
-#if __GLASGOW_HASKELL__ >= 801
+#if MIN_VERSION_GLASGOW_HASKELL(8,0,1,0)
 import Data.Kind (Constraint)
 #else
 import GHC.Exts (Constraint)
diff --git a/src/Control/Monad/Graph.hs b/src/Control/Monad/Graph.hs
--- a/src/Control/Monad/Graph.hs
+++ b/src/Control/Monad/Graph.hs
@@ -34,19 +34,31 @@
     type family Bind m (i :: p) (j :: p) :: p
     type instance Bind m i j = Combine m i j
 
+    -- | An invariant on the indexes of 'Bind'.
+    --
+    -- Default instance: @BindInv m i j = 'Inv' m i j@
+    type family BindInv m (i :: p) (j :: p) :: Constraint
+    type instance BindInv m i j = Inv m i j
+
     -- | The join operation ('Control.Monad.join') on the graph index.
     --
     -- Default instance: @Join m i j = 'Bind' m i j@ 
     type family Join m (i :: p) (j :: p) :: p
     type instance Join m i j = Bind m i j
 
+    -- | An invariant on the indexes of 'Join'.
+    --
+    -- Default instance: @JoinInv m i j = 'BindInv' m i j@
+    type family JoinInv m (i :: p) (j :: p) :: Constraint
+    type instance JoinInv m i j = BindInv m i j
+
     -- | Sequentially compose two actions, with the second dependent on the first.
-    gbind :: Inv m i j => m i a -> (a -> m j b) -> m (Bind m i j) b
+    gbind :: BindInv m i j => m i a -> (a -> m j b) -> m (Bind m i j) b
 
     -- | Remove one level of nested structure. 
     --
     -- Default implementation requires the default instance of 'Join'.
     {-# INLINE gjoin #-}
-    gjoin :: (Inv m i j) => m i (m j b) -> m (Join m i j) b
-    default gjoin :: (Bind m i j ~ Join m i j, Inv m i j) => m i (m j b) -> m (Join m i j) b
+    gjoin :: (JoinInv m i j) => m i (m j b) -> m (Join m i j) b
+    default gjoin :: (Bind m i j ~ Join m i j, BindInv m i j) => m i (m j b) -> m (Join m i j) b
     gjoin x = x `gbind` id
diff --git a/src/Control/MonadOr/Graph.hs b/src/Control/MonadOr/Graph.hs
--- a/src/Control/MonadOr/Graph.hs
+++ b/src/Control/MonadOr/Graph.hs
@@ -10,6 +10,7 @@
 
 -}
 
+{-# LANGUAGE ConstraintKinds       #-}
 {-# LANGUAGE DefaultSignatures     #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -29,12 +30,18 @@
 --
 -- See the typeclassopedia <https://wiki.haskell.org/Typeclassopedia>.
 class GMonadZero m => GMonadOr (m :: p -> * -> *) where
-    
+
     -- | The or operation ('<|>') on the graph index.
     --
-    -- Default instance: @Or m i j = 'Combine' m i j@ 
+    -- Default instance: @Or m i j = 'Combine' m i j@
     type family Or m (i :: p) (j :: p) :: p
     type instance Or m i j = Combine m i j
 
+    -- | An invariant on the indexes of 'Or'.
+    --
+    -- Default instance: @OrInv m i j = 'Inv' m i j@
+    type family OrInv m (i :: p) (j :: p) :: Constraint
+    type instance OrInv m i j = Inv m i j
+
     -- | An associative binary operation ('<|>').
-    gorelse :: m i a -> m j a -> m (Or m i j) a
+    gorelse :: OrInv m i j => m i a -> m j a -> m (Or m i j) a
diff --git a/src/Control/MonadPlus/Graph.hs b/src/Control/MonadPlus/Graph.hs
--- a/src/Control/MonadPlus/Graph.hs
+++ b/src/Control/MonadPlus/Graph.hs
@@ -10,6 +10,7 @@
 
 -}
 
+{-# LANGUAGE ConstraintKinds       #-}
 {-# LANGUAGE DefaultSignatures     #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -32,9 +33,15 @@
 
     -- | The or operation ('mplus') on the graph index.
     --
-    -- Default instance: @Plus m i j = 'Combine' m i j@ 
+    -- Default instance: @Plus m i j = 'Combine' m i j@
     type family Plus m (i :: p) (j :: p) :: p
     type instance Plus m i j = Combine m i j
 
+    -- | An invariant on the indexes of 'Plus'.
+    --
+    -- Default instance: @PlusInv m i j = 'Inv' m i j@
+    type family PlusInv m (i :: p) (j :: p) :: Constraint
+    type instance PlusInv m i j = Inv m i j
+
     -- | An associative binary operation ('mplus').
-    gplus :: m i a -> m j a -> m (Plus m i j) a
+    gplus :: PlusInv m i j => m i a -> m j a -> m (Plus m i j) a
diff --git a/src/Data/GWrapped.hs b/src/Data/GWrapped.hs
--- a/src/Data/GWrapped.hs
+++ b/src/Data/GWrapped.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP           #-}
 {- |
 Module      :  Data.GWrapped
 Description :  Wrapped type constructors (typically Monad), graphted.
@@ -9,8 +10,6 @@
 
 -}
 
-{-# LANGUAGE CPP #-}
-
 {-# LANGUAGE GADTs         #-}
 {-# LANGUAGE PolyKinds     #-}
 {-# LANGUAGE TypeFamilies  #-}
@@ -21,12 +20,14 @@
 import Control.Graphted
 
 import Control.Applicative (Alternative (..))
-import Control.Monad (MonadPlus (..))
+import Control.Monad       (MonadPlus (..))
 -- import Data.Type.Equality (type (~~))
 
 -- | Wrap a non-indexed type constructor:
 newtype GWrapped (m :: * -> *) (p :: *) a = GWrapped { unG :: m a }
 
+newtype Singleton i = Singleton i
+
 -- | Lift an object to 'GWrapped'.
 liftG :: m a -> GWrapped m p a
 liftG = GWrapped
@@ -37,10 +38,13 @@
     type Combine (GWrapped m) i j = i
 
 instance Applicative f => GPointed (GWrapped f) where
-#if __GLASGOW_HASKELL__ >= 801
-    gpoint' = GWrapped . pure
+#if MIN_VERSION_GLASGOW_HASKELL(8,0,1,0)
+    type PureCxt (GWrapped f) i = ()
+    gpure' = GWrapped . pure
+
+    -- type Point (GWrapped f) i = Singleton i 
 #else
-    gpoint = GWrapped . pure
+    gpure = GWrapped . pure
 #endif
 
 instance Functor f => GFunctor (GWrapped f) where
@@ -48,6 +52,7 @@
     gconst f = GWrapped . ((<$) f) . unG
 
 instance Applicative f => GApplicative (GWrapped f) where
+    type But (GWrapped m) i j = i
     gap   (GWrapped m) (GWrapped k) = GWrapped $ m <*> k
     gthen (GWrapped m) (GWrapped k) = GWrapped $ m  *> k
     gbut  (GWrapped m) (GWrapped k) = GWrapped $ m <* k
diff --git a/src/Data/GWrappedIx.hs b/src/Data/GWrappedIx.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/GWrappedIx.hs
@@ -0,0 +1,95 @@
+{-# LANGUAGE CPP                  #-}
+
+{- |
+Module      :  Data.WrappedIxIx
+Description :  Wrapped type constructors (typically Monad), graphted.
+Copyright   :  (c) Aaron Friel
+License     :  BSD-3
+Maintainer  :  Aaron Friel <mayreply@aaronfriel.com>
+Stability   :  unstable
+Portability :  portable
+
+-}
+
+{-# LANGUAGE ConstraintKinds      #-}
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE InstanceSigs         #-}
+{-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Data.GWrappedIx where
+
+import Control.Graphted
+import Control.Monad.Indexed
+import Data.Functor.Indexed
+
+import Control.Applicative (Alternative (..))
+import Control.Monad       (MonadPlus (..))
+
+import GHC.Exts (Any)
+
+-- | Wrap a two-parameter-indexed type constructor:
+newtype WrappedIx (m :: * -> * -> * -> *) (p :: (*, *)) a = WrappedIx { unIx :: m (FstIx p) (SndIx p) a }
+
+type family FstIx p :: * where
+    FstIx '(i, j) = i
+
+type family SndIx p :: * where
+    SndIx '(i, j) = j
+
+instance Graphted (WrappedIx m) where
+    -- Hackish?
+    -- Ideally we would separate out 'Unit' and 'Pure', such that:
+    -- 
+    -- point :: GPointed f => forall t a. a -> f (Pure f t) a
+    --
+    -- And with impredicative types:
+    --
+    -- But f i j = Apply f (Apply f (forall t. Pure f t) i) j
+    type Unit (WrappedIx m) = '(Any, Any)
+
+    type Inv (WrappedIx m) i j = SndIx i ~ FstIx j
+
+    type Combine (WrappedIx m) i j = '( FstIx i, SndIx j )
+
+-- | Lift an object to 'WrappedIx'.
+liftIx :: m i j a -> WrappedIx m '(i, j) a
+liftIx = WrappedIx
+
+instance IxPointed f => GPointed (WrappedIx f) where
+#if MIN_VERSION_GLASGOW_HASKELL(8,0,1,0)
+    type PureCxt (WrappedIx f) i = FstIx i ~ SndIx i
+    gpure' = WrappedIx . ireturn
+
+    -- type Point (WrappedIx f) i = '(i, i)
+#else
+    gpure = WrappedIx . ireturn
+#endif
+
+instance IxFunctor f => GFunctor (WrappedIx f) where
+    gmap f = WrappedIx . imap f . unIx
+    gconst a = WrappedIx . imap (const a) . unIx
+
+instance IxApplicative f => GApplicative (WrappedIx f) where
+    type But   (WrappedIx m) l r = '( FstIx l, SndIx r )
+    gap   (WrappedIx m) (WrappedIx k) = WrappedIx $ m <<*>> k
+    gthen (WrappedIx m) (WrappedIx k) = WrappedIx $ m *>> k
+    gbut (WrappedIx m) (WrappedIx k) = WrappedIx $ m <<* k
+
+instance IxMonad m => GMonad (WrappedIx m) where
+    gbind (WrappedIx m) k = WrappedIx $ m >>>= unIx . k
+    gjoin (WrappedIx m) = WrappedIx $ m >>>= unIx
+
+instance IxMonadZero m => GMonadFail (WrappedIx m) where
+    gfail _ = WrappedIx imzero
+
+instance IxMonadZero m => GMonadZero (WrappedIx m) where
+    gzero = WrappedIx imzero
+
+instance IxMonadPlus m => GMonadPlus (WrappedIx m) where
+    type PlusInv (WrappedIx m) l r = ( FstIx l ~ FstIx r, SndIx l ~ SndIx r )
+    gplus (WrappedIx m) (WrappedIx k) = WrappedIx $ m `implus` k
diff --git a/src/Data/Pointed/Graph.hs b/src/Data/Pointed/Graph.hs
--- a/src/Data/Pointed/Graph.hs
+++ b/src/Data/Pointed/Graph.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                  #-}
 {- |
 Module      :  Control.Applicative.Graph
 Description :  Graph indexed applicative functors
@@ -10,47 +11,75 @@
 
 -}
 
-{-# LANGUAGE CPP #-}
-
+{-# LANGUAGE ConstraintKinds      #-}
+{-# LANGUAGE DefaultSignatures    #-}
 {-# LANGUAGE PolyKinds            #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE TypeFamilies         #-}
 
-#if __GLASGOW_HASKELL__ >= 801
+#if MIN_VERSION_GLASGOW_HASKELL(8,0,1,0)
 {-# LANGUAGE TypeApplications     #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE ImpredicativeTypes #-}
 #endif
 
-{-# LANGUAGE TypeFamilies         #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module Data.Pointed.Graph where
 
 import Control.Graphted.Class
 
+
 -- | Graph indexed pointed functor.
 class GPointed (f :: p -> * -> *) where
-    
+
     -- | The pure element of the graph index.
     type family Pure f :: p
     type instance Pure f = Unit f
 
     -- | Return a pointed functor indexed by the 'Pure' type instance ('pure').
     --
-    -- >>> :t gpoint @_ @(GWrapped Maybe) "Hello, World"
+    -- >>> :t gpure @_ @(GWrapped Maybe) "Hello, World"
     -- :: GWrapped Maybe () [Char]
-    gpoint :: forall a. a -> f (Pure f) a
+    gpure :: forall a. a -> f (Pure f) a
 
 -- This implementation will only work with type applications.
-#if __GLASGOW_HASKELL__ >= 801
-    gpoint = gpoint' @p @f @(Pure f)
+#if MIN_VERSION_GLASGOW_HASKELL(8,0,1,0)
+    default gpure :: PureCxt f (Pure f) => a -> f (Pure f) a
+    gpure = gpureAt @(Pure f)
 
+    -- | A constraint on generating a pure index from a free variable. Default is empty.
+    type family PureCxt f (i :: p) :: Constraint
+    type instance PureCxt f i = ()
+
+
     -- | Return a pointed functor indexed by a type 't' in the domain of 'p'.
     --
     -- Accessible with type applications, e.g.:
-    -- 
-    -- >>> :t gpoint' @_ @(GWrapped Maybe) @Int
-    -- gpoint' @_ @(GWrapped Maybe) @Int :: a -> GWrapped Maybe Int a
-    -- 
-    gpoint' :: forall t a. a -> f t a
+    --
+    -- >>> :t gpure' @_ @(GWrapped Maybe) @Int
+    -- gpure' @_ @(GWrapped Maybe) @Int :: a -> GWrapped Maybe Int a
+    --
+    gpure' :: forall t a. PureCxt f t => a -> f t a
 
-    {-# MINIMAL gpoint' #-}
+    {-# MINIMAL gpure' #-}
+
+{-
+    -- | A point element of the graph index.
+    type family Point f t = (i :: p) | i -> t
+    type instance Point f t = Unit f
+
+    gpoint :: forall a. a -> f (forall t. Point f t) a
+-}
+#endif
+
+#if MIN_VERSION_GLASGOW_HASKELL(8,0,1,0)
+-- | Return a pointed functor with a given type in the index.
+--
+-- Accessible with type applications, e.g.:
+-- 
+-- >>> :t gpureAt @Int 
+-- gpureAt @Int :: (GPointed f, PureCxt f Int) => a -> f Int a
+gpureAt :: forall t a f. (GPointed f, PureCxt f t) => a -> f t a
+gpureAt = gpure' @_ @_ @t
 #endif
diff --git a/src/Prelude/Graphted.hs b/src/Prelude/Graphted.hs
--- a/src/Prelude/Graphted.hs
+++ b/src/Prelude/Graphted.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                   #-}
 {- |
 Module      :  Prelude.Graphted
 Description :  Prelude with operators overridden by graph-indexed implementations
@@ -10,9 +11,7 @@
 
 -}
 
-{-# LANGUAGE CPP #-}
-
-#if __GLASGOW_HASKELL__ >= 801
+#if MIN_VERSION_GLASGOW_HASKELL(8,0,1,0)
 {-# LANGUAGE ApplicativeDo         #-}
 #endif
 
@@ -39,7 +38,7 @@
     (<**>), liftA, liftA2, liftA3,
     join, liftM, liftM2, liftM3, liftM4, liftM5, ap,
 
-#if __GLASGOW_HASKELL__ >= 801
+#if MIN_VERSION_GLASGOW_HASKELL(8,0,1,0)
     mapM_, sequence_,
 #endif
 
@@ -67,24 +66,24 @@
 (<$>) = fmap
 
 pure :: GPointed f => a -> f (Pure f) a
-pure = gpoint
+pure = gpure
 
-(<*>) :: (GApplicative f, Inv f i j) => f i (a -> b) -> f j a -> f (Apply f i j) b
+(<*>) :: (GApplicative f, ApplyInv f i j) => f i (a -> b) -> f j a -> f (Apply f i j) b
 (<*>) = gap
 
-(*>) :: (GApplicative f, Inv f i j) => f i a -> f j b -> f (Then f i j) b
+(*>) :: (GApplicative f, ThenInv f i j) => f i a -> f j b -> f (Then f i j) b
 (*>)= gthen
 
-(<*) :: (GApplicative f, Inv f i j) => f i a -> f j b -> f (But f i j) a
+(<*) :: (GApplicative f, ButInv f i j) => f i a -> f j b -> f (But f i j) a
 (<*) = gbut
 
 return :: GPointed m => a -> m (Pure m) a
-return = gpoint
+return = gpure
 
-(>>=) :: (GMonad m, Inv m i j) => m i a -> (a -> m j b) -> m (Bind m i j) b
+(>>=) :: (GMonad m, BindInv m i j) => m i a -> (a -> m j b) -> m (Bind m i j) b
 (>>=) = gbind
 
-(=<<) :: (GMonad m, Inv m i j) => (a -> m j b) -> m i a -> m (Bind m i j) b
+(=<<) :: (GMonad m, BindInv m i j) => (a -> m j b) -> m i a -> m (Bind m i j) b
 (=<<) = flip (>>=)
 
 zero :: GMonadZero m => m (Zero m) a
@@ -93,22 +92,22 @@
 fail :: GMonadFail m => String -> m (Fail m) a
 fail = gfail
 
-(<+>) :: (GMonadPlus f, Inv f i j) => f i a -> f j a -> f (Plus f i j) a
+(<+>) :: (GMonadPlus f, PlusInv f i j) => f i a -> f j a -> f (Plus f i j) a
 (<+>) = gplus
 
-(<|>) :: (GMonadOr f, Inv f i j) => f i a -> f j a -> f (Or f i j) a
+(<|>) :: (GMonadOr f, OrInv f i j) => f i a -> f j a -> f (Or f i j) a
 (<|>) = gorelse
 
 -- Simplified binding, what GHC.Base would like to do but cannot for backwards compatbility.
-(>>) :: (GApplicative m, Inv m i j) => m i a -> m j b -> m (Then m i j) b
+(>>) :: (GApplicative m, ThenInv m i j) => m i a -> m j b -> m (Then m i j) b
 (>>) = gthen
 
-join :: (GMonad m, Inv m i j) => m i (m j b) -> m (Join m i j) b
+join :: (GMonad m, JoinInv m i j) => m i (m j b) -> m (Join m i j) b
 join = gjoin
 
-(<**>) :: (GApplicative f, Inv f (Pure f) i1, Inv f ((Apply f (Pure f) i1)) i2) => f i1 a -> f i2 (a -> b)
+(<**>) :: (GApplicative f, _) => f i1 a -> f i2 (a -> b)
        -> f (Apply f (Apply f (Pure f) i1) i2) b
-(<**>) = liftA2 (flip ($))
+a <**> b = pure (flip ($)) <*> a <*> b
 
 liftA :: (GApplicative f, _) => (a -> b) -> f i1 a
       -> f (Apply f (Pure f) i1) b
@@ -159,15 +158,15 @@
        -> m (Apply m (Apply m (Apply m (Apply m (Fmap m i4) i3) i2) i1) i) b
 liftM5 f m1 m2 m3 m4 m5 = do { x1 <- m1; x2 <- m2; x3 <- m3; x4 <- m4; x5 <- m5; return (f x1 x2 x3 x4 x5) }
 
-#if __GLASGOW_HASKELL__ >= 801
-ap :: (GApplicative m, Inv m (Fmap m i) j) => m i (t -> b) -> m j t -> m (Apply m (Fmap m i) j) b
+#if MIN_VERSION_GLASGOW_HASKELL(8,0,1,0)
+ap :: (GApplicative m, _) => m i (t -> b) -> m j t -> m (Apply m (Fmap m i) j) b
 ap m1 m2 = do { x1 <- m1; x2 <- m2; return (x1 x2) }
 #else
 -- ap :: (GApplicative m, Inv m (Fmap m i) j) => m i (t -> b) -> m j t -> m (Apply m (Fmap m i) j) b
 ap m1 m2 = liftM m1 m2
 #endif
 
-#if __GLASGOW_HASKELL__ >= 801
+#if MIN_VERSION_GLASGOW_HASKELL(8,0,1,0)
 -- Recursive bindings may be impossible. This type is inferred, but not always satisfiable.
 -- We will need to implement our own folds and control flow.
 mapM_ :: (GApplicative m, Foldable t, Apply m (Fmap m i) (Pure m) ~ Pure m, _)