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
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
