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:
- Introduce
Proxyargument and disambiguatefwith explicit type annotation. - With injective type families (coming Real Soon Now) we can declare
TFas injective and this code will compile. That obviously won't work ifTFis 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 |