#12362: don't complain about type variable ambiguity when the expression is parametrically polymorphic -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: Type: feature | Status: new request | Priority: low | Milestone: Component: Compiler | Version: 8.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I'm not sure this is really a good idea, but it did come up in practice. Consider the following rather contrived program: {{{#!hs {-# LANGUAGE TypeFamilies, RankNTypes, ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications #-} module E where type family T a type instance T Int = Char type instance T String = Char type instance T Bool = () newtype FT a = FT [T a] m :: forall a. (forall x. T x -> Int) -> FT a -> [Int] m f (FT xs) = map f xs }}} GHC rejects it with the error: {{{ E.hs:14:21: error: • Couldn't match type ‘T a’ with ‘T x0’ Expected type: [T x0] Actual type: [T a] NB: ‘T’ is a type function, and may not be injective The type variable ‘x0’ is ambiguous • In the second argument of ‘map’, namely ‘xs’ In the expression: map f xs In an equation for ‘m’: m f (FT xs) = map f xs • Relevant bindings include xs :: [T a] (bound at E.hs:14:9) m :: (forall x. T x -> Int) -> FT a -> [Int] (bound at E.hs:14:1) }}} The problem seems to be that GHC doesn't know at what type to instantiate `f`, because it can't conclude from the argument of `f` being `T a` that the type parameter of `f` needs to be `x`. In fact, `T` here really is not injective, so if `a` is `Int`, `x` could just as well be `String`. However, in this case the ambiguity doesn't actually matter. If `f @Int` and `f @String` have the same type because `T Int ~ T String`, then they are actually the same value too by parametricity, because there is no class constraint on `x`. Since GHC prints a message saying that `T` is not known to be injective, it sounds like it knows about the possible solution `x0 = a`. So it could just pick it, and accept the original program. With TypeApplications I can just specify the intended value of `x` by writing {{{ m f (FT xs) = map (f @a) xs }}} which is a reasonable workaround in my real use case also. Interestingly I can't seem to achieve the same thing without TypeApplications without adding a proxy argument to `f`, which I don't much want to do. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12362 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler