[Haskell-cafe] Type synonym involing quantified constraint?

[Richard Eisenberg]

Hm. Interesting. You are trying to work around the fact that okk is not in scope.

The problem is that GHC does not currently allow you to specify a tuple as the head of a quantified constraint. The thinking is that (forall x. premise => (conclusion1, conclusion2)) can always be refactored into (forall x. premise => conclusion1, forall x. premise => conclusion2).

In your case, the refactoring is not so simple, but it can be done. Try

> type OkProd k = forall (okk :: Type -> Constraint) x y. (okk ~ Ok k, okk x, okk y) => okk (Prod k x y)

Does that work for you? If not, it may be helpful to see a function that uses the OkProd constraint somewhere.

I hope this helps!
Richard


> On Sep 1, 2021, at 6:47 AM, Michael Sperber <sperber at deinprogramm.de> wrote:
> 
> 
> Thanks for looking at this!
> 
> On Tue, Aug 31 2021, Richard Eisenberg <lists at richarde.dev> wrote:
> 
>> This looks like a bug, which I've now filed: https://gitlab.haskell.org/ghc/ghc/-/issues/20318
>> 
>> The workaround is to enable ImpredicativeTypes.
> 
> So I did that and then tried defining it like this:
> 
> type OkProd'' :: (Type -> Type -> Type) -> Constraint
> type OkProd'' k = forall okk. (okk ~ Ok k, forall x y. (okk x, okk y) => okk (Prod k x y))
> 
> ... but get:
> 
> src/ConCat/Category.hs:228:1: error:
>    • You can't specify an instance for a tuple constraint
>    • In the quantified constraint ‘forall (okk :: * -> Constraint).
>                                    (okk ~ Ok k, forall x y. (okk x, okk y) => okk (Prod k x y))’
>      In the type synonym declaration for ‘OkProd''’
> 
> (What does this message even mean? :-) )
> 
> -- 
> Regards,
> Mike
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.