Disambiguate type variables using dictionaries

Consider this code:

type family TF t
type instance TF (Maybe a) = Maybe a

class Id f where
    idTF :: TF f -> TF f

instance Id (Maybe a) where
    idTF x = x

g = idTF (Just 'c')

Definition of g is rejected due to ambiguity:

Couldn't match expected type ‘TF f0’ with actual type ‘Maybe Char’
The type variable ‘f0’ is ambiguous
Relevant bindings include g :: TF f0 (bound at T6018.hs:18:1)
In the first argument of ‘idTF’, namely ‘(Just 'c')’
In the expression: idTF (Just 'c')

There are two ways to proceed:

1. Introduce Proxy argument and disambiguate f with explicit type annotation.
2. With injective type families (coming Real Soon Now) we can declare TF as injective and this code will compile. That obviously won't work if TF is not injective.

I think we could do better here. idTF is a type class function and when it is called GHC uses a concrete implementation from a dictionary. But notice that if we have the dictionary we could equally well use it to disambiguate f. In this example we call idTF with a Maybe Char argument, which means we are using Id (Maybe a) instance. Knowing this we could infer that f is Maybe a.

Trac metadata

Trac field	Value
Version	7.11
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture