Simon Peyton Jones pushed to branch wip/T23162-part2 at Glasgow Haskell Compiler / GHC Commits: a2e35bf3 by Simon Peyton Jones at 2025-12-18T17:42:44+00:00 More wibbles - - - - - 14 changed files: - compiler/GHC/Tc/Errors.hs - compiler/GHC/Tc/Errors/Ppr.hs - compiler/GHC/Tc/Errors/Types.hs - compiler/GHC/Tc/Solver.hs - compiler/GHC/Tc/Solver/FunDeps.hs - compiler/GHC/Tc/Types/Constraint.hs - testsuite/tests/pmcheck/should_compile/T15753c.hs - + testsuite/tests/pmcheck/should_compile/T15753c.stderr - testsuite/tests/pmcheck/should_compile/T15753d.hs - + testsuite/tests/pmcheck/should_compile/T15753d.stderr - + testsuite/tests/pmcheck/should_compile/T22652a.hs - testsuite/tests/pmcheck/should_compile/all.T - testsuite/tests/typecheck/should_fail/T5236.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -1509,11 +1509,12 @@ coercion. mkIrredErr :: SolverReportErrCtxt -> NonEmpty ErrorItem -> TcM SolverReport mkIrredErr ctxt items = do { (ctxt, binds, item1) <- relevantBindings True ctxt item1 - ; couldNotDeduceErr <- mkCouldNotDeduceErr (getUserGivens ctxt) (item1 :| others) Nothing + ; couldNotDeduceErr <- mkCouldNotDeduceErr useful_givens (item1 :| others) Nothing ; let msg = important ctxt $ mkPlainMismatchMsg couldNotDeduceErr ; return $ add_relevant_bindings binds msg } where item1:|others = tryFilter (not . ei_suppress) items + useful_givens = getUsefulGivens ctxt item1 {- Note [Constructing Hole Errors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1694,8 +1695,8 @@ validHoleFits ctxt@(CEC { cec_encl = implics givenConstraints :: SolverReportErrCtxt -> [(Type, RealSrcSpan)] -- Returned outermost first -- See Note [Constraints include ...] -givenConstraints ctxt - = do { implic@Implic{ ic_given = given } <- getUserGivens ctxt +givenConstraints (CEC { cec_encl = implics }) + = do { implic@Implic{ ic_given = given } <- getGivensFromImplics implics ; constraint <- given ; return (varType constraint, getCtLocEnvLoc (ic_env implic)) } @@ -2105,6 +2106,7 @@ eqInfoMsgs ty1 ty2 misMatchOrCND :: SolverReportErrCtxt -> ErrorItem -> TcType -> TcType -> TcM MismatchMsg +-- Make a message for a failed equality constraint (t1 ~ t2) -- If oriented then ty1 is actual, ty2 is expected misMatchOrCND ctxt item ty1 ty2 | ei_insoluble item -- See Note [Insoluble mis-match] @@ -2120,7 +2122,8 @@ misMatchOrCND ctxt item ty1 ty2 where level = ctLocTypeOrKind_maybe (errorItemCtLoc item) `orElse` TypeLevel - givens = [ given | given <- getUserGivens ctxt, ic_given_eqs given /= NoGivenEqs ] + givens = [ given | given <- getUsefulGivens ctxt item + , ic_given_eqs given /= NoGivenEqs ] -- Keep only UserGivens that have some equalities. -- See Note [Suppress redundant givens during error reporting] @@ -2302,7 +2305,8 @@ mkQCErr :: HasDebugCallStack => SolverReportErrCtxt -> NonEmpty ErrorItem -> TcM mkQCErr ctxt items | item1 :| _ <- tryFilter (not . ei_suppress) items -- Ignore multiple qc-errors on the same line - = do { couldNotDeduceErr <- mkCouldNotDeduceErr (getUserGivens ctxt) (item1 :| []) Nothing + = do { couldNotDeduceErr <- mkCouldNotDeduceErr (getUsefulGivens ctxt item1) + (item1 :| []) Nothing ; return $ important ctxt $ mkPlainMismatchMsg couldNotDeduceErr } @@ -2332,7 +2336,8 @@ mkDictErr ctxt orig_items@(item1 :| others) where items = tryFilter (not . ei_suppress) orig_items - no_givens = null (getUserGivens ctxt) + useful_givens = getUsefulGivens ctxt item1 + no_givens = null useful_givens is_no_inst (item, (matches, unifiers, _)) = no_givens @@ -2471,9 +2476,9 @@ mkCouldNotDeduceErr -> NonEmpty ErrorItem -> Maybe CND_ExpectedActual -> TcM MismatchMsg -mkCouldNotDeduceErr user_givens items@(item :| _) mb_ea +mkCouldNotDeduceErr useful_givens items@(item :| _) mb_ea = do { mb_noBuiltinInst_info <- getNoBuiltinInstMsg item - ; return $ CouldNotDeduce user_givens items mb_ea mb_noBuiltinInst_info } + ; return $ CouldNotDeduce useful_givens items mb_ea mb_noBuiltinInst_info } getNoBuiltinInstMsg :: ErrorItem -> TcM (Maybe NoBuiltinInstanceMsg) getNoBuiltinInstMsg item = ===================================== compiler/GHC/Tc/Errors/Ppr.hs ===================================== @@ -4178,7 +4178,7 @@ pprTcSolverReportMsg _ (ExpectingMoreArguments n thing) = | n == 1 = text "more argument to" | otherwise = text "more arguments to" -- n > 1 pprTcSolverReportMsg ctxt (UnboundImplicitParams (item :| items)) = - let givens = getUserGivens ctxt + let givens = getUsefulGivens ctxt item in if null givens then addArising (errorItemCtLoc item) $ sep [ text "Unbound implicit parameter" <> plural preds @@ -4233,7 +4233,7 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics}) (ambig_kvs, ambig_tvs) = ambigTkvsOfTy pred ambigs = ambig_kvs ++ ambig_tvs has_ambigs = not (null ambigs) - useful_givens = discardProvCtxtGivens orig (getUserGivensFromImplics implics) + useful_givens = getUsefulGivens ctxt item -- useful_givens are the enclosing implications with non-empty givens, -- modulo the horrid discardProvCtxtGivens lead_with_ambig = not (null ambigs) @@ -4298,7 +4298,7 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics}) = empty ----------- Possible fixes ---------------- - ctxt_fixes = ctxtFixes has_ambigs pred implics + ctxt_fixes = ctxtFixes ctxt has_ambigs pred drv_fixes = case orig of DerivOrigin standalone -> [drv_fix standalone] @@ -4332,7 +4332,7 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics}) Just (_, tys) -> not (all isTyVarTy tys) Nothing -> False -pprTcSolverReportMsg (CEC {cec_encl = implics}) (OverlappingInstances item matches unifiers) = +pprTcSolverReportMsg ctxt (OverlappingInstances item matches unifiers) = vcat [ addArising ct_loc $ (text "Overlapping instances for" @@ -4375,7 +4375,7 @@ pprTcSolverReportMsg (CEC {cec_encl = implics}) (OverlappingInstances item match (clas, tys) = getClassPredTys pred tyCoVars = tyCoVarsOfTypesList tys famTyCons = filter isFamilyTyCon $ concatMap (nonDetEltsUniqSet . tyConsOfType) tys - useful_givens = discardProvCtxtGivens orig (getUserGivensFromImplics implics) + useful_givens = getUsefulGivens ctxt item matching_givens = mapMaybe matchable useful_givens matchable implic@(Implic { ic_given = evvars, ic_info = skol_info }) = case ev_vars_matching of @@ -4707,10 +4707,13 @@ pprMismatchMsg ctxt | otherwise = vcat ( addArising ct_loc no_deduce_msg : pp_from_givens useful_givens) - ea_supplementary = case mb_ea of - Nothing -> empty - Just (CND_ExpectedActual level ty1 ty2) -> - mk_supplementary_ea_msg ctxt level ty1 ty2 orig + ea_supplementary + | Just (CND_ExpectedActual level ty1 ty2) <- mb_ea + = mk_supplementary_ea_msg ctxt level ty1 ty2 orig + | Just InsolubleFunDepReason <- ei_m_reason item + = text "The functional dependencies arising from this constraint are insoluble" + | otherwise + = empty ct_loc = errorItemCtLoc item orig = ctLocOrigin ct_loc @@ -5583,8 +5586,8 @@ show_fixes [] = empty show_fixes (f:fs) = sep [ text "Possible fix:" , nest 2 (vcat (f : map (text "or" <+>) fs))] -ctxtFixes :: Bool -> PredType -> [Implication] -> [SDoc] -ctxtFixes has_ambig_tvs pred implics +ctxtFixes :: SolverReportErrCtxt -> Bool -> PredType -> [SDoc] +ctxtFixes (CEC {cec_encl = implics}) has_ambig_tvs pred | not has_ambig_tvs , isTyVarClassPred pred -- Don't suggest adding (Eq T) to the context, say , (skol:skols) <- usefulContext implics pred ===================================== compiler/GHC/Tc/Errors/Types.hs ===================================== @@ -62,7 +62,7 @@ module GHC.Tc.Errors.Types ( , SolverReport(..), SupplementaryInfo(..) , SolverReportWithCtxt(..) , SolverReportErrCtxt(..) - , getUserGivens, discardProvCtxtGivens + , getUsefulGivens , TcSolverReportMsg(..) , CannotUnifyVariableReason(..) , MismatchMsg(..) @@ -5409,10 +5409,6 @@ data SolverReportErrCtxt -- See Note [Suppressing error messages] } -getUserGivens :: SolverReportErrCtxt -> [UserGiven] --- One item for each enclosing implication -getUserGivens (CEC {cec_encl = implics}) = getUserGivensFromImplics implics - ---------------------------------------------------------------------------- -- -- ErrorItem @@ -5438,7 +5434,7 @@ data ErrorItem , ei_loc :: CtLoc , ei_m_reason :: Maybe CtIrredReason -- If this ErrorItem was made from a -- CtIrred, this stores the reason - , ei_insoluble :: Bool -- True if the constraint is defdinitely insoluble + , ei_insoluble :: Bool -- True if the constraint is definitely insoluble -- Cache of `insolubleCt` , ei_suppress :: Bool -- Suppress because of @@ -5513,6 +5509,19 @@ message (showing both problems): -} +getUsefulGivens :: SolverReportErrCtxt -> ErrorItem -> [UserGiven] +-- One item for each enclosing implication +getUsefulGivens (CEC {cec_encl = implics}) item + | ei_insoluble item + = [] -- If the constraint is insoluble anyway, we won't try to solve it + -- from the inert Givens, so it's positively confusing to list them. + -- Otherwise we get "Can't deduce X from X". + | otherwise + = discardProvCtxtGivens orig $ + getGivensFromImplics implics + where + orig = errorItemOrigin item + discardProvCtxtGivens :: CtOrigin -> [UserGiven] -> [UserGiven] discardProvCtxtGivens orig givens -- See Note [discardProvCtxtGivens] | ProvCtxtOrigin (PSB {psb_id = L _ name}) <- orig ===================================== compiler/GHC/Tc/Solver.hs ===================================== @@ -738,14 +738,15 @@ tcCheckGivens inerts given_ids ; mb_res <- tryM $ -- try_to_solve may throw an exception; -- e.g. reduction stack overflow - discardErrs $ -- An exception id not an error; + discardErrs $ -- An exception is not an error; -- just means "not definitely unsat" runTcSInerts inerts $ try_to_solve given_cts -- If mb_res = Left err, solving threw an exception, e.g. reduction stack -- overflow. So return the original incoming inerts to say "not definitely - -- unsatisfiable". + -- unsatisfiable". See (CF3) in Note [Exploiting closed type families], and + -- test T15753c. ; let res = case mb_res of Right res -> res Left {} -> Just inerts ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -523,7 +523,7 @@ tryEqFunDeps :: EqCt -> SolverStage () tryEqFunDeps work_item@(EqCt { eq_lhs = work_lhs , eq_rhs = work_rhs , eq_eq_rel = eq_rel }) - | NomEq <- eq_rel + | NomEq <- eq_rel -- Functional dependencies only work for nominal equalities , TyFamLHS fam_tc work_args <- work_lhs -- We have F args ~N# rhs = do { eqs_for_me <- simpleStage $ getInertFamEqsFor fam_tc work_args work_rhs ; simpleStage $ traceTcS "tryEqFunDeps" (ppr work_item $$ ppr eqs_for_me) @@ -1071,7 +1071,12 @@ Key point: equations that are not relevant do not need to be considered for fund And now we are back where we started -- loop. We solve this by bumping the `ctLocDepth` in `solveFunDeps`, and imposing - a depth bound. See the call to `bumpReductionDepth`. + a depth bound. See the call to `bumpReductionDepth`. If the depth limit + is exceeded we add an error message and fail in the monad. + + Take care: when we are solving-for-unsatisfiability, in the pattern match + checker, we must carefully catch this failure: see the use of `tryM` in + `tcCheckGivens`. (CF4) If one of the fundeps generated by interacting with the local equalities is definitely insoluble (e.g. Int~Bool) then there is no point in continuing to ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -66,7 +66,7 @@ module GHC.Tc.Types.Constraint ( Implication(..), implicationPrototype, checkTelescopeSkol, ImplicStatus(..), isInsolubleStatus, isSolvedStatus, - UserGiven, getUserGivensFromImplics, + UserGiven, getGivensFromImplics, HasGivenEqs(..), checkImplicationInvariants, EvNeedSet(..), emptyEvNeedSet, unionEvNeedSet, extendEvNeedSet, delGivensFromEvNeedSet, @@ -1637,10 +1637,10 @@ data HasGivenEqs -- See Note [HasGivenEqs] type UserGiven = Implication -getUserGivensFromImplics :: [Implication] -> [UserGiven] +getGivensFromImplics :: [Implication] -> [UserGiven] -- The argument [Implication] is innermost first; -- the returned [UserGiven] is outermost first -getUserGivensFromImplics implics +getGivensFromImplics implics = get [] implics where get :: [UserGiven] -> [Implication] -> [UserGiven] ===================================== testsuite/tests/pmcheck/should_compile/T15753c.hs ===================================== @@ -5,6 +5,11 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wincomplete-patterns #-} + +-- NB: After fixing #22652 this program right produces warnings +-- because (F u1 u1 ~ Char) is unsatisfiable +-- But it produces too many warnings: #26685 + module Bug where import Data.Kind (Type) @@ -34,22 +39,6 @@ type family F (u1 :: ()) (u2 :: ()) :: Type where type family Case (u :: ()) :: Type where Case '() = Int ---------------------------------------- --- The checker can (now, Dec 25) see that (F u1 u2 ~ Char) is --- unsatisfiable, so the empty pattern match is fine -g1a :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void -g1a r _ _ = case r of {} - -{- Why [G] F u1 u2 ~ Char is unsatisfiable - -[G] F u1 u2 ~ Char =>rewrite [G] If (IsUnit u1) (Case u2) Int ~ Char - =>(fundep) [W] IsUnit u1 ~ True - [W] Case u2 ~ Char <<-- insoluble: no relevant eqns --} - ---------------------------------------- --- This older test matches on Refl (which is unsatisfiable) --- but we now get complaints from inside g1 :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void @@ -57,8 +46,6 @@ g1 Refl su1 su2 | STrue <- sIsUnit su1 = case su2 of {} - - g2 :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void ===================================== testsuite/tests/pmcheck/should_compile/T15753c.stderr ===================================== @@ -0,0 +1,19 @@ +T15753c.hs:46:5: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)] + Pattern match has inaccessible right hand side + In an equation for ‘g1’: + g1 Refl su1 su2 | STrue <- sIsUnit su1 = ... + +T15753c.hs:47:5: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)] + Pattern match(es) are non-exhaustive + In a case alternative: + Patterns of type ‘SUnit u2’ not matched: SUnit + +T15753c.hs:52:1: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)] + Pattern match has inaccessible right hand side + In an equation for ‘g2’: g2 Refl su1 su2 = ... + +T15753c.hs:55:9: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)] + Pattern match(es) are non-exhaustive + In a case alternative: + Patterns of type ‘SUnit u2’ not matched: SUnit + ===================================== testsuite/tests/pmcheck/should_compile/T15753d.hs ===================================== @@ -8,7 +8,11 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wall -Wno-unticked-promoted-constructors #-} -module Bug where + +-- NB: After fixing #22652 this program right produces warnings +-- But it produces too many warnings: #26685 + +module T15753d where import Data.Kind import Data.Type.Bool ===================================== testsuite/tests/pmcheck/should_compile/T15753d.stderr ===================================== @@ -0,0 +1,40 @@ +T15753d.hs:83:5: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)] + Pattern match has inaccessible right hand side + In an equation for ‘mapInsertWithNonEmpty1’: + mapInsertWithNonEmpty1 sf + snew_k + snew_v + (SMkMap sm) + Refl + Refl | STuple2 sold_k _ `SCons` sold_kvs <- sm, + SFalse <- sold_k %== snew_k = ... + +T15753d.hs:85:5: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)] + Pattern match(es) are non-exhaustive + In a case alternative: + Patterns of type ‘Sing + (MapInsertWith f new_k new_v (MkMap xs))’ not matched: + SMkMap _ + +T15753d.hs:95:5: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)] + Pattern match has inaccessible right hand side + In an equation for ‘mapInsertWithNonEmpty2’: + mapInsertWithNonEmpty2 sf + snew_k + snew_v + (SMkMap sm) + Refl + Refl | STuple2 sold_k _ `SCons` sold_kvs <- sm = ... + +T15753d.hs:96:5: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)] + Pattern match(es) are non-exhaustive + In a case alternative: + Patterns of type ‘Sing (x == new_k)’ not matched: STrue + +T15753d.hs:98:9: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)] + Pattern match(es) are non-exhaustive + In a case alternative: + Patterns of type ‘Sing + (MapInsertWith f new_k new_v (MkMap xs))’ not matched: + SMkMap _ + ===================================== testsuite/tests/pmcheck/should_compile/T22652a.hs ===================================== @@ -0,0 +1,49 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wincomplete-patterns #-} + +-- This test is a spin-off from the test T15753c + +module T22652a where + +import Data.Kind (Type) +import Data.Type.Equality ((:~:)(..)) +import Data.Void (Void) + +data SBool :: Bool -> Type where + SFalse :: SBool False + STrue :: SBool True + +data SUnit :: () -> Type where + SUnit :: SUnit '() + +type family IsUnit (u :: ()) :: Bool where + IsUnit '() = True + +type family If (c :: Bool) (t :: Type) (f :: Type) :: Type where + If True t _ = t + If False _ f = f + +type family F (u1 :: ()) (u2 :: ()) :: Type where + F u1 u2 = + If (IsUnit u1) (Case u2) Int + +type family Case (u :: ()) :: Type where + Case '() = Int + +--------------------------------------- +-- The checker can (now, Dec 25) see that (F u1 u2 ~ Char) is +-- unsatisfiable, so the empty pattern match is fine +g1a :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void +g1a r _ _ = case r of {} + +{- Why [G] F u1 u2 ~ Char is unsatisfiable + +[G] F u1 u2 ~ Char =>rewrite [G] If (IsUnit u1) (Case u2) Int ~ Char + =>(fundep) [W] IsUnit u1 ~ True + [W] Case u2 ~ Char <<-- insoluble: no relevant eqns +-} ===================================== testsuite/tests/pmcheck/should_compile/all.T ===================================== @@ -180,3 +180,4 @@ test('T24891', normal, compile, ['-Wincomplete-record-selectors']) test('T25257', normal, compile, [overlapping_incomplete]) test('T24845', [], compile, [overlapping_incomplete]) test('T22652', [], compile, [overlapping_incomplete]) +test('T22652a', [], compile, [overlapping_incomplete]) ===================================== testsuite/tests/typecheck/should_fail/T5236.stderr ===================================== @@ -0,0 +1,7 @@ +T5236.hs:16:9: error: [GHC-39999] + • No instance for ‘Id A B’ + The functional dependencies arising from this constraint are insoluble + • In the ambiguity check for ‘loop’ + To defer the ambiguity check to use sites, enable AllowAmbiguousTypes + In the type signature: loop :: Id A B => Bool + ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -250,7 +250,7 @@ test('SilentParametersOverlapping', normal, compile, ['']) test('FailDueToGivenOverlapping', normal, compile_fail, ['']) test('LongWayOverlapping', normal, compile_fail, ['']) test('T5051', normal, compile, ['']) -test('T5236',normal,compile,['']) +test('T5236',normal,compile_fail,['']) test('T5246',normal,compile_fail,['']) test('T5300',normal,compile_fail,['']) test('T5095',normalise_fun(normalise_errmsg),compile_fail,['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a2e35bf3cc33177353e2f7a244877e8e... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a2e35bf3cc33177353e2f7a244877e8e... You're receiving this email because of your account on gitlab.haskell.org.