Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC Commits: e0a84ca0 by Simon Peyton Jones at 2025-10-27T16:36:30+00:00 Comments only - - - - - 7 changed files: - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Utils/Concrete.hs - compiler/GHC/Tc/Utils/Instantiate.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Utils/EndoOS.hs Changes: ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -128,7 +128,7 @@ Note [Instantiation variables are short lived] TL;DR: instantiation variables are short-lived. So it is fine for them to have an infinite level (=QLInstVar) because they are monomorphised - before do anything like skolem-escape checks. + before we do anything like skolem-escape checks. * The constraint solver never sees an instantiation variable [not quite true; see below] ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -648,16 +648,22 @@ There are lots of wrinkles of course: because we want to /gather/ the equality constraint (to put in the implication) rather than /emit/ them into the monad, as `wrapUnifierAndEmit` does. -(SF6) We solve the nested constraints right away. In the past we instead generated - an `Implication` to be solved later, but we no longer have a convenient place - to accumulate such an implication for later solving. Instead we just try to solve - them on the spot, and abandon the attempt if we fail. - - In the latter case we are left with an unsolved (forall a. blah) ~ (forall b. blah), - and it may not be clear /why/ we couldn't solve it. But on balance the error - messages improve: it is easier to understand that - (forall a. a->a) ~ (forall b. b->Int) - is insoluble than it is to understand a message about matching `a` with `Int`. +(SF6) We solve the nested constraints right away. In a type-correct program, + this attempt will usually succeed. But if we don't completely solve it, we + abandon the attempt and keep the origin forall-equality. + + In the abandon-the-attempt case, we are left with an unsolved + (forall a. blah) ~ (forall b. blah) + + and it may not be immediately apparent /why/ we couldn't solve it. But actually + such errors messages can be /better/. For example, it is easier to understand + that (forall a. a->a) ~ (forall b. b->Int) is insoluble than it is to understand a + message about matching `a` with `Int`, because `a` is a skolem. + + Historical note: In the past we instead generated an `Implication`, storing it in + a dedicated field `wl_implics` in the work-list to be solved later. But that + plumbing was tiresome, and now we just try to solve them on the spot, and abandon + the attempt if we fail. -} {- Note [Unwrap newtypes first] @@ -2942,15 +2948,14 @@ lookup_eq_in_qcis :: CtEvidence -> EqRel -> TcType -> TcType -> SolverStage () -- Why? See Note [Looking up primitive equalities in quantified constraints] -- See also GHC.Tc.Solver.Dict Note [Equality superclasses in quantified constraints] lookup_eq_in_qcis (CtGiven {}) _ _ _ - = nopStage () + = nopStage () -- Never look up Givens in quantified constraints lookup_eq_in_qcis ev@(CtWanted (WantedCt { ctev_dest = dest, ctev_loc = loc })) eq_rel lhs rhs = do { ev_binds_var <- simpleStage getTcEvBindsVar ; ics <- simpleStage getInertCans - ; if null (inert_qcis ics) + ; if null (inert_qcis ics) -- Shortcut common case || isCoEvBindsVar ev_binds_var -- See Note [Instances in no-evidence implications] - then -- Shortcut common case - nopStage () + then nopStage () else -- Try looking for both (lhs~rhs) anr (rhs~lhs); see #23333 do { try NotSwapped; try IsSwapped } } where ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -414,18 +414,18 @@ updInertIrreds irred {- Note [Kick out after filling a coercion hole] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -If we we solve `kco` and have `co` in the inert set whose rewriter-set includes `kco`, +If we solve `kco` and have `co` in the inert set whose rewriter-set includes `kco`, we should kick out `co` so that we can now unify it, which might unlock other stuff. See Note [Unify only if the rewriter set is empty] in GHC.Tc.Solver.Equality for why solving `kco` might unlock `co`, especially (URW2). Hence `kickOutAfterFillingCoercionHole`. It looks at inert constraints that are * Wanted - * Of form alpha ~ rhs, where alpha is a unification variable + * Of the form alpha ~ rhs, where alpha is a unification variable and kicks out any that will have an empty rewriter set after filling the hole. Wrinkles: -(KOC1) If co's rewriter-set is {kco, xco}, there is on point in kicking it out, +(KOC1) If co's rewriter-set is {kco, xco}, there is no point in kicking it out, because it still can't be unified. So we only kick out if the co's rewriter-set becomes empty. ===================================== compiler/GHC/Tc/Utils/Concrete.hs ===================================== @@ -529,7 +529,7 @@ Here are the moving parts: IdDetails: RepPolyId [ r :-> ConcreteFRR (FixedRuntimeRepOrigin b (..)) ] * When instantiating the type of an Id at a call site, at the call to - GHC.Tc.Utils.Instantiate.instantiateSigma in GHC.Tc.Gen.App.tcInstFun, + GHC.Tc.Utils.Instantiate.instantiateSigmaQL in GHC.Tc.Gen.App.tcInstFun, create ConcreteTv metavariables (instead of TauTvs) based on the ConcreteTyVars stored in the IdDetails of the Id. ===================================== compiler/GHC/Tc/Utils/Instantiate.hs ===================================== @@ -285,7 +285,7 @@ topInstantiate orig sigma , (theta, body_ty) <- tcSplitPhiTy phi_ty , not (null tvs && null theta) = do { (subst, inst_tvs) <- newMetaTyVarsX empty_subst tvs - -- No need to worry about concrete tyvars here (c.f. instantiateSigma) + -- No need to worry about concrete tyvars here (c.f. instantiateSigmaQL) -- See Note [Representation-polymorphism checking built-ins] -- in GHC.Tc.Utils.Concrete. ===================================== compiler/GHC/Tc/Utils/TcMType.hs ===================================== @@ -1084,7 +1084,7 @@ When we instantiate 'coerce' in the previous example, we obtain a substitution which we need to apply to the 'frr_type' field in order for the type variables in the error message to match up. -This is done by the call to 'substConcreteTvOrigin' in 'instantiateSigma'. +This is done by the call to 'substConcreteTvOrigin' in 'instantiateSigmaQL'. Wrinkle [Extending the substitution] @@ -1094,7 +1094,7 @@ Wrinkle [Extending the substitution] bad2 :: forall {s} (z :: TYPE s). z -> z bad2 = coerce @z - Then 'instantiateSigma' will only instantiate the inferred type variable 'r' + Then 'instantiateSigmaQL' will only instantiate the inferred type variable 'r' of 'coerce', as it needs to leave 'a' un-instantiated so that the visible type application '@z' makes sense. In this case, we end up with a substitution ===================================== compiler/GHC/Utils/EndoOS.hs ===================================== @@ -4,7 +4,7 @@ -- Mostly for backwards compatibility. -- One-shot endomorphisms --- Like GHC.Internal.Data.Semigroup.Internal.Endo, but uting +-- Like GHC.Internal.Data.Semigroup.Internal.Endo, but using -- the one-shot trick from -- Note [The one-shot state monad trick] in GHC.Utils.Monad. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e0a84ca02839f463a9fd7cb0f11da0d8... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e0a84ca02839f463a9fd7cb0f11da0d8... You're receiving this email because of your account on gitlab.haskell.org.