Functional dependencies (for classes or type familes alike) can not refine given equality constraints
Motivation
Consider these two versions of foo
:
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE TypeFamilyDependencies #}
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE TypeOperators #}
import Data.Type.Equality
type family Foo a = r  r > a
fooTF :: (Foo a ~ Foo a') => a :~: a'
fooTF = Refl
class FooC a r  r > a
fooC :: (FooC a r, FooC a' r) => a :~: a'
fooC = Refl
However, both fail to type check (as of 8.1):
loop.hs:11:9: error:
• Could not deduce: a ~ a'
from the context: Foo a ~ Foo a'
bound by the type signature for:
fooTF :: forall a a'. (Foo a ~ Foo a') => a :~: a'
at loop.hs:10:137
‘a’ is a rigid type variable bound by
the type signature for:
fooTF :: forall a a'. (Foo a ~ Foo a') => a :~: a'
at loop.hs:10:137
‘a'’ is a rigid type variable bound by
the type signature for:
fooTF :: forall a a'. (Foo a ~ Foo a') => a :~: a'
at loop.hs:10:137
Expected type: a :~: a'
Actual type: a :~: a
• In the expression: Refl
In an equation for ‘fooTF’: fooTF = Refl
• Relevant bindings include
fooTF :: a :~: a' (bound at loop.hs:11:1)

11  fooTF = Refl
 ^^^^
loop.hs:16:8: error:
• Couldn't match type ‘a’ with ‘a'’
‘a’ is a rigid type variable bound by
the type signature for:
fooC :: forall a r a'. (FooC a r, FooC a' r) => a :~: a'
at loop.hs:15:141
‘a'’ is a rigid type variable bound by
the type signature for:
fooC :: forall a r a'. (FooC a r, FooC a' r) => a :~: a'
at loop.hs:15:141
Expected type: a :~: a'
Actual type: a :~: a
• In the expression: Refl
In an equation for ‘fooC’: fooC = Refl
• Relevant bindings include
fooC :: a :~: a' (bound at loop.hs:16:1)

16  fooC = Refl
 ^^^^
I would have thought that trying to decompose qualities like this is the very essence of what functional dependencies are for, so I am quite confused.
Proposal
Make this work. I'm not sure exactly what this entails, because I don't currently understand the difference between what functional dependencies do do and this.
I will note, however, that doing so perhaps makes existing issues with functional dependencies like #10675 worse because we could get unsound equality evidence to do unsafe coercions with.