[GHC] #15453: Bug in opt_trans_rule in OptCoercion

[GHC]

#15453: Bug in opt_trans_rule in OptCoercion
-------------------------------------+-------------------------------------
           Reporter:  ningning       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The ForAllCo case in the definition of opt_trans_rule in OptCoercion is
 not right:

 {{{#!hs
   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

 {{{#!hs
     co1 = \/ tv1 : eta1. r1
     co2 = \/ tv2 : eta2. r2
 }}}

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

 {{{#!hs
 \/tv1 : (eta1;eta2).  (r1; r2[tv2 |-> tv1 |> eta1])
 }}}

 Namely it should be

 {{{#!hs
 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15453>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler