Получение datakind признано в GADT

Question

Я не уверен, что так я хочу, чтобы мой дизайн действительно выглядел, но есть ли способ получить мой GADT, чтобы увидеть, что аргумент mt должен иметь вид MarketType, потому что он является аргументом типа до MarketIndex?

Я думаю, что текущий контроль типов будет mt :: * так MarketIndex mt выходит из строя, а не мы должны Bulid в MarketIndex mt в какой-то момент так необходимо ограничить 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 

Ошибки я получаю:

[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. 

Может быть, у меня есть синтаксис неправильно, или, может быть, я прошу слишком много?

Answer 1

Вашего синтаксиса GADT это хорошо, но только типы любезного * могут иметь значение и так mt используется как поле он получает вынужден родом * пути умозаключений типа. Обходной путь к тому, что вы пытаетесь сделать, - создать так называемый одноэлементный тип, который сопоставляет типы вашего пользовательского вида с уровнем ценности.

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

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

Answer 2

@shang уже ответил. Я просто хотел добавить, что при отладке таких проблем полезно найти явные аннотации типа/вида. Например, аннотирования код с видами следующим

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

дает (возможно) более четкое сообщение:

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’ 

В вашей ошибки mt выводится как тип (:: *), который позже конфликтует с MarketIndex mt. Заставляя такого рода, теперь хорошо писать MarketIndex mt, но теперь ошибка указывает, что mt должен быть :: *, который может звонить в колокол.

ИМХО, я хотел бы, чтобы ошибка была по линии

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