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

Be more aggressive when checking constraints for custom type errors.

This fixes #11990.

The current rule is simpler than before: if we encounter an unsolved
constraint that contains any mentions of properly applied `TypeError`,
then we report the type error.

If there are multiple `TypeErrors`, then we just report one of them.

Reviewers: simonpj, bgamari, austin

Reviewed By: simonpj

Subscribers: thomie

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

GHC Trac Issues: #11990
parent aa5e2ddc
......@@ -1782,18 +1782,53 @@ 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 a b c
-- 2. TypeError msg a b c ~ Something (and the other way around)
-- 4. C (TypeError msg a b c) (for any parameter of class constraint)
{- Note [Custom type errors in constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When GHC reports a type-error about an unsolved-constraint, we check
to see if the constraint contains any custom-type errors, and if so
we report them. Here are some examples of constraints containing type
errors:
TypeError msg -- The actual constraint is a type error
TypError msg ~ Int -- Some type was supposed to be Int, but ended up
-- being a type error instead
Eq (TypeError msg) -- A class constraint is stuck due to a type error
F (TypeError msg) ~ a -- A type function failed to evaluate due to a type err
It is also possible to have constraints where the type error is nested deeper,
for example see #11990, and also:
Eq (F (TypeError msg)) -- Here the type error is nested under a type-function
-- call, which failed to evaluate because of it,
-- and so the `Eq` constraint was unsolved.
-- This may happen when one function calls another
-- and the called function produced a custom type error.
-}
-- | A constraint is considered to be a custom type error, if it contains
-- custom type errors anywhere in it.
-- See Note [Custom type errors in constraints]
getUserTypeErrorMsg :: Ct -> Maybe Type
getUserTypeErrorMsg ct
| Just (_,t1,t2) <- getEqPredTys_maybe ctT = oneOf [t1,t2]
| Just (_,ts) <- getClassPredTys_maybe ctT = oneOf ts
| otherwise = userTypeError_maybe ctT
getUserTypeErrorMsg ct = findUserTypeError (ctPred ct)
where
ctT = ctPred ct
oneOf xs = msum (map userTypeError_maybe xs)
findUserTypeError t = msum ( userTypeError_maybe t
: map findUserTypeError (subTys t)
)
subTys t = case splitAppTys t of
(t,[]) ->
case splitTyConApp_maybe t of
Nothing -> []
Just (_,ts) -> ts
(t,ts) -> t : ts
isUserTypeErrorCt :: Ct -> Bool
isUserTypeErrorCt ct = case getUserTypeErrorMsg ct of
......
{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
{-# LANGUAGE UndecidableInstances, ScopedTypeVariables, FlexibleContexts #-}
module T11990a where
import GHC.TypeLits
import Data.Proxy
type family PartialTF t :: Symbol where
PartialTF Int = "Int"
PartialTF Bool = "Bool"
PartialTF a = TypeError (Text "Unexpected type @ PartialTF: "
:<>: ShowType a)
testPartialTF :: forall a.(KnownSymbol (PartialTF a)) => a -> String
testPartialTF t = symbolVal (Proxy :: Proxy (PartialTF a))
t1 = testPartialTF 'a'
{- Above code rightly fails with the following error:
• Unexpected type: Char
• In the expression: testPartialTF 'a'
In an equation for ‘t1’: t1 = testPartialTF 'a'
-}
T11990a.hs:18:6:
Unexpected type @ PartialTF: Char
In the expression: testPartialTF 'a'
In an equation for ‘t1’: t1 = testPartialTF 'a'
{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
{-# LANGUAGE UndecidableInstances, ScopedTypeVariables, FlexibleContexts #-}
module T11990b where
import GHC.TypeLits
import Data.Proxy
type family PartialTF t :: Symbol where
PartialTF Int = "Int"
PartialTF Bool = "Bool"
PartialTF a = TypeError (Text "Unexpected type @ PartialTF: "
:<>: ShowType a)
type family NestedPartialTF (tsym :: Symbol) :: Symbol where
NestedPartialTF "Int" = "int"
NestedPartialTF "Bool" = "bool"
NestedPartialTF a =
TypeError (Text "Unexpected type @ NestedPartialTF: " :<>: ShowType a)
testPartialTF :: forall a.(KnownSymbol (PartialTF a)) => a -> String
testPartialTF t = symbolVal (Proxy :: Proxy (PartialTF a))
testNesPartialTF ::
forall a.(KnownSymbol (NestedPartialTF (PartialTF a))) => a -> String
testNesPartialTF t = symbolVal (Proxy :: Proxy (NestedPartialTF (PartialTF a)))
t2 = testNesPartialTF 'a'
T11990b.hs:28:6:
Unexpected type @ PartialTF: Char
In the expression: testNesPartialTF 'a'
In an equation for ‘t2’: t2 = testNesPartialTF 'a'
......@@ -416,3 +416,5 @@ test('BadUnboxedTuple', normal, compile_fail, [''])
test('T11698', normal, compile_fail, [''])
test('T11947a', normal, compile_fail, [''])
test('T11948', normal, compile_fail, [''])
test('T11990a', normal, compile_fail, [''])
test('T11990b', 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