Data type parametrized by constant in Haskell

Question

I would like to define a data type in Haskell which is parametrized by an Int constant along the lines:

data Q (n :: Int) = Q n (Int,Int) -- non-working code

in order to allow me to define functions of the type:

addQ :: (Q n)->(Q n)->(Q n)
addQ (Q k (i1,j1)) (Q k (i2,j2))) = Q k (i1+i2,j1+j2)

The idea is that in this way I am able to restrict addition to Q's that have the same n. Intuitively, it feels that this should be possible, but so far all my (admittedly newbie) attempts have stranded on the rigors of GHC.

Answer 1

As the comments say, this is possible with the DataKinds extension (technically it's possible to achieve something very similar without it, but it's very unergonomic).

{-# LANGUAGE DataKinds, ExplicitForAll, KindSignatures #-}

import GHC.TypeLits (Nat)
data Q (n :: Nat) = Q Int

addQ :: forall (n :: Nat). Q n -> Q n -> Q n
addQ (Q x) (Q y) = Q (x + y)

---

let q1 = Q 1 :: Q 3
    q2 = Q 2 :: Q 3
in addQ q1 q2
-- => Q 3 :: Q 3

If you put the KnownNat constraint on n (also from GHC.TypeLits) you can also get the n as a regular term using the natVal function.

Answer 2

Based on the hints and answer kindly supplied, I can give the answer I was looking for, including an example of how to unpack n from the parametrized data type.

{-# LANGUAGE DataKinds, ExplicitForAll, KindSignatures #-}

import GHC.TypeLits (Nat,KnownNat,natVal)

data Q (n :: Nat) = Q (Int,Int)

instance (KnownNat n) => Show (Q n) where
    show q@(Q (i,j)) = "("++(show i)++","++(show j)++")::"++(show (natVal q))

addQ :: forall (n :: Nat). Q n -> Q n -> Q n
addQ (Q (i1,j1)) (Q (i2,j2)) = Q (i1+i2,j1+j2)