Quantcast

Why isn't this Overlapping?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Why isn't this Overlapping?

AntC
--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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: 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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Why isn't this Overlapping?

AntC
In reply to this post by AntC
> 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
> > [hidden email]
> >
>
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
> >
>
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

RE: Why isn't this Overlapping?

Haskell - Glasgow-haskell-users mailing list
In reply to this post by Iavor Diatchki

Moreover, as discussed in the user manual section, GHC doesn’t complain about overlapping instances at the instance decl, but rather where the instances are used. That’s why there is no overlap complaint here

 

Simon

 

 

From: Glasgow-haskell-users [mailto:[hidden email]] On Behalf Of Iavor Diatchki
Sent: 18 April 2017 01:50
To: [hidden email]
Cc: GHC Users Mailing List <[hidden email]>
Subject: Re: Why isn't this Overlapping?

 

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

 


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

RE: Why isn't this Overlapping?

AntC
In reply to this post by AntC
> On Tue Apr 18 10:31:30 UTC 2017, Simon Peyton Jones wrote:
>
> Moreover, as discussed in the user manual section,
> GHC doesn’t complain about overlapping instances at the
instance decl,
> but rather where the instances are used.

Thank you Simon, yes I knew that, so I'd written a usage
(just didn't bother putting it in the message ):

foo :: (TypeEq a a' b) => a -> a' -> String
foo _ _ = "blah"

x = foo 'c' "String"

> That’s why there is no overlap complaint here

I didn't get a complaint about `x`, contrary to what I
expected.

On trying again just now:

y = foo 'c' 'd'

GHC _does_ complain of overlap.

I apologise for the distraction.


AntC

>> On 18 April 2017 01:50, 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).


>>> 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.


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Loading...