Simon Peyton Jones pushed to branch wip/T26003 at Glasgow Haskell Compiler / GHC
Commits:
-
cdcced46
by Simon Peyton Jones at 2025-05-08T12:40:30+01:00
8 changed files:
- compiler/GHC/Core/Predicate.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Types/Error/Codes.hs
Changes:
| ... | ... | @@ -14,7 +14,7 @@ module GHC.Core.Predicate ( |
| 14 | 14 | EqRel(..), eqRelRole,
|
| 15 | 15 | isEqPred, isReprEqPred, isEqClassPred, isCoVarType,
|
| 16 | 16 | getEqPredTys, getEqPredTys_maybe, getEqPredRole,
|
| 17 | - predTypeEqRel,
|
|
| 17 | + predTypeEqRel, pprPredType,
|
|
| 18 | 18 | mkNomEqPred, mkReprEqPred, mkEqPred, mkEqPredRole,
|
| 19 | 19 | |
| 20 | 20 | -- Class predicates
|
| ... | ... | @@ -50,6 +50,7 @@ import GHC.Core.TyCo.Compare( tcEqTyConApps ) |
| 50 | 50 | import GHC.Core.TyCo.FVs( tyCoVarsOfTypeList, tyCoVarsOfTypesList )
|
| 51 | 51 | import GHC.Core.TyCon
|
| 52 | 52 | import GHC.Core.TyCon.RecWalk
|
| 53 | +import GHC.Types.Name( getOccName )
|
|
| 53 | 54 | import GHC.Types.Var
|
| 54 | 55 | import GHC.Types.Var.Set
|
| 55 | 56 | import GHC.Core.Multiplicity ( scaledThing )
|
| ... | ... | @@ -246,6 +247,16 @@ predTypeEqRel ty |
| 246 | 247 | | isReprEqPred ty = ReprEq
|
| 247 | 248 | | otherwise = NomEq
|
| 248 | 249 | |
| 250 | +pprPredType :: PredType -> SDoc
|
|
| 251 | +-- Special case for (t1 ~# t2) and (t1 ~R# t2)
|
|
| 252 | +pprPredType pred
|
|
| 253 | + = case classifyPredType pred of
|
|
| 254 | + EqPred eq_rel t1 t2 -> sep [ ppr t1, ppr (getOccName eq_tc) <+> ppr t2 ]
|
|
| 255 | + where
|
|
| 256 | + eq_tc = case eq_rel of
|
|
| 257 | + NomEq -> eqPrimTyCon
|
|
| 258 | + ReprEq -> eqReprPrimTyCon
|
|
| 259 | + _ -> ppr pred
|
|
| 249 | 260 | |
| 250 | 261 | {- *********************************************************************
|
| 251 | 262 | * *
|
| ... | ... | @@ -1741,12 +1741,12 @@ mkEqErr_help :: SolverReportErrCtxt |
| 1741 | 1741 | -> ErrorItem
|
| 1742 | 1742 | -> TcType -> TcType -> TcM TcSolverReportMsg
|
| 1743 | 1743 | mkEqErr_help ctxt item ty1 ty2
|
| 1744 | - | Just casted_tv1 <- getCastedTyVar_maybe ty1
|
|
| 1745 | - = mkTyVarEqErr ctxt item casted_tv1 ty2
|
|
| 1744 | + | Just (tv1, _co) <- getCastedTyVar_maybe ty1
|
|
| 1745 | + = mkTyVarEqErr ctxt item tv1 ty2
|
|
| 1746 | 1746 | |
| 1747 | 1747 | -- ToDo: explain.. Cf T2627b Dual (Dual a) ~ a
|
| 1748 | - | Just casted_tv2 <- getCastedTyVar_maybe ty2
|
|
| 1749 | - = mkTyVarEqErr ctxt item casted_tv2 ty1
|
|
| 1748 | + | Just (tv2, _co) <- getCastedTyVar_maybe ty2
|
|
| 1749 | + = mkTyVarEqErr ctxt item tv2 ty1
|
|
| 1750 | 1750 | |
| 1751 | 1751 | | otherwise
|
| 1752 | 1752 | = reportEqErr ctxt item ty1 ty2
|
| ... | ... | @@ -1779,16 +1779,15 @@ coercible_msg ty1 ty2 |
| 1779 | 1779 | return $ mkCoercibleExplanation rdr_env fam_envs ty1 ty2
|
| 1780 | 1780 | |
| 1781 | 1781 | mkTyVarEqErr :: SolverReportErrCtxt -> ErrorItem
|
| 1782 | - -> (TcTyVar, TcCoercionN) -> TcType -> TcM TcSolverReportMsg
|
|
| 1782 | + -> TcTyVar -> TcType -> TcM TcSolverReportMsg
|
|
| 1783 | 1783 | -- tv1 and ty2 are already tidied
|
| 1784 | -mkTyVarEqErr ctxt item casted_tv1 ty2
|
|
| 1785 | - = do { traceTc "mkTyVarEqErr" (ppr item $$ ppr casted_tv1 $$ ppr ty2)
|
|
| 1786 | - ; mkTyVarEqErr' ctxt item casted_tv1 ty2 }
|
|
| 1784 | +mkTyVarEqErr ctxt item tv1 ty2
|
|
| 1785 | + = do { traceTc "mkTyVarEqErr" (ppr item $$ ppr tv1 $$ ppr ty2)
|
|
| 1786 | + ; mkTyVarEqErr' ctxt item tv1 ty2 }
|
|
| 1787 | 1787 | |
| 1788 | 1788 | mkTyVarEqErr' :: SolverReportErrCtxt -> ErrorItem
|
| 1789 | - -> (TcTyVar, TcCoercionN) -> TcType -> TcM TcSolverReportMsg
|
|
| 1790 | -mkTyVarEqErr' ctxt item (tv1, _co1) ty2
|
|
| 1791 | - -- ToDo: eliminate _co1???
|
|
| 1789 | + -> TcTyVar -> TcType -> TcM TcSolverReportMsg
|
|
| 1790 | +mkTyVarEqErr' ctxt item tv1 ty2
|
|
| 1792 | 1791 | |
| 1793 | 1792 | -- Is this a representation-polymorphism error, e.g.
|
| 1794 | 1793 | -- alpha[conc] ~# rr[sk] ? If so, handle that first.
|
| ... | ... | @@ -2003,16 +2002,6 @@ misMatchOrCND ctxt item ty1 ty2 |
| 2003 | 2002 | -- Keep only UserGivens that have some equalities.
|
| 2004 | 2003 | -- See Note [Suppress redundant givens during error reporting]
|
| 2005 | 2004 | |
| 2006 | -{-
|
|
| 2007 | --- These are for the "blocked" equalities, as described in GHC.Tc.Solver.Equality
|
|
| 2008 | --- Note [Equalities with incompatible kinds], wrinkle (EIK2). There should
|
|
| 2009 | --- always be another unsolved wanted around, which will ordinarily suppress
|
|
| 2010 | --- this message. But this can still be printed out with -fdefer-type-errors
|
|
| 2011 | --- (sigh), so we must produce a message.
|
|
| 2012 | -mkBlockedEqErr :: ErrorItem -> TcSolverReportMsg
|
|
| 2013 | -mkBlockedEqErr item = BlockedEquality item
|
|
| 2014 | --}
|
|
| 2015 | - |
|
| 2016 | 2005 | {-
|
| 2017 | 2006 | Note [Suppress redundant givens during error reporting]
|
| 2018 | 2007 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
| ... | ... | @@ -4060,10 +4060,6 @@ pprTcSolverReportMsg _ (FixedRuntimeRepError frr_origs) = |
| 4060 | 4060 | = quotes (text "Levity")
|
| 4061 | 4061 | | otherwise
|
| 4062 | 4062 | = text "type"
|
| 4063 | -pprTcSolverReportMsg _ (BlockedEquality item) =
|
|
| 4064 | - vcat [ hang (text "Cannot use equality for substitution:")
|
|
| 4065 | - 2 (ppr (errorItemPred item))
|
|
| 4066 | - , text "Doing so would be ill-kinded." ]
|
|
| 4067 | 4063 | pprTcSolverReportMsg _ (ExpectingMoreArguments n thing) =
|
| 4068 | 4064 | text "Expecting" <+> speakN (abs n) <+>
|
| 4069 | 4065 | more <+> quotes (ppr thing)
|
| ... | ... | @@ -5071,8 +5067,6 @@ tcSolverReportMsgHints ctxt = \case |
| 5071 | 5067 | -> mismatchMsgHints ctxt mismatch_msg
|
| 5072 | 5068 | FixedRuntimeRepError {}
|
| 5073 | 5069 | -> noHints
|
| 5074 | - BlockedEquality {}
|
|
| 5075 | - -> noHints
|
|
| 5076 | 5070 | ExpectingMoreArguments {}
|
| 5077 | 5071 | -> noHints
|
| 5078 | 5072 | UnboundImplicitParams {}
|
| ... | ... | @@ -7465,4 +7459,4 @@ pprErrCtxtMsg = \case |
| 7465 | 7459 | --------------------------------------------------------------------------------
|
| 7466 | 7460 | |
| 7467 | 7461 | pprThBindLevel :: Set.Set ThLevelIndex -> SDoc
|
| 7468 | -pprThBindLevel levels_set = text "level" <> pluralSet levels_set <+> pprUnquotedSet levels_set |
|
| \ No newline at end of file | ||
| 7462 | +pprThBindLevel levels_set = text "level" <> pluralSet levels_set <+> pprUnquotedSet levels_set |
| ... | ... | @@ -5583,17 +5583,6 @@ data TcSolverReportMsg |
| 5583 | 5583 | -- See 'FixedRuntimeRepErrorInfo' and 'FixedRuntimeRepContext' for more information.
|
| 5584 | 5584 | | FixedRuntimeRepError [FixedRuntimeRepErrorInfo]
|
| 5585 | 5585 | |
| 5586 | - -- | An equality between two types is blocked on a kind equality
|
|
| 5587 | - -- between their kinds.
|
|
| 5588 | - --
|
|
| 5589 | - -- Test cases: none.
|
|
| 5590 | - | BlockedEquality ErrorItem
|
|
| 5591 | - -- These are for the "blocked" equalities, as described in
|
|
| 5592 | - -- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality,
|
|
| 5593 | - -- wrinkle (EIK2). There should always be another unsolved wanted around,
|
|
| 5594 | - -- which will ordinarily suppress this message. But this can still be printed out
|
|
| 5595 | - -- with -fdefer-type-errors (sigh), so we must produce a message.
|
|
| 5596 | - |
|
| 5597 | 5586 | -- | Something was not applied to sufficiently many arguments.
|
| 5598 | 5587 | --
|
| 5599 | 5588 | -- Example:
|
| ... | ... | @@ -1328,6 +1328,7 @@ canDecomposableTyConAppOK ev eq_rel tc (ty1,tys1) (ty2,tys2) |
| 1328 | 1328 | -- guaranteed that cos has the same length as tys1 and tys2
|
| 1329 | 1329 | -- See Note [Fast path when decomposing TyConApps]
|
| 1330 | 1330 | -> do { (co, _, _) <- wrapUnifierTcS ev role $ \uenv ->
|
| 1331 | +-- do { cos <- zipWith4M (u_arg uenv) new_locs tc_roles (reverse tys1) (reverse tys2)
|
|
| 1331 | 1332 | do { cos <- zipWith4M (u_arg uenv) new_locs tc_roles tys1 tys2
|
| 1332 | 1333 | -- zipWith4M: see Note [Work-list ordering]
|
| 1333 | 1334 | -- in GHC.Tc.Solved.Equality
|
| ... | ... | @@ -2094,7 +2095,7 @@ Wrinkles: |
| 2094 | 2095 | the kind of the parent type-equality. See the calls to `mkKindEqLoc`
|
| 2095 | 2096 | in `canEqCanLHSHetero`.
|
| 2096 | 2097 | |
| 2097 | - * We /also/ these unsolved kind equalities to the `RewriterSet` of the
|
|
| 2098 | + * We /also/ add these unsolved kind equalities to the `RewriterSet` of the
|
|
| 2098 | 2099 | parent constraint; see `do_rewrite` in `canEqCanLHSHetero`.
|
| 2099 | 2100 | |
| 2100 | 2101 | * When filling a coercion hole we kick out any equality constraints whose
|
| ... | ... | @@ -2314,9 +2314,9 @@ instance Outputable WantedCtEvidence where |
| 2314 | 2314 | |
| 2315 | 2315 | instance Outputable CtEvidence where
|
| 2316 | 2316 | ppr ev = ppr (ctEvFlavour ev)
|
| 2317 | - <+> pp_ev <+> braces (ppr (ctl_depth (ctEvLoc ev)) <> pp_rewriters)
|
|
| 2317 | + <+> hang (pp_ev <+> braces (ppr (ctl_depth (ctEvLoc ev)) <> pp_rewriters))
|
|
| 2318 | 2318 | -- Show the sub-goal depth too
|
| 2319 | - <> dcolon <+> ppr (ctEvPred ev)
|
|
| 2319 | + 2 (dcolon <+> pprPredType (ctEvPred ev))
|
|
| 2320 | 2320 | where
|
| 2321 | 2321 | pp_ev = case ev of
|
| 2322 | 2322 | CtGiven ev -> ppr (ctev_evar ev)
|
| ... | ... | @@ -3578,11 +3578,6 @@ But there are several cases we need to be wary of: |
| 3578 | 3578 | (2) We must still make sure that no variable in a coercion is at too
|
| 3579 | 3579 | high a level. But, when unifying, we can promote any variables we encounter.
|
| 3580 | 3580 | |
| 3581 | -{- Don't do this
|
|
| 3582 | -(3) We do not unify variables with a type with a free coercion hole.
|
|
| 3583 | - See (COERCION-HOLE) in Note [Unification preconditions].
|
|
| 3584 | --}
|
|
| 3585 | - |
|
| 3586 | 3581 | Note [Promotion and level-checking]
|
| 3587 | 3582 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
| 3588 | 3583 | "Promotion" happens when we have this:
|
| ... | ... | @@ -411,7 +411,6 @@ type family GhcDiagnosticCode c = n | n -> c where |
| 411 | 411 | GhcDiagnosticCode "UnsatisfiableError" = 22250
|
| 412 | 412 | GhcDiagnosticCode "ReportHoleError" = 88464
|
| 413 | 413 | GhcDiagnosticCode "FixedRuntimeRepError" = 55287
|
| 414 | - GhcDiagnosticCode "BlockedEquality" = 06200
|
|
| 415 | 414 | GhcDiagnosticCode "ExpectingMoreArguments" = 81325
|
| 416 | 415 | GhcDiagnosticCode "UnboundImplicitParams" = 91416
|
| 417 | 416 | GhcDiagnosticCode "AmbiguityPreventsSolvingCt" = 78125
|