Ambiguity check too eager in presence of RankNTypes and TypeFamilies
The following code compiles in 7.6.1 but not in 7.7:
{-# LANGUAGE TypeFamilies, RankNTypes #-}
type family F f a
type family G f
data Proxy a = P
sDFMap :: (forall a. Proxy f -> Proxy a -> Proxy (F f a)) -> Proxy (G f)
sDFMap _ = P
Here is the error message:
Couldn't match type `G f0' with `G f'
NB: `G' is a type function, and may not be injective
The type variable `f0' is ambiguous
Expected type: (forall a. Proxy f -> Proxy a -> Proxy (F f a))
-> Proxy (G f)
Actual type: (forall a. Proxy f0 -> Proxy a -> Proxy (F f0 a))
-> Proxy (G f0)
In the ambiguity check for:
forall f.
(forall a. Proxy f -> Proxy a -> Proxy (F f a)) -> Proxy (G f)
In the type signature for `sDFMap':
sDFMap :: (forall a. Proxy f -> Proxy a -> Proxy (F f a))
-> Proxy (G f)
It is true that sDFMap
is sometimes ambiguous, but it is not always ambiguous. For example, if we have
foo :: Proxy Bool -> Proxy a -> Proxy (F Bool a)
foo _ _ = P
bar = sDFMap foo
the call to sDFMap
is well defined, with f ~ Bool
. If the type signature for foo
did not specify the value of f
, the call to sDFMap
would indeed be ambiguous and should be rejected. GHC 7.6.1 does catch the error when the type of foo
uses a variable instead of Bool
.
Trac metadata
Trac field | Value |
---|---|
Version | 7.7 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |