Во вчерашнем вопросе было определение HList (из HList), который использует семейства данных. В принципе:
data family HList (l :: [*])
data instance HList '[] = HNil
newtype instance HList (x ': xs) = HCons1 (x, HList xs)
pattern HCons x xs = HCons1 (x, xs)
вместо обычного (IMO более элегантного и интуитивно понятного) определения GADT
data HList (l :: [*]) where
HNil :: HList '[]
HCons :: x -> HList xs -> HList (x ': xs)
Это связано с тем, что версия семейства данных позволяет нам принуждать (мы можем принуждать только случай HList (x ': xs), поскольку это newtype instance, но этого достаточно), в то время как GADT определяет только номинальную роль для l (таким образом блокируя любое приведение). (В моем ответе на упомянутый вопрос есть конкретный пример этого.)
Недостатки ролевой системы для GADT в отношении HList обсуждаются в этом вопрос двухлетней давности. По сути, GHC автоматически помечает любую переменную типа "GADT" как номинальную.
Учитывая, что с тех пор прошло некоторое время и есть разговоры о том, чтобы сделать роли более гибкими в отношении типа/данных. семьи, есть ли какие-то дальнейшие действия (т. е. какая-то существующая идея, какой-нибудь открытый билет Trac, что-нибудь на самом деле) для проверки более интересных ролей в GADT (например, HList)? Есть ли здесь какие-то фундаментальные ограничения, связанные с GADT или взаимодействием DataKinds и ролей? Что нужно реализовать/создать, чтобы это работало?
