CODEWITHSUNDEEP
haskell
dbeacham
dbeacham

Reputation: 1006

Getting datakind recognised in GADT

I'm not certain this is how I want my design to actually look like, but is there any way of getting my GADT to see that the mt argument must have kind MarketType due its being the type argument to MarketIndex?

I think the current type checking is going mt :: * so MarketIndex mt fails, rather than we need to bulid a MarketIndex mt at some point so must restrict mt :: MarketType.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

module Market.TypesDK where

data MarketType = WinDrawWin
                | AsianHandicap
                deriving (Show)

type family MarketIndex (mt :: MarketType) :: *

type instance MarketIndex WinDrawWin = ()
type instance MarketIndex AsianHandicap = Double

data Market :: MarketType -> * where
  Instance :: mt -> MarketIndex mt -> Market mt

The error I get is:

[1 of 1] Compiling Market.TypesDK   ( TypesDK.hs, interpreted )

TypesDK.hs:32:33:
    The first argument of ‘MarketIndex’ should have kind ‘MarketType’,
      but ‘mt’ has kind ‘*’
    In the type ‘MarketIndex mt’
    In the definition of data constructor ‘Instance’
    In the data declaration for ‘Market’
Failed, modules loaded: none.

Maybe I've got the syntax wrong, or maybe I'm asking too much?

Upvotes: 1

Views: 137

Answers (2)

chi
chi

Reputation: 116139

@shang has already answered. I just wanted to add that I find it useful to provide explicit type/kind annotations when debugging such problems. For instance, annotating the code with kinds as follows

data Market :: MarketType -> * where
  Instance :: forall (mt :: MarketType) .  mt -> MarketIndex mt -> Market mt

yields an (arguably) clearer message:

Expected a type, but ‘mt’ has kind ‘MarketType’
In the type ‘mt’
In the definition of data constructor ‘Instance’
In the data declaration for ‘Market’

In your error mt is inferred to be a type (:: *) which later conflicts with MarketIndex mt. By forcing the kind, it is now fine to write MarketIndex mt, but now the error states that mt should be :: * which can ring a bell.

IMHO, I would like the error to be along the line of

The type constructor (->) has kind * -> * -> *
but is applied to an argument of kind ‘MarketType’
In ‘mt -> ...’

Upvotes: 0

shang
shang

Reputation: 24802

Your GADT syntax is fine, but only types of kind * can have values and since mt is used as a field it gets forced to kind * by type inference. The workaround to what you are trying to do is to create a a so called singleton type that maps the types of your custom kind to the value level.

data SMarketType mt where
    SWinDrawWin :: SMarketType WinDrawWin
    SAsianHandicap :: SMarketType AsianHandicap

data Market :: MarketType -> * where
    Instance :: SMarketType mt -> MarketIndex mt -> Market mt

Upvotes: 6

Related Questions