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

14 files changed, 237 insertions, 4 deletions

diff --git a/compiler/prelude/PrelNames.hs b/compiler/prelude/PrelNames.hs
index 7229f76401..74c3118a71 100644
--- a/compiler/prelude/PrelNames.hs
+++ b/compiler/prelude/PrelNames.hs
@@ -360,6 +360,13 @@ basicKnownKeyNames
         -- Fingerprint
         , fingerprintDataConName
 
+        -- Custom type errors
+        , errorMessageTypeErrorFamName
+        , typeErrorTextDataConName
+        , typeErrorAppendDataConName
+        , typeErrorVAppendDataConName
+        , typeErrorShowTypeDataConName
+
     ] ++ case cIntegerLibraryType of
            IntegerGMP    -> [integerSDataConName]
            IntegerSimple -> []
@@ -1102,6 +1109,30 @@ mkAppTyName           = varQual tYPEABLE_INTERNAL (fsLit "mkAppTy")        mkApp
 typeNatTypeRepName    = varQual tYPEABLE_INTERNAL (fsLit "typeNatTypeRep") typeNatTypeRepKey
 typeSymbolTypeRepName = varQual tYPEABLE_INTERNAL (fsLit "typeSymbolTypeRep") typeSymbolTypeRepKey
 
+-- Custom type errors
+errorMessageTypeErrorFamName
+  , typeErrorTextDataConName
+  , typeErrorAppendDataConName
+  , typeErrorVAppendDataConName
+  , typeErrorShowTypeDataConName
+  :: Name
+
+errorMessageTypeErrorFamName =
+  tcQual gHC_TYPELITS (fsLit "TypeError") errorMessageTypeErrorFamKey
+
+typeErrorTextDataConName =
+  dcQual gHC_TYPELITS (fsLit "Text") typeErrorTextDataConKey
+
+typeErrorAppendDataConName =
+  dcQual gHC_TYPELITS (fsLit ":<>:") typeErrorAppendDataConKey
+
+typeErrorVAppendDataConName =
+  dcQual gHC_TYPELITS (fsLit ":$$:") typeErrorVAppendDataConKey
+
+typeErrorShowTypeDataConName =
+  dcQual gHC_TYPELITS (fsLit "ShowType") typeErrorShowTypeDataConKey
+
+
 
 -- Dynamic
 toDynName :: Name
@@ -1585,6 +1616,12 @@ typeNatSubTyFamNameKey    = mkPreludeTyConUnique 170
 typeSymbolCmpTyFamNameKey = mkPreludeTyConUnique 171
 typeNatCmpTyFamNameKey    = mkPreludeTyConUnique 172
 
+-- Custom user type-errors
+errorMessageTypeErrorFamKey :: Unique
+errorMessageTypeErrorFamKey =  mkPreludeTyConUnique 173
+
+
+
 ntTyConKey:: Unique
 ntTyConKey = mkPreludeTyConUnique 174
 coercibleTyConKey :: Unique
@@ -1705,6 +1742,16 @@ trTyConDataConKey                       = mkPreludeDataConUnique 40
 trModuleDataConKey                      = mkPreludeDataConUnique 41
 trNameSDataConKey                       = mkPreludeDataConUnique 42
 
+typeErrorTextDataConKey,
+  typeErrorAppendDataConKey,
+  typeErrorVAppendDataConKey,
+  typeErrorShowTypeDataConKey
+  :: Unique
+typeErrorTextDataConKey                 = mkPreludeDataConUnique 50
+typeErrorAppendDataConKey               = mkPreludeDataConUnique 51
+typeErrorVAppendDataConKey              = mkPreludeDataConUnique 52
+typeErrorShowTypeDataConKey             = mkPreludeDataConUnique 53
+
 ---------------- Template Haskell -------------------
 --      THNames.hs: USES DataUniques 100-150
 -----------------------------------------------------
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 8c88d22dd3..5fdd7def0d 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -352,7 +352,9 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
     -- (see TcRnTypes.trulyInsoluble) is caught here, otherwise
     -- we might suppress its error message, and proceed on past
     -- type checking to get a Lint error later
