content: {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE DeriveFunctor #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE NoMonomorphismRestriction #-}
  {-# LANGUAGE UndecidableInstances      #-}
  {-# LANGUAGE GADTs                     #-}
  {-# LANGUAGE PolyKinds                 #-}
  {-# LANGUAGE TypeApplications          #-}
  
  ---------------  The original bug report --------------
  --
  -- See T12734a for a smaller version
  
  module T12734 where
  
  import Prelude
  import Data.Kind
  import Control.Applicative
  import Control.Monad.Fix
  import Control.Monad.Trans.Identity
  import Control.Monad.Trans.Class
  import Control.Monad.IO.Class
  
  
  data A
  data B
  data Net
  data Ty
  
  data Layer4 t l
  data TermStore
  
  -- Helpers: Stack
  
  data Stack layers (t :: Type -> Type) where
      SLayer :: t l -> Stack ls t -> Stack (l ': ls) t
      SNull  :: Stack '[] t
  
  instance ( Constructor m (t l)
           , Constructor m (Stack ls t)) => Constructor m (Stack (l ': ls) t)
  instance Monad m                       => Constructor m (Stack '[]       t)
  
  
  -- Helpers: Expr
  
  newtype Expr  t layers    = Expr (TermStack t layers)
  type TermStack t layers = Stack layers (Layer4 (Expr t layers))
  
  
  -- Helpers: Funny typeclass
  
  class Monad m => Constructor m t
  
  instance ( Monad m, expr ~ Expr t layers, Constructor m (TermStack t layers)
           ) => Constructor m (Layer4 expr Ty)
  
  
  -- HERE IS A FUNNY BEHAVIOR: the commented line raises context reduction stack
  -- overflow
  test_gr ::
      ( Constructor m (TermStack t layers), Inferable A layers m, Inferable B t m
        , bind ~ Expr t layers
  --  ) => m (Expr t layers)
      ) => m bind
  test_gr = undefined
  
  
  -- Explicit information about a type which could be inferred
  
  class Monad m => Inferable (cls :: Type) (t :: k) m | cls m -> t
  
  newtype KnownTyx (cls :: Type) (t :: k) (m :: Type -> Type) (a :: Type) =
      KnownTyx (IdentityT m a)
    deriving (Show, Functor, Monad, MonadIO, MonadFix, MonadTrans,
              Applicative, Alternative)
  
  instance {-# OVERLAPPABLE #-} (t ~ t', Monad m) =>
    Inferable cls t (KnownTyx cls t' m)
  instance {-# OVERLAPPABLE #-} (Inferable cls t n, MonadTrans m, Monad (m n)) =>
    Inferable cls t (m n)
  
  
  runInferenceTx :: forall cls t m a. KnownTyx cls t m a -> m a
  runInferenceTx = undefined
  
  
  
  -- running it
  
  test_ghc_err :: (MonadIO m, MonadFix m)
          => m (Expr Net '[Ty])
  test_ghc_err = runInferenceTx @B  @Net
               $ runInferenceTx @A @'[Ty]
               $ (test_gr)
  