How to get better error messages with type-families?

user_534481 0
Viewed 211

I'm trying to build a statically-typed authorisation system and have the following working code-snippet:

{-# 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

And this is how it gets used:

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

All is good when the types and stars align. However, if the types don't align, the error message is a classic 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

I tried searching and stumbled upon https://kcsongor.github.io/report-stuck-families/, which talks of TypeError I tried using it like this, but it didn't work:

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"
--    |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

What is the correct way to use TypeError? Alternatively, is there any other way to get better error messages?

type-families data-kinds haskell
2 Answers

Sure it's possible to provide better compile-time error message using custom type errors. I've described how to use them in my blog post:

However, in your case, you need to use some additional utilities because your approach is not typeclass-based. Specifically, you need to use type-errors package.

Here is how custom error message looks like:

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

Below I provide complete code:

{-# 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
user_29005020

Okay, I found a "compromise" solution, but I'm not completely happy with it. There has to be better / built-in way to deal with this.

data FeatureFlag = Feature1 | Feature2 | FeatureNotFound

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

type NeedFeature (f :: FeatureFlag) (fs :: [FeatureFlag]) = (Feature f fs ~ f)

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

Now, if the types don't align, I get error messages that look like the following:

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

    • Couldn't match type ‘'FeatureNotFound’
                     with ‘'FeatureBookingEngine’
        arising from a use of ‘lockedFeatureAction’
user_5344810
Related