Why isn't this Overlapping?

[Anthony Clayden]

> On Tue Apr 18 00:50:20 UTC 2017, Iavor Diatchki wrote:
> 
> 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).
> 

Thanks Iavor, it was a propos those tickets I'm asking.
See my comments on #10675 -- we'll have to agree
to disagree on "not quite correct".
(If you want to ban instance selecting on type equality,
 you'll make a lot of people grumpy.)

My surprise here is why GHC doesn't complain about overlaps.
(Separately from whether it's doing the right thing.)

Here's another example [GHC 7.10] and here I agree
the FunDep consistency is well broken,
again needs UndecidableInstances:

{-# LANGUAGE      MultiParamTypeClasses, GADTs,
                               FunctionalDependencies,
                               FlexibleInstances,
UndecidableInstances   #-}

class C a b  | a -> b   where 
  foo :: a -> b -> String

instance C Int Bool where foo _ _ = "Bool called"

{- So far so good: no bare typevars in instance head;
    don't need UndecidableInstances for that   -}

instance  (b ~ Char) => C Int b where
  foo _ _ = "b ~ Char called"

I can't write that instance head `C Int Char`.
GHC complains inconsistent with FunDep [quite correct].

But I can call `foo (5 :: Int) 'c'`  ==> "b ~ Char called".

If I call `foo (5 :: Int) undefined` ==> GHC complains of
overlaps.
[I would say fair enough too, except ...]

If I change the instance to

instance {-# OVERLAPPABLE #-}  (b ~ Char) => C Int b where
..

Then `foo (5 :: Int) undefined` ==> "Bool called"

So GHC both uses the FunDep to improve the type,
and uses the improvement to select an instance;
and yet seems blind to FunDep inconsistencies in the
instance decls.


AntC

> 
> > On Sun, Apr 16, 2017 at 12:13 AM, Anthony Clayden 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
> >
>