[GHC] #4347: Asymmetry of (impredicative) instantiation/higher rank types

[GHC]

#4347: Asymmetry of (impredicative) instantiation/higher rank types
----------------------------------------+-----------------------------------
    Reporter:  dolio                    |        Owner:                           
        Type:  bug                      |       Status:  new                      
    Priority:  normal                   |    Milestone:  7.4.1                    
   Component:  Compiler (Type checker)  |      Version:  7.1                      
    Keywords:                           |     Testcase:                           
   Blockedby:                           |   Difficulty:                           
          Os:  Linux                    |     Blocking:                           
Architecture:  x86_64 (amd64)           |      Failure:  GHC rejects valid program
----------------------------------------+-----------------------------------
Changes (by simonpj):

 * cc: dimitris@… (added)


Comment:

 Here's a version that works
 {{{
 type Blob = (forall a. Random a => (forall g. RandomGen g => g -> (a, g))
 -> IO a)

 dumbTrick :: IO Blob
 dumbTrick = do
     gen <- newMVar =<< newStdGen
     let apply :: forall b. Random b => (forall g'. RandomGen g' => g' ->
 (b, g')) -> IO b
         apply f = modifyMVar gen (\x -> (\(a, b) -> return (b, a)) (f x))
     (return :: Blob -> IO Blob) apply
 --     ((return apply) :: IO Blob)
 }}}
 The `(return :: Blob -> IO Blob)` fixes the instantiation of `return ::
 forall a. a -> IO a` to instantiate `a := Blob`, and then all is well.  Bu
 the commented out line does not work, becuase apply is implicitly
 instantiated.

 What GHC lacks at the moment is a "rigid type signature" in the QML sense.
 If we have that we could write
 {{{
      return (apply ! :: Blob)
 }}}
 where I'm using "`!` to indicate a rigid signature.  The "rigid" part
 means that the polymorphic type is not instantiated, so all will be well.

 I plan to add rigid type signatures to GHC, but I keep hesitating over
 syntax.  It's quite attractive to use `(apply ::: Blob)`, but `(:::)` is
 currently available for users so it seems bad to steal it.  But maybe
 worth it.  Other ideas welcome.

 Read the QML paper: it's well explained.

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