Commit 7639e751 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Fix a nasty scoping error in OptCoercion (EtaAllR/L)

Sing ho for ASSERTs!
parent 773884a0
......@@ -239,15 +239,17 @@ opt_trans_rule is co1 co2@(TyConAppCo tc cos2)
opt_trans_rule is co1 co2
| Just (tv1,r1) <- splitForAllCo_maybe co1
, Just (tv2,r2) <- etaForAllCo_maybe co2
, let r2' = substCoWithTy is tv2 (mkTyVarTy tv1) r2
, let r2' = substCoWithTy is' tv2 (mkTyVarTy tv1) r2
is' = is `extendInScopeSet` tv1
= fireTransRule "EtaAllL" co1 co2 $
mkForAllCo tv1 (opt_trans2 (extendInScopeSet is tv1) r1 r2')
mkForAllCo tv1 (opt_trans2 is' r1 r2')
| Just (tv2,r2) <- splitForAllCo_maybe co2
, Just (tv1,r1) <- etaForAllCo_maybe co1
, let r1' = substCoWithTy is tv1 (mkTyVarTy tv2) r1
, let r1' = substCoWithTy is' tv1 (mkTyVarTy tv2) r1
is' = is `extendInScopeSet` tv2
= fireTransRule "EtaAllR" co1 co2 $
mkForAllCo tv1 (opt_trans2 (extendInScopeSet is tv2) r1' r2)
mkForAllCo tv1 (opt_trans2 is' r1' r2)
-- Push transitivity inside axioms
opt_trans_rule is co1 co2
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment