#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