如何获得类型家族更好的错误消息？

Question

我正在尝试构建一个静态类型的授权系统，并具有以下工作代码片段：

{-# LANGUAGE DataKinds, ScopedTypeVariables, TypeFamilies #-}

module Try where

import Data.Singletons.TH

data FeatureFlag = Feature1 | Feature2 deriving (Eq, Show)
$(genSingletons [''FeatureFlag])

type family Feature (f :: FeatureFlag) (fs :: [FeatureFlag]) where
  Feature f '[] = 'False
  Feature f (f:fs) = 'True
  Feature f (q:fs) = Feature f fs  


lockedFeatureAction :: (MonadIO (m fs), Feature 'Feature1 fs ~ 'True) => m fs ()
lockedFeatureaction = undefined

checkFeatureFlagsAndRun :: forall (fs :: [FeatureFlag]) . (SingI fs) => Proxy fs -> AppM fs () -> IO ()
checkFeatureFlagsAndRun = undefined

这就是它的用法：

ghci> checkFeatureFlagsAndRun (Proxy :: Proxy '[ 'Feature1]) lockedFeatureAction

当类型和星形对齐时，一切都很好。但是，如果类型不对齐，则错误消息是经典的Sherlock Holmes“ whodunnit”：

ghci> checkFeatureFlagsAndRun (Proxy :: Proxy '[ 'Feature2]) lockedFeatureAction

<interactive>:462:32: error:
    • Couldn't match type ‘'False’ with ‘'True’
        arising from a use of ‘lockedFeatureAction’
    • In the second argument of ‘checkFeatureFlagsAndRun’, namely ‘lockedFeatureAction’
      In the expression: checkFeatureFlagsAndRun (Proxy :: Proxy '[ 'Feature2]) lockedFeatureAction
      In an equation for ‘it’: it = checkFeatureFlagsAndRun (Proxy :: Proxy '[ 'Feature2]) lockedFeatureAction

我尝试搜索并偶然发现https://kcsongor.github.io/report-stuck-families/，上面提到TypeError我曾尝试像这样使用它，但没有成功：

type family Feature (f :: FeatureFlag) (fs :: [FeatureFlag]) where
  Feature f '[] = TypeError "Could not satisfy FeatureFlag conditions"
  Feature f (f:fs) = 'True
  Feature f (q:fs) = Feature f fs

--     • Expected kind ‘ghc-prim-0.5.2.0:GHC.Types.Symbol -> Bool’,
--         but ‘TypeError’ has kind ‘*’
--     • In the type ‘TypeError "Could not satisfy FeatureFlag conditions"’
--       In the type family declaration for ‘Feature’
--    |
-- 19 |   Feature f '[] = TypeError "Could not satisfy FeatureFlag conditions"
--    |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

正确的使用方法是TypeError什么？另外，还有其他方法可以获取更好的错误消息吗？

Answer 1

当然，可以使用自定义类型错误提供更好的编译时错误消息。我已经在博客文章中介绍了如何使用它们：

• Type Errors讲述的一个故事

但是，在您的情况下，您需要使用一些其他实用程序，因为您的方法不是基于类型类的。具体来说，您需要使用type-errors包。

自定义错误消息如下所示：

ghci> checkFeatureFlagsAndRun (Proxy :: Proxy '[ 'Feature1]) lockedFeatureAction
<works as expected>

ghci> :t checkFeatureFlagsAndRun (Proxy :: Proxy '[ 'Feature2]) lockedFeatureAction

    • Type-level list of features should contain feature: 'Feature1
      But it doesn't:

          '[ 'Feature2]

    • In the second argument of ‘checkFeatureFlagsAndRun’, namely
        ‘lockedFeatureAction’
      In the expression:
        checkFeatureFlagsAndRun
          (Proxy :: Proxy '[ 'Feature2]) lockedFeatureAction

下面我提供完整的代码：

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TemplateHaskell      #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module Feature where

import Control.Monad.IO.Class (MonadIO)
import Data.Kind (Constraint)
import Data.Proxy (Proxy)
import Data.Singletons.TH (SingI, genSingletons)
import Data.Type.Bool (If)
import Fcf (Stuck)
import GHC.TypeLits (ErrorMessage (..), TypeError)
import Type.Errors (DelayError, WhenStuck)


data FeatureFlag = Feature1 | Feature2 deriving (Eq, Show)
$(genSingletons [''FeatureFlag])

data AppM (fs :: [FeatureFlag]) a

type family HasFeature (f :: FeatureFlag) (fs :: [FeatureFlag]) :: Constraint where
    HasFeature f fs = WhenStuck (Elem f fs) (DelayError (NoFeature f fs))

type family Elem (x :: k) (xs :: [k]) :: Bool where
    Elem _ '[]       = Stuck
    Elem x (x ': xs) = 'True
    Elem x (y ': xs) = Elem x xs

type NoFeature (f :: FeatureFlag) (fs :: [FeatureFlag]) =
        'Text "Type-level list of features should contain feature: " ':<>: 'ShowType f
  ':$$: 'Text "But it doesn't:"
  ':$$: 'Text ""
  ':$$: 'Text "    " ':<>: 'ShowType fs
  ':$$: 'Text ""

lockedFeatureAction :: (MonadIO (m fs), HasFeature 'Feature1 fs) => m fs ()
lockedFeatureAction = undefined

checkFeatureFlagsAndRun :: forall (fs :: [FeatureFlag]) . (SingI fs) => Proxy fs -> AppM fs () -> IO ()
checkFeatureFlagsAndRun = undefined

Answer 2

好吧，我找到了一个“妥协”的解决方案，但我对此并不完全满意。必须有更好/内置的方法来处理这个问题。

\n\n

data FeatureFlag = Feature1 | Feature2 | FeatureNotFound\n\ntype family Feature (f :: FeatureFlag) (fs :: [FeatureFlag]) where\n  Feature f \'[] = \'FeatureNotFound\n  Feature f (f:fs) = f\n  Feature f (q:fs) = Feature f fs\n\ntype NeedFeature (f :: FeatureFlag) (fs :: [FeatureFlag]) = (Feature f fs ~ f)\n\nlockedFeatureAction :: (MonadIO (m fs), NeedFeature \'Feature1 fs) => m fs ()\nlockedFeatureaction = undefined\n

\n\n

现在，如果类型不对齐，我会收到如下所示的错误消息：

\n\n

ghci> checkFeatureFlagsAndRun (Proxy :: Proxy \'[ \'Feature2]) lockedFeatureAction\n\n    \xe2\x80\xa2 Couldn\'t match type \xe2\x80\x98\'FeatureNotFound\xe2\x80\x99\n                     with \xe2\x80\x98\'FeatureBookingEngine\xe2\x80\x99\n        arising from a use of \xe2\x80\x98lockedFeatureAction\xe2\x80\x99\n

\n