Possible type-checker regression in GHC 8.0
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...
Trac metadata
Trac field | Value |
---|---|
Version | 8.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | highest |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | bgamari, simonpj |
Operating system | |
Architecture |