Opened 5 years ago

Closed 5 years ago

## #5596 closed bug (invalid)

# "f c = a $ b c", "f = a . b" does not.

Reported by: | guest | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler (Type checker) | Version: | 7.2.1 |

Keywords: | Cc: | ||

Operating System: | Linux | Architecture: | x86_64 (amd64) |

Type of failure: | GHC rejects valid program | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

the following code produces a type error, and i think it shouldn't:

{-# LANGUAGE ScopedTypeVariables, MultiParamTypeClasses #-} module Main where import Control.Monad.ST import Data.STRef import Text.Parsec type P v a = ParsecT TokStream () (ST v) a data TokStream = TokStream [Char] instance Stream TokStream (ST v) Char where uncons (TokStream []) = return Nothing uncons (TokStream (t:ts)) = return (Just (t, TokStream ts)) c :: P v () c = return () works :: [Char] -> Either ParseError () works toks = runST $ f $ TokStream toks where f :: forall v . TokStream -> ST v (Either ParseError ()) f = runPT c () "<sourcefile>" doesnt :: [Char] -> Either ParseError () doesnt = runST . f . TokStream where f :: forall v . TokStream -> ST v (Either ParseError ()) f = runPT c () "<sourcefile>"

doesnt should be equivalent to works, but works works and doesnt doesn't. the type error:

Couldn't match expected type `forall s. ST s (Either ParseError ())' with actual type `ST v0 (Either ParseError ())' Expected type: TokStream -> forall s. ST s (Either ParseError ()) Actual type: TokStream -> ST v0 (Either ParseError ()) In the first argument of `(.)', namely `f' In the second argument of `(.)', namely `f . TokStream'

I tried this on 7.2.1 and 7.0.3. may be related to tickets 4347 or 4310, but I don't know enough about the ghc type engine to tell.

**Note:**See TracTickets for help on using tickets.

Yes, this is bad, but it's because GHC is trying to help!

Fundamentally, neither

`(runST $ f)`

nor`(runST . f)`

should work, because both require calling`($)`

or`$(.)`

respectivelyat a polymorpic type; that is, they both require impredicative polymoprhism. (In earlier versions of GHC Dimitrios and I implemented our boxy-type paper, but the implementation was grotesquely complicated and unpredicatable, so we rolled it back.)However, the idiom

`(runST $ do ...blah...)`

had become very common in practice, so I added a TOTALLY AD-HOC special case typing rule, for terms of the form`(e1 $ e2)`

. In this special se there is no problem with impredicativity, so away we go. And that's why the two differ: there is no special case for`(.)`

.I could compound the problem by adding a special typing rule for

`(e1 . e2)`

as well, but I'm not sure that would really be an improvement.The special typing rule for

`($)`

isn't even documented in the manual, because I didn't really want to encourage people to exploit it. It's a secret feature.Cf #4295.

I'll close this as invalid, but acknowledging that things are not great.