[GHC] #15346: Core Lint error in GHC 8.6.1: From-type of Cast differs from type of enclosed expression

[GHC]

#15346: Core Lint error in GHC 8.6.1: From-type of Cast differs from type of
enclosed expression
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  merge
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Compile-time      |            Test Case:
  crash or panic                     |  dependent/should_compile/T15346
      Blocked By:                    |             Blocking:
 Related Tickets:  #15419            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Note to Ben: the commit in comment:11 depends on commit
 55a3f8552c9dc9b84e204ec6623c698912795347 (`Refactor coercion rule`), which
 is not present in the GHC 8.6 branch. Moreover, it's a fairly hefty
 commit, so I'm not sure we'd want to backport it, either.

 If you don't want to backport that commit, the following patch should also
 work, without needing `GRefl`. (I've left out the test cases here for the
 sake of brevity.)

 {{{#!diff
 diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
 index 8684c84..11cbd1e 100644
 --- a/compiler/coreSyn/CoreOpt.hs
 +++ b/compiler/coreSyn/CoreOpt.hs
 @@ -979,7 +979,7 @@ pushCoTyArg co ty

    | isForAllTy tyL
    = ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
 -    Just (ty `mkCastTy` mkSymCo co1, MCo co2)
 +    Just (ty `mkCastTy` co1, MCo co2)

    | otherwise
    = Nothing
 @@ -989,8 +989,8 @@ pushCoTyArg co ty
         -- tyL = forall (a1 :: k1). ty1
         -- tyR = forall (a2 :: k2). ty2

 -    co1 = mkNthCo Nominal 0 co
 -       -- co1 :: k1 ~N k2
 +    co1 = mkSymCo (mkNthCo Nominal 0 co)
 +       -- co1 :: k2 ~N k1
         -- Note that NthCo can extract a Nominal equality between the
         -- kinds of the types related by a coercion between forall-types.
         -- See the NthCo case in CoreLint.
 diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
 index 2ca5151..1557ce0 100644
 --- a/compiler/types/Coercion.hs
 +++ b/compiler/types/Coercion.hs
 @@ -1812,7 +1812,7 @@ liftCoSubstVarBndrUsing fun lc@(LC subst cenv)
 old_var
      Pair k1 _    = coercionKind eta
      new_var      = uniqAway (getTCvInScope subst) (setVarType old_var k1)

 -    lifted   = Refl (TyVarTy new_var)
 +    lifted   = mkNomReflCo (TyVarTy new_var) `mkCoherenceRightCo` eta
      new_cenv = extendVarEnv cenv old_var lifted

  -- | Is a var in the domain of a lifting context?
 }}}

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