[Haskell-cafe] Type synonym involing quantified constraint?

[Michael Sperber]

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