Can't capture improvement of functional dependencies

Type Families with Class, Type Classes with Family discusses instance improvement with the example

class Collection c e | c -> e where
  empty :: c
  add   :: e -> c -> c

instance Collection [a] a where
  empty :: [a]
  empty = []

  add :: a -> [a] -> [a]
  add = (:)

I wondered how to express that x ~ Int can be deduced from Collection [Int] x using improvement, I first attempted using the constraints machinery:

data Dict c where
  Dict :: c => Dict c

newtype a :- b = Sub (a => Dict b)

but I'm not able to construct a term of type Collection [Int] x :- (Int ~ x) proving that Collection [Int] x entails Int ~ x:

ghci> Sub Dict :: Collection [Int] x :- (Int ~ x)

<interactive>:52:5: error:
    • Couldn't match type ‘x1’ with ‘Int’ arising from a use of ‘Dict’
      ‘x1’ is a rigid type variable bound by
        an expression type signature:
          forall x1. Collection [Int] x1 :- Int ~ x1
        at <interactive>:52:13
    • In the first argument of ‘Sub’, namely ‘Dict’
      In the expression: Sub Dict :: Collection [Int] x :- (Int ~ x)
      In an equation for ‘it’:
          it = Sub Dict :: Collection [Int] x :- (Int ~ x)

Is this due to overlapping instances or something?

Trac metadata

Trac field	Value
Version	8.0.1
Type	Task
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	None
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added FunctionalDependencies Ttask Trac import labels

Functional dependencies, as implemented in GHC, are used purely for disambiguating otherwise-ambiguous variables. That's it! In particular, a "given" fundep goes unused.

There is much room for improvement here, but it would take a dedicated soul, and quite likely an update to the core language, with proofs and possibly a paper.

Thanks for the response!

Interesting, since I'm maintaining notes on type classes what should I say about ​instance improvement, that it's not supported by the compiler or is it more complicated?

Instance improvement happens only when you have a "wanted" constraint -- that is, when you're typechecking a function call of f where f has a class constraint with a functional dependency.

Does that help?

See related discussion at http://stackoverflow.com/questions/34645745/can-i-magic-up-type-equality-from-a-functional-dependency/, #11534, and various other Trac tickets linked from there.

added Pnormal label