Apartness checker should take impossible equalities into consideration #3329
Description
Given the following setup:
class Inject f g where
inj :: f -> g
prj :: g -> Maybe f
instance injectRefl :: Inject x x where
inj x = x
prj x = Just x
else instance injectLeft :: Inject l (Either l r) where
inj x = Left x
prj (Left x) = Just x
prj _ = Nothing
else instance injectRight :: Inject x r => Inject x (Either l r) where
inj x = Right (inj x)
prj (Right x) = prj x
prj _ = NothingWith the following scenario:
-- should work but doesn't
injL :: forall f g. f -> Either f g
injL = inj
injR :: forall f g. g -> Either f g
injR = injIn the case of injL the reason is that the apartness checker doesn't know that f can't possibly be Either f g because that would lead to an infinite type: Either (Either (Either ... g) g) g.
But injR shouldn't work, because we don't know that f /~ g.