Re: [Haskell-cafe] Type synonym involing quantified constraint?

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 wrote:

Thanks for looking at this!

On Tue, Aug 31 2021, Richard Eisenberg 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.