Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 7471eb6a by sheaf at 2025-10-07T21:39:43-04:00 Improve how we detect user type errors in types This commit cleans up all the code responsible for detecting whether a type contains "TypeError msg" applications nested inside it. All the logic is now in 'userTypeError_maybe', which is always deep. Whether it looks inside type family applications is determined by the passed-in boolean flag: - When deciding whether a constraint is definitely insoluble, don't look inside type family applications, as they may still reduce -- in which case the TypeError could disappear. - When reporting unsolved constraints, look inside type family applications: they had the chance to reduce but didn't, and the custom type error might contain valuable information. All the details are explained in Note [Custom type errors in constraints] in GHC.Tc.Types.Constraint. Another benefit of this change is that it allows us to get rid of the deeply dodgy 'getUserTypeErrorMsg' function. This commit also improves the detection of custom type errors, for example in equality constraints: TypeError blah ~# rhs It used to be the case that we didn't detect the TypeError on the LHS, because we never considered that equality constraints could be insoluble due to the presence of custom type errors. Addressing this oversight improves detection of redundant pattern match warnings, fixing #26400. - - - - - 14 changed files: - compiler/GHC/Core/Predicate.hs - compiler/GHC/Core/Type.hs - compiler/GHC/Tc/Errors.hs - compiler/GHC/Tc/Solver.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Validity.hs - + testsuite/tests/pmcheck/should_compile/T26400.hs - + testsuite/tests/pmcheck/should_compile/T26400.stderr - + testsuite/tests/pmcheck/should_compile/T26400b.hs - testsuite/tests/pmcheck/should_compile/all.T - testsuite/tests/typecheck/should_fail/T20241b.stderr - testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr Changes: ===================================== compiler/GHC/Core/Predicate.hs ===================================== @@ -217,7 +217,7 @@ in GHC.Tc.Solver.Dict. -- See Note [Types for coercions, predicates, and evidence] in "GHC.Core.TyCo.Rep" isEqPred :: PredType -> Bool -- True of (s ~# t) (s ~R# t) --- NB: but NOT true of (s ~ t) or (s ~~ t) or (Coecible s t) +-- NB: but NOT true of (s ~ t) or (s ~~ t) or (Coercible s t) isEqPred ty | Just tc <- tyConAppTyCon_maybe ty = tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey ===================================== compiler/GHC/Core/Type.hs ===================================== @@ -74,8 +74,7 @@ module GHC.Core.Type ( mkCastTy, mkCoercionTy, splitCastTy_maybe, - ErrorMsgType, - userTypeError_maybe, deepUserTypeError_maybe, pprUserTypeErrorTy, + ErrorMsgType, pprUserTypeErrorTy, coAxNthLHS, stripCoercionTy, @@ -272,7 +271,7 @@ import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Data.FastString -import GHC.Data.Maybe ( orElse, isJust, firstJust ) +import GHC.Data.Maybe ( orElse, isJust ) import GHC.List (build) -- $type_classification @@ -1223,45 +1222,6 @@ isLitTy ty -- | A type of kind 'ErrorMessage' (from the 'GHC.TypeError' module). type ErrorMsgType = Type --- | Is this type a custom user error? --- If so, give us the error message. -userTypeError_maybe :: Type -> Maybe ErrorMsgType -userTypeError_maybe ty - | Just ty' <- coreView ty = userTypeError_maybe ty' -userTypeError_maybe (TyConApp tc (_kind : msg : _)) - | tyConName tc == errorMessageTypeErrorFamName - -- There may be more than 2 arguments, if the type error is - -- used as a type constructor (e.g. at kind `Type -> Type`). - = Just msg -userTypeError_maybe _ - = Nothing - -deepUserTypeError_maybe :: Type -> Maybe ErrorMsgType --- Look for custom user error, deeply inside the type -deepUserTypeError_maybe ty - | Just ty' <- coreView ty = userTypeError_maybe ty' -deepUserTypeError_maybe (TyConApp tc tys) - | tyConName tc == errorMessageTypeErrorFamName - , _kind : msg : _ <- tys - -- There may be more than 2 arguments, if the type error is - -- used as a type constructor (e.g. at kind `Type -> Type`). - = Just msg - - | tyConMustBeSaturated tc -- Don't go looking for user type errors - -- inside type family arguments (see #20241). - = foldr (firstJust . deepUserTypeError_maybe) Nothing (drop (tyConArity tc) tys) - | otherwise - = foldr (firstJust . deepUserTypeError_maybe) Nothing tys -deepUserTypeError_maybe (ForAllTy _ ty) = deepUserTypeError_maybe ty -deepUserTypeError_maybe (FunTy { ft_arg = arg, ft_res = res }) - = deepUserTypeError_maybe arg `firstJust` deepUserTypeError_maybe res -deepUserTypeError_maybe (AppTy t1 t2) - = deepUserTypeError_maybe t1 `firstJust` deepUserTypeError_maybe t2 -deepUserTypeError_maybe (CastTy ty _) - = deepUserTypeError_maybe ty -deepUserTypeError_maybe _ -- TyVarTy, CoercionTy, LitTy - = Nothing - -- | Render a type corresponding to a user type error into a SDoc. pprUserTypeErrorTy :: ErrorMsgType -> SDoc pprUserTypeErrorTy ty = ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -671,11 +671,14 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics non_tv_eq _ _ = False -- Catch TypeError and Unsatisfiable. - -- Here, we want any nested TypeErrors to bubble up, so we use - -- 'containsUserTypeError' and not 'isTopLevelUserTypeError'. + -- Here, we want any nested TypeErrors to bubble up, even if they are + -- inside type family applications, so we pass 'True' to + -- 'containsUserTypeError'. -- -- See also Note [Implementation of Unsatisfiable constraints], point (F). - is_user_type_error item _ = containsUserTypeError (errorItemPred item) + is_user_type_error item _ = containsUserTypeError True (errorItemPred item) + -- True <=> look under ty-fam apps, AppTy etc. + -- See (UTE2) in Note [Custom type errors in constraints]. is_implicit_lifting item _ = case (errorItemOrigin item) of @@ -977,6 +980,8 @@ Its implementation consists of the following: This is the only way that "Unsatisfiable msg" constraints are reported, which makes their behaviour much more predictable than TypeError. + We don't go looking for Unsatisfiable constraints deeply nested inside + a type like we do for TypeError. -} @@ -1124,12 +1129,21 @@ mkUserTypeErrorReporter ctxt ; maybeReportError ctxt (item :| []) err ; addSolverDeferredBinding err item } + + mkUserTypeError :: ErrorItem -> TcSolverReportMsg mkUserTypeError item - | Just msg <- getUserTypeErrorMsg pty - = UserTypeError msg | Just msg <- isUnsatisfiableCt_maybe pty = UnsatisfiableError msg + | Just msg <- userTypeError_maybe True pty + -- ^^^^ + -- Look under type-family applications! We are reporting an error, + -- so we may as well look to see if there are any custom type errors + -- anywhere, as they might be helpful to the user. We gave the type + -- family application the chance to reduce, but it didn't. + -- + -- See (UTE2) in Note [Custom type errors in constraints] in GHC.Tc.Types.Constraint. + = UserTypeError msg | otherwise = pprPanic "mkUserTypeError" (ppr item) where ===================================== compiler/GHC/Tc/Solver.hs ===================================== @@ -659,20 +659,70 @@ equality constraint, but it is also important to detect custom type errors: To see that we can't call `foo (MkT2)`, we must detect that `NotInt Int` is insoluble because it is a custom type error. -Failing to do so proved quite inconvenient for users, as evidence by the +Failing to do so proved quite inconvenient for users, as evidenced by the tickets #11503 #14141 #16377 #20180. Test cases: T11503, T14141. -Examples of constraints that tcCheckGivens considers insoluble: +To do this, tcCheckGivens calls getInertInsols, which returns all Given +constraints that are definitely insoluble. See Note [When is a constraint insoluble?]. + +Note [When is a constraint insoluble?] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Whether a constraint is insoluble matters for accurate pattern-match +warnings, as explained in Note [Pattern match warnings with insoluble Givens]. + +We consider a constraint to be insoluble if it definitely cannot be solved, +no matter what information we might further discover. For example, the following +constraints are insoluble: + - Int ~ Bool, - Coercible Float Word, - - TypeError msg. - -Non-examples: - - constraints which we know aren't satisfied, - e.g. Show (Int -> Int) when no such instance is in scope, - - Eq (TypeError msg), - - C (Int ~ Bool), with @class C (c :: Constraint)@. + - TypeError msg + - TypeError msg ~ Int + - Unsatisfiable msg + +Many constraints that look like they can't be solved are in fact not reported +as insoluble, as there might still be a possibility (no matter how remote) that +they can still be solved: + + 1: Show (Int -> Int) + + Reason: even though there is no relevant instance in scope, this constraint + could later get solved by a new instance. + + 2: C (Int ~ Bool), where C :: Constraint -> Constraint + + Reason: even though 'Int ~ Bool' is insoluble, the constraint 'C (Int ~ Bool)' + might be soluble, e.g. if 'C' is a class and we have 'instance forall c. C c', + or 'C' is a type family and we have 'type instance C c = (() :: Constraint)'. + + 3: Nested occurences of TypeError don't always lead to insolubility. For + example, none of the following constraints are definitely insoluble: + + (a) F alpha (TypeError msg) -- 'F' is an arity 2 type family + (b) Eq (TypeError msg) + (c) c (TypeError msg) -- 'c' is a metavariable + (d) (TC alpha) (TypeError msg) -- 'TC' is an arity 1 type family + (e) TypeError msg ~ rhs -- (depends on rhs) + + None of these constraints are definitely insoluble: + + (a) Can be solved if 'F' reduces, e.g. 'alpha := Int', 'type instance F Int a = (() :: Constraint)'. + (b) Can be solved by 'instance forall x. Eq x'. + (c) Can be solved if 'c' unifies with 'C', as in example (2). + (d) Can be solved if 'TC alpha' reduces to 'C', as in example (2). + (e) If 'rhs' is a rigid type such as 'Int' or 'Maybe Char', then this + constraint is definitely insoluble. Otherwise, however, the constraint + could be soluble: + - rhs = G alpha, for an arity 1 type family G + G alpha could reduce to TypeError msg. + - rhs = k, for a skolem type variable k. + We could instantiate k to something else, and then the constraint + could become soluble. + + For this reason, we are careful to not pull out certain occurrences of TypeError, + e.g. inside type family applications and class constraints. + See Note [Custom type errors in constraints]. -} tcCheckGivens :: InertSet -> Bag EvVar -> TcM (Maybe InertSet) ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -172,7 +172,7 @@ import GHC.Tc.Types.Origin import GHC.Tc.Types.CtLoc import GHC.Tc.Types.Constraint -import GHC.Builtin.Names ( unsatisfiableClassNameKey, callStackTyConName, exceptionContextTyConName ) +import GHC.Builtin.Names ( callStackTyConName, exceptionContextTyConName ) import GHC.Core.Type import GHC.Core.TyCo.Rep as Rep @@ -185,6 +185,10 @@ import GHC.Core.Class import GHC.Core.TyCon import GHC.Core.Unify (typesAreApart) +import GHC.LanguageExtensions as LangExt +import GHC.Rename.Env +import qualified GHC.Rename.Env as TcM + import GHC.Types.Name import GHC.Types.TyThing import GHC.Types.Name.Reader @@ -199,8 +203,7 @@ import GHC.Types.ThLevelIndex (thLevelIndexFromImportLevel) import GHC.Types.SrcLoc import GHC.Unit.Module -import qualified GHC.Rename.Env as TcM -import GHC.Rename.Env +import GHC.Unit.Module.Graph import GHC.Utils.Outputable import GHC.Utils.Panic @@ -220,15 +223,13 @@ import Data.List ( mapAccumL ) import Data.List.NonEmpty ( nonEmpty ) import qualified Data.List.NonEmpty as NE import qualified Data.Semigroup as S -import GHC.LanguageExtensions as LangExt +import qualified Data.Set as Set #if defined(DEBUG) import GHC.Types.Unique.Set (nonDetEltsUniqSet) import GHC.Data.Graph.Directed #endif -import qualified Data.Set as Set -import GHC.Unit.Module.Graph {- ********************************************************************* * * @@ -666,9 +667,10 @@ getInnermostGivenEqLevel = do { inert <- getInertCans -- This consists of: -- -- - insoluble equalities, such as @Int ~# Bool@; --- - constraints that are top-level custom type errors, of the form --- @TypeError msg@, but not constraints such as @Eq (TypeError msg)@ --- in which the type error is nested; +-- - constraints that are custom type errors, of the form +-- @TypeError msg@ or @Maybe (TypeError msg)@, but not constraints such as +-- @F x (TypeError msg)@ in which the type error is nested under +-- a type family application, -- - unsatisfiable constraints, of the form @Unsatisfiable msg@. -- -- The inclusion of Givens is important for pattern match warnings, as we @@ -676,21 +678,26 @@ getInnermostGivenEqLevel = do { inert <- getInertCans -- redundant (see Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver). getInertInsols :: TcS Cts getInertInsols - = do { inert <- getInertCans - ; let insols = filterBag insolubleIrredCt (inert_irreds inert) - unsats = findDictsByTyConKey (inert_dicts inert) unsatisfiableClassNameKey - ; return $ fmap CDictCan unsats `unionBags` fmap CIrredCan insols } + -- See Note [When is a constraint insoluble?] + = do { inert_cts <- getInertCts + ; return $ filterBag insolubleCt inert_cts } + +getInertCts :: TcS Cts +getInertCts + = do { inerts <- getInertCans + ; return $ + unionManyBags + [ fmap CIrredCan $ inert_irreds inerts + , foldDicts (consBag . CDictCan) (inert_dicts inerts) emptyBag + , foldFunEqs (consBag . CEqCan ) (inert_funeqs inerts) emptyBag + , foldTyEqs (consBag . CEqCan ) (inert_eqs inerts) emptyBag + ] } getInertGivens :: TcS [Ct] -- Returns the Given constraints in the inert set getInertGivens - = do { inerts <- getInertCans - ; let all_cts = foldIrreds ((:) . CIrredCan) (inert_irreds inerts) - $ foldDicts ((:) . CDictCan) (inert_dicts inerts) - $ foldFunEqs ((:) . CEqCan) (inert_funeqs inerts) - $ foldTyEqs ((:) . CEqCan) (inert_eqs inerts) - $ [] - ; return (filter isGivenCt all_cts) } + = do { all_cts <- getInertCts + ; return (filter isGivenCt $ bagToList all_cts) } getPendingGivenScs :: TcS [Ct] -- Find all inert Given dictionaries, or quantified constraints, such that ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -471,7 +471,9 @@ findRedundantGivens (Implic { ic_info = info, ic_need = need, ic_given = givens | otherwise = filterOut is_minimal givens -- See #15232 - is_type_error id = isTopLevelUserTypeError (idType id) + is_type_error id = containsUserTypeError False (idType id) + -- False <=> do not look under ty-fam apps, AppTy etc. + -- See (UTE1) in Note [Custom type errors in constraints]. is_improving pred -- (transSuperClasses p) does not include p = any isImprovementPred (pred : transSuperClasses pred) ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -1,6 +1,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE TypeApplications #-} -- | This module defines types and simple operations over constraints, as used @@ -13,7 +14,7 @@ module GHC.Tc.Types.Constraint ( isPendingScDictCt, isPendingScDict, pendingScDict_maybe, superClassesMightHelp, getPendingWantedScs, isWantedCt, isGivenCt, - isTopLevelUserTypeError, containsUserTypeError, getUserTypeErrorMsg, + userTypeError_maybe, containsUserTypeError, isUnsatisfiableCt_maybe, ctEvidence, updCtEvidence, ctLoc, ctPred, ctFlavour, ctEqRel, ctOrigin, @@ -59,7 +60,7 @@ module GHC.Tc.Types.Constraint ( addInsols, dropMisleading, addSimples, addImplics, addHoles, addNotConcreteError, addMultiplicityCoercionError, addDelayedErrors, tyCoVarsOfWC, tyCoVarsOfWCList, - insolubleWantedCt, insolubleCt, insolubleIrredCt, + insolubleWantedCt, insolubleCt, insolubleImplic, nonDefaultableTyVarsOfWC, approximateWCX, approximateWC, @@ -113,6 +114,7 @@ import GHC.Core.Coercion import GHC.Core.Class import GHC.Core.TyCon import GHC.Core.TyCo.Ppr +import GHC.Core.TyCo.Rep import GHC.Types.Name import GHC.Types.Var @@ -136,16 +138,13 @@ import GHC.Utils.Constants (debugIsOn) import GHC.Data.Bag +import Control.Monad ( when ) import Data.Coerce -import qualified Data.Semigroup as S -import Control.Monad ( msum, when ) +import Data.List ( intersperse ) import Data.Maybe ( mapMaybe, isJust ) - --- these are for CheckTyEqResult +import GHC.Data.Maybe ( firstJust, firstJusts ) +import qualified Data.Semigroup as S import Data.Word ( Word8 ) -import Data.List ( intersperse ) - - {- ************************************************************************ @@ -1198,73 +1197,53 @@ insolubleWC (WC { wc_impl = implics, wc_simple = simples, wc_errors = errors }) is_insoluble (DE_Multiplicity {}) = False insolubleWantedCt :: Ct -> Bool --- Definitely insoluble, in particular /excluding/ type-hole constraints --- Namely: --- a) an insoluble constraint as per 'insolubleIrredCt', i.e. either --- - an insoluble equality constraint (e.g. Int ~ Bool), or --- - a custom type error constraint, TypeError msg :: Constraint --- b) that does not arise from a Given or a Wanted/Wanted fundep interaction +-- | Is this a definitely insoluble Wanted constraint? Namely: +-- +-- - a Wanted, +-- - which is insoluble (as per 'insolubleCt'), +-- - that does not arise from a Given or a Wanted/Wanted fundep interaction. +-- -- See Note [Insoluble Wanteds] insolubleWantedCt ct - | CIrredCan ir_ct <- ct - -- CIrredCan: see (IW1) in Note [Insoluble Wanteds] - , IrredCt { ir_ev = ev } <- ir_ct - , CtWanted (WantedCt { ctev_loc = loc, ctev_rewriters = rewriters }) <- ev + | CtWanted (WantedCt { ctev_loc = loc, ctev_rewriters = rewriters }) + <- ctEvidence ct -- It's a Wanted - , insolubleIrredCt ir_ct + , insolubleCt ct -- It's insoluble , isEmptyRewriterSet rewriters - -- It has no rewriters; see (IW2) in Note [Insoluble Wanteds] + -- It has no rewriters – see (IW1) in Note [Insoluble Wanteds] , not (isGivenLoc loc) - -- isGivenLoc: see (IW3) in Note [Insoluble Wanteds] + -- It doesn't arise from a Given – see (IW2) in Note [Insoluble Wanteds] , not (isWantedWantedFunDepOrigin (ctLocOrigin loc)) - -- origin check: see (IW4) in Note [Insoluble Wanteds] + -- It doesn't arise from a W/W fundep interaction – see (IW3) in Note [Insoluble Wanteds] = True | otherwise = False --- | Returns True of constraints that are definitely insoluble, --- as well as TypeError constraints. --- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'. +-- | Returns True of constraints that are definitely insoluble, including +-- constraints that include custom type errors, as per (1) +-- in Note [Custom type errors in constraints]. -- --- The function is tuned for application /after/ constraint solving --- i.e. assuming canonicalisation has been done --- That's why it looks only for IrredCt; all insoluble constraints --- are put into CIrredCan +-- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'. insolubleCt :: Ct -> Bool -insolubleCt (CIrredCan ir_ct) = insolubleIrredCt ir_ct -insolubleCt _ = False - -insolubleIrredCt :: IrredCt -> Bool --- Returns True of Irred constraints that are /definitely/ insoluble --- --- This function is critical for accurate pattern-match overlap warnings. --- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver --- --- Note that this does not traverse through the constraint to find --- nested custom type errors: it only detects @TypeError msg :: Constraint@, --- and not e.g. @Eq (TypeError msg)@. -insolubleIrredCt (IrredCt { ir_ev = ev, ir_reason = reason }) - = isInsolubleReason reason - || isTopLevelUserTypeError (ctEvPred ev) - -- NB: 'isTopLevelUserTypeError' detects constraints of the form "TypeError msg" - -- and "Unsatisfiable msg". It deliberately does not detect TypeError - -- nested in a type (e.g. it does not use "containsUserTypeError"), as that - -- would be too eager: the TypeError might appear inside a type family - -- application which might later reduce, but we only want to return 'True' - -- for constraints that are definitely insoluble. - -- - -- For example: Num (F Int (TypeError "msg")), where F is a type family. - -- - -- Test case: T11503, with the 'Assert' type family: - -- - -- > type Assert :: Bool -> Constraint -> Constraint - -- > type family Assert check errMsg where - -- > Assert 'True _errMsg = () - -- > Assert _check errMsg = errMsg +insolubleCt ct + | CIrredCan (IrredCt { ir_reason = reason }) <- ct + , isInsolubleReason reason + = True + | isJust $ isUnsatisfiableCt_maybe pred + = True + | containsUserTypeError False pred + -- False <=> do not look under ty-fam apps, AppTy etc. + -- See (UTE1) in Note [Custom type errors in constraints]. + = True + | otherwise + = False + where + pred = ctPred ct -- | Does this hole represent an "out of scope" error? +-- -- See Note [Insoluble holes] isOutOfScopeHole :: Hole -> Bool isOutOfScopeHole (Hole { hole_occ = occ }) = not (startsWithUnderscore (occName occ)) @@ -1312,12 +1291,7 @@ Note [Insoluble Wanteds] insolubleWantedCt returns True of a Wanted constraint that definitely can't be solved. But not quite all such constraints; see wrinkles. -(IW1) insolubleWantedCt is tuned for application /after/ constraint - solving i.e. assuming canonicalisation has been done. That's why - it looks only for IrredCt; all insoluble constraints are put into - CIrredCan - -(IW2) We only treat it as insoluble if it has an empty rewriter set. (See Note +(IW1) We only treat it as insoluble if it has an empty rewriter set. (See Note [Wanteds rewrite Wanteds].) Otherwise #25325 happens: a Wanted constraint A that is /not/ insoluble rewrites some other Wanted constraint B, so B has A in its rewriter set. Now B looks insoluble. The danger is that we'll @@ -1325,10 +1299,10 @@ can't be solved. But not quite all such constraints; see wrinkles. reporting A because there is an insoluble B lying around. (This suppression happens in GHC.Tc.Errors.mkErrorItem.) Solution: don't treat B as insoluble. -(IW3) If the Wanted arises from a Given (how can that happen?), don't +(IW2) If the Wanted arises from a Given (how can that happen?), don't treat it as a Wanted insoluble (obviously). -(IW4) If the Wanted came from a Wanted/Wanted fundep interaction, don't +(IW3) If the Wanted came from a Wanted/Wanted fundep interaction, don't treat the constraint as insoluble. See Note [Suppressing confusing errors] in GHC.Tc.Errors @@ -1354,71 +1328,165 @@ Yuk! {- 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 good use-case is described in "Detecting the undetectable" - https://blog.csongor.co.uk/report-stuck-families/ -which features - type family Assert (err :: Constraint) (break :: Type -> Type) (a :: k) :: k where - Assert _ Dummy _ = Any - Assert _ _ k = k -and an unsolved constraint like - Assert (TypeError ...) (F ty1) ty1 ~ ty2 -that reports that (F ty1) remains stuck. +A custom type error is a type family application 'TypeError msg' where +'msg :: ErrorMessage', or an Unsatisfiable constraint. +See Note [Custom type errors] and Note [The Unsatisfiable constraint] +in GHC.Internal.TypeError. + +There are two ways in which the presence of such custom type errors inside a +type impact GHC's behaviour: + + (UTE1) + Constraints that contain a custom type error are considered to be + insoluble. This affects pattern-match warnings, as explained in + Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver. + + This includes examples such as: + + TypeError msg -- The actual constraint is a type error + + TypeError msg ~# Int -- Some type was supposed to be Int, but ended up + -- being a type error instead + + However, we must be careful about occurrences of custom type errors + nested inside the constraint, as they may not make the constraint + insoluble. This is explained in Note [When is a constraint insoluble?] + in GHC.Tc.Solver. In particular: + + a. Do not look inside type family applications. + b. Do not look inside class constraints. + c. Do not look inside AppTy or in arguments of a type family past its arity. + d. Only consider 'TypeError msg ~ rhs' to be insoluble if rhs definitely + cannot unify with 'TypeError msg', e.g. if 'rhs = Int' the constraint + is insoluble, but if 'rhs = k[sk]' then it isn't. + + These subtle cases are tested in T26400b. + + A good use-case for type errors nested under type family applications is + described in "Detecting the undetectable" (https://blog.csongor.co.uk/report-stuck-families/) + which features: + type family Assert (err :: Constraint) (break :: Type -> Type) (a :: k) :: k where + Assert _ Dummy _ = Any + Assert _ _ k = k + and an unsolved constraint like 'Assert (TypeError ...) (F ty1) ty1 ~ ty2' + which reports when (F ty1) remains stuck. + + (UTE2) + When reporting unsolved constraints, we pull out any custom type errors + and report the corresponding message to the user. + + Unlike in (UTE1), we do want to pull out 'TypeError' wherever it occurs + inside the type, including inside type-family applications. We tried to + solve the constraint, reduce type families etc, but the constraint + remained unsolved all the way till the end. Now that we are reporting the + error, it makes sense to pull out the 'TypeError' and report the custom + error message to the user, as the intention is that this message might + be informative. + + Examples: + + Num (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 error + + 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. + +We use a single function, 'userTypeError_maybe', to pull out TypeError according +to the rules of either (UTE1) or (UTE2), depending on the passed in boolean +flag to 'userTypeError_maybe': 'False' for (UTE1) and 'True' for (UTE2). -} --- | 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 :: PredType -> Maybe ErrorMsgType -getUserTypeErrorMsg pred = msum $ userTypeError_maybe pred - : map getUserTypeErrorMsg (subTys pred) +-- | Does this type contain 'TypeError msg', either at the top-level or +-- nested within it somewhere? +-- +-- If so, return the error message. +-- +-- See Note [Custom type errors in constraints]. +userTypeError_maybe + :: Bool -- ^ Look everywhere: inside type-family applications, class constraints, AppTys etc? + -> Type + -> Maybe ErrorMsgType +userTypeError_maybe look_everywhere = go where - -- Richard thinks this function is very broken. What is subTys - -- supposed to be doing? Why are exactly-saturated tyconapps special? - -- What stops this from accidentally ripping apart a call to TypeError? - subTys t = case splitAppTys t of - (t,[]) -> - case splitTyConApp_maybe t of - Nothing -> [] - Just (_,ts) -> ts - (t,ts) -> t : ts - --- | Is this an user error message type, i.e. either the form @TypeError err@ or --- @Unsatisfiable err@? -isTopLevelUserTypeError :: PredType -> Bool -isTopLevelUserTypeError pred = - isJust (userTypeError_maybe pred) || isJust (isUnsatisfiableCt_maybe pred) + go ty + | Just ty' <- coreView ty + = go ty' + go (TyConApp tc tys) + | tyConName tc == errorMessageTypeErrorFamName + , _kind : msg : _ <- tys + -- There may be more than 2 arguments, if the type error is + -- used as a type constructor (e.g. at kind `Type -> Type`). + = Just msg + + -- (UTE1.d) TypeError msg ~ a is only insoluble if 'a' cannot be a type error + | not look_everywhere + , tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey + , [ ki1, ki2, ty1, ty2 ] <- tys + = if | Just msg <- go ki1 + , isRigidTy ki2 + -> Just msg + | Just msg <- go ki2 + , isRigidTy ki1 + -> Just msg + | Just msg <- go ty1 + , isRigidTy ty2 + -> Just msg + | Just msg <- go ty2 + , isRigidTy ty1 + -> Just msg + | otherwise + -> Nothing + + -- (UTE1.a) Don't look under type family applications. + | tyConMustBeSaturated tc + , not look_everywhere + = Nothing + -- (UTE1.c) Don't even look in the arguments past the arity of the TyCon. + + -- (UTE1.b) Don't look inside class constraints. + | isClassTyCon tc + , not look_everywhere + = foldr (firstJust . go) Nothing (drop (tyConArity tc) tys) + | otherwise + = foldr (firstJust . go) Nothing tys + go (ForAllTy (Bndr tv _) ty) = go (tyVarKind tv) `firstJust` go ty + go (FunTy { ft_mult = mult, ft_arg = arg, ft_res = res }) + = firstJusts + [ go mult + , go (typeKind arg) + , go (typeKind res) + , go arg + , go res ] + go (AppTy t1 t2) + -- (UTE1.c) Don't look inside AppTy. + | not look_everywhere + = Nothing + | otherwise + = go t1 `firstJust` go t2 + go (CastTy ty _co) = go ty + go (TyVarTy tv) = go (tyVarKind tv) + go (CoercionTy {}) = Nothing + go (LitTy {}) = Nothing -- | Does this constraint contain an user error message? -- -- That is, the type is either of the form @Unsatisfiable err@, or it contains -- a type of the form @TypeError msg@, either at the top level or nested inside -- the type. -containsUserTypeError :: PredType -> Bool -containsUserTypeError pred = - isJust (getUserTypeErrorMsg pred) || isJust (isUnsatisfiableCt_maybe pred) +-- +-- See Note [Custom type errors in constraints]. +containsUserTypeError + :: Bool -- ^ look inside type-family applications, 'AppTy', etc? + -> PredType + -> Bool +containsUserTypeError look_in_famapps pred = + isJust (isUnsatisfiableCt_maybe pred) + || + isJust (userTypeError_maybe look_in_famapps pred) -- | Is this type an unsatisfiable constraint? -- If so, return the error message. ===================================== compiler/GHC/Tc/Validity.hs ===================================== @@ -31,6 +31,7 @@ import GHC.Tc.Instance.Family import GHC.Tc.Types.Origin import GHC.Tc.Types.Rank import GHC.Tc.Errors.Types +import GHC.Tc.Types.Constraint ( userTypeError_maybe ) import GHC.Tc.Utils.Env (tcLookupId) import GHC.Tc.Utils.TcType import GHC.Tc.Utils.Monad @@ -282,7 +283,12 @@ checkUserTypeError ctxt ty | TySynCtxt {} <- ctxt -- Do not complain about TypeError on the = return () -- RHS of type synonyms. See #20181 - | Just msg <- deepUserTypeError_maybe ty + | Just msg <- userTypeError_maybe False ty + -- ^^^^^ + -- Don't look under type-family applications! We only want to pull out + -- definite errors. + -- + -- See (UTE1) in Note [Custom type errors in constraints] in GHC.Tc.Types.Constraint. = do { env0 <- liftZonkM tcInitTidyEnv ; let (env1, tidy_msg) = tidyOpenTypeX env0 msg ; failWithTcM (env1, TcRnUserTypeError tidy_msg) } ===================================== testsuite/tests/pmcheck/should_compile/T26400.hs ===================================== @@ -0,0 +1,37 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UnliftedDatatypes #-} + +module T26400 where + +import GHC.Exts ( UnliftedType ) +import GHC.TypeLits ( TypeError, ErrorMessage(..) ) + +data N = Z | S N + +-- Make this type unlifted to avoid any subtleties about laziness +type SNat :: N -> UnliftedType +data SNat n where + SZ :: SNat Z + SS :: SNat n -> SNat (S n) + +type (-) :: N -> N -> N +type family a - b where + n - Z = n + Z - S _ = TypeError ( Text "impossible" ) + S n - S m = n - m + +testFn :: SNat n -> SNat m -> SNat (n - m) -> Int +testFn SZ (SS _) SZ = 666 +testFn SZ (SS _) (SS _) = 999 + -- [G] g1 :: n ~ Z + -- [G] g2 :: m ~ S m1 + -- [G] g3 :: (n-m) ~ S m2 + -- Use the first two givens to substitute in the third, we get: + -- [G] g3' :: Z - S m1 ~ S m2 + -- Reduce the LHS using the type family + -- [G] g3'' :: TypeError ... ~ S m2 + -- Hence g3'' is insoluble and the equation can never match +testFn _ _ _ = 1 ===================================== testsuite/tests/pmcheck/should_compile/T26400.stderr ===================================== @@ -0,0 +1,8 @@ +T26400.hs:27:1: warning: [GHC-53633] [-Woverlapping-patterns (in -Wdefault)] + Pattern match is redundant + In an equation for ‘testFn’: testFn SZ (SS _) SZ = ... + +T26400.hs:28:1: warning: [GHC-53633] [-Woverlapping-patterns (in -Wdefault)] + Pattern match is redundant + In an equation for ‘testFn’: testFn SZ (SS _) (SS _) = ... + ===================================== testsuite/tests/pmcheck/should_compile/T26400b.hs ===================================== @@ -0,0 +1,39 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} + +module T26400b where + +import Data.Kind +import GHC.TypeLits ( TypeError, ErrorMessage(..) ) + +type F :: Type -> Type -> Type +type family F a b where + F Float _ = Bool + F _ a = a + +type C :: Type -> Type -> Constraint +class C a b +instance C () b + +type Boom :: Type -> Type +type family Boom a where + Boom () = TypeError (Text "boom") + +type TF :: Type -> ( Type -> Type -> Constraint ) +type family TF a where + TF () = C + +type G :: Type -> Type -> Type +data G a b where + G1 :: a -> F b (Boom a) -> G a b + G2 :: C a (Boom a) => a -> G a b + G3 :: (TF b) a (Boom a) => a -> G a b + G4 :: (b ~ Boom a) => G a b + +g :: G () b -> Int +g (G1 {}) = 1 -- not redundant: F b (TypeError ...) can be solved if F reduces +g (G2 {}) = 2 -- not redundant: C () (TypeError ...) is not insoluble +g (G3 {}) = 3 -- not redundant: TF b () (TypeError ...) could reduce to C () (TypeError ...) +g (G4 {}) = 4 -- not redundant: b ~ TypeError ... could be solved depending on instantiation of b ===================================== testsuite/tests/pmcheck/should_compile/all.T ===================================== @@ -123,6 +123,8 @@ test('T21761', [], compile, [overlapping_incomplete]) test('T22964', [], compile, [overlapping_incomplete]) test('T23445', [], compile, [overlapping_incomplete]) test('T24234', [], compile, [overlapping_incomplete+'-Wincomplete-uni-patterns']) +test('T26400', [], compile, [overlapping_incomplete]) +test('T26400b', [], compile, [overlapping_incomplete]) # Series (inspired) by Luke Maranget ===================================== testsuite/tests/typecheck/should_fail/T20241b.stderr ===================================== @@ -1,4 +1,3 @@ - T20241b.hs:16:8: error: [GHC-47403] • Boom • In the type signature: @@ -6,11 +5,14 @@ T20241b.hs:16:8: error: [GHC-47403] -> Type -> Constraint) IO) a => Proxy a -> () -T20241b.hs:20:8: error: [GHC-47403] +T20241b.hs:20:8: error: [GHC-64725] • Boom - • In the type signature: + • In the ambiguity check for ‘bar’ + To defer the ambiguity check to use sites, enable AllowAmbiguousTypes + In the type signature: bar :: ((c :: Constraint -> Type -> Constraint) (((TypeError (Text "Boom") :: (Type -> Type) -> Type -> Constraint) IO) a)) a => Proxy a -> () + ===================================== testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr ===================================== @@ -9,11 +9,11 @@ UnliftedNewtypesFamilyKindFail2.hs:12:20: error: [GHC-83865] • In the first argument of ‘F’, namely ‘5’ In the newtype family instance declaration for ‘F’ -UnliftedNewtypesFamilyKindFail2.hs:12:31: [GHC-83865] - Expected a type, +UnliftedNewtypesFamilyKindFail2.hs:12:31: error: [GHC-83865] + • Expected a type, but ‘5’ has kind ‘GHC.Internal.Bignum.Natural.Natural’ - In the first argument of ‘F’, namely ‘5’ + • In the first argument of ‘F’, namely ‘5’ In the type ‘(F 5)’ In the definition of data constructor ‘MkF’ View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7471eb6a250ff713f9416346478f46b9... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7471eb6a250ff713f9416346478f46b9... You're receiving this email because of your account on gitlab.haskell.org.