Commit 2d1a563b authored by Iavor S. Diatchki's avatar Iavor S. Diatchki Committed by Ben Gamari

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
parent e2d9821b
......@@ -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
-----------------------------------------------------
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
{-# 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
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
{-# 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
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
{-# LANGUAGE DataKinds #-}
module T3 where
import GHC.TypeLits
f :: TypeError (Text "This is a type error")
f = undefined
CustomTypeErrors03.hs:6:6: error:
This is a type error
In the type signature for ‘f’:
f :: TypeError (Text "This is a type error")
......@@ -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, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment