Haskell - соответствие шаблона GADT с ограничениями класса

Question

Рассмотрим следующий пример

{-# LANGUAGE DataKinds, GADTs #-}
data Phantom = A | B
data Foo (a :: Phantom) where
  FooA :: Foo 'A
  FooB :: Foo 'B
class PhantomConstraint (a :: Phantom)
instance PhantomConstraint 'A -- Note: No instance for 'B
someFunc :: PhantomConstraint a => Foo a -> ()
someFunc FooA = ()

Если я делаю что-то подобное, GHC жалуется на то, что совпадения по шаблону не исчерпывают someFuncоднако, если я попытаюсь включить случай для FooB (что я не хочу делать по доменным причинам), он пожалуется, что не может вывести случай PhantomConstraint за Foo 'B

Есть ли способ сделать так, чтобы сопоставление с шаблоном GADT учитывало ограничения класса типов, чтобы исключить необходимые ветви сопоставления с образцом?

РЕДАКТИРОВАТЬ: Более подробную информацию о том, что я хочу сделать. У меня есть набор типов, которые все связаны, но имеют разные свойства. В мире ОО это то, для чего люди используют подтипы и наследование. Однако в сообществе FP, похоже, все согласны с тем, что нет действительно хорошего способа сделать подтип, поэтому в этом случае мне нужно взломать его. Таким образом, у меня есть GADT, который объединяет все типы, но с различными параметрами для этого типа. Затем я перехожу к написанию различных классов типов и экземпляров классов типов для параметров типа (включается datakinds, нет представления термина). Я хочу иметь возможность выразить, что некоторые из этих типов из типов данных имеют свойство, которого нет у других, но все они имеют определенные общие свойства, поэтому я не хочу разбивать тип. Единственный другой вариант, который я могу предвидеть, - это создать таксономию для части типа, но затем типы DataKinds будут испорчены.

Answer 1

Я не могу воспроизвести проблему. Это загружает без предупреждений или ошибок в GHCi 8.4.3.

{-# LANGUAGE GADTs, DataKinds, KindSignatures #-}
{-# OPTIONS -Wall #-}
module GADTwarning2 where

data Phantom = A | B

data Foo (a :: Phantom) where
  FooA :: Foo 'A
  FooB :: Foo 'B

class PhantomConstraint (a :: Phantom)

instance PhantomConstraint 'A -- Note: No instance for 'B

someFunc :: PhantomConstraint a => Foo a -> ()
someFunc FooA = ()
someFunc FooB = ()

Как пояснил Луки в комментарии, мы не можем избежать FooB случай, так как классы типов открыты, и другой экземпляр может быть добавлен позже другим модулем, что делает сопоставление с образцом не исчерпывающим.

Если вы абсолютно уверены, что вам не нужны никакие другие экземпляры, кроме A, вы можете попробовать использовать

class a ~ 'A => PhantomConstraint (a :: Phantom)

Или, если индекс a может быть 'A или же 'B, но никогда не третий конструктор 'CТогда мы можем попытаться подтвердить этот факт:

class PhantomConstraint (a :: Phantom) where
   aIsAOrB :: Either (a :~: 'A) (a :~: 'B)

а затем использовать этот член позже.