RE: Why isn't this Overlapping?

2017-04-18 Thread Anthony Clayden
> 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
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


RE: Why isn't this Overlapping?

2017-04-18 Thread Simon Peyton Jones via Glasgow-haskell-users
Moreover, as discussed in the user manual 
section<http://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html#overlapping-instances>,
 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:glasgow-haskell-users-boun...@haskell.org] 
On Behalf Of Iavor Diatchki
Sent: 18 April 2017 01:50
To: anthony_clay...@clear.net.nz
Cc: GHC Users Mailing List 
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 
mailto:anthony_clay...@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<mailto:Glasgow-haskell-users@haskell.org>
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-users&data=02%7C01%7Csimonpj%40microsoft.com%7Cc6be4bcfd23946f5f4fc08d485f4f93a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636280734593515972&sdata=Us2Ovast3dKEpNkfEDbejyBHGmGKh2ElAi6%2FqQY8iFE%3D&reserved=0>

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


Re: Why isn't this Overlapping?

2017-04-17 Thread 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@haskell.org
> >
>
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
> >
> 
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


Re: Why isn't this Overlapping?

2017-04-17 Thread 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_clay...@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
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


Why isn't this Overlapping?

2017-04-16 Thread Anthony Clayden
--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