Implement support for user-defined type errors.

Implements Lennart's idea from the Haskell Symposium.
Users may use the special type function `TypeError`, which is
similar to `error` at the value level.

See Trac ticket https://ghc.haskell.org/trac/ghc/ticket/9637, and wiki
page https://ghc.haskell.org/trac/ghc/wiki/CustomTypeErros

Test Plan: Included testcases

Reviewers: simonpj, austin, hvr, goldfire, bgamari

Reviewed By: goldfire, bgamari

Subscribers: adamgundry, thomie

Differential Revision: https://phabricator.haskell.org/D1236

GHC Trac Issues: #9637

1 files changed, 27 insertions, 0 deletions

diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index dafdb57c69..f124017be2 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/libraries/base/GHC/TypeLits.hs
@@ -12,6 +12,7 @@
 {-# LANGUAGE UndecidableInstances #-}  -- for compiling instances of (==)
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
 
 {-| This module is an internal GHC module.  It declares the constants used
 in the implementation of type-level natural numbers.  The programmer interface
@@ -36,6 +37,10 @@ module GHC.TypeLits
   , type (<=), type (<=?), type (+), type (*), type (^), type (-)
   , CmpNat, CmpSymbol
 
+  -- * User-defined type errors
+  , TypeError
+  , ErrorMessage(..)
+
   ) where
 
 import GHC.Base(Eq(..), Ord(..), Bool(True,False), Ordering(..), otherwise)
@@ -191,6 +196,28 @@ type family (m :: Nat) ^ (n :: Nat) :: Nat
 type family (m :: Nat) - (n :: Nat) :: Nat
 
 
+-- | A description of a custom type error.
+data {-kind-} ErrorMessage = Text Symbol
+                             -- ^ Show the text as is.
+
+                           | forall t. ShowType t
+                             -- ^ Pretty print the type.
+                             -- @ShowType :: k -> ErrorMessage@
+
+                           | ErrorMessage :<>: ErrorMessage
+                             -- ^ Put two pieces of error message next
+                             -- to each other.
+
+                           | ErrorMessage :$$: ErrorMessage
+                             -- ^ Stack two pieces of error message on top
+                             -- of each other.
+
+infixl 5 :$$:
+infixl 6 :<>:
+
+type family TypeError (a :: ErrorMessage) :: b where
+
+
 --------------------------------------------------------------------------------
 
 -- | We either get evidence that this function was instantiated with the