## don't complain about type variable ambiguity when the expression is parametrically polymorphic

I'm not sure this is really a good idea, but it did come up in practice. Consider the following rather contrived program:

```
{-# 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.

## Trac metadata

Trac field | Value |
---|---|

Version | 8.1 |

Type | FeatureRequest |

TypeOfFailure | OtherFailure |

Priority | low |

Resolution | Unresolved |

Component | Compiler (Type checker) |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |