Ambiguity check too eager with unconstrained type variable
Consider the following code:
{-# LANGUAGE TypeFamilies, DataKinds, GADTs #-}
type family F (b :: Bool) a
type instance F False a = a
type instance F True a = Int
data SBool :: Bool -> * where
SFalse :: SBool False
STrue :: SBool True
foo :: SBool b -> [F b a]
foo _ = []
GHC 7.6.1 compiles this code without a problem, and both foo STrue
and foo SFalse
are well typed and evaluate to []
. HEAD (even after yesterday's ambiguity patch for #7804 (closed)) does not compile this code, complaining about ambiguity. Here is the error:
Couldn't match type ‛F b a0’ with ‛F b a’
NB: ‛F’ is a type function, and may not be injective
The type variable ‛a0’ is ambiguous
Expected type: SBool b -> [F b a]
Actual type: SBool b -> [F b a0]
In the ambiguity check for:
forall (b :: Bool) a. SBool b -> [F b a]
In the type signature for ‛foo’: foo :: SBool b -> [F b a]
This is admittedly a weird corner case, but it's one I've run into in real(ish) code. On first glance, the type variable a
really is ambiguous in the type signature for foo
. But, it turns out that this is a benign ambiguity, because the variable is either ignored or, after type family simplification, appears in an inferrable location within the type.
Trac metadata
Trac field | Value |
---|---|
Version | 7.7 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |