如何在类型族中为使用类型相等的约束定义自定义类型错误？答案

【问题标题】：How to define a custom type error within a type family for a constraint that uses type equality?如何在类型族中为使用类型相等的约束定义自定义类型错误？
【发布时间】：2021-09-14 15:55:46
【问题描述】：

因此，可以像这样定义成员约束：

{-# 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 愉快地统一了？

有没有办法得到一个不错的类型错误，同时保留成员行为？

【问题讨论】：

我确实得到了错误：29:7: error: • not a member • In the expression: foo In an equation for ‘bar’: bar = foo
哇，也许我应该更新我的 GHC！？让我检查一下！
哈，我把问题简单化了，现在更新它......
@dfeuer ha，我更新了代码，但没有更新错误信息，现在已修复

标签： haskell type-constraints type-families

【解决方案1】：

好吧，它不使用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 = ()
   |                ^^^^^^^

【讨论】：

绝招！除非有人使用TypeError 提供答案，否则我可能会接受这是我最接近完美的答案。

【解决方案2】：

exhaustive 正在处理一个永远不会发生的情况，但这并不是真正的错误。或者至少，它现在按预期工作，即使可以改进类型系统以不允许处理不可能的情况。

Action2 上的模式匹配为您提供约束Member 'A '[ 'B, 'C ] 到您的上下文中。这与使用Action2 作为表达式不同，后者需要该约束，这会导致约束求解器出错。

【讨论】：

您如何将此解释与编译器抱怨在不使用 TypeError 时无法证明 'False ~ 'True 的观察结果相一致？如果我从字面上看这个答案，我会认为编译器只会将'False ~ 'True 引入上下文，不会产生错误。
@DanielWagner，类型检查器尝试查看模式匹配是否是多余的；它并不总是成功。
@DanielWagner 实际上，我希望约束没有被证明，而是由类型检查器假设。在其他情况下，GHC 以某种方式决定，如果本地假设不一致，则它必须报告错误——在这种情况下，它不会。也许一般情况下的不一致无法确定，所以GHC必须是不完善的？有时我希望 GHC 让我注释这种“不可能”的情况，就像 Agda () 模式一样。
@chi 啊，好吧，that much at least you can do -- with some effort。我之前写了一个答案，没有给出exhaustive 的错误，但确实使用EmptyCase 断言额外的情况是不可能的......但我在此期间想到的技巧似乎更好。

【解决方案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)

【讨论】：

这仍然不会对我产生类型错误。适合你吗？
@DanielWagner，不，在这种情况下似乎不是。在其他一些情况下，它应该 ....

【解决方案4】：

我在将约束作为错误解决时偶然发现了这个答案。经过一番摆弄，我设法通过使用类型相等将自定义错误编码为约束：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
import Data.Kind
import GHC.TypeLits

type family F a :: Constraint where
  F Foo = ()
  F t = () ~ TypeError ('Text "Type " :<>: 'ShowType t :<>: 'Text " is not supported.")

class C1 a where
  cc :: a -> a
  default cc :: F a => a -> a
  cc = id

data Foo
  deriving anyclass C1

data Bar
  deriving anyclass C1

main :: IO ()
main = pure ()

 /run/user/1000/tmp.53OJoiuM9m ghc -Wall -Wno-unused-top-binds foo.hs
[1 of 1] Compiling Main             ( foo.hs, foo.o )

foo.hs:24:21: error:
    • Type Bar is not supported.
    • When deriving the instance for (C1 Bar)
   |
24 |   deriving anyclass C1
   |                     ^^

【讨论】：