| ... |
... |
@@ -282,18 +282,24 @@ optCoRefl subst in_co |
|
282
|
282
|
#endif
|
|
283
|
283
|
|
|
284
|
284
|
|
|
285
|
|
-opt_co_refl :: Subst -> Coercion -> Coercion
|
|
|
285
|
+opt_co_refl :: Subst -> InCoercion -> OutCoercion
|
|
286
|
286
|
opt_co_refl subst co = go co
|
|
287
|
287
|
where
|
|
288
|
288
|
go_m MRefl = MRefl
|
|
289
|
289
|
go_m (MCo co) = MCo (go co)
|
|
290
|
290
|
|
|
|
291
|
+ go_ty ty = substTy subst ty
|
|
|
292
|
+
|
|
291
|
293
|
go_s cos = map go cos
|
|
292
|
294
|
|
|
293
|
|
- go co@(Refl {}) = co
|
|
294
|
|
- go co@(GRefl {}) = co
|
|
295
|
|
- go co@(CoVarCo {}) = co
|
|
296
|
|
- go co@(HoleCo {}) = co
|
|
|
295
|
+ -- See Note [Substituting in a coercion hole]
|
|
|
296
|
+ go_hole h@(CoercionHole { ch_co_var = cv })
|
|
|
297
|
+ = h { ch_co_var = updateVarType go_ty cv }
|
|
|
298
|
+
|
|
|
299
|
+ go (Refl ty) = Refl (substTy subst ty)
|
|
|
300
|
+ go (GRefl r ty mco) = GRefl r (go_ty ty) (go_m mco)
|
|
|
301
|
+ go (CoVarCo cv) = substCoVar subst cv
|
|
|
302
|
+ go (HoleCo h) = HoleCo $!! go_hole h
|
|
297
|
303
|
go (SymCo co) = mkSymCo (go co)
|
|
298
|
304
|
go (KindCo co) = mkKindCo (go co)
|
|
299
|
305
|
go (SubCo co) = mkSubCo (go co)
|
| ... |
... |
@@ -315,28 +321,30 @@ opt_co_refl subst co = go co |
|
315
|
321
|
-- This is the main payload
|
|
316
|
322
|
go (TransCo co1 co2) = gobble gs0 co1 [co2]
|
|
317
|
323
|
where
|
|
318
|
|
- lk = coercionLKind co1
|
|
|
324
|
+ lk' = substTy subst (coercionLKind co1)
|
|
319
|
325
|
role = coercionRole co1
|
|
320
|
326
|
|
|
321
|
327
|
gs0 :: GobbleState
|
|
322
|
|
- gs0 = GS (mkReflCo role lk) (insertTM lk gs0 emptyTM)
|
|
|
328
|
+ gs0 = GS (mkReflCo role lk') (insertTM lk' gs0 emptyTM)
|
|
323
|
329
|
|
|
324
|
|
- gobble :: GobbleState -> Coercion -> [Coercion] -> Coercion
|
|
|
330
|
+ gobble :: GobbleState -> InCoercion -> [InCoercion] -> OutCoercion
|
|
325
|
331
|
-- gobble (GS co1 tm) co2 cos returns a coercion equivalent to (co1;co2;cos)
|
|
326
|
332
|
gobble gs (TransCo co2 co3) cos
|
|
327
|
333
|
= gobble gs co2 (co3 : cos)
|
|
328
|
|
- gobble (GS co1 tm) co2 cos
|
|
329
|
|
- = case lookupTM rk tm of
|
|
|
334
|
+ gobble (GS co1' tm) co2 cos
|
|
|
335
|
+ = case lookupTM rk' tm of
|
|
330
|
336
|
Just gs -> gobble0 gs cos
|
|
331
|
337
|
Nothing -> gobble0 gs' cos
|
|
332
|
338
|
where
|
|
333
|
|
- rk = coercionRKind co2
|
|
334
|
|
- gs' = GS (co1 `mkTransCo` co2) (insertTM rk gs' tm)
|
|
|
339
|
+ co2' = go co2
|
|
|
340
|
+ rk' = coercionRKind co2'
|
|
|
341
|
+ gs' = GS (co1' `mkTransCo` co2') (insertTM rk' gs' tm)
|
|
335
|
342
|
|
|
336
|
343
|
gobble0 (GS co _) [] = co
|
|
337
|
344
|
gobble0 gs (co:cos) = gobble gs co cos
|
|
338
|
345
|
|
|
339
|
|
-data GobbleState = GS Coercion (TypeMap GobbleState)
|
|
|
346
|
+data GobbleState = GS OutCoercion (TypeMap GobbleState)
|
|
|
347
|
+ -- The map is keyed by OutType
|
|
340
|
348
|
|
|
341
|
349
|
{- **********************************************************************
|
|
342
|
350
|
%* *
|