haskell

Problem with quantified types and pattern matching


In a small library connected to parsing, I initially had an error type of the form (using GADT syntax):

data ParseError s e where
    -- | Error with no indication of its origin.
    Fail :: ParseError s e
    ParseError
        :: !Text                                       -- ^ Error message.
        -> !s                                          -- ^ State component.
        -> !e                                          -- ^ Error component.
        -> ParseError s e

The Text field is to be able to attach some info to the error and the the s field is to capture the parser's state (e. g. source position, an offset, etc.). The important field however is the e field, which serves as a sort of classifcation tag. Typically, it will be a singleton type (or maybe a newtype around some extra data), or a coproduct of such types. Say EndOfInputError, ValidationError, Either EndOfInputError ValidationError, etc.

Then I thought, wouldn't it be nice to add backtraces to errors? Given that the backtrace can contain errors with e of different types, the field must be a quantified type, so that we end up with:

data ParseError s e where
    -- | Error with no indication of its origin.
    Fail :: ParseError s e
    ParseError
        :: !Text                               -- ^ Error message.
        -> (forall d . Maybe (ParseError s d)) -- ^ Error backtrace.
        -> !s                                  -- ^ State component.
        -> !e                                  -- ^ Error component.
        -> ParseError s e

In practice, the quantified field is a list of ParseError of varying e, so for general processing, I have:

backtrace :: (forall d . Text -> s -> d -> a) -> ParseError s e -> [a]
backtrace f  = go
    where
        go Fail = []
        go (ParseError xs Nothing s e)  = [f xs s e]
        go (ParseError xs (Just b) s e) = f xs s e : backtrace f b

Unfortunately, cabal errors with:

src/Bins/Types/ParseError.hs:38:9: error: [GHC-62161] [-Wincomplete-patterns, Werror=incomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘go’:
        Patterns of type ‘ParseError s e’ not matched: ParseError _ _ _ _
   |
38 |         go Fail = []
   |         ^^^^^^^^^^^^...

I do not understand why this is giving me an error about non-exhaustive patterns. To my untrained eye, the equations cover all possible cases, so I am clearly missing a piece of information on how quantified types interact with pattern matching. Can anyone explain it to me?

Just in case it is important: language GHC2021 and at GHC v9.10.1. More details needed, just ask.


Solution

  • What you have written says that if I have a value ParseError desc stack state err, then no matter what type of error I choose, stack can deliver me a parse error containing that type. I suspect what you intended was that the fellow who's building the ParseError value gets to choose what types are stored in the stack. To express that, you would write this instead:

    ParseError :: forall d.
           !Text                               -- ^ Error message.
        -> Maybe (ParseError s d)              -- ^ Error backtrace.
        -> !s                                  -- ^ State component.
        -> !e                                  -- ^ Error component.
        -> ParseError s e
    

    You are almost certainly going to want some typeclass constraint on d -- otherwise you can't do anything with values of type d!

    ParseError :: forall d. Exception d
        => !Text                               -- ^ Error message.
        -> Maybe (ParseError s d)              -- ^ Error backtrace.
        -> !s                                  -- ^ State component.
        -> !e                                  -- ^ Error component.
        -> ParseError s e
    

    For uniformity, I'd be very tempted to move the existential one layer up the stack.

    data ParseError s where
        -- | Error with no indication of its origin.
        Fail :: ParseError s
        ParseError :: forall e. Exception e
            => !Text                               -- ^ Error message.
            -> Maybe (ParseError s)                -- ^ Error backtrace.
            -> !s                                  -- ^ State component.
            -> !e                                  -- ^ Error component.
            -> ParseError s
    

    Is there a meaningful difference between ParseError _ (Just Fail) _ _ and ParseError _ Nothing _ _? If not, perhaps a list would suit you.

    type ParseErrorStack s = [ParseError s]
    data ParseError s where
        ParseError :: forall e. Exception e
            => !Text                               -- ^ Error message.
            -> !s                                  -- ^ State component.
            -> !e                                  -- ^ Error component.
            -> ParseError s