#7812: Ambiguity check too eager with unconstrained type variable -----------------------------+---------------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Component: Compiler (Type checker) Version: 7.7 | Keywords: AmbiguityCheck Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: None/Unknown | Blockedby: Blocking: | Related: -----------------------------+---------------------------------------------- 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) 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. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7812 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler