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?