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

[Richard Eisenberg]

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
>