Ограничивающие типы в конструкторе GADT

Question

У меня простой ADT

data Concept a = Entity  a |  Role a | Relation a | Resource a | Sub (Concept a)

Теперь я хочу создать GADT, используя этот ADT, который будет ограничивать сигнатуру типа его конструкторов. Этот код не будет работать, но я хочу сделать что-то вроде этого:

data Construct a b where
      Has :: Concept a -> 'Resource b -> Construct (Concept a) ('Resource b)

Т.е. Has конструктор для Construct может иметь первый тип параметра как Concept любой формы, но параметр второго типа должен быть Resource конструктор (повышен до типа). Эта подпись не работает, так как я использую вид вместо типа. Но я хочу понять что-то подобное и не могу понять, как сделать то же самое.

Я импортирую {-# LANGUAGE GADTs, TypeInType #-},

Редактировать:

На основании одного комментария, если я сделаю это

 data Construct (a :: Concept ak) (b :: Concept bk)  where
  Has :: Construct a ('Resource b)

Тогда это проверка типов. Но теперь, как я могу извлечь значения при сопоставлении с образцом на Has

f :: Construct a b -> T.Text
f Has = ???

Мое требование - я хочу ограничить типы для Has a b конструктор, так что он может позволить только a :: Concept ak (т.е. любая концепция) и (b ~ 'Resource *) => (b :: Concept bk)[1] (т.е. только тип ресурса Концепции), например

-- Concept values
person = Entity "person"
name = Resource "name"
role = Role "father"

-- I want this to be valid
personHasName = Has person name

-- And this to be invalid
personHasRole = Has person role

[1] - После некоторого прочтения Ограничений в Видах, Семействах Типов и Типах Singleton, я думаю, что возможно реализовать этот тип ограничений через эти принципы. Но я в полном недоумении заставить его работать

Answer 1

Спасибо Cale из #haskel-beginners за предложение этого решения, введя фантомный тип и пометив его в Concept GADT

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

data ConceptType = EntityT | RoleT | RelationT | ResourceT | SubT ConceptType

data Concept (t :: ConceptType) a where
  Entity :: a -> Concept EntityT a
  Role :: a -> Concept RoleT a
  Relation :: a -> Concept RelationT a
  Resource :: a -> Concept ResourceT a
  Sub :: Concept t a -> Concept (SubT t) a

data Construct t a b where
  Has :: Concept t a -> Concept ResourceT b -> Construct t a b