Type for "ways values can be different"
I think you are looking for a typed variant of anti-unification. Anti-unification can be described as follows. First, suppose that we have a grammar of terms as follows:

t ::= () | (t, t) | C t | X 


Here, () and (t, t) denote units and pairs, C t is a term with a leading constructor, and X is a term variable, which could be substituted for any term. 

The anti-unification problem says, if you give two terms t1 and t2, what is the least general term t such that there are substitutions s1 and s2 such that s1(t) = t1 and s2(t) = t2. 

As a concrete example, given two terms 

t1 = Cons(3, Cons(2, Cons(1, Nil)))
t2 = Cons(1, Cons(2, Cons(3, Nil)))


the anti-unification algorithm would return the anti-unifier 

t = Cons(X, Cons(2, Cons(Y, Nil)))


because the substitutions s1 = [X:3, Y:1] and s2 = [X:1, Y:3] applied to t would give you t1 and t2 back. As an aside, we needed to  specify "least general" because otherwise:

t' = Z 


with the substitutions s1 = [Z:t1] and s2 = [Z:t2] would do the trick. 

Anti-unification was invented by Gordon Plotkin, and is a delightfully simple algorithm. Assume you have an injective name-generation function gen $: \mathrm{Term} \times \mathrm{Term} \to \mathrm{Var}$. Then we can find an antiunifier as follows

antiunify ()       ()         = ()
antiunify (t1, t2) (t1', t2') = (antiunify t1 t1', antiunify t2 t2')
antiunify (C t)    (C t')     = C (antiunify t t')
antiunify t        t'         = gen(t, t') -- default: t and t' dissimilar 


Augmenting this algorithm to return the two substitutions s1 and s2 I leave as an exercise.