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