I am using the GHC extension -XDataKinds and have -Wall turned on in a Haskell library I am writing. I am getting a warning about using unticked promoted constructors because -Wall implies -Wunticked-promoted-constructors. I'm wondering why this warning is important; if I am allowed to write in an unticked style in the default syntax, what's the harm?
Most of the dependently typed code I've written has been in Idris (and a little in Agda) and so I'm used to a unified namespace of types and values. As such it feels natural to me to write in an unticked style. However, if there is potential harm in it, I will add the ticks. But I don't want to do that without understanding why.
So for example, if I have a data type like this:
data HasDefault = IsDefaulted | NotDefaulted
that is used in a function signature like this:
setDefault :: a -> T p NotDefaulted a -> T p IsDefaulted a
then I get a warning like this (with -Werror also set):
C:\path-to-my-lib\src\Lib.hs:103:46: error: [-Wunticked-promoted-constructors, -Werror=unticked-promoted-constructors]
Unticked promoted constructor: `IsDefaulted'.
Use 'IsDefaulted instead of `IsDefaulted'.
|
103 | setDefault :: a -> T p NotDefaulted a -> T p IsDefaulted a
| ^^^^^^^^^^^
Should I worry about this, and make sure to be diligent about the ticking lifted constructors? Or should I turn the warning off?