CODEWITHSUNDEEP
haskell
Björn Gohla
Björn Gohla

Reputation: 33

Can I generalize over class constraints in Haskell?

In my application I have a type definition that looks like this:

{-# LANGUAGE ExistentialQuantification #-}

class C a where

data A = forall a. C a => A { unA :: a }

I most definitely want the kind signature A :: Type.

I would like to generalize over the class constraint, like so:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE ScopedTypeVariables       #-}

import Data.Kind (Type, Constraint)

class C a where

data A' (c :: Type -> Constraint) where
  A' :: forall a. c a => { unA :: a } -> A' c

type A = A' C

Note that A should be isomorphic to the A as defined in the beginning.

However GHC (8.6.5) rejects the generalized definition:


generalize.hs:11:19: error: Not in scope: type variable ‘c’
   |
11 |   A' :: forall a. c a => { unA :: a } -> A' c
   |                   ^

generalize.hs:11:45: error: Not in scope: type variable ‘c’
   |
11 |   A' :: forall a. c a => { unA :: a } -> A' c
   |                                             ^

I don't understand the error, since I did enable ScopedTypeVariables.

Am I missing something obvious, or is what I'm trying to do not possible? If so, why not?

Upvotes: 2

Views: 135

Answers (1)

Cubic
Cubic

Reputation: 15673

You got it almost right, what you want is

data HasConstraint (c :: Type -> Constraint) where
  Pack :: forall (c :: Type -> Constraint) a . c a => { unPack :: a } -> HasConstraint c

so you have to include c as inside your constructor type signature as well because it's completely separate from the data declaration for GADTs.

I imagine you'd want to use it like this:

instance Show (HasConstraint Show) where show (Pack x) = show x
show (Pack 10 :: HasConstraint Show) -- => "10"

You could also write

withPacked :: forall (c :: Type -> Constraint) b. (forall a. c a => a -> b) -> HasConstraint c -> b
withPacked f (Pack x) = f x
withPacked @Show show (Pack 10) -- => "10"

I'm not sure if there's much else you can do with this though.

(Note that the "getter" unPack here actually isn't usable with GADTs either, you'll always have to pattern match on the constructor if you want to actually unpack things).

Upvotes: 6

Related Questions