| ... |
... |
@@ -135,8 +135,51 @@ maybeSymCo NotSwapped co = co |
|
135
|
135
|
************************************************************************
|
|
136
|
136
|
-}
|
|
137
|
137
|
|
|
138
|
|
-{- Note [WpSubType]
|
|
139
|
|
-~~~~~~~~~~~~~~~~~~~
|
|
|
138
|
+{- Note [Deep subsumption and WpSubType]
|
|
|
139
|
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
140
|
+When making DeepSubsumption checks, we may end up with hard-to-spot identity wrappers.
|
|
|
141
|
+For example (#26255) suppose we have
|
|
|
142
|
+ (forall a. Eq a => a->a) -> Int <= (forall a. Eq a => a->a) -> Int
|
|
|
143
|
+The two types are equal so we should certainly get an identity wrapper. But we'll get
|
|
|
144
|
+tihs wrapper from `tcSubType`:
|
|
|
145
|
+ WpFun (WpTyLam a <.> WpEvLam dg <.> WpLet (dw=dg) <.> WpEvApp dw <.> WpTyApp a)
|
|
|
146
|
+ WpHole
|
|
|
147
|
+That elaborate wrapper is really just a no-op, but it's far from obvious. If we just
|
|
|
148
|
+desugar (HsWrap f wp) straightforwardly we'll get
|
|
|
149
|
+ \(g:forall a. Eq a => a -> a).
|
|
|
150
|
+ f (/\a. \(dg:Eq a). let dw=dg in g a dw)
|
|
|
151
|
+
|
|
|
152
|
+To recognise that as just `f`, we'd have to eta-reduce twice. But eta-reduction
|
|
|
153
|
+is not sound in general, so we'll end up retaining the lambdas. Two bad results
|
|
|
154
|
+
|
|
|
155
|
+* Adding DeepSubsumption gratuitiously makes programs less efficient.
|
|
|
156
|
+
|
|
|
157
|
+* When the subsumption is on the LHS of a rule, or in a SPECIALISE pragma, we
|
|
|
158
|
+ may not be able to make a decent RULE at all, and will fail with "LHS of rule
|
|
|
159
|
+ is too complicated to desugar (#26255)
|
|
|
160
|
+
|
|
|
161
|
+It'd be nicest to solve the problem at source, by never generating those
|
|
|
162
|
+gruesome wrappers in the first place, but we can't do that because
|
|
|
163
|
+
|
|
|
164
|
+* The WpTyLam and WpTyApp are not introduced together in `tcSubType`, so we can't
|
|
|
165
|
+ easily cancel them out. Even if we have
|
|
|
166
|
+ forall a. t1 <= forall a. t2
|
|
|
167
|
+ there is no guarantee that these are the "same" a. E.g.
|
|
|
168
|
+ forall a b. a -> b -> b <= forall x y. y -> x - >x
|
|
|
169
|
+ Similarly WpEvLam and WpEvApp
|
|
|
170
|
+
|
|
|
171
|
+* We have not yet done constraint solving so we don't know what evidence will
|
|
|
172
|
+ end up in those WpLet bindings.
|
|
|
173
|
+
|
|
|
174
|
+TL;DR we must generate
|
|
|
175
|
+Here's our solution
|
|
|
176
|
+
|
|
|
177
|
+(DSST1) Tag the wrappers generated from a subtype check with WpSubType. In normal
|
|
|
178
|
+ wrappers the binders of a WpTyLam or WpEvLam can scope over the "hole" of the
|
|
|
179
|
+ wrapper -- that is how we introduce type-lambdas and dictionary-lambda into the
|
|
|
180
|
+ terms! But in /subtype/ wrappers, these type/dictionary lambdas only scope over
|
|
|
181
|
+ the WpTyApp and WpEvApp nodes in the /same/ wrapper. That is w
|
|
|
182
|
+
|
|
140
|
183
|
(WpSubType wp) means the same as `wp`, but with the added promise that
|
|
141
|
184
|
the binders in `wp` do not scope over the hole
|
|
142
|
185
|
-}
|
| ... |
... |
@@ -378,7 +421,7 @@ collectHsWrapBinders wrap = go wrap [] |
|
378
|
421
|
|
|
379
|
422
|
optSubTypeHsWrapper :: HsWrapper -> HsWrapper
|
|
380
|
423
|
optSubTypeHsWrapper wrap
|
|
381
|
|
- = pprTrace "optHsWrapper" (vcat [ text "in:" <+> ppr wrap, text "out:" <+> ppr (opt wrap) ]) $
|
|
|
424
|
+ = -- pprTrace "optHsWrapper" (vcat [ text "in:" <+> ppr wrap, text "out:" <+> ppr (opt wrap) ]) $
|
|
382
|
425
|
opt wrap
|
|
383
|
426
|
where
|
|
384
|
427
|
opt :: HsWrapper -> HsWrapper
|