GADT 构造函数中的约束类型

Question

我有一个简单的ADT

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

现在我想使用此 ADT 创建一个 GADT，它将约束其构造函数的类型签名。这段代码不起作用，但我想做这样的事情：

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

即HasConstruct的构造函数可以将第一个类型参数作为任何形式的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] - 在阅读了Constraints in Kinds， Type Families and Singleton Types之后，我想通过这些原则可以实现这种约束。但我完全不知所措，无法让它工作

Answer 1

感谢 #haskel 初学者的 Cale 通过引入幻像类型并在 GADTConcept中标记相同的内容来建议此解决方案

{-# 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