Bug in opt_trans_rule in OptCoercion

The ForAllCo case in the definition of opt_trans_rule in OptCoercion is not right:

  push_trans tv1 eta1 r1 tv2 eta2 r2
   = fireTransRule "EtaAllTy" co1 co2 $
      mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
    where
      is' = is `extendInScopeSet` tv1
      r2' = substCoWithUnchecked [tv2] [TyVarTy tv1] r2  -- ill-kinded!

Given co1;co2, where

    co1 = \/ tv1 : eta1. r1
    co2 = \/ tv2 : eta2. r2

We would like optimize the transitivity coercion. I think what we want is

\/tv1 : (eta1;eta2).  (r1; r2[tv2 |-> tv1 |> eta1])

Namely it should be

r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2

If there is any program that could hit the bug it would be better, as we can add it to test cases.

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture