[GHC] #11125: Typechecker can't infer StM m Bool ~ Bool from StM m a ~ a

23 Nov 2015


      #11125: Typechecker can't infer StM m Bool ~ Bool from StM m a ~ a
-------------------------------------+-------------------------------------
           Reporter:  nikomi         |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 We found a problem where TC correctly infers StM m a ~ a but fails to
 infer StM m Bool ~ Bool in what appears to be the same situation. Here is
 a small sample showing the problem:
 {{{#!hs
 {-# LANGUAGE FlexibleContexts, FlexibleInstances  #-}

 module Problem where

 import qualified Control.Monad.STM              as STM
 import           Control.Monad.STM              (STM)
 import           Control.Monad.Trans.Control    (MonadBaseControl,
 liftBaseWith)

 class MonadSTM m where liftSTM :: STM a -> m a

 instance MonadSTM STM where liftSTM = id

 always :: (Monad m, MonadSTM m, MonadBaseControl STM m) => m Bool -> m ()
 always inv = liftBaseWith $ \runInSTM -> STM.always (runInSTM inv)

 alwaysSucceeds :: (Monad m, MonadSTM m, MonadBaseControl STM m) => m a ->
 m ()
 alwaysSucceeds inv = liftBaseWith $ \runInSTM -> STM.alwaysSucceeds
 (runInSTM inv)
 }}}
 The compiler error is
 {{{
 Problem.hs:15:54:
     Couldn't match type ‘Control.Monad.Trans.Control.StM m Bool’
                    with ‘Bool’
     Expected type: STM Bool
       Actual type: STM (Control.Monad.Trans.Control.StM m Bool)
     Relevant bindings include
       runInSTM :: Control.Monad.Trans.Control.RunInBase m STM
         (bound at Problem.hs:15:30)
       inv :: m Bool (bound at Problem.hs:15:8)
       always :: m Bool -> m () (bound at Problem.hs:15:1)
     In the first argument of ‘STM.always’, namely ‘(runInSTM inv)’
     In the expression: STM.always (runInSTM inv)
 }}}
 Function {{{always}}} can be made to compile by adding {{{StM m Bool ~
 Bool}}}:
 {{{#!hs
 always :: (Monad m, MonadSTM m, MonadBaseControl STM m, StM m Bool ~ Bool)
 => m Bool -> m ()
 }}}
 but then the problem is just shifted to the caller:
 {{{
    Couldn't match type ‘(Either [Char] Bool, Int)’ with ‘Bool’
    Expected type: Bool
      Actual type: StM (RSET TestData Int String STM) Bool
    In the second argument of ‘($)’, namely ‘always sanityCheck’
    In a stmt of a 'do' block: atomically $ always sanityCheck
    In the expression:
      do { atomically $ always sanityCheck;
           atomically $ updateTX 1 2;
           atomically stashSum }
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11125
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler