[Haskell-cafe] What are the problems with instances for polymorphic types?

[Gábor Lehel]

On Tue, Jun 17, 2014 at 9:43 PM, Adam Gundry <adam at well-typed.com> wrote:

> On 16/06/14 11:14, Niklas Haas wrote:
> > On Sun, 15 Jun 2014 21:47:52 +0200, Gábor Lehel <glaebhoerl at gmail.com>
> wrote:
> >> In other words instances for forall-types, such as:
> >>
> >>     instance Foo (forall a. [a]) where ...
> >>
> >> It feels obvious to me that there *would* be problems with this, but I'm
> >> curious about what, exactly, they are.
> >>
> >> Could someone familiar with the matter either elaborate on them, or
> refer
> >> me to an existing explanation, a previous discussion, or something of
> the
> >> sort?
> >>
> >> I *don't* have any kind of use case in mind, I'm merely seeking a better
> >> understanding of the type-system issues involved.
> >>
> >> (I attempted Google, but didn't have much success.)
> >>
> >> Thanks in advance.
> >
> > It seems to me that it may be possible to get more information about
> > this by searching for issues related to ImpredicativeTypes, which seem
> > to be similar. (In fact, one could simulate instances like these by
> > implementing type classes using ImplicitParams + ImpredicativeTypes +
> > explicit instance records)
>
> I don't think there has been much research on type inference for these
> kind of instances (though I'd be happy to be corrected). They are sort
> of like ImpredicativeTypes but worse, in that it is very hard to tell
> where the invisible type abstractions and applications go.
>
> For example, suppose we have these declarations:
>
>     class Foo t where
>        useFoo :: t -> Int
>
>     instance Foo (forall a. [a]) where
>         useFoo x = length (x :: [()])
>
>     f = useFoo []
>
> The class and instance declarations make sense (the instance declaration
> ends up checking `useFoo` with a higher-rank type, but that's okay). But
> when inferring the type of `f`, we have
>
>     useFoo :: forall t . Foo t => t -> Int
>
> and the typechecker needs to magically guess that
>
>     t ~ forall a . [a]
>
> which is difficult.  If there was some way of explicitly writing the
> type at which to instantiate `t`, for example
>
>     f = useFoo @(forall a. [a]) []
>
> then it might be possible to make progress. [1]
>
> All this would, however, make perfect sense in System FC, once type
> abstractions and applications have been made explicit, and typeclass
> constraints have been replaced with visible dictionaries.
>

I see. Thanks a lot! So there wouldn't be any issues with coherence, or
with typechecking itself: only with inference?

Would the foralls in instances essentially be treated as another type
constructor under this scenario?


>
> Hope this helps,
>
> Adam
>
> [1] https://ghc.haskell.org/trac/ghc/wiki/TypeApplication
>
>
> --
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140618/7d61e70b/attachment.html>