Fix some casts.
authorBen Gamari <ben@smart-cactus.org>
Tue, 31 Jul 2018 20:44:12 +0000 (16:44 -0400)
committerBen Gamari <ben@smart-cactus.org>
Tue, 31 Jul 2018 20:44:12 +0000 (16:44 -0400)
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}.

compiler/coreSyn/CoreOpt.hs
compiler/types/Coercion.hs

index 0353ab6..5e37fee 100644 (file)
@@ -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.
index 4111516..651e5bf 100644 (file)
@@ -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?