Skip to content

User defined Type Warnings

Motivation

GHC Allows users to specify custom type errors for type level literals.

type family TypeError (a :: ErrorMessage) :: b where ...

This is obviously useful. For example in the listed example:

type family ByteSize x where
   ByteSize Word16   = 2
   ByteSize Word8    = 1
   ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
                                  Text " is not exportable.")

What about the reverse? If we want to go from bytes to types we could use.

type family FitsIn x where
   FitsIn 0        = ()
   FitsIn 1        = Word8
   ...
   FitsIn a        = TypeWarning (Text "The byte size " :<>: ShowType a :<>:
                                  Text " is defaulted to Integer.")
                                  Integer

This would warn users in a similar fashion to how GHC warns about defaulting literals to Integers.

Proposal

Add TypeWarning:

type family TypeWarning (a :: ErrorMessage) b :: b where ...

I will not be implementing this (anytime soon at least) and it might need a ghc-proposal. But seems like an obvious idea.

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