Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC Commits: 41bdb16f by Andreas Klebinger at 2025-10-06T18:04:34-04:00 Add a perf test for #26425 - - - - - 1da0c700 by Andreas Klebinger at 2025-10-06T18:05:14-04:00 Testsuite: Silence warnings about Wx-partial in concprog001 - - - - - e56ee4c4 by sheaf at 2025-10-07T09:58:58-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. - - - - - 742ae2b4 by Rodrigo Mesquita at 2025-10-07T09:58:59-04:00 cleanup: Drop obsolete settings from config.mk.in These values used to be spliced into the bindist's `config.mk` s.t. when `make` was run, the values were read and written into the bindist installation `settings` file. However, we now carry these values to the bindist directly in the default.target toolchain file, and `make` writes almost nothing to `settings` now (see #26227) The entries deleted in this MR were already unused. Fixes #26478 - - - - - 18 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 - hadrian/bindist/config.mk.in - testsuite/tests/concurrent/prog001/all.T - + testsuite/tests/perf/compiler/T26425.hs - testsuite/tests/perf/compiler/all.T - + 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) } ===================================== hadrian/bindist/config.mk.in ===================================== @@ -174,34 +174,3 @@ UseLibffiForAdjustors=@UseLibffiForAdjustors@ # rts/Libdw.c:set_initial_registers() UseLibdw=$(strip $(if $(filter $(TargetArch_CPP),i386 x86_64 s390x),@UseLibdw@,NO)) -#----------------------------------------------------------------------------- -# Settings - -# We are in the process of moving the settings file from being entirely -# generated by configure, to generated being by the build system. Many of these -# might become redundant. -# See Note [tooldir: How GHC finds mingw on Windows] - -LdHasFilelist = @LdHasFilelist@ -MergeObjsSupportsResponseFiles = @MergeObjsSupportsResponseFiles@ -LdHasBuildId = @LdHasBuildId@ -LdHasFilelist = @LdHasFilelist@ -LdIsGNULd = @LdIsGNULd@ -LdHasNoCompactUnwind = @LdHasNoCompactUnwind@ -LdHasSingleModule = @LdHasSingleModule@ -ArArgs = @ArArgs@ -ArSupportsAtFile = @ArSupportsAtFile@ -ArSupportsDashL = @ArSupportsDashL@ -HaskellHostOs = @HaskellHostOs@ -HaskellHostArch = @HaskellHostArch@ -HaskellTargetOs = @HaskellTargetOs@ -HaskellTargetArch = @HaskellTargetArch@ -TargetWordSize = @TargetWordSize@ -TargetWordBigEndian = @TargetWordBigEndian@ -TargetHasGnuNonexecStack = @TargetHasGnuNonexecStack@ -TargetHasIdentDirective = @TargetHasIdentDirective@ -TargetHasSubsectionsViaSymbols = @TargetHasSubsectionsViaSymbols@ -TargetHasLibm = @TargetHasLibm@ -TablesNextToCode = @TablesNextToCode@ -LeadingUnderscore = @LeadingUnderscore@ -LlvmTarget = @LlvmTarget@ ===================================== testsuite/tests/concurrent/prog001/all.T ===================================== @@ -16,4 +16,4 @@ test('concprog001', [extra_files(['Arithmetic.hs', 'Converter.hs', 'Mult.hs', 'S when(fast(), skip), only_ways(['threaded2']), fragile(16604), run_timeout_multiplier(2)], - multimod_compile_and_run, ['Mult', '']) + multimod_compile_and_run, ['Mult', '-Wno-x-partial']) ===================================== testsuite/tests/perf/compiler/T26425.hs ===================================== @@ -0,0 +1,664 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Reproducer (strToInt) where + +import qualified Data.Text as T + +{- This program results in a nested chain of join points and cases which tests + primarily OccAnal and Unfolding performance. +-} + +strToInt :: T.Text -> Maybe Int +strToInt txt = case txt of + "0" -> Just 0 + "1" -> Just 1 + "2" -> Just 2 + "3" -> Just 3 + "4" -> Just 4 + "5" -> Just 5 + "6" -> Just 6 + "7" -> Just 7 + "8" -> Just 8 + "9" -> Just 9 + "10" -> Just 10 + "11" -> Just 11 + "12" -> Just 12 + "13" -> Just 13 + "14" -> Just 14 + "15" -> Just 15 + "16" -> Just 16 + "17" -> Just 17 + "18" -> Just 18 + "19" -> Just 19 + "20" -> Just 20 + "21" -> Just 21 + "22" -> Just 22 + "23" -> Just 23 + "24" -> Just 24 + "25" -> Just 25 + "26" -> Just 26 + "27" -> Just 27 + "28" -> Just 28 + "29" -> Just 29 + "30" -> Just 30 + "31" -> Just 31 + "32" -> Just 32 + "33" -> Just 33 + "34" -> Just 34 + "35" -> Just 35 + "36" -> Just 36 + "37" -> Just 37 + "38" -> Just 38 + "39" -> Just 39 + "40" -> Just 40 + "41" -> Just 41 + "42" -> Just 42 + "43" -> Just 43 + "44" -> Just 44 + "45" -> Just 45 + "46" -> Just 46 + "47" -> Just 47 + "48" -> Just 48 + "49" -> Just 49 + "50" -> Just 50 + "51" -> Just 51 + "52" -> Just 52 + "53" -> Just 53 + "54" -> Just 54 + "55" -> Just 55 + "56" -> Just 56 + "57" -> Just 57 + "58" -> Just 58 + "59" -> Just 59 + "60" -> Just 60 + "61" -> Just 61 + "62" -> Just 62 + "63" -> Just 63 + "64" -> Just 64 + "65" -> Just 65 + "66" -> Just 66 + "67" -> Just 67 + "68" -> Just 68 + "69" -> Just 69 + "70" -> Just 70 + "71" -> Just 71 + "72" -> Just 72 + "73" -> Just 73 + "74" -> Just 74 + "75" -> Just 75 + "76" -> Just 76 + "77" -> Just 77 + "78" -> Just 78 + "79" -> Just 79 + "80" -> Just 80 + "81" -> Just 81 + "82" -> Just 82 + "83" -> Just 83 + "84" -> Just 84 + "85" -> Just 85 + "86" -> Just 86 + "87" -> Just 87 + "88" -> Just 88 + "89" -> Just 89 + "90" -> Just 90 + "91" -> Just 91 + "92" -> Just 92 + "93" -> Just 93 + "94" -> Just 94 + "95" -> Just 95 + "96" -> Just 96 + "97" -> Just 97 + "98" -> Just 98 + "99" -> Just 99 + "100" -> Just 100 + "101" -> Just 101 + "102" -> Just 102 + "103" -> Just 103 + "104" -> Just 104 + "105" -> Just 105 + "106" -> Just 106 + "107" -> Just 107 + "108" -> Just 108 + "109" -> Just 109 + "110" -> Just 110 + "111" -> Just 111 + "112" -> Just 112 + "113" -> Just 113 + "114" -> Just 114 + "115" -> Just 115 + "116" -> Just 116 + "117" -> Just 117 + "118" -> Just 118 + "119" -> Just 119 + "120" -> Just 120 + "121" -> Just 121 + "122" -> Just 122 + "123" -> Just 123 + "124" -> Just 124 + "125" -> Just 125 + "126" -> Just 126 + "127" -> Just 127 + "128" -> Just 128 + "129" -> Just 129 + "130" -> Just 130 + "131" -> Just 131 + "132" -> Just 132 + "133" -> Just 133 + "134" -> Just 134 + "135" -> Just 135 + "136" -> Just 136 + "137" -> Just 137 + "138" -> Just 138 + "139" -> Just 139 + "140" -> Just 140 + "141" -> Just 141 + "142" -> Just 142 + "143" -> Just 143 + "144" -> Just 144 + "145" -> Just 145 + "146" -> Just 146 + "147" -> Just 147 + "148" -> Just 148 + "149" -> Just 149 + "150" -> Just 150 + "151" -> Just 151 + "152" -> Just 152 + "153" -> Just 153 + "154" -> Just 154 + "155" -> Just 155 + "156" -> Just 156 + "157" -> Just 157 + "158" -> Just 158 + "159" -> Just 159 + "160" -> Just 160 + "161" -> Just 161 + "162" -> Just 162 + "163" -> Just 163 + "164" -> Just 164 + "165" -> Just 165 + "166" -> Just 166 + "167" -> Just 167 + "168" -> Just 168 + "169" -> Just 169 + "170" -> Just 170 + "171" -> Just 171 + "172" -> Just 172 + "173" -> Just 173 + "174" -> Just 174 + "175" -> Just 175 + "176" -> Just 176 + "177" -> Just 177 + "178" -> Just 178 + "179" -> Just 179 + "180" -> Just 180 + "181" -> Just 181 + "182" -> Just 182 + "183" -> Just 183 + "184" -> Just 184 + "185" -> Just 185 + "186" -> Just 186 + "187" -> Just 187 + "188" -> Just 188 + "189" -> Just 189 + "190" -> Just 190 + "191" -> Just 191 + "192" -> Just 192 + "193" -> Just 193 + "194" -> Just 194 + "195" -> Just 195 + "196" -> Just 196 + "197" -> Just 197 + "198" -> Just 198 + "199" -> Just 199 + "200" -> Just 200 + "201" -> Just 201 + "202" -> Just 202 + "203" -> Just 203 + "204" -> Just 204 + "205" -> Just 205 + "206" -> Just 206 + "207" -> Just 207 + "208" -> Just 208 + "209" -> Just 209 + "210" -> Just 210 + "211" -> Just 211 + "212" -> Just 212 + "213" -> Just 213 + "214" -> Just 214 + "215" -> Just 215 + "216" -> Just 216 + "217" -> Just 217 + "218" -> Just 218 + "219" -> Just 219 + "220" -> Just 220 + "221" -> Just 221 + "222" -> Just 222 + "223" -> Just 223 + "224" -> Just 224 + "225" -> Just 225 + "226" -> Just 226 + "227" -> Just 227 + "228" -> Just 228 + "229" -> Just 229 + "230" -> Just 230 + "231" -> Just 231 + "232" -> Just 232 + "233" -> Just 233 + "234" -> Just 234 + "235" -> Just 235 + "236" -> Just 236 + "237" -> Just 237 + "238" -> Just 238 + "239" -> Just 239 + "240" -> Just 240 + "241" -> Just 241 + "242" -> Just 242 + "243" -> Just 243 + "244" -> Just 244 + "245" -> Just 245 + "246" -> Just 246 + "247" -> Just 247 + "248" -> Just 248 + "249" -> Just 249 + "250" -> Just 250 + "251" -> Just 251 + "252" -> Just 252 + "253" -> Just 253 + "254" -> Just 254 + "255" -> Just 255 + "256" -> Just 256 + "257" -> Just 257 + "258" -> Just 258 + "259" -> Just 259 + "260" -> Just 260 + "261" -> Just 261 + "262" -> Just 262 + "263" -> Just 263 + "264" -> Just 264 + "265" -> Just 265 + "266" -> Just 266 + "267" -> Just 267 + "268" -> Just 268 + "269" -> Just 269 + "270" -> Just 270 + "271" -> Just 271 + "272" -> Just 272 + "273" -> Just 273 + "274" -> Just 274 + "275" -> Just 275 + "276" -> Just 276 + "277" -> Just 277 + "278" -> Just 278 + "279" -> Just 279 + "280" -> Just 280 + "281" -> Just 281 + "282" -> Just 282 + "283" -> Just 283 + "284" -> Just 284 + "285" -> Just 285 + "286" -> Just 286 + "287" -> Just 287 + "288" -> Just 288 + "289" -> Just 289 + "290" -> Just 290 + "291" -> Just 291 + "292" -> Just 292 + "293" -> Just 293 + "294" -> Just 294 + "295" -> Just 295 + "296" -> Just 296 + "297" -> Just 297 + "298" -> Just 298 + "299" -> Just 299 + "300" -> Just 300 + "301" -> Just 301 + "302" -> Just 302 + "303" -> Just 303 + "304" -> Just 304 + "305" -> Just 305 + "306" -> Just 306 + "307" -> Just 307 + "308" -> Just 308 + "309" -> Just 309 + "310" -> Just 310 + "311" -> Just 311 + "312" -> Just 312 + "313" -> Just 313 + "314" -> Just 314 + "315" -> Just 315 + "316" -> Just 316 + "317" -> Just 317 + "318" -> Just 318 + "319" -> Just 319 + "320" -> Just 320 + "321" -> Just 321 + "322" -> Just 322 + "323" -> Just 323 + "324" -> Just 324 + "325" -> Just 325 + "326" -> Just 326 + "327" -> Just 327 + "328" -> Just 328 + "329" -> Just 329 + "330" -> Just 330 + "331" -> Just 331 + "332" -> Just 332 + "333" -> Just 333 + "334" -> Just 334 + "335" -> Just 335 + "336" -> Just 336 + "337" -> Just 337 + "338" -> Just 338 + "339" -> Just 339 + "340" -> Just 340 + "341" -> Just 341 + "342" -> Just 342 + "343" -> Just 343 + "344" -> Just 344 + "345" -> Just 345 + "346" -> Just 346 + "347" -> Just 347 + "348" -> Just 348 + "349" -> Just 349 + "350" -> Just 350 + "351" -> Just 351 + "352" -> Just 352 + "353" -> Just 353 + "354" -> Just 354 + "355" -> Just 355 + "356" -> Just 356 + "357" -> Just 357 + "358" -> Just 358 + "359" -> Just 359 + "360" -> Just 360 + "361" -> Just 361 + "362" -> Just 362 + "363" -> Just 363 + "364" -> Just 364 + "365" -> Just 365 + "366" -> Just 366 + "367" -> Just 367 + "368" -> Just 368 + "369" -> Just 369 + "370" -> Just 370 + "371" -> Just 371 + "372" -> Just 372 + "373" -> Just 373 + "374" -> Just 374 + "375" -> Just 375 + "376" -> Just 376 + "377" -> Just 377 + "378" -> Just 378 + "379" -> Just 379 + "380" -> Just 380 + "381" -> Just 381 + "382" -> Just 382 + "383" -> Just 383 + "384" -> Just 384 + "385" -> Just 385 + "386" -> Just 386 + "387" -> Just 387 + "388" -> Just 388 + "389" -> Just 389 + "390" -> Just 390 + "391" -> Just 391 + "392" -> Just 392 + "393" -> Just 393 + "394" -> Just 394 + "395" -> Just 395 + "396" -> Just 396 + "397" -> Just 397 + "398" -> Just 398 + "399" -> Just 399 + "400" -> Just 400 + "401" -> Just 401 + "402" -> Just 402 + "403" -> Just 403 + "404" -> Just 404 + "405" -> Just 405 + "406" -> Just 406 + "407" -> Just 407 + "408" -> Just 408 + "409" -> Just 409 + "410" -> Just 410 + "411" -> Just 411 + "412" -> Just 412 + "413" -> Just 413 + "414" -> Just 414 + "415" -> Just 415 + "416" -> Just 416 + "417" -> Just 417 + "418" -> Just 418 + "419" -> Just 419 + "420" -> Just 420 + "421" -> Just 421 + "422" -> Just 422 + "423" -> Just 423 + "424" -> Just 424 + "425" -> Just 425 + "426" -> Just 426 + "427" -> Just 427 + "428" -> Just 428 + "429" -> Just 429 + "430" -> Just 430 + "431" -> Just 431 + "432" -> Just 432 + "433" -> Just 433 + "434" -> Just 434 + "435" -> Just 435 + "436" -> Just 436 + "437" -> Just 437 + "438" -> Just 438 + "439" -> Just 439 + "440" -> Just 440 + "441" -> Just 441 + "442" -> Just 442 + "443" -> Just 443 + "444" -> Just 444 + "445" -> Just 445 + "446" -> Just 446 + "447" -> Just 447 + "448" -> Just 448 + "449" -> Just 449 + "450" -> Just 450 + "451" -> Just 451 + "452" -> Just 452 + "453" -> Just 453 + "454" -> Just 454 + "455" -> Just 455 + "456" -> Just 456 + "457" -> Just 457 + "458" -> Just 458 + "459" -> Just 459 + "460" -> Just 460 + "461" -> Just 461 + "462" -> Just 462 + "463" -> Just 463 + "464" -> Just 464 + "465" -> Just 465 + "466" -> Just 466 + "467" -> Just 467 + "468" -> Just 468 + "469" -> Just 469 + "470" -> Just 470 + "471" -> Just 471 + "472" -> Just 472 + "473" -> Just 473 + "474" -> Just 474 + "475" -> Just 475 + "476" -> Just 476 + "477" -> Just 477 + "478" -> Just 478 + "479" -> Just 479 + "480" -> Just 480 + "481" -> Just 481 + "482" -> Just 482 + "483" -> Just 483 + "484" -> Just 484 + "485" -> Just 485 + "486" -> Just 486 + "487" -> Just 487 + "488" -> Just 488 + "489" -> Just 489 + "490" -> Just 490 + "491" -> Just 491 + "492" -> Just 492 + "493" -> Just 493 + "494" -> Just 494 + "495" -> Just 495 + "496" -> Just 496 + "497" -> Just 497 + "498" -> Just 498 + "499" -> Just 499 + "500" -> Just 500 + "501" -> Just 501 + "502" -> Just 502 + "503" -> Just 503 + "504" -> Just 504 + "505" -> Just 505 + "506" -> Just 506 + "507" -> Just 507 + "508" -> Just 508 + "509" -> Just 509 + "510" -> Just 510 + "511" -> Just 511 + "512" -> Just 512 + "513" -> Just 513 + "514" -> Just 514 + "515" -> Just 515 + "516" -> Just 516 + "517" -> Just 517 + "518" -> Just 518 + "519" -> Just 519 + "520" -> Just 520 + "521" -> Just 521 + "522" -> Just 522 + "523" -> Just 523 + "524" -> Just 524 + "525" -> Just 525 + "526" -> Just 526 + "527" -> Just 527 + "528" -> Just 528 + "529" -> Just 529 + "530" -> Just 530 + "531" -> Just 531 + "532" -> Just 532 + "533" -> Just 533 + "534" -> Just 534 + "535" -> Just 535 + "536" -> Just 536 + "537" -> Just 537 + "538" -> Just 538 + "539" -> Just 539 + "540" -> Just 540 + "541" -> Just 541 + "542" -> Just 542 + "543" -> Just 543 + "544" -> Just 544 + "545" -> Just 545 + "546" -> Just 546 + "547" -> Just 547 + "548" -> Just 548 + "549" -> Just 549 + "550" -> Just 550 + "551" -> Just 551 + "552" -> Just 552 + "553" -> Just 553 + "554" -> Just 554 + "555" -> Just 555 + "556" -> Just 556 + "557" -> Just 557 + "558" -> Just 558 + "559" -> Just 559 + "560" -> Just 560 + "561" -> Just 561 + "562" -> Just 562 + "563" -> Just 563 + "564" -> Just 564 + "565" -> Just 565 + "566" -> Just 566 + "567" -> Just 567 + "568" -> Just 568 + "569" -> Just 569 + "570" -> Just 570 + "571" -> Just 571 + "572" -> Just 572 + "573" -> Just 573 + "574" -> Just 574 + "575" -> Just 575 + "576" -> Just 576 + "577" -> Just 577 + "578" -> Just 578 + "579" -> Just 579 + "580" -> Just 580 + "581" -> Just 581 + "582" -> Just 582 + "583" -> Just 583 + "584" -> Just 584 + "585" -> Just 585 + "586" -> Just 586 + "587" -> Just 587 + "588" -> Just 588 + "589" -> Just 589 + "590" -> Just 590 + "591" -> Just 591 + "592" -> Just 592 + "593" -> Just 593 + "594" -> Just 594 + "595" -> Just 595 + "596" -> Just 596 + "597" -> Just 597 + "598" -> Just 598 + "599" -> Just 599 + "600" -> Just 600 + "601" -> Just 601 + "602" -> Just 602 + "603" -> Just 603 + "604" -> Just 604 + "605" -> Just 605 + "606" -> Just 606 + "607" -> Just 607 + "608" -> Just 608 + "609" -> Just 609 + "610" -> Just 610 + "611" -> Just 611 + "612" -> Just 612 + "613" -> Just 613 + "614" -> Just 614 + "615" -> Just 615 + "616" -> Just 616 + "617" -> Just 617 + "618" -> Just 618 + "619" -> Just 619 + "620" -> Just 620 + "621" -> Just 621 + "622" -> Just 622 + "623" -> Just 623 + "624" -> Just 624 + "625" -> Just 625 + "626" -> Just 626 + "627" -> Just 627 + "628" -> Just 628 + "629" -> Just 629 + "630" -> Just 630 + "631" -> Just 631 + "632" -> Just 632 + "633" -> Just 633 + "634" -> Just 634 + "635" -> Just 635 + "636" -> Just 636 + "637" -> Just 637 + "638" -> Just 638 + "639" -> Just 639 + "640" -> Just 640 + "641" -> Just 641 + "642" -> Just 642 + "643" -> Just 643 + "644" -> Just 644 + "645" -> Just 645 + "646" -> Just 646 + "647" -> Just 647 + "648" -> Just 648 + "649" -> Just 649 + "650" -> Just 650 + _ -> Nothing ===================================== testsuite/tests/perf/compiler/all.T ===================================== @@ -792,3 +792,8 @@ test('interpreter_steplocal', ], ghci_script, ['interpreter_steplocal.script']) + +test ('T26425', + [ collect_compiler_stats('all',5) ], + compile, + ['-O']) ===================================== 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/-/compare/64f8ecd611661e91057be7b5e36a6ed... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/64f8ecd611661e91057be7b5e36a6ed... You're receiving this email because of your account on gitlab.haskell.org.