| ... |
... |
@@ -188,6 +188,40 @@ that it is a no-op. Here's our solution |
|
188
|
188
|
|
|
189
|
189
|
(DSST3) When desugaring, try eta-reduction on the payload of a WpSubType.
|
|
190
|
190
|
This is done in `GHC.HsToCore.Binds.dsHsWrapper` by the call to `optSubTypeHsWrapper`.
|
|
|
191
|
+
|
|
|
192
|
+Note [Smart contructor for WpFun]
|
|
|
193
|
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
194
|
+In `matchExpectedFunTys` (and the moribund `matchActualFunTys`) we use the smart
|
|
|
195
|
+constructor `mkWpFun` to optimise away a `WpFun`. This is important (T1753b, T15105).
|
|
|
196
|
+Suppose we have `type instance F Int = Type`, and we are typechecking this:
|
|
|
197
|
+ (\x. True) :: (a :: F Int) -> a
|
|
|
198
|
+We cannot desugar this to
|
|
|
199
|
+ \(x::a::F Int). True
|
|
|
200
|
+because then `x` does not have a fixed runtime representation.
|
|
|
201
|
+See Note [Representation polymorphism invariants] in GHC.Core.
|
|
|
202
|
+
|
|
|
203
|
+So we must cast the entire lambda first. We want to end up with
|
|
|
204
|
+ (\(x::(a |> kco). x) |> (FunCo co <Bool>)
|
|
|
205
|
+where
|
|
|
206
|
+ kco :: F Int ~ Type = ... -- From the type instance
|
|
|
207
|
+ co :: (a |> kco) ~ a = GRefl a kco
|
|
|
208
|
+Note that we /cast/ the lambda with a /coercion/. We must not
|
|
|
209
|
+/wrap/ it in a /WpFun/ because the latter generates a lambda that won't obey
|
|
|
210
|
+the runtime-rep rules.
|
|
|
211
|
+
|
|
|
212
|
+The check is done by the `hasFixedRuntimeRep` magic in `matchExpectedFunTys`.
|
|
|
213
|
+
|
|
|
214
|
+QUESTIONS:
|
|
|
215
|
+
|
|
|
216
|
+* What happens if we can't build a cast? What error is produced, and how?
|
|
|
217
|
+
|
|
|
218
|
+* What about mkWpFun (WpCast co) (WpTyLam ...), which might arise from
|
|
|
219
|
+ (a :: F Int -> forall b. b->b)
|
|
|
220
|
+ Will we generate a cast and then a WpFun. Surely we should?
|
|
|
221
|
+ Test case?
|
|
|
222
|
+
|
|
|
223
|
+* I think it's really only matchExpectedFunTys that is implicated here.
|
|
|
224
|
+ (Apart from matchActualFunTys.) Anything else?
|
|
191
|
225
|
-}
|
|
192
|
226
|
|
|
193
|
227
|
-- We write wrap :: t1 ~> t2
|
| ... |
... |
@@ -276,20 +310,31 @@ WpCast c1 <.> WpCast c2 = WpCast (c2 `mkTransCo` c1) |
|
276
|
310
|
-- This is thus the same as WpCast (c2 ; c1) and not WpCast (c1 ; c2).
|
|
277
|
311
|
c1 <.> c2 = c1 `WpCompose` c2
|
|
278
|
312
|
|
|
279
|
|
--- | Smart constructor to create a 'WpFun' 'HsWrapper', which avoids introducing
|
|
280
|
|
--- a lambda abstraction if the two supplied wrappers are either identities or
|
|
281
|
|
--- casts.
|
|
282
|
|
---
|
|
283
|
|
--- PRECONDITION: either:
|
|
284
|
|
---
|
|
285
|
|
--- 1. both of the 'HsWrapper's are identities or casts, or
|
|
286
|
|
--- 2. both the "from" and "to" types of the first wrapper have a syntactically
|
|
287
|
|
--- fixed RuntimeRep (see Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete).
|
|
288
|
313
|
mkWpFun :: HsWrapper -> HsWrapper
|
|
289
|
314
|
-> Scaled TcTypeFRR -- ^ the "from" type of the first wrapper
|
|
290
|
315
|
-> TcType -- ^ Either "from" type or "to" type of the second wrapper
|
|
291
|
316
|
-- (used only when the second wrapper is the identity)
|
|
292
|
317
|
-> HsWrapper
|
|
|
318
|
+-- ^ Smart constructor to create a 'WpFun' 'HsWrapper'
|
|
|
319
|
+-- See Note [Smart contructor for WpFun] for why we need a smart constructor
|
|
|
320
|
+--
|
|
|
321
|
+-- PRECONDITION: either:
|
|
|
322
|
+--
|
|
|
323
|
+-- 1. Both of the 'HsWrapper's are WpHole or WpCast.
|
|
|
324
|
+-- In this we optimise away the WpFun entirely
|
|
|
325
|
+-- OR
|
|
|
326
|
+-- 2. Both the "from" and "to" types of the first wrapper have a syntactically
|
|
|
327
|
+-- fixed RuntimeRep (see Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete).
|
|
|
328
|
+-- If we retain the WpFun (i.e. not case 1), it will desugar to a lambda
|
|
|
329
|
+-- \x. w_res[ e w_arg[x] ]
|
|
|
330
|
+-- To satisfy Note [Representation polymorphism invariants] in GHC.Core,
|
|
|
331
|
+-- it must be the case that both the lambda bound variable x and the function
|
|
|
332
|
+-- argument w_arg[x] have a fixed runtime representation, i.e. that both the
|
|
|
333
|
+-- "from" and "to" types of the first wrapper "w_arg" have a fixed runtime
|
|
|
334
|
+-- representation.
|
|
|
335
|
+--
|
|
|
336
|
+-- Unfortunately, we can't check precondition (2) with an assertion here, because of
|
|
|
337
|
+-- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
|
|
293
|
338
|
mkWpFun w1 w2 st1@(Scaled m1 t1) t2
|
|
294
|
339
|
= case (w1,w2) of
|
|
295
|
340
|
(WpHole, WpHole) -> WpHole
|
| ... |
... |
@@ -297,17 +342,6 @@ mkWpFun w1 w2 st1@(Scaled m1 t1) t2 |
|
297
|
342
|
(WpCast co1, WpHole) -> WpCast (mk_wp_fun_co m1 (mkSymCo co1) (mkRepReflCo t2))
|
|
298
|
343
|
(WpCast co1, WpCast co2) -> WpCast (mk_wp_fun_co m1 (mkSymCo co1) co2)
|
|
299
|
344
|
(_, _) -> WpFun w1 w2 st1 t2
|
|
300
|
|
- -- In the WpFun case, we will desugar to a lambda
|
|
301
|
|
- --
|
|
302
|
|
- -- \x. w_res[ e w_arg[x] ]
|
|
303
|
|
- --
|
|
304
|
|
- -- To satisfy Note [Representation polymorphism invariants] in GHC.Core,
|
|
305
|
|
- -- it must be the case that both the lambda bound variable x and the function
|
|
306
|
|
- -- argument w_arg[x] have a fixed runtime representation, i.e. that both the
|
|
307
|
|
- -- "from" and "to" types of the first wrapper "w_arg" have a fixed runtime representation.
|
|
308
|
|
- --
|
|
309
|
|
- -- Unfortunately, we can't check this with an assertion here, because of
|
|
310
|
|
- -- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
|
|
311
|
345
|
|
|
312
|
346
|
mkWpSubType :: HsWrapper -> HsWrapper
|
|
313
|
347
|
-- See (DSST2) in Note [Deep subsumption and WpSubType]
|