On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
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