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

AntC anthony_clayden at clear.net.nz
Mon Jun 8 09:49:09 UTC 2015


> Richard Eisenberg writes:
> 
> This is all expected behavior. ...

Thank you Richard. So to be clear what it is that's expected:

For any class with overlapping instances
that calls on a Closed Type Family,
for all [**] instances,
expect to put a type equality constraint,
whose LHS is exactly the instance head,
and whose RHS is exactly the RHS
of the corresponding type family equation.
IOW expect the type equation to appear twice
(with `=` changed to `~`, modulo alpha renaming).

Note [**] not quite all instances.
The instance whose head is the first family equation
can have the constraint omitted.

> GHC's lazy overlap checking for class instances ...

Hmm? I don't think it's the lazy checking
of whether overlapping instances apply at a use site.
I think it's the eager checking
at the instance declaration.

> ... I'm afraid I don't see what can be improved here.

Two suggestions:
1. Automatically generate the type eq constraint.
   (Or at least suggest that as a Possible fix
    in the error message.)
2. Don't bother with a type family in such cases.
   Instead use Overlaps with FunDeps.
   (And needs UndecidableInstances.)

> > On Jun 6, 2015, at 2:04 AM, AntC wrote:
> > 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
> > 


More information about the Glasgow-haskell-users mailing list