[GHC] #12734: Missed use of solved dictionaries leads to context stack overflow (was: Unexpected context reduction stack overflow)

[GHC]

#12734: Missed use of solved dictionaries leads to context stack overflow
-------------------------------------+-------------------------------------
        Reporter:  danilo2           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Here's a cut-down version:
 {{{
 {-# 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          #-}


 module T12734 where

 import Prelude
 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 Type

 data Layer4 t l
 data TermStore

 -- Helpers: Stack

 data Stack lrs (t :: * -> *) where
     SLayer :: t l -> Stack ls t -> Stack (l ': ls) t
     SNull  :: Stack '[] t

 instance ( Con m (t l)
          , Con m (Stack ls t)) => Con m (Stack (l ': ls) t)
 instance Monad m               => Con m (Stack '[]       t)
 instance ( expr ~ Expr t lrs
          , Con m (TStk t lrs)) => Con m (Layer4 expr Type)


 newtype Expr  t lrs    = Expr (TStk t lrs)
 type TStk t lrs = Stack lrs (Layer4 (Expr t lrs))

 class Con m t


 -- HERE IS A FUNNY BEHAVIOR: the commented line raises context reduction
 stack overflow
 test_gr :: forall m t lrs bind.
            ( Con m (TStk t lrs)
             , bind ~ Expr t lrs
 --        ) => m (Expr t lrs)    -- Works with this line
           ) => m bind            -- Does not work with this line
 test_gr = undefined

 newtype KT (cls :: *) (t :: k) (m :: * -> *) (a :: *)
    = KT (IdentityT m a)

 test_ghc_err :: KT A '[Type] IO (Expr Net '[Type])
 test_ghc_err = test_gr @(KT A '[Type] IO) @_ @'[Type] @(Expr Net '[Type])
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12734#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler