<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Jun 17, 2014 at 9:43 PM, Adam Gundry <span dir="ltr"><<a href="mailto:adam@well-typed.com" target="_blank">adam@well-typed.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="">On 16/06/14 11:14, Niklas Haas wrote:<br>
> On Sun, 15 Jun 2014 21:47:52 +0200, Gábor Lehel <<a href="mailto:glaebhoerl@gmail.com">glaebhoerl@gmail.com</a>> wrote:<br>
>> In other words instances for forall-types, such as:<br>
>><br>
>> instance Foo (forall a. [a]) where ...<br>
>><br>
>> It feels obvious to me that there *would* be problems with this, but I'm<br>
>> curious about what, exactly, they are.<br>
>><br>
>> Could someone familiar with the matter either elaborate on them, or refer<br>
>> me to an existing explanation, a previous discussion, or something of the<br>
>> sort?<br>
>><br>
>> I *don't* have any kind of use case in mind, I'm merely seeking a better<br>
>> understanding of the type-system issues involved.<br>
>><br>
>> (I attempted Google, but didn't have much success.)<br>
>><br>
>> Thanks in advance.<br>
><br>
> It seems to me that it may be possible to get more information about<br>
> this by searching for issues related to ImpredicativeTypes, which seem<br>
> to be similar. (In fact, one could simulate instances like these by<br>
> implementing type classes using ImplicitParams + ImpredicativeTypes +<br>
> explicit instance records)<br>
<br>
</div>I don't think there has been much research on type inference for these<br>
kind of instances (though I'd be happy to be corrected). They are sort<br>
of like ImpredicativeTypes but worse, in that it is very hard to tell<br>
where the invisible type abstractions and applications go.<br>
<br>
For example, suppose we have these declarations:<br>
<br>
class Foo t where<br>
useFoo :: t -> Int<br>
<div class=""><br>
instance Foo (forall a. [a]) where<br>
</div> useFoo x = length (x :: [()])<br>
<br>
f = useFoo []<br>
<br>
The class and instance declarations make sense (the instance declaration<br>
ends up checking `useFoo` with a higher-rank type, but that's okay). But<br>
when inferring the type of `f`, we have<br>
<br>
useFoo :: forall t . Foo t => t -> Int<br>
<br>
and the typechecker needs to magically guess that<br>
<br>
t ~ forall a . [a]<br>
<br>
which is difficult. If there was some way of explicitly writing the<br>
type at which to instantiate `t`, for example<br>
<br>
f = useFoo @(forall a. [a]) []<br>
<br>
then it might be possible to make progress. [1]<br>
<br>
All this would, however, make perfect sense in System FC, once type<br>
abstractions and applications have been made explicit, and typeclass<br>
constraints have been replaced with visible dictionaries.<br></blockquote><div><br></div><div>I see. Thanks a lot! So there wouldn't be any issues with coherence, or with typechecking itself: only with inference?<br>
<br>Would the foralls in instances essentially be treated as another type constructor under this scenario?<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Hope this helps,<br>
<br>
Adam<br>
<br>
[1] <a href="https://ghc.haskell.org/trac/ghc/wiki/TypeApplication" target="_blank">https://ghc.haskell.org/trac/ghc/wiki/TypeApplication</a><br>
<span class="HOEnZb"><font color="#888888"><br>
<br>
--<br>
Adam Gundry, Haskell Consultant<br>
Well-Typed LLP, <a href="http://www.well-typed.com/" target="_blank">http://www.well-typed.com/</a><br>
</font></span><div class="HOEnZb"><div class="h5">_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br></div></div>