Как определить пользовательскую ошибку типа в семействе типов для ограничения, использующего равенство типов?

Question

Итак, можно определить ограничение членства следующим образом:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}

module Whatever where

type family MemberB (x :: k) (l :: [k]) where
  MemberB _ '[]      = 'False
  MemberB a (a : xs) = 'True
  MemberB a (b : xs) = MemberB a xs

type Member x xs = MemberB x xs ~ 'True

data Configuration = A | B | C

data Action (configuration :: Configuration) where
  Action1 :: Member cfg '[ 'A ]     => Action cfg
  Action2 :: Member cfg '[ 'B, 'C ] => Action cfg
  Action3 :: Member cfg '[ 'A, 'C ] => Action cfg

exhaustive :: Action 'A -> ()
exhaustive Action1 = ()
exhaustive Action3 = ()
exhaustive Action2 = ()

Но полученное нами сообщение об ошибке не очень информативно:

 • Couldn't match type ‘'False’ with ‘'True’
   Inaccessible code in
     a pattern with constructor:
       Action2 :: forall (cfg :: Configuration).
                  Member cfg '['B, 'C] =>
                  Action cfg,
     in an equation for ‘exhaustive’
 • In the pattern: Action2
   In an equation for ‘exhaustive’: exhaustive Action2 = () (intero)

Было бы неплохо использоватьновая функция TypeError для улучшения этого сообщения, однако наивное решение поглощает ошибку:

import GHC.TypeLits

type family MemberB (x :: k) (l :: [k]) where
  MemberB _ '[]      = TypeError ('Text "not a member")
  MemberB a (a : xs) = 'True
  MemberB a (b : xs) = MemberB a xs

Кажется, что, возможно, TypeError ведет себя как любой тип, и поэтому он счастливо объединяется с'True?

Есть ли способ получить приятную ошибку типа при сохранении поведения членства?

Answer 1

exhaustive обрабатывает случай, который никогда не может произойти, но на самом деле это не ошибка.Или, по крайней мере, пока он работает так, как задумано, даже если система типов может быть улучшена, чтобы не допускать обработки невозможных случаев.

Сопоставление с образцом при Action2 обеспечивает ограничениеMember 'A '[ 'B, 'C ] в вашем контексте.Это отличается от использования Action2 в качестве выражения, для которого требуется это ограничение, и это приведет к ошибке в решателе ограничений.

Answer 2

Ну, он не использует TypeError, но вы все равно можете найти его интересным:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}

module Whatever where

data IsMember k = IsMember | Isn'tMember k [k]

type family MemberB (x :: k) (l :: [k]) (orig :: [k]) where
  MemberB a '[]      ys = 'Isn'tMember a ys
  MemberB a (a : xs) ys = 'IsMember
  MemberB a (b : xs) ys = MemberB a xs ys

type Member x xs = MemberB x xs xs ~ 'IsMember

data Configuration = A | B | C

data Action (configuration :: Configuration) where
  Action1 :: Member cfg '[ 'A ]     => Action cfg
  Action2 :: Member cfg '[ 'B, 'C ] => Action cfg
  Action3 :: Member cfg '[ 'A, 'C ] => Action cfg

exhaustive :: Action 'A -> ()
exhaustive Action1 = ()
exhaustive Action3 = ()
exhaustive Action2 = ()

Ошибка немного более информативна:

test.hs:32:16: error:
    • Couldn't match type ‘'Isn'tMember 'A '['B, 'C]’ with ‘'IsMember’
      Inaccessible code in
        a pattern with constructor:
          Action2 :: forall (cfg :: Configuration).
                     Member cfg '['B, 'C] =>
                     Action cfg,
        in an equation for ‘exhaustive’
    • In the pattern: Action2
      In an equation for ‘exhaustive’: exhaustive Action2 = ()
   |
32 |     exhaustive Action2 = ()
   |                ^^^^^^^

Answer 3

Я думаю, что вы, вероятно, хотите вернуться к первой попытке:

type family MemberB (x :: k) (l :: [k]) where
  MemberB _ '[]      = 'False
  MemberB a (a : xs) = 'True
  MemberB a (b : xs) = MemberB a xs

Но давайте исправим Member.

type Member x l = Member' x l (MemberB x l)

type family Member' x l mem :: Constraint where
  Member' x l 'True = ()
  Member' x l 'False =
    TypeError ('ShowType x :<>:
               'Text " is not a member of " :<>:
               'ShowType l)