Why isn't this Overlapping?

[Iavor Diatchki]

Hello,

these two instances really should be rejected as they violate the FD of the
class: we can derive `TypeEq a a True` using the first instance and `TypeEq
a a False` using the second one.  Unfortunately, the check that we are
using to validate FDs when `UndecidableInstances` is on, is not quite
correct (relevant tickets are #9210 and #10675 where there are similar
examples).

-Iavor



On Sun, Apr 16, 2017 at 12:13 AM, Anthony Clayden <
anthony_clayden at clear.net.nz> wrote:

> --ghc 7.10 or 8.0.1
>
> {-# LANGUAGE DataKinds, KindSignatures, GADTs,
>                           MultiParamTypeClasses,
> FunctionalDependencies, FlexibleInstances,
>                           UndecidableInstances,
> NoOverlappingInstances   #-}
>
> class TypeEq a a' (b :: Bool) | a a' -> b
>
> instance (b ~ True) => TypeEq a a b
> instance (b ~ False) => TypeEq a a' b
>
> Those two instance heads are nearly identical, surely they
> overlap?
> And for a type-level type equality test, they must be
> unifiable.
> But GHC doesn't complain.
>
> If I take off the FunDep, then GHC complains.
>
> AFAICT none of those extensions imply Overlaps,
> but to be sure I've put NoOverlapping.
>
>
> AntC
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20170417/a626e55a/attachment.html>