Type error in GHC7 but not in GHC6.12.3
Simon PeytonJones
simonpj at microsoft.com
Mon Nov 1 05:26:27 EDT 2010
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/enus/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: glasgowhaskellusers at haskell.org
 Cc: Simon PeytonJones
 Subject: Re: Type error in GHC7 but not in GHC6.12.3

 On Fri, Oct 29, 2010 at 5:42 PM, Simon PeytonJones
 <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 usbsafe (on the latest ghcHEAD (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
More information about the Glasgowhaskellusers
mailing list