-    report1 = [ ("insoluble1",   is_given,        True, mkGroupReporter mkEqErr)
+    report1 = [ ("custom_error", is_user_type_error,
+                                                  True, mkUserTypeErrorReporter)
+              , ("insoluble1",   is_given,        True, mkGroupReporter mkEqErr)
               , ("insoluble2",   utterly_wrong,   True, mkGroupReporter mkEqErr)
               , ("insoluble3",   rigid_nom_tv_eq, True, mkSkolReporter)
               , ("insoluble4",   rigid_nom_eq,    True, mkGroupReporter mkEqErr)
@@ -376,7 +378,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
 
     is_out_of_scope ct _ = isOutOfScopeCt ct
     is_hole         ct _ = isHoleCt ct
-
+    is_user_type_error ct _ = isUserTypeErrorCt ct
     is_given  ct _ = not (isWantedCt ct)  -- The Derived ones are actually all from Givens
 
     -- Skolem (i.e. non-meta) type variable on the left
@@ -437,6 +439,18 @@ mkHoleReporter ctxt
        ; maybeReportHoleError ctxt ct err
        ; maybeAddDeferredHoleBinding ctxt err ct }
 
+mkUserTypeErrorReporter :: Reporter
+mkUserTypeErrorReporter ctxt
+  = mapM_ $ \ct -> maybeReportError ctxt =<< mkUserTypeError ctxt ct
+
+mkUserTypeError :: ReportErrCtxt -> Ct -> TcM ErrMsg
+mkUserTypeError ctxt ct = mkErrorMsgFromCt ctxt ct
+                        $ pprUserTypeErrorTy
+                        $ case getUserTypeErrorMsg ct of
+                            Just (_,msg) -> msg
+                            Nothing      -> pprPanic "mkUserTypeError" (ppr ct)
+
+
 mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
                              -- Make error message for a group
                 -> Reporter  -- Deal with lots of constraints
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 06ab9c2eda..3f703fa9e3 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -61,6 +61,7 @@ module TcRnTypes(
         isCDictCan_Maybe, isCFunEqCan_maybe,
         isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
         isGivenCt, isHoleCt, isOutOfScopeCt, isExprHoleCt, isTypeHoleCt,
+        isUserTypeErrorCt, getUserTypeErrorMsg,
         ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
         mkNonCanonical, mkNonCanonicalCt,
         ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
@@ -145,7 +146,7 @@ import ListSetOps
 import FastString
 import GHC.Fingerprint
 
-import Control.Monad (ap, liftM)
+import Control.Monad (ap, liftM, msum)
 
 #ifdef GHCI
 import Data.Map      ( Map )
@@ -1426,6 +1427,24 @@ isTypeHoleCt :: Ct -> Bool
 isTypeHoleCt (CHoleCan { cc_hole = TypeHole }) = True
 isTypeHoleCt _ = False
 
+-- | The following constraints are considered to be a custom type error:
+--    1. TypeError msg
+--    2. TypeError msg ~ Something  (and the other way around)
+--    3. C (TypeError msg)          (for any parameter of class constraint)
+getUserTypeErrorMsg :: Ct -> Maybe (Kind, Type)
+getUserTypeErrorMsg ct
+  | Just (_,t1,t2) <- getEqPredTys_maybe ctT    = oneOf [t1,t2]
+  | Just (_,ts)    <- getClassPredTys_maybe ctT = oneOf ts
+  | otherwise                                   = isUserErrorTy ctT
+  where
+  ctT       = ctPred ct
+  oneOf xs  = msum (map isUserErrorTy xs)
+
+isUserTypeErrorCt :: Ct -> Bool
+isUserTypeErrorCt ct = case getUserTypeErrorMsg ct of
+                         Just _ -> True
+                         _      -> False
+
 instance Outputable Ct where
   ppr ct = ppr (cc_ev ct) <+> parens (text ct_sort)
          where ct_sort = case ct of
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 62449beaa4..3b5d206a67 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -232,6 +232,16 @@ checkAmbiguity ctxt ty
        mk_msg ty = pprSigCtxt ctxt (ptext (sLit "the ambiguity check for")) (ppr ty)
        ambig_msg = ptext (sLit "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes")
 
+
+checkUserTypeError :: Type -> TcM ()
+checkUserTypeError = check
+  where
+  check ty
+    | Just (_,msg) <- isUserErrorTy ty = failWithTc (pprUserTypeErrorTy msg)
+    | Just (_,ts)  <- splitTyConApp_maybe ty  = mapM_ check ts
+    | Just (t1,t2) <- splitAppTy_maybe ty     = check t1 >> check t2
+    | otherwise                               = return ()
+
 {-
 ************************************************************************
 *                                                                      *
@@ -312,6 +322,8 @@ checkValidType ctxt ty
         -- the kind of an ill-formed type such as (a~Int)
        ; check_kind ctxt ty
 
+       ; checkUserTypeError ty
+
        -- Check for ambiguous types.  See Note [When to call checkAmbiguity]
        -- NB: this will happen even for monotypes, but that should be cheap;
        --     and there may be nested foralls for the subtype test to examine
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 0c8ed35776..a7d6ca96bf 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -39,6 +39,8 @@ module Type (
         mkNumLitTy, isNumLitTy,
         mkStrLitTy, isStrLitTy,
 
+        isUserErrorTy, pprUserTypeErrorTy,
+
         coAxNthLHS,
 
         -- (Newtypes)
@@ -165,7 +167,13 @@ import TysPrim
 import {-# SOURCE #-} TysWiredIn ( eqTyCon, coercibleTyCon, typeNatKind, typeSymbolKind )
 import PrelNames ( eqTyConKey, coercibleTyConKey,
                    ipTyConKey, openTypeKindTyConKey,
-                   constraintKindTyConKey, liftedTypeKindTyConKey )
+                   constraintKindTyConKey, liftedTypeKindTyConKey,
+                   errorMessageTypeErrorFamName,
+                   typeErrorTextDataConName,
+                   typeErrorShowTypeDataConName,
+                   typeErrorAppendDataConName,
+                   typeErrorVAppendDataConName
+                )
 import CoAxiom
 
 -- others
@@ -448,6 +456,44 @@ isStrLitTy ty | Just ty1 <- tcView ty = isStrLitTy ty1
 isStrLitTy (LitTy (StrTyLit s)) = Just s
 isStrLitTy _                    = Nothing
 
+
+-- | Is this type a custom user error?
+-- If so, give us the kind and the error message.
+isUserErrorTy :: Type -> Maybe (Kind,Type)
+isUserErrorTy t = do (tc,[k,msg]) <- splitTyConApp_maybe t
+                     guard (tyConName tc == errorMessageTypeErrorFamName)
+                     return (k,msg)
+
+-- | Render a type corresponding to a user type error into a SDoc.
+pprUserTypeErrorTy :: Type -> SDoc
+pprUserTypeErrorTy ty =
+  case splitTyConApp_maybe ty of
+
+    -- Text "Something"
+    Just (tc,[txt])
+      | tyConName tc == typeErrorTextDataConName
+      , Just str <- isStrLitTy txt -> ftext str
+
+    -- ShowType t
+    Just (tc,[_k,t])
+      | tyConName tc == typeErrorShowTypeDataConName -> ppr t
+
+    -- t1 :<>: t2
+    Just (tc,[t1,t2])
+      | tyConName tc == typeErrorAppendDataConName ->
+        pprUserTypeErrorTy t1 <> pprUserTypeErrorTy t2
+
+    -- t1 :$$: t2
+    Just (tc,[t1,t2])
+      | tyConName tc == typeErrorVAppendDataConName ->
+        pprUserTypeErrorTy t1 $$ pprUserTypeErrorTy t2
+
+    -- An uneavaluated type function
+    _ -> ppr ty
+
+
+
+
 {-
 ---------------------------------------------------------------------
                                 FunTy
diff --git a/compiler/types/TypeRep.hs b/compiler/types/TypeRep.hs
index 7f57073da8..e09c9377b6 100644
--- a/compiler/types/TypeRep.hs
+++ b/compiler/types/TypeRep.hs
@@ -713,6 +713,8 @@ pprTyTcApp p tc tys
     if gopt Opt_PrintExplicitKinds dflags then pprTcApp  p ppr_type tc tys
                                    else pprTyList p ty1 ty2
 
+  | tc `hasKey` errorMessageTypeErrorFamKey = text "(TypeError ...)"
+
   | otherwise
   = pprTcApp p ppr_type tc tys
 
@@ -722,6 +724,7 @@ pprTcApp _ pp tc [ty]
   | tc `hasKey` listTyConKey = pprPromotionQuote tc <> brackets   (pp TopPrec ty)
   | tc `hasKey` parrTyConKey = pprPromotionQuote tc <> paBrackets (pp TopPrec ty)
 
+
 pprTcApp p pp tc tys
   | Just sort <- tyConTuple_maybe tc
   , tyConArity tc == length tys
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
diff --git a/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.hs b/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.hs
new file mode 100644
index 0000000000..c44da1d6b9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds, UndecidableInstances #-}
+module T1 where
+import GHC.TypeLits
+
+
+data MyType = MyType
+
+instance
+  TypeError (Text "Values of type 'MyType' cannot be compared for equality.")
+    => Eq MyType where (==) = undefined
+
+err x = x == MyType
+
+
diff --git a/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.stderr b/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.stderr
new file mode 100644
index 0000000000..d95de09530
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.stderr
@@ -0,0 +1,5 @@
+
+CustomTypeErrors01.hs:12:11: error:
+    Values of type 'MyType' cannot be compared for equality.
+    In the expression: x == MyType
+    In an equation for ‘err’: err x = x == MyType
diff --git a/testsuite/tests/typecheck/should_fail/CustomTypeErrors02.hs b/testsuite/tests/typecheck/should_fail/CustomTypeErrors02.hs
new file mode 100644
index 0000000000..06eb234071
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/CustomTypeErrors02.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE DataKinds, UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleContexts #-}
+module T2 where
+
+import GHC.TypeLits
+
+type family IntRep a where
+  IntRep Int      = Integer
+  IntRep Integer  = Integer
+  IntRep Bool     = Integer
+  IntRep a        = TypeError (Text "The type '" :<>: ShowType a :<>:
+                               Text "' cannot be represented as an integer.")
+
+convert :: Num (IntRep a) => a -> IntRep a
+convert _ = 5
+
+err = convert id
+
+
diff --git a/testsuite/tests/typecheck/should_fail/CustomTypeErrors02.stderr b/testsuite/tests/typecheck/should_fail/CustomTypeErrors02.stderr
new file mode 100644
index 0000000000..9ca22eebbd
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/CustomTypeErrors02.stderr
@@ -0,0 +1,10 @@
+
+CustomTypeErrors02.hs:17:1: error:
+    The type 'a_aES -> a_aES' cannot be represented as an integer.
+    When checking that ‘err’ has the inferred type
+      err :: (TypeError ...)
+
+CustomTypeErrors02.hs:17:7: error:
+    The type 'a0 -> a0' cannot be represented as an integer.
+    In the expression: convert id
+    In an equation for ‘err’: err = convert id
diff --git a/testsuite/tests/typecheck/should_fail/CustomTypeErrors03.hs b/testsuite/tests/typecheck/should_fail/CustomTypeErrors03.hs
new file mode 100644
index 0000000000..8c122276ec
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/CustomTypeErrors03.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE DataKinds #-}
+module T3 where
+
+import GHC.TypeLits
+
+f :: TypeError (Text "This is a type error")
+f = undefined
diff --git a/testsuite/tests/typecheck/should_fail/CustomTypeErrors03.stderr b/testsuite/tests/typecheck/should_fail/CustomTypeErrors03.stderr
new file mode 100644
index 0000000000..330fadb6fd
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/CustomTypeErrors03.stderr
@@ -0,0 +1,5 @@
+
+CustomTypeErrors03.hs:6:6: error:
+    This is a type error
+    In the type signature for ‘f’:
+      f :: TypeError (Text "This is a type error")
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 0a222bde90..c2ec10526f 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -390,3 +390,8 @@ test('T10715', normal, compile_fail, [''])
 test('T10715b', normal, compile_fail, [''])
 test('T10971b', normal, compile_fail, [''])
 test('T10971d', extra_clean(['T10971c.hi', 'T10971c.o']), multimod_compile_fail, ['T10971d','-v0'])
+test('CustomTypeErrors01', normal, compile_fail, [''])
+test('CustomTypeErrors02', normal, compile_fail, [''])
+test('CustomTypeErrors03', normal, compile_fail, [''])
+
+