Opened 5 years ago

Closed 5 years ago

#10086 closed feature request (invalid)

Disambiguate type variables using dictionaries

Reported by: jstolarek Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.11
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Other Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.
  1. 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.

Change History (2)

comment:1 Changed 5 years ago by rwbarton

In this example we call idTF with a Maybe Char argument, which means we are using Id (Maybe a) instance.

But you can't infer that because there could be another instance TF (Either Int a) = Maybe a that you can't see. Or put differently, adding a new (compatible) instance for a type family is not supposed to break any uses of that type family.

If TF was a closed type family, then perhaps GHC could make this sort of inference. It amounts to checking injectivity "locally" for particular types as needed: i.e. check not that TF x = y has at most one solution for every y, but just for the particular y that is needed.

comment:2 Changed 5 years ago by jstolarek

Resolution: invalid
Status: newclosed

Looks like you're right. I'll close this as invalid.

Note: See TracTickets for help on using tickets.