Type error in GHC-7 but not in GHC-6.12.3
Hello, I'm updating my usb-safe package for GHC-7: darcs get http://code.haskell.org/~basvandijk/code/usb-safe It depends on the HEAD version of regions: darcs get http://code.haskell.org/~basvandijk/code/regions I think I'm suffering from the new implied MonoLocalBinds extension (I'm using GADTs) as described in: http://hackage.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7 However, I'm not sure this is the problem because I'm not using local bindings and use explicit type signatures everywhere. I try to make a small isolated example when I have time but for now let's use the actual definitions: The following function type-checked fine in GHC-6.12.3 but fails in GHC-7.1.20101027: 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 The error I get is: 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' These are the types and definitions of the other functions involved: useWhich ∷ ∀ k desc e (m ∷ * → *) α . (GetDescriptor e desc, MonadIO m) ⇒ [e] → (e → k → m α) → (desc → Bool) → k → m α useWhich ds w p f = case find (p ∘ getDesc) ds of Nothing → throw USB.NotFoundException Just d → w d f withDevice ∷ MonadCatchIO pr ⇒ USB.Device → (∀ s. RegionalDeviceHandle (RegionT s pr) → RegionT s pr α) → pr α withDevice dev f = runRegionT $ openDevice dev >>= f Note that when I inline the definition of useWhich it type-checks fine: withDeviceWhich ctx p f = do devs ← liftIO $ USB.getDevices ctx case find (p ∘ getDesc) devs of Nothing → throw USB.NotFoundException Just d → withDevice d f Since I'm not using local bindings and use explicit type signatures everywhere, I'm not sure MonoLocalBinds is the problem. Note that other applications of useWhich which also use RankNTypes type-check just fine in both GHC-6.12.3 and GHC-7.1.20101027: ------------------------------------------------------------------------------- setConfigWhich ∷ ∀ pr cr α . (pr `AncestorRegion` cr, MonadCatchIO cr) ⇒ RegionalDeviceHandle pr → (USB.ConfigDesc → Bool) → (∀ sCfg. ConfigHandle sCfg → cr α) → cr α setConfigWhich h = useWhich (getConfigs h) setConfig getConfigs ∷ RegionalDeviceHandle r → [Config r] setConfig ∷ ∀ pr cr α . (pr `AncestorRegion` cr, MonadCatchIO cr) ⇒ Config pr → (∀ sCfg. ConfigHandle sCfg → cr α) → cr α ------------------------------------------------------------------------------- withInterfaceWhich ∷ ∀ pr sCfg α . MonadCatchIO pr ⇒ ConfigHandle sCfg → (USB.Interface → Bool) → (∀ s. RegionalInterfaceHandle sCfg (RegionT s pr) → RegionT s pr α) → pr α withInterfaceWhich h = useWhich (getInterfaces h) withInterface getInterfaces ∷ ConfigHandle sCfg → [Interface sCfg] withInterface ∷ ∀ pr sCfg α . MonadCatchIO pr ⇒ Interface sCfg → (∀ s. RegionalInterfaceHandle sCfg (RegionT s pr) → RegionT s pr α) → pr α ------------------------------------------------------------------------------- setAlternateWhich ∷ ∀ pr cr sCfg α . (pr `AncestorRegion` cr, MonadCatchIO cr) ⇒ RegionalInterfaceHandle sCfg pr → (USB.InterfaceDesc → Bool) → (∀ sAlt. AlternateHandle sAlt pr → cr α) → cr α setAlternateWhich h = useWhich (getAlternates h) setAlternate getAlternates ∷ RegionalInterfaceHandle sCfg r → [Alternate sCfg r] setAlternate ∷ ∀ pr cr sCfg α . (pr `AncestorRegion` cr, MonadCatchIO cr) ⇒ Alternate sCfg pr → (∀ sAlt. AlternateHandle sAlt pr → cr α) → cr α ------------------------------------------------------------------------------- I'm happy to provide more info when needed. Regards, Bas
On Fri, Oct 29, 2010 at 5:42 PM, Simon Peyton-Jones <simonpj@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
(resending this to the list because this failed yesterday because of the mailinglist downtime) On Sat, Oct 30, 2010 at 1:57 AM, Bas van Dijk <v.dijk.bas@gmail.com> wrote:
I could isolate it a bit more if you want.
And so I did. The following is another instance of the problem I'm having but set in a more familiar setting: {-# LANGUAGE RankNTypes #-} import Control.Monad.ST foo :: (forall s. ST s a) -> a foo st = ($) runST st Couldn't match expected type `forall s. ST s a' with actual type `ST s a' In the second argument of `($)', namely `st' Note that: 'foo st = runST st' type checks as expected. Surprisingly 'foo st = runST $ st' also type checks! I find the latter surprising because according to the report[1]: e1 op e2 = (op) e1 e2. So either both should type check or both should fail. I guess that a RULE somewhere eliminates the ($) before the type-checker kicks in. I do find that a little strange because I thought RULES where applied after type checking. Regards, Bas [1] http://www.haskell.org/onlinereport/exps.html#operators
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@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 | <simonpj@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
participants (2)
-
Bas van Dijk -
Simon Peyton-Jones