Re: Why isn't this Overlapping?

17 Apr 2017

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