On Tue, Jun 17, 2014 at 9:43 PM, Adam Gundry wrote:

...

On Sun, 15 Jun 2014 21:47:52 +0200, Gábor Lehel 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

On 16/06/14 11:14, Niklas Haas wrote: 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe