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")