Currently all error messages that can be thrown in the TCM are in a monster TypeError type in Mikan.TypeChecking.Monad.Base, and all warning messages that can be reported are in a monster Warning type. This means adding a new error/warning requires recompiling the entire type checker. Also, only Warnings can be reported non-fatally, and only TypeErrors can be thrown, which makes dynamically modifying the severity of a diagnostic very difficult (in one direction there is NonFatalErrors, which is a fatal error consisting of a bag of warnings).
If we implement the DiagnosticReason refactoring from #99, we can instead have something like
class (Pretty a, Typeable a) => Diagnostic a where
-- | The 'static reason' for throwing this diagnostic.
-- Informs what its severity should be after user options are taken into account.
diagnosticReason :: a -> DiagnosticReason
-- structured hints!? multiple locations!?
typeError :: (HasCallStack, MonadTCError m, Diagnostic err) => err -> m a
warning :: (HasCallStack, MonadWarning m, Diagnostic err) => err -> m ()
where now the only difference between typeError and warning is control flow. Code like catchIllTypedPatternBlockedOnMeta and catchCutConversionErrors can make use of the Typeable constraint to determine at each landing pad whether the error is one of the ones they care about, just like with base Exception. This would make error recovery strategies easier to implement, since we could just catch "SomeDiagnostic", report it with warning, and return whatever is appropriate (e.g. a meta, if it was caught when checking an expression), instead of having to twist WarningName and ErrorName into eachother.