Review higher-rank and impredicative types

[simonpj]

The ticket is a placeholder to remind me to work through the test cases for impredicative and higher rank types in the new typechecker. For now, I'm marking many of them as expect_broken on this ticket, although I think many of them really should fail.

• tc150
• tc194
• tcfail198
• tcfail174
• tcfail165
• tcfail145
• tcfail104
• tc211
• indexed-types/should_compile/T4120
• simpl017
• Many tests in boxy/ (see also #1330 for Church2)
• #2193
• #2846
• #4347
•  Lennart's blog post has an interesting use case of impredicative polymorphism; it worked in 7.0, but alas not in the new typechecker.

[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@haskell.org/index.html#18905

[simonpj]

See also #5596 (impredicative).

[benmos]

Just a note that I've also been tripped up by #5596. (I was initially very puzzled why my own version of ($) copied and pasted from Prelude with the same pragmas didn't work the same as the built-in one...)