Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,862
    • Issues 4,862
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 455
    • Merge requests 455
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #18977
Closed
Open
Created Nov 23, 2020 by sheaf@sheafMaintainer

Allow type-checking plugins to emit custom error messages

@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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking