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....@gmail.com]
| Sent: 30 October 2010 00:58
| To: glasgow-haskell-users@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
| <simo...@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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
