Overlapping families (specificity/degrees of freedom)

[Gabor Greif]

Errr. Messed this up, correction:

> minUnion :: DecEq a b -> Sing (a :: Symbol) -> Sing (b :: Symbol) -> Sing (MinUnion a b)
> minUnion (Right Refl) a b -> Cons a Nil
> minUnion (Left disproved) a b -> Cons a (Cons b Nil)

Anyway will GHC understand that a != b given (Left disproved) and thus
exclude the first case in MinUnion, which would in turn allow to
unambiguously select the second case of MinUnion?

Or is GHCs type-level logic still unprepared to see the (Inhabited ->
Uninhabited) type-level facts as negation?

    Gabor