[GHC] #4295: Review higher-rank and impredicative types

[GHC]

#4295: Review higher-rank and impredicative types
---------------------------------+------------------------------------------
    Reporter:  simonpj           |        Owner:  simonpj     
        Type:  bug               |       Status:  new         
    Priority:  normal            |    Milestone:  7.2.1       
   Component:  Compiler          |      Version:  6.12.3      
    Keywords:                    |     Testcase:              
   Blockedby:                    |   Difficulty:              
          Os:  Unknown/Multiple  |     Blocking:              
Architecture:  Unknown/Multiple  |      Failure:  None/Unknown
---------------------------------+------------------------------------------

Comment(by simonpj):

 Here's an example from Bas van Dijk that needs a rigid type signature:
 {{{
 {-# LANGUAGE UnicodeSyntax
            , KindSignatures
            , RankNTypes
            , MultiParamTypeClasses
            , FunctionalDependencies
   #-}

 module Bas where

 import Data.List (find)

 data Ctx = Ctx
 data Device = Device
 data DeviceDesc = DeviceDesc

 data RegionalDeviceHandle (r ∷ * → *) = RegionalDeviceHandle
 data RegionT s (pr ∷ * → *) α = RegionT

 instance Monad pr ⇒ Monad (RegionT s pr) where
     return = undefined
     (>>=)  = undefined

 runRegionT ∷ (∀ s. RegionT s pr α) → pr α
 runRegionT = undefined

 openDevice ∷ Device → RegionT s pr (RegionalDeviceHandle (RegionT s pr))
 openDevice = undefined

 withDevice ∷ Monad pr
            ⇒ Device
            → (∀ s. RegionalDeviceHandle (RegionT s pr) → RegionT s pr α)
            → pr α
 withDevice dev f = runRegionT $ openDevice dev >>= f

 withDeviceWhich ∷ ∀ pr α
                 . Monad pr
                 ⇒ Ctx
                 → (DeviceDesc → Bool)
                 → (∀ s. RegionalDeviceHandle (RegionT s pr) → RegionT s pr
 α)
                 → pr α
 withDeviceWhich ctx p f = do devs ← return [Device]
                              useWhich devs withDevice p f

 useWhich ∷ ∀ k desc e (m ∷ * → *) α
          . (GetDescriptor e desc)
          ⇒ [e]
          → (e → k → m α)
          → (desc → Bool)
          → k
          → m α
 useWhich ds w p f = case find (p . getDesc) ds of
                       Nothing → error "not found"
                       Just d  → w d f

 class GetDescriptor α desc | α → desc, desc → α where
     getDesc ∷ α → desc

 instance GetDescriptor Device DeviceDesc where
     getDesc = undefined
 }}}
 See the thread at http://www.mail-archive.com/glasgow-haskell-
 users at haskell.org/index.html#18905

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