Thanks for looking at this! On Tue, Aug 31 2021, Richard Eisenberg <lists@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

On Thu, Sep 02 2021, Richard Eisenberg <lists@richarde.dev> wrote:

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.

Unfortunately, no. I've attached a self-contained example. It works as-is. But when I replace, in the ProductCat (Same k) instance, OkProdInstance (CPP FTW) by OkProdInstance' (the definition you suggested), I get: classes/src/ConCat/Constraints.hs:55:10: error: • Could not deduce: Ok k ~ Ok' (Same k) arising from the superclasses of an instance declaration from the context: (Ok' (Same k) x, Ok' (Same k) y) bound by a quantified context at classes/src/ConCat/Constraints.hs:1:1 • In the instance declaration for ‘ProductCat (Same k)’ | 55 | instance (ProductCat k, OkProdInstance'(k)) => ProductCat (Same k) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- Regards, Mike {-# LANGUAGE CPP #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE UndecidableSuperClasses #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE StandaloneKindSignatures #-} module ConCat.Constraints where import Prelude hiding (id,(.)) import GHC.Types (Constraint, Type) class Yes1 a instance Yes1 a class Category k where type Ok k :: Type -> Constraint type Ok k = Yes1 id :: Ok k a => a `k` a infixr 9 . (.) :: forall b c a. (Ok k a, Ok k b, Ok k c) => (b `k` c) -> (a `k` b) -> (a `k` c) class Ok k a => Ok' k a instance Ok k a => Ok' k a type OkProd :: (Type -> Type -> Type) -> Constraint type OkProd k = forall x y. (Ok' k x, Ok' k y) => Ok' k (x, y) #define OkProdInstance(k) okk ~ Ok (k), forall x y. (okk x, okk y) => okk (x, y) type OkProdInstance' :: (Type -> Type -> Type) -> Constraint type OkProdInstance' k = forall (okk :: Type -> Constraint) x y. (okk ~ Ok k, okk x, okk y) => okk (x, y) class (Category k, OkProd k) => ProductCat k where exl :: (Ok k a, Ok k b) => (a, b) `k` a exr :: (Ok k a, Ok k b) => (a, b) `k` b dup :: Ok k a => a `k` (a, a) data Same k a b = Same (a `k` b) instance Category k => Category (Same k) where type Ok (Same k) = Ok k id = Same id Same g . Same f = Same (g . f) instance (ProductCat k, OkProdInstance'(k)) => ProductCat (Same k) where exl = Same exl exr = Same exr dup = Same dup