Skip to content

Allow users to define an error message that is displayed when a constraint can't be solved

I would like to enable users to annotate constraints with custom error messages; such a message would be displayed by GHC in the case that an annotated constraint could not be satisfied.

That is, I propose a special type family:

type Annotate :: ErrorMessage -> Constraint -> Constraint

Minimal illustration of the functionality:

type F :: Type -> Constraint
type family F x where
  F (a,b) = Annotate ( Text "F needs pair components to have the same type" ) ( a ~ b )

f :: F a => ()
f = ()

g :: ()
g = f @(Int, Bool)

would produce the error message:

    * F needs pair components to have the same type
    * Arising from a use of `f'
    * In the expression: f @(Int, Bool)
      In an equation for `g': g = f @(Int, Bool)
   |
13 | g = f @(Int, Bool)
   |     ^^^^^^^^^^^^^^

instead of the decidably less helpful:

    * Couldn't match type `Int' with `Bool' arising from a use of `f'
    * In the expression: f @(Int, Bool)
      In an equation for `g': g = f @(Int, Bool)
   |
13 | g = f @(Int, Bool)
   |     ^^^^^^^^^^^^^^

I think this would be generally useful. For instance, one of my use cases is as follows: I have written a graphics shader library which uses type families to validate programs. When a user tries to read from an image or sample from a texture, we validate the operation using the image properties (available at the type level) as well as the arguments to the image operation that the user has provided (see here). This works well when the type family computation directly hits an error message, but can result in confusing messages when the type family application computes to another constraint. For instance, I have a constraint of the form

type family TypeMatchesFormat (fmt :: ImageFormat) (a :: Type) :: Constraint where
  MatchesFormat IntegralFormat a = Integral a
  MatchesFormat FloatingFormat a = Floating a
  MatchesFormat UnknownFormat  _ = TypeError (Text "Unknown image format")

This leads to error messages of the form Could not deduce Floating Word32 that are rather inscrutable, whereas with Annotate I could write:

type family TypeMatchesFormat (fmt :: ImageFormat) (a :: Type) :: Constraint where
  MatchesFormat IntegralFormat a = Annotate ( Text "Cannot use non-integral type " :<>: ShowType a :<>: Text " with an integral image format" ) ( Integral a )
  MatchesFormat FloatingFormat a = Annotate ( Text "Cannot use non-float type " :<>: ShowType a :<>: Text " with a floating-point image format" ) ( Floating a )
  MatchesFormat UnknownFormat  _ = TypeError (Text "Unknown image format")
Edited by sheaf
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information