[Haskell-cafe] Type synonym involing quantified constraint?

[Michael Sperber]

On Thu, Sep 02 2021, Richard Eisenberg <lists at 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