Re: [GHC] #15453: Bug in opt_trans_rule in OptCoercion

#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5018 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Krzysztof Gogolewski ): In [changeset:"11de4380c2f16f374c6e8fbacf8dce00376e7efb/ghc" 11de438/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="11de4380c2f16f374c6e8fbacf8dce00376e7efb" Fix #15453: bug in ForAllCo case in opt_trans_rule Summary: Given ``` co1 = \/ tv1 : eta1. r1 co2 = \/ tv2 : eta2. r2 ``` We would like to optimize `co1; co2` so we push transitivity inside forall. It should be ``` \/tv1 : (eta1;eta2). (r1; r2[tv2 |-> tv1 |> eta1]) ``` It is implemented in the ForAllCo case in opt_trans_rule in OptCoercion. However current implementation is not right: ``` r2' = substCoWithUnchecked [tv2] [TyVarTy tv1] r2 -- ill-kinded! ``` This patch corrects it to be ``` r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2 ``` Test Plan: validate Reviewers: bgamari, goldfire, RyanGlScott Reviewed By: RyanGlScott Subscribers: rwbarton, thomie, carter GHC Trac Issues: #15453 Differential Revision: https://phabricator.haskell.org/D5018 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler