#11339 closed bug (fixed)
Possible type-checker regression in GHC 8.0
Reported by: | hvr | Owned by: | simonpj |
---|---|---|---|
Priority: | highest | Milestone: | 8.0.2 |
Component: | Compiler (Type checker) | Version: | 8.0.1-rc1 |
Keywords: | Cc: | simonpj, bgamari, Artyom.Kazak | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | typecheck/should_compile/T11339, T11339b, T11339c, T11339d; partial-sigs/should_compile/T11339a |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
The following code (extracted from hackage:microlens) type-checks on GHC 7.10 but not on GHC 8.0/8.1:
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-} module Failing where import Control.Applicative ( Const(Const, getConst) ) import Data.Functor.Identity ( Identity(Identity) ) type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t failing :: forall s t a b . Traversal s t a b -> Traversal s t a b -> Traversal s t a b failing left right afb s = case pins t of [] -> right afb s _ -> t afb where -- t :: (a -> f b) -> f t -- TYPECHECKS with GHC 7.10, but not with GHC 8.x: Bazaar { getBazaar = t } = left sell s -- FAILS TO TYPECHECK with GHC 7.10 and GHC 8.x: -- t = getBazaar (left sell s) sell :: a -> Bazaar a b b sell w = Bazaar ($ w) pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a] pins f = getConst (f (\ra -> Const [Identity ra])) newtype Bazaar a b t = Bazaar { getBazaar :: (forall f. Applicative f => (a -> f b) -> f t) } instance Functor (Bazaar a b) where fmap f (Bazaar k) = Bazaar (fmap f . k) instance Applicative (Bazaar a b) where pure a = Bazaar $ \_ -> pure a Bazaar mf <*> Bazaar ma = Bazaar $ \afb -> mf afb <*> ma afb
The following error is emitted on GHC 8.0:
failing.hs:13:11: error: • Couldn't match type ‘f’ with ‘Const [Identity a]’ ‘f’ is a rigid type variable bound by the type signature for: failing :: forall (f :: * -> *). Applicative f => Traversal s t a b -> Traversal s t a b -> (a -> f b) -> s -> f t at failing.hs:11:1 Expected type: a -> Const [Identity a] b Actual type: a -> f b • In the first argument of ‘t’, namely ‘afb’ In the expression: t afb In a case alternative: _ -> t afb • Relevant bindings include t :: (a -> Const [Identity a] b) -> Const [Identity a] t (bound at failing.hs:18:26) sell :: a -> Bazaar a b b (bound at failing.hs:24:5) pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a] (bound at failing.hs:27:5) afb :: a -> f b (bound at failing.hs:11:20) right :: Traversal s t a b (bound at failing.hs:11:14) left :: Traversal s t a b (bound at failing.hs:11:9) failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b (bound at failing.hs:11:1)
I don't understand why Bazaar t = ...
vs t = getBazaar ...
makes a difference in GHC 7.10 at all. So I'm not sure if this is a regression or actually something that got fixed in GHC 8.0...
Change History (16)
comment:1 Changed 3 years ago by
Owner: | set to goldfire |
---|
comment:2 Changed 3 years ago by
This is truly bizarre.
Here are a few things I've learned:
- The module compiles with
-XNoMonomorphismRestriction
. This is actually correct behavior. The issue is that the inferred type oft
is quantified (byApplicative f
). The monomorphism restriction forbids this. So the new behavior is correct, I think.
- Sadly, adding
t :: Applicative f => (a -> f b) -> f t
, by itself, doesn't fix the problem
- The line that you say doesn't compile does indeed compile if you add
t :: Applicative f => (a -> f b) -> f t
- The line that you say doesn't compile does indeed compile if you add
-XMonoLocalBinds
.
- Saying
t :: _
emits no warning. I have no idea why.
Here is some interpretation of the above:
- Fact (2) is a consequence of the fact that GHC considers itself to be inferring a type for all pattern bindings, even if there is a complete type signature. (See
TcBinds.decideGeneralisationPlan
) I don't know why this is the case; I did not change this behavior. Visible type application does a little extra jiggery pokery when inferring types. SeeNote [Instantiate when inferring a type]
in TcBinds. This jiggery pokery is triggered because we're inferring the type oft
, even when a type signature is given.
- Facts (3) and (4) (really the fact that the commented line doesn't compile in the first place) is because we're in the quite rare scenario where
-XMonLocalBinds
is a good idea, even absent type families / GADTs. This is not the first such example, but I don't have a link to a previous one. PerhapsRankNTypes
should implyMonoLocalBinds
.
Bottom line: The only real bug in here is (2). It really should compile with the type signature, regardless of the monomorphism restriction. But it doesn't. However, the example as submitted should be rejected, I believe.
comment:3 Changed 3 years ago by
Keywords: | TypeInType added |
---|
comment:4 Changed 3 years ago by
Keywords: | TypeInType removed |
---|
On further thought, (5) from comment:2 is a bug, too.
In any case, this one isn't my fault. I'm responsible for point (1) in comment:2, but that's an improvement (the file submitted ought not to be accepted, because it runs afoul of the monomorphism restriction).
On the other hand, points (2) and (5), the real bugs, are around in 7.10. With 7.10.2,
module Mono where foo :: Show a => a -> String (foo) = show
fails unless you enable -XNoMonomorphismRestriction
. And
module Mono where foo :: _ (foo) = id
succeeds, with no warnings.
I conjecture that both problems are related to the fact that decideGeneralisationPlan
always infers for pattern bindings. But I haven't looked into it more than that.
comment:5 Changed 3 years ago by
Owner: | changed from goldfire to simonpj |
---|
comment:6 Changed 3 years ago by
Version: | 8.1 → 8.0.1-rc1 |
---|
comment:7 Changed 3 years ago by
Interestingly, the code in the Description typechecks fine in HEAD.
comment:8 Changed 3 years ago by
So it does. How maddening. I don't know why. I stand by my analysis that the original program should be rejected according to the monomorphism restriction.
comment:9 Changed 2 years ago by
Cc: | Artyom.Kazak added |
---|
comment:11 Changed 2 years ago by
Milestone: | 8.0.1 → 8.0.2 |
---|
This will not be addressed for 8.0.1. If you encounter this bug please add a type signature.
comment:12 Changed 2 years ago by
This also affects machines. This is the code that is affected (simplified version reproduced below):
{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} -- Simplified code from the machines package module Data.Machine.Fanout where class Semigroup a where (<>) :: a -> a -> a sconcat :: NonEmpty a -> a data NonEmpty a = a :| [a] -- | Witnessed type equality data Is a b where Refl :: Is a a -- | This is the base functor for a 'Machine' or 'MachineT'. -- -- Note: A 'Machine' is usually constructed from 'Plan', so it does not need to be CPS'd. data Step k o r = Stop | Yield o r | forall t. Await (t -> r) (k t) r -- | A 'MachineT' reads from a number of inputs and may yield results before stopping -- with monadic side-effects. newtype MachineT m k o = MachineT { runMachineT :: m (Step k o (MachineT m k o)) } -- | A @'ProcessT' m a b@ is a stream transducer that can consume values of type @a@ -- from its input, and produce values of type @b@ and has side-effects in the -- 'Monad' @m@. type ProcessT m a b = MachineT m (Is a) b continue :: ([b] -> r) -> [(a -> b, b)] -> Step (Is a) o r continue _ [] = Stop continue f ws = Await (f . traverse fst ws) Refl (f $ map snd ws) -- | Pack a 'Step' of a 'Machine' into a 'Machine'. encased :: Monad m => Step k o (MachineT m k o) -> MachineT m k o encased = MachineT . return semigroupDlist :: Semigroup a => ([a] -> [a]) -> Maybe a semigroupDlist f = case f [] of [] -> Nothing x:xs -> Just $ sconcat (x:|xs) -- | Share inputs with each of a list of processes in lockstep. Any -- values yielded by the processes are combined into a single yield -- from the composite process. fanout :: (Functor m, Monad m, Semigroup r) => [ProcessT m a r] -> ProcessT m a r fanout = MachineT . go id id where go waiting acc [] = case waiting [] of ws -> return . maybe k (\x -> Yield x $ encased k) $ semigroupDlist acc where k = continue fanout ws go waiting acc (m:ms) = runMachineT m >>= \v -> case v of Stop -> go waiting acc ms Yield x k -> go waiting (acc . (x:)) (k:ms) Await f Refl k -> go (waiting . ((f, k):)) acc ms -- | Share inputs with each of a list of processes in lockstep. If -- none of the processes yields a value, the composite process will -- itself yield 'mempty'. The idea is to provide a handle on steps -- only executed for their side effects. For instance, if you want to -- run a collection of 'ProcessT's that await but don't yield some -- number of times, you can use 'fanOutSteps . map (fmap (const ()))' -- followed by a 'taking' process. fanoutSteps :: (Functor m, Monad m, Monoid r) => [ProcessT m a r] -> ProcessT m a r fanoutSteps = MachineT . go id id where go waiting acc [] = case (waiting [], mconcat (acc [])) of (ws, xs) -> return . Yield xs $ encased (continue fanoutSteps ws) go waiting acc (m:ms) = runMachineT m >>= \v -> case v of Stop -> go waiting acc ms Yield x k -> go waiting (acc . (x:)) (k:ms) Await f Refl k -> go (waiting . ((f, k):)) acc ms
The workaround is to change the definitions of fanout
and fanoutSteps
to the following:
-- | Share inputs with each of a list of processes in lockstep. Any -- values yielded by the processes are combined into a single yield -- from the composite process. fanout :: forall m a r. (Functor m, Monad m, Semigroup r) => [ProcessT m a r] -> ProcessT m a r fanout = MachineT . go id id where go :: ([(a -> ProcessT m a r, ProcessT m a r)] -> [(a -> ProcessT m a r, ProcessT m a r)]) -> ([r] -> [r]) -> [ProcessT m a r] -> m (Step (Is a) r (ProcessT m a r)) go waiting acc [] = case waiting [] of ws -> return . maybe k (\x -> Yield x $ encased k) $ semigroupDlist acc where k = continue fanout ws go waiting acc (m:ms) = runMachineT m >>= \v -> case v of Stop -> go waiting acc ms Yield x k -> go waiting (acc . (x:)) (k:ms) Await f Refl k -> go (waiting . ((f, k):)) acc ms -- | Share inputs with each of a list of processes in lockstep. If -- none of the processes yields a value, the composite process will -- itself yield 'mempty'. The idea is to provide a handle on steps -- only executed for their side effects. For instance, if you want to -- run a collection of 'ProcessT's that await but don't yield some -- number of times, you can use 'fanOutSteps . map (fmap (const ()))' -- followed by a 'taking' process. fanoutSteps :: forall m a r. (Functor m, Monad m, Monoid r) => [ProcessT m a r] -> ProcessT m a r fanoutSteps = MachineT . go id id where go :: ([(a -> ProcessT m a r, ProcessT m a r)] -> [(a -> ProcessT m a r, ProcessT m a r)]) -> ([r] -> [r]) -> [ProcessT m a r] -> m (Step (Is a) r (ProcessT m a r)) go waiting acc [] = case (waiting [], mconcat (acc [])) of (ws, xs) -> return . Yield xs $ encased (continue fanoutSteps ws) go waiting acc (m:ms) = runMachineT m >>= \v -> case v of Stop -> go waiting acc ms Yield x k -> go waiting (acc . (x:)) (k:ms) Await f Refl k -> go (waiting . ((f, k):)) acc ms
comment:14 Changed 2 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → typecheck/should_compile/T11339, T11339b, T11339c, T11339d; partial-sigs/should_compile/T11339a |
This is a complicated ticket, and I've spent an unreasonably long time on the patch. But I'm very happy with the result.
There are a number of separate strands
- comment:12, I think
fanout
definitely needs a type signature forgo
. Look at the GADT pattern match onRefl
in theAwait
branch... GADTs always need a type signature! I have no idea how 7.10 compiled this program; maybe a bug!
- Difference between these two bindings:
Bazaar { getBazaar = t } = left sell s t = getBazaar (left sell s)
Well, the first falls under the Monomorphism Restriction, while the second does not. Simple as that.
- comment:4, item (2). I disagree:
foo :: Show a => a -> String (foo) = show
Here the binding falls under the monomorphism restriction, and cannot be rescued by a type signature. Test:typecheck/should_compile/T11339
• Overloaded signature conflicts with monomorphism restriction t :: forall (f :: * -> *). Applicative f => (a -> f b) -> f t
Adding-XNoMonomorhismRestriction
makes it fine. Test:typecheck/should_compile/T11339b
- comment:4, item (5), yes this was a bad bug
foo :: _ (foo) = id
Fixed: test ispartial-sigs/should_compile/T11339a
Tricky stuff.
comment:15 Changed 2 years ago by
Agreed about comment:4 item (2): it does hit the MR, when reading the Report closely. I hadn't known that the MR struck annotated variables if they are bound in a pattern binding.
Otherwise, hooray! This does seem all fixed now -- including rejecting (once again) the original program in the description. (That should be rejected as it correctly runs afoul of the MR.)
Thanks! :)
Richard,
I threw
git bisect
at this issue, and the winner was 2db18b8135335da2da9918b722699df684097be9 (aka Visible Type Application)! :-)Can you look at this and find out whether the type-checking failure is legitimate or not?