Closed Type Families: type checking dumbness? [was: separate instance groups]

[adam vogt]

Hi,

AntC's f can be done without -XOverlappingInstances <
http://lpaste.net/7559485273839501312>, using the trick didn't work in
#9918. I'm not sure extra syntax is justified to clean up this rare case.

Regards,
Adam




On Sun, Jun 7, 2015 at 11:12 AM, Dan Doel <dan.doel at gmail.com> wrote:

> It seems to me the problem is that there's no way to define classes by
> consecutive cases to match the family definitions. I don't know what a good
> syntax for that would be, since 'where' syntax is taken for those. But it
> seems like it would correspond fill the hole here.
>
> On Sun, Jun 7, 2015 at 7:27 AM, Richard Eisenberg <eir at cis.upenn.edu>
> wrote:
>
>> This is all expected behavior. GHC's lazy overlap checking for class
>> instances simply cannot apply to type families -- it would be unsound. I'm
>> afraid I don't see what can be improved here.
>>
>> Richard
>>
>> On Jun 6, 2015, at 2:04 AM, AntC <anthony_clayden at clear.net.nz> wrote:
>>
>> >> From: AntC
>> >> Date: 2015-06-04 22:39:25 GMT
>> >>
>> >> Take the standard example for partial overlaps.
>> >> Suppose I have a class: ...
>> >
>> >> I'm also getting (in more complex examples)
>> >> GHC complaining it can't infer the types
>> >> for the result of f.
>> >> So now I'm having to put type equality
>> >> constraints on the class instances,
>> >> to assure it that F comes up with
>> >> the right type.
>> >
>> > In a reduced example, I'm still getting
>> > poor type checking. This is GHC 7.8.3.
>> > This seems so dumb, I'm suspecting a defect,
>> > It's similar to
>> > but much more glaring than:
>> > https://ghc.haskell.org/trac/ghc/ticket/10227
>> > https://ghc.haskell.org/trac/ghc/ticket/9918
>> >
>> > {-# LANGUAGE TypeFamilies,
>> >             FlexibleInstances
>> >   #-}
>> > module ClosedTypeFamily where
>> >
>> >    data Foo b c = Foo b c deriving (Eq, Read, Show)
>> >
>> >    type family F a    where
>> >      F (Foo Int c)  = Int        -- Foo Int is first instance
>> >      F (Foo b Char) = Char
>> >
>> >    class C a where f :: a -> F a
>> >
>> >    instance C (Foo Int c) where  -- compiles OK
>> >      f (Foo x _) = x
>> >
>> >    instance (F (Foo b Char) ~ Char) => C (Foo b Char) where
>> >      f (Foo _ y) = y
>> >
>> > needs the eq constraint. Without it, GHC complains:
>> >    Couldn't match expected type ‘F (Foo b Char)’
>> >                with actual type ‘Char’
>> >    Relevant bindings include
>> >      f :: Foo b Char -> F (Foo b Char)
>> >    In the expression: y
>> >    In an equation for ‘f’: f (Foo _ y) = y
>> >
>> > Note that if I change the sequence
>> > of the family instances for F,
>> > then GHC instead complains
>> > about the class instance for (Foo Int c).
>> >
>> > OK these are overlapping class instances.
>> > But GHC's usual behaviour
>> > (without closed type families)
>> > is to postpone complaining
>> > until and unless a usage
>> > (Foo Int Char) actually turns up.
>> >
>> > BTW if I put a first family instance
>> >      F (Foo Int Char) = Int
>> > to explicitly catch the overlap,
>> > then GHC complains about **both** class instances.
>> >
>> > Reminder [to Richard]
>> > I need not only types but also terms.
>> >
>> > AntC
>> > _______________________________________________
>> > Glasgow-haskell-users mailing list
>> > Glasgow-haskell-users at haskell.org
>> > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>> >
>>
>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20150607/7dd748ed/attachment.html>