[Haskellcafe] Type synonym involing quantified constraint?
Michael Sperber
sperber at deinprogramm.de
Tue Sep 7 11:21:44 UTC 2021
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 selfcontained example. It works asis. 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
More information about the HaskellCafe
mailing list