GitLab

@rae has indicated that the type-checking plugin API is going to change with the upcoming refactors to constraint solving (removal of flattening variables, removal of derived constraints), which will require plugin authors to adjust their plugins.

This seems like it could be a good time to add a new piece of functionality to the API, by allowing plugins to emit an error message directly rather than reporting insoluble constraints. I suggest changing TcPluginResult from

 data TcPluginResult
  = TcPluginContradiction [Ct]
  | TcPluginOk [(EvTerm,Ct)] [Ct]

to

data Insolubles
  = Insolubles
  { insolubleWantedConstraints :: [Ct]
  , insolubleErrorMessages     :: [SDoc]
  }
  deriving (Show, Semigroup, Monoid)

 data TcPluginResult
  = TcPluginInsolubles Insolubles
  | TcPluginOk [(EvTerm,Ct)] [Ct]

allowing the plugin to directly report error messages in the form of SDoc. We would require a similar property as currently: one of the fields of Insolubles must be non-empty.

This would allow one to write error-message plugins which would never produce any evidence, i.e. they would always return either TcPluginInsolubles ( mempty { insolubleErrorMessages = messages } ) or TcPluginOk [] cts. This could also be a way to experiment with interactive error messages, if we parametrise over the error message field:

class DisplayableFormat messageFormat where { ... }

data Insolubles messageFormat
  = Insolubles
  { insolubleWantedConstraints :: [Ct]
  , insolubleErrorMessages     :: [messageFormat]
  }

data TcPluginResult where
  TcPluginInsolubles
    :: DisplayableFormat messageFormat
    => Insolubles messageFormat
    -> TcPluginResult
  TcPluginOk
    :: [(EvTerm,Ct)]
    -> [Ct]
    -> TcPluginResult

pattern TcPluginContradiction :: [Ct] -> TcPluginResult
pattern TcPluginContradiction insolubles = TcPluginInsolubles (Insolubles insolubles ([] :: [SDoc]))

Currently, if a plugin wants to report a specific error message, I believe the only option is to emit constraints using the TypeError mechanism.