On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
<dominique.devri...@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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
