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

Dan Doel dan.doel at gmail.com
Sun Jun 7 15:12:15 UTC 2015


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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20150607/5a4bc618/attachment.html>


More information about the Glasgow-haskell-users mailing list