[commit: ghc] ghc-8.6: Fix some casts. (06c29dd)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : ghc-8.6
Link       : http://ghc.haskell.org/trac/ghc/changeset/06c29ddc113e5225ebc0aa37a81d9d1cf0b7f15a/ghc

>---------------------------------------------------------------

commit 06c29ddc113e5225ebc0aa37a81d9d1cf0b7f15a
Author: Ben Gamari <ben at smart-cactus.org>
Date:   Tue Jul 31 16:44:12 2018 -0400

    Fix some casts.
    
    This fixes #15346, and is a team effort between Ryan Scott and
    myself (mostly Ryan). We discovered two errors related to FC's
    "push" rules, one in the TPush rule (as implemented in pushCoTyArg)
    and one in KPush rule (it shows up in liftCoSubstVarBndr).
    
    The solution: do what the paper says, instead of whatever random
    thoughts popped into my head as I was actually implementing.
    
    Note that this is a backport of the fix merged to master,
    af624071fa063158d6e963e171280676f9c0a0b0.
    
    Also fixes #15419, which is actually the same underlying problem.
    
    Test case: dependent/should_compile/T{15346,15419}.


>---------------------------------------------------------------

06c29ddc113e5225ebc0aa37a81d9d1cf0b7f15a
 compiler/coreSyn/CoreOpt.hs | 6 +++---
 compiler/types/Coercion.hs  | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
index 0353ab6..5e37fee 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 4111516..651e5bf 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -1732,7 +1732,7 @@ liftCoSubstVarBndrUsing fun lc@(LC subst cenv) old_var
     Pair k1 _    = coercionKind eta
     new_var      = uniqAway (getTCvInScope subst) (setVarType old_var k1)
 
-    lifted   = Refl Nominal (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?