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@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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users