Fix flattening of FunTy

3 files changed, 25 insertions, 18 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 9d2acfc9f7..bc6458c988 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1868,9 +1868,9 @@ canEqTyVar ev eq_rel swapped tv1 ps_xi1 xi2 ps_xi2
                               , text "~"
                               , parens (ppr xi2 <+> dcolon <+> ppr k2) ]
                         , ppr flat_k1
-                        , ppr k1_co
+                        , ppr k1_co <+> dcolon <+> ppr (coercionKind k1_co)
                         , ppr flat_k2
-                        , ppr k2_co ])
+                        , ppr k2_co <+> dcolon <+> ppr (coercionKind k2_co)])
 
          -- We know the LHS is a tyvar. So let's dump all the coercions on the RHS
          -- If flat_k1 == flat_k2, let's dump all the coercions on the RHS and
@@ -1892,6 +1892,15 @@ canEqTyVar ev eq_rel swapped tv1 ps_xi1 xi2 ps_xi2
                                                (mkTcReflCo role xi1) rhs_co
                        -- NB: rewriteEqEvidence executes a swap, if any, so we're
                        -- NotSwapped now.
+
+                 ; traceTcS "canEqTyVar2"
+                      (vcat [ text "rhs_kind_co" <+> ppr rhs_kind_co <+>
+                                 dcolon <+> ppr (coercionKind rhs_kind_co)
+                            , text "new_rhs" <+> ppr new_rhs
+                            , text "ps_rhs" <+> ppr ps_rhs
+                            , text "rhs_co" <+> ppr rhs_co
+                            , text "new_ev" <+> ppr new_ev ])
+
                  ; canEqTyVarHomo new_ev eq_rel NotSwapped tv1 ps_xi1 new_rhs ps_rhs }
          else
     do { let sym_k1_co = mkTcSymCo k1_co  -- :: kind(xi1) ~N flat_k1
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index fe5d44827b..ec84528996 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -1179,27 +1179,26 @@ flatten_one ty@(FunTy _ ty1 ty2)
        ; role <- getRole
        ; let sym_kco1 = mkTcSymCo kco1
              sym_kco2 = mkTcSymCo kco2
-             co1' = co1 `mkTcTransCo` mkGReflRightCo role xi1 sym_kco1
-       ; let co2' = co2 `mkTcTransCo` mkGReflRightCo role xi2 sym_kco2
+             co1' = mkGReflLeftCo role xi1 sym_kco1 `mkTcTransCo` co1
+             co2' = mkGReflLeftCo role xi2 sym_kco2 `mkTcTransCo` co2
        ; return (ty { ft_arg = xi1 `mkTcCastTy` sym_kco1
                     , ft_res = xi2 `mkTcCastTy` sym_kco2 }
-                , mkSymCo (mkFunCo role co1' co2')) }
+                , mkFunCo role co1' co2') }
   -- This is a specialised version of the cleverness in flatten_ty_con_app
+  -- It's as if we had (->) @r1 @r2 t1 t2.  We flatten r1 and r2, so we must
+  -- ensure that the flattened versions of t1, t2 have those flattened kinds
+  --
   -- Input: (ty1 -> ty2)
   -- co1 :: xi1 ~ ty1
   -- co2 :: xi2 ~ ty2
-  -- kco1 :: kxi1 ~ kind(xi1)
-  -- kco2 :: kxi2 ~ kind(xi2)
+  -- kco1 :: flat_kxi1 ~ kind(xi1)
+  -- kco2 :: flat_kxi2 ~ kind(xi2)
   -- res_ty = (xi1 |> sym kco1) -> (xi2 |> sym kco2)
-  -- res_co :: ty ~ res_ty = mkFunCo co1' co2'
-  -- co1' :: ty1 ~ (xi1 |> sym kco1)
-  --      = co1 ; grefl1
-  -- grefl1 :: xi1 ~ (xi1 |> sym kco1)
-  --        =  Grefl xi1 (MCo kco1)
-  -- co2' :: ty2 ~ (xi2 |> sym kco2)
-  -- grefl2 :: xi2 ~ (xi1 |> sym kco2)
-  --        =  Grefl xi2 (MCo kco2)
-  -- Result: (res_ty, sym res_co)
+  -- res_co :: res_ty ~ ty             = mkFunCo co1' co2'
+  -- co1'   :: (xi1 |> sym kco1) ~ ty1 = gr1 ; co1
+  -- gr1    :: (xi1 |> sym kco1) ~ xi1 = mkGReflLeft xi (sym kco1)
+  -- co2'   :: (xi2 |> sym kco2) ~ ty2 = gr2 ; co2
+  -- gr2    :: (xi2 |> sym kco2) ~ xi2 = mkGReflLeft xi (sym kco2)
 
 flatten_one ty@(ForAllTy {})
 -- TODO (RAE): This is inadequate, as it doesn't flatten the kind of
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 8cb7257229..d9d5603bcf 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1360,8 +1360,7 @@ Specifically
 -- Some very important subtleties here: see Note [mkCastTy subtleties]
 mkCastTy :: Type -> Coercion -> Type
 mkCastTy ty co
-  | let co_res_kind = pSnd (coercionKind co)
-  , typeKind ty `eqType` co_res_kind     -- (EQ2) from the Note
+  | typeKind ty `eqType` coercionRKind co     -- (EQ2) from the Note
     -- Not isReflexiveCo!  See Note [mkCastTy subtleties]
   = ty