Type error in GHC-7 but not in GHC-6.12.3

[Simon Peyton-Jones]

OK now I see.  

You are using impredicative polymorphism.  As I mentioned in my last message I've simplified the treatment of impredicativity to follow (more or less) QML: http://research.microsoft.com/en-us/um/people/crusso/qml/


In the call to useWhich

	useWhich devs withDevice p f

you can see that 
	withDevice ∷ Monad pr
           ⇒ Device
           → (∀ s. RegionalDeviceHandle (RegionT s pr) → RegionT s pr α)
           → pr α

	useWhich ∷ ∀ k desc e (m ∷ * → *) α
         . (GetDescriptor e desc)
         ⇒ [e]
         → (e → k → m α)
         → (desc → Bool)
         → k
         → m α

So it follows that you must instantiate 
	k = (∀ s. RegionalDeviceHandle (RegionT s pr) → RegionT s pr α)
Arguably GHC should complain at this point unless you use -XImpredicativePolymorphism, but it doesn't.
       
Now, the arguemnnt 'f' in the call, is apparently compatible with this type *except* that f's type is instantiated.  What you want is a way to say "don't instantiate f here".  QML provides a way to do that, via a "rigid" type signature, but GHC currently does not.  (Pressure of time, plus impredicativity is a somewhat obscure feature.)

So I guess I should implement rigid type signatures.  As ever the problem is syntax.

To work around this, use a newtype to the forall in the last argument of useWhich.

Simon

	
| -----Original Message-----
| From: Bas van Dijk [mailto:v.dijk.bas at gmail.com]
| Sent: 30 October 2010 00:58
| To: glasgow-haskell-users at haskell.org
| Cc: Simon Peyton-Jones
| Subject: Re: Type error in GHC-7 but not in GHC-6.12.3
| 
| On Fri, Oct 29, 2010 at 5:42 PM, Simon Peyton-Jones
| <simonpj at microsoft.com> wrote:
| > That looks odd.
| >
| > Can you isolate it for us?  The easiest thing is usually to start with the
| offending code:
| > withDeviceWhich ∷
| >  ∀ pr α
| >  . MonadCatchIO pr
| >  ⇒ USB.Ctx
| >  → (USB.DeviceDesc → Bool)
| >  → (∀ s. RegionalDeviceHandle (RegionT s pr) → RegionT s pr α)
| >  → pr α
| > withDeviceWhich ctx p f = do
| >  devs ← liftIO $ USB.getDevices ctx
| >  useWhich devs withDevice p f
| >
| > Now add local definitions for each of the functions mentioned, with definition foo
| = undefined.
| >
| > useWhich ∷
| >  ∀ k desc e (m ∷ * → *) α
| >  . (GetDescriptor e desc, MonadIO m)
| >  ⇒ [e]
| >  → (e → k → m α)
| >  → (desc → Bool)
| >  → k
| >  → m α
| > useWhich = undefined.
| >
| > Now all you need is the types involved, and you can probably define them as
| >
| > data RegionT s pr a
| >
| > etc
| >
| > That should give a standalone test case.
| >
| > Thanks!
| >
| > SImon
| >
| 
| Ok, Here's the more isolated program which still gives the same error
| as the full usb-safe (on the latest ghc-HEAD (7.1.20101029)):
| 
| 
| USBSafeTest.hs:39:57:
|     Couldn't match expected type `forall s.
|                                   RegionalDeviceHandle (RegionT s pr)
| -> RegionT s pr α'
|                 with actual type `RegionalDeviceHandle (RegionT s pr)
|                                   -> RegionT s pr α'
|     In the fourth argument of `useWhich', namely `f'
|     In the expression: useWhich devs withDevice p f
|     In the expression:
|       do { devs <- return [Device];
|            useWhich devs withDevice p f }
| 
| 
| {-# LANGUAGE UnicodeSyntax
|            , KindSignatures
|            , RankNTypes
|            , MultiParamTypeClasses
|            , FunctionalDependencies
|   #-}
| 
| 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
| 
| 
| I could isolate it a bit more if you want.
| 
| Thanks,
| 
| Bas