Error handling

Example.hs

-- <a_ton_of_LANGUAGE_pragmas>.
-- <some_imports>

data SList as where
    SNil  :: SList '[]
    SCons :: Proxy a -> SList as -> SList (a ': as)

class IList as where
    slist :: SList as

instance IList '[] where
    slist = SNil

instance IList as => IList (a ': as) where
    slist = SCons Proxy slist

type family SubtypeOf a :: [*]

type family Head (as :: [k]) :: k where
    Head (a ': _) = a

type family Append as bs :: [k] where
    Append '[]       bs = bs
    Append (a ': as) bs = a ': Append as bs

type family ConcatMapPaths p a bs :: [[*]] where
    ConcatMapPaths p a '[]       = '[]
    ConcatMapPaths p a (b ': bs) = Append (Paths p a b) (ConcatMapPaths p a bs)

type family Paths p a b :: [[*]] where
    Paths p a a = p ': '[]
    Paths p a b = ConcatMapPaths (b ': p) a (SubtypeOf b)

type family Path a b where
    Path a b = Head (Paths '[] a b)

class a <! b where
    upcastDirect :: a -> b

type family Connect a (bs :: [*]) c :: Constraint where
    Connect a '[]       c = a ~ c
    Connect a (b ': bs) c = (a <! b, Connect b bs c)

upcastProxy :: a <! b => proxy a -> proxy b -> a -> b
upcastProxy _ _ = upcastDirect

upcastBy :: forall a ps b. Connect a ps b => SList ps -> a -> b
upcastBy  SNil        x = x
upcastBy (SCons p ps) x = upcastBy ps $ upcastProxy Proxy p x

class a <: b where
    upcast :: a -> b

instance (Connect a (Path a b) b, IList (Path a b)) => a <: b where
    upcast = upcastBy (slist :: SList (Path a b))

type instance SubtypeOf Err1 = '[]
type instance SubtypeOf Err2 = '[]
type instance SubtypeOf Err3 = '[Err1, Err2]
type instance SubtypeOf Err4 = '[Err3]
type instance SubtypeOf Err5 = '[Err2]

instance Err1 <! Err3 where
    upcastDirect = Err31

instance Err2 <! Err3 where
    upcastDirect = Err32

instance Err3 <! Err4 where
    upcastDirect = Err43

instance Err2 <! Err5 where
    upcastDirect = Err52

test1 :: Err1 -> Err3
test1 = upcast

test2 :: Err2 -> Err3
test2 = upcast

test3 :: Err1 -> Err4
test3 = upcast

test4 :: Err2 -> Err4
test4 = upcast

test5 :: Err2 -> Err5
test5 = upcast

Thoughts.md

Current situation

Right now we use Control.Monad.Error.Lens and there are a number of problems with it.

I've recently added the value restriction check and now the type signature of parseTypecheck looks like this:

parseTypecheck
    :: (AsParseError e AlexPosn,
        AsValueRestrictionError e TyName AlexPosn,
        AsUniqueError e AlexPosn,
        AsNormalizationError e TyName Name AlexPosn,
        AsTypeError e AlexPosn,
        MonadError e m,
        MonadQuote m)
    => TypeCheckConfig -> BSL.ByteString -> m (NormalizedType TyName ())

This is quite unwieldy. Moreover, printType, printNormalizeType and parseScoped -- all of them needed to be updated. What we really want to write is

parseTypecheck
    :: (AsError e AlexPosn,
        MonadError e m,
        MonadQuote m)
    => TypeCheckConfig -> BSL.ByteString -> m (NormalizedType TyName ())

Where AsError subsumes all the other errors as it's actually defined like that.

So we get an O(n) overhead in O(m) functions, that's a O(n*m) overhead in total, which is pretty bad.

In addition to this overhead, we also need to write boilerplate like

instance ann ~ () => AsError TypeEvalCheckError ann where
    _Error = _TypeEvalCheckErrorIllFormed . _Error

instance (tyname ~ TyName, ann ~ ()) => AsValueRestrictionError TypeEvalCheckError tyname ann where
    _ValueRestrictionError = _TypeEvalCheckErrorIllFormed . _ValueRestrictionError

We know that AsError err ann implies AsValueRestrictionError err tyname ann, but the current approach does not allow to communicate this information to the compiler.

Description of the problem

Arbitrary error types form the following DAG:

                 ...
                   \
Err6     ...        Err7
    \    /         /    \
     Err4      Err5      \
    /    \    /    \      \
 ...      Err1      Err2   Err3
                          /
                      Err8

There shouldn't be any "diamonds" (a "diamond" means that an error can be embedded into another error via distinct constructors). What we would like to have is a system where you can say that the children of Err7 are Err5 and Err3 (denoted as Err3 <: Err7 and Err5 <: 7) and automatically get Err1 <: Err7. Err2 <: Err7, Err3 <: Err7, so that you can directly throw an Err1 in a context that allows to throw Err7.

An example

We'll be using the following example to show how various approaches work:

data Err1 = Err1
data Err2 = Err2
data Err3 = Err31 Err1 | Err32 Err2
newtype Err4 = Err43 Err3
newtype Err5 = Err52 Err2

which forms the following DAG:

      Err4
        |
      Err3      Err5
     /    \    /
 Err1      Err2

A non-solution

Bottom-up type inference:

type family SupertypeOf e
type instance SupertypeOf Err1 = Err3
type instance SupertypeOf Err2 = Err3
type instance SupertypeOf Err2 = Err5
type instance SupertypeOf Err3 = Err4

Here we define a single type family SupertypeOf and specify the super type of each of the errors.

"What do you mean "the" supertype? There can be many!" "Wait a minute, Err2 does have two supertypes, these type family instances are incorrect! There can be only one instance per type."

Yep, but if we define those type instances in different files, then we're fine. This means that we won't be able to use Err3 and Err5 in the same file, but maybe this is acceptable sometimes.

But this approach is super fragile and my mom told me to be a responsible person and never cheat on my compiler, so we won't implement that.

An imaginary solution

It would be just great, if it was possible to write the following (I'm using functions as opposed to prisms for simplicity):

class SuperOfErr1 a where
  upcastErr1 :: Err1 -> a

class SuperOfErr1 a => SuperOfErr3 a where
  upcastErr3 :: Err3 -> a

  instance SuperOfErr1 a where
    upcastErr1 = upcastErr3 . Err3_1

Here we declare two classes, SuperOfErr1 and SuperOfErr3, and say that any SuperOfErr3 a instance also brings in scope the SuperOfErr1 a instance. And we don't need to manually satisfy the SuperOfErr1 a constraint of SuperOfErr3 a -- it's satisfied automatically!

Unfortunately, this feature does not seem to exist and I'm not able to emulate it in any way.

A possible solution

But what about top-down inference? We can have the following type family:

type family SubtypeOf a :: [*]
type instance SubtypeOf Err3 = '[Err1, Err2]
type instance SubtypeOf Err4 = '[Err3]

<end_of_the_manuscript>