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:


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

{-# LANGUAGE ScopedTypeVariables, MultiParamTypeClasses #-}
module Main

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
      f :: forall v . TokStream -> ST v (Either ParseError ())
      f = runPT c () "<sourcefile>"

doesnt :: [Char] -> Either ParseError ()
doesnt = runST . f . TokStream
      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.

Change History (1)

comment:1 Changed 5 years ago by simonpj

Resolution: invalid
Status: newclosed

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 $(.) respectively at 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.

Note: See TracTickets for help on using tickets.