[GHC] #11125: Typechecker can't infer StM m Bool ~ Bool from StM m a ~ a
#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
#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 (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by hvr): * component: Compiler => Compiler (Type checker) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11125#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nomeata): Are you sure that it indeed solves `StM m a ~ a`, because how could it? From reading the type signatures, I get the impression that `STM.alwaysSucceeds`’s is rather instantiated with `StM m a`. Note that {{{ alwaysSucceeds :: forall m a. (Monad m, MonadSTM m, MonadBaseControl STM m) => m a -> m () alwaysSucceeds inv = liftBaseWith $ \runInSTM -> STM.alwaysSucceeds (runInSTM inv :: STM (StM m a)) }}} compiles, but {{{ alwaysSucceeds :: forall m a. (Monad m, MonadSTM m, MonadBaseControl STM m) => m a -> m () alwaysSucceeds inv = liftBaseWith $ \runInSTM -> STM.alwaysSucceeds (runInSTM inv :: STM a) }}} does not (`Couldn't match type ‘a’ with ‘StM m a’`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11125#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by hvr): Btw, it may be useful to know the definition of the associated type `StM`: {{{#!hs class MonadBase b m => MonadBaseControl b m | m -> b where type StM m a :: * liftBaseWith :: (RunInBase m b -> b a) -> m a restoreM :: StM m a -> m a instance MonadBaseControl IO IO where type StM IO a = a liftBaseWith f = f id restoreM = return instance MonadBaseControl STM STM where type StM STM a = a liftBaseWith f = f id restoreM = return }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11125#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nikomi): The definitions of the original STM functions could also be useful: {{{#!hs always :: STM Bool -> STM () alwaysSucceeds :: STM a -> STM () }}} In my sample code I can see no relevant difference between {{{always}}} and {{{alwaysSucceeds}}} other than the argument type: m Bool vs. m a - conforming the argument types of the functions I want to lift: STM Bool vs. STM a. Yet the function with the generic type {{{a}}} compiles and the one with the specific type {{{Bool}}} does not - I have another sample where a usage of {{{m ()}}} fails to compile with exactly the same error right next to {{{m a}}}s that compile file (in those cases the base monad is IO, not STM) So from my limited point of view (with no insight into the TC) the difference is generic vs. specific. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11125#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
The difference with liftBase is that before lifting the base computation
#11125: Typechecker can't infer StM m Bool ~ Bool from StM m a ~ a -------------------------------------+------------------------------------- Reporter: nikomi | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by nomeata): * status: new => closed * resolution: => invalid Comment: More relevant types: {{{ liftBaseWith :: (RunInBase m b -> b a) -> m a type RunInBase m b = forall a. m a -> b (StM m a) }}} so the `runInST` function in your code changes the return type from `a` to `StM m a`. Note the docs: liftBaseWith captures the state of m. It then provides the base computation with a RunInBase function that allows running m computations in the base monad on the captured state. I’m confident that GHC is doing the right thing here, and it’s just `monad-control`’s API that is confusing here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11125#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11125: Typechecker can't infer StM m Bool ~ Bool from StM m a ~ a -------------------------------------+------------------------------------- Reporter: nikomi | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nikomi): Regardless of the API being confusing or not - using exactly the same thing with {{{a}}} vs. any specific type and one works but the other doesn't makes me rather confident something is fishy here :-( Any suggestions how to circumvent this non-bug? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11125#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
Regardless of the API being confusing or not - using exactly the same
#11125: Typechecker can't infer StM m Bool ~ Bool from StM m a ~ a -------------------------------------+------------------------------------- Reporter: nikomi | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nomeata): thing with a vs. any specific type and one works but the other doesn't makes me rather confident something is fishy here :-( `a` can be instantiated to `StM m a` (note that these are different `a`s), but `Bool` cannot be instantiated, and is different from `StM m Bool`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11125#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC