Re: Overlapping families (specificity/degrees of freedom)

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