Write GADT record with constrained type

gadt, haskell, record, type-constraints

Solution

You can achieve this by declaring the record destructors within the type of the constructor as follows:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}

data Foo :: * -> * where
    Foo :: HasData a => { -- look - the context declared upfront
        getStr :: String, -- wow - function declaration in type sig!
        getData :: Data a, -- only allowed with a HasData instance
        getInt :: Int
    } -> Foo a

but I suspect there's an easier way of achieving what you intend to do, unless you're doing something more cunning with the type `a` than it seems. Here's a simpler way to insist on showable data:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}

data Bar a where
    Bar :: Show a => {
        getStr' :: String,
        getData' :: a, -- can Show 
        getInt' :: Int
    } -> Bar a -- have (Show a)
deriving instance Show (Bar a)

This way has the benefit of working for arbitrary Showable data, without making instances of the `HasData` class nor using all those compiler pragmas, but that's only of help to you if your `HasData` class was just there to make things Showable. You might have some deeper purpose I'm not seeing.

(You might consider dropping the `Show` context altogether except for where you actually use it, to simplify things more and allow you to make Functor instances. That would be simpler and wouldn't require any compiler pragmas at all. Over the years I've become fonder of keeping things general and making Functor instances.)

Problem

I have the following code that compiles in my program: ``` {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} class (Show (Data a)) => HasData (a :: *) where type Data a :: * data Foo :: * -> * where Foo :: (HasData a) => String -> Data a -> Int -> Foo a -- bunch of args deriving instance Show (Foo a) ``` Since the number of arguments for the `Foo` contructor can be many, I would like to write the code using record syntax, but I cannot figure out how to do this with GADT syntax (GHC deprecated datatype contexts, so I'm trying to avoid them): ``` data Foo :: * -> * where Foo { getStr :: String, getData :: Data a, -- want (HasData a) getInt :: Int } :: Foo a -- want (HasData a) ``` I need to constrain `a` in `Foo`'s constructor just like I did above without record syntax. How can I do this?

Original source