Simon Peyton Jones pushed to branch wip/T26349 at Glasgow Haskell Compiler / GHC Commits: 66ad3ca0 by Simon Peyton Jones at 2025-10-25T13:18:56+01:00 Remove trace - - - - - 1 changed file: - compiler/GHC/Tc/Types/Evidence.hs Changes: ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -135,8 +135,51 @@ maybeSymCo NotSwapped co = co ************************************************************************ -} -{- Note [WpSubType] -~~~~~~~~~~~~~~~~~~~ +{- Note [Deep subsumption and WpSubType] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When making DeepSubsumption checks, we may end up with hard-to-spot identity wrappers. +For example (#26255) suppose we have + (forall a. Eq a => a->a) -> Int <= (forall a. Eq a => a->a) -> Int +The two types are equal so we should certainly get an identity wrapper. But we'll get +tihs wrapper from `tcSubType`: + WpFun (WpTyLam a <.> WpEvLam dg <.> WpLet (dw=dg) <.> WpEvApp dw <.> WpTyApp a) + WpHole +That elaborate wrapper is really just a no-op, but it's far from obvious. If we just +desugar (HsWrap f wp) straightforwardly we'll get + \(g:forall a. Eq a => a -> a). + f (/\a. \(dg:Eq a). let dw=dg in g a dw) + +To recognise that as just `f`, we'd have to eta-reduce twice. But eta-reduction +is not sound in general, so we'll end up retaining the lambdas. Two bad results + +* Adding DeepSubsumption gratuitiously makes programs less efficient. + +* When the subsumption is on the LHS of a rule, or in a SPECIALISE pragma, we + may not be able to make a decent RULE at all, and will fail with "LHS of rule + is too complicated to desugar (#26255) + +It'd be nicest to solve the problem at source, by never generating those +gruesome wrappers in the first place, but we can't do that because + +* The WpTyLam and WpTyApp are not introduced together in `tcSubType`, so we can't + easily cancel them out. Even if we have + forall a. t1 <= forall a. t2 + there is no guarantee that these are the "same" a. E.g. + forall a b. a -> b -> b <= forall x y. y -> x - >x + Similarly WpEvLam and WpEvApp + +* We have not yet done constraint solving so we don't know what evidence will + end up in those WpLet bindings. + +TL;DR we must generate +Here's our solution + +(DSST1) Tag the wrappers generated from a subtype check with WpSubType. In normal + wrappers the binders of a WpTyLam or WpEvLam can scope over the "hole" of the + wrapper -- that is how we introduce type-lambdas and dictionary-lambda into the + terms! But in /subtype/ wrappers, these type/dictionary lambdas only scope over + the WpTyApp and WpEvApp nodes in the /same/ wrapper. That is w + (WpSubType wp) means the same as `wp`, but with the added promise that the binders in `wp` do not scope over the hole -} @@ -378,7 +421,7 @@ collectHsWrapBinders wrap = go wrap [] optSubTypeHsWrapper :: HsWrapper -> HsWrapper optSubTypeHsWrapper wrap - = pprTrace "optHsWrapper" (vcat [ text "in:" <+> ppr wrap, text "out:" <+> ppr (opt wrap) ]) $ + = -- pprTrace "optHsWrapper" (vcat [ text "in:" <+> ppr wrap, text "out:" <+> ppr (opt wrap) ]) $ opt wrap where opt :: HsWrapper -> HsWrapper View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/66ad3ca0e80547646d98a3df5f35133f... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/66ad3ca0e80547646d98a3df5f35133f... You're receiving this email because of your account on gitlab.haskell.org.