Proposal: ValidateMonoLiterals - Initial bikeshed discussion

[Erik Hesselink]

On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
<dominique.devriese at cs.kuleuven.be> wrote:
> Agreed.  For the idea to scale, good support for type-level
> programming with Integers/Strings/... is essential.  Something else
> that would be useful is an unsatisfiable primitive constraint
> constructor `UnsatisfiableConstraint :: String -> Constraint` that can
> be used to generate custom error messages. Then one could write
> something like
>
>   type family MustBeTrue (t :: Bool) (error :: String) :: Constraint
>   type family MustBeTrue True _ = ()
>   type family MustBeTrue False error = UnsatisfiableConstraint error
>
>   type family MustBeEven (n :: Nat) :: Constraint
>   type family MustBeEven n = MustBeTrue (IsEven n) ("Error in Even
> literal :'" ++ show n ++ "' is not even!")
>
>   instance (KnownNat n, MustBeEven n) => HasIntegerLiteral Even n where ...

Note that there is a trick to fake this with current GHC: you can
write an equality constraint that is false, involving the type level
string:

>   type family MustBeTrue False error = (() ~ error)

Erik