Expand synonyms in mkCastTy when necessarywip/T19742

Doing so is important to maintain invariants (EQ3) and (EQ4) from
`Note [Respecting definitional equality]` in `GHC.Core.TyCo.Rep`. For the
details, see the new `Note [Using coreView in mk_cast_ty]`.

Fixes #19742.

3 files changed, 72 insertions, 20 deletions

diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 5ed621d404..aed365656a 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -1528,33 +1528,64 @@ splitCastTy_maybe ty
 
 -- | Make a 'CastTy'. The Coercion must be nominal. Checks the
 -- Coercion for reflexivity, dropping it if it's reflexive.
--- See Note [Respecting definitional equality] in "GHC.Core.TyCo.Rep"
+-- See @Note [Respecting definitional equality]@ in "GHC.Core.TyCo.Rep"
 mkCastTy :: Type -> Coercion -> Type
-mkCastTy ty co | isReflexiveCo co = ty  -- (EQ2) from the Note
+mkCastTy orig_ty co | isReflexiveCo co = orig_ty  -- (EQ2) from the Note
 -- NB: Do the slow check here. This is important to keep the splitXXX
 -- functions working properly. Otherwise, we may end up with something
 -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
 -- fails under splitFunTy_maybe. This happened with the cheaper check
 -- in test dependent/should_compile/dynamic-paper.
+mkCastTy orig_ty co = mk_cast_ty orig_ty co
 
-mkCastTy (CastTy ty co1) co2
-  -- (EQ3) from the Note
-  = mkCastTy ty (co1 `mkTransCo` co2)
-      -- call mkCastTy again for the reflexivity check
-
-mkCastTy (ForAllTy (Bndr tv vis) inner_ty) co
-  -- (EQ4) from the Note
-  -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep.
-  | isTyVar tv
-  , let fvs = tyCoVarsOfCo co
-  = -- have to make sure that pushing the co in doesn't capture the bound var!
-    if tv `elemVarSet` fvs
-    then let empty_subst = mkEmptyTCvSubst (mkInScopeSet fvs)
-             (subst, tv') = substVarBndr empty_subst tv
-         in ForAllTy (Bndr tv' vis) (substTy subst inner_ty `mkCastTy` co)
-    else ForAllTy (Bndr tv vis) (inner_ty `mkCastTy` co)
-
-mkCastTy ty co = CastTy ty co
+-- | Like 'mkCastTy', but avoids checking the coercion for reflexivity,
+-- as that can be expensive.
+mk_cast_ty :: Type -> Coercion -> Type
+mk_cast_ty orig_ty co = go orig_ty
+  where
+    go :: Type -> Type
+    -- See Note [Using coreView in mk_cast_ty]
+    go ty | Just ty' <- coreView ty = go ty'
+
+    go (CastTy ty co1)
+      -- (EQ3) from the Note
+      = mkCastTy ty (co1 `mkTransCo` co)
+          -- call mkCastTy again for the reflexivity check
+
+    go (ForAllTy (Bndr tv vis) inner_ty)
+      -- (EQ4) from the Note
+      -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep.
+      | isTyVar tv
+      , let fvs = tyCoVarsOfCo co
+      = -- have to make sure that pushing the co in doesn't capture the bound var!
+        if tv `elemVarSet` fvs
+        then let empty_subst = mkEmptyTCvSubst (mkInScopeSet fvs)
+                 (subst, tv') = substVarBndr empty_subst tv
+             in ForAllTy (Bndr tv' vis) (substTy subst inner_ty `mk_cast_ty` co)
+        else ForAllTy (Bndr tv vis) (inner_ty `mk_cast_ty` co)
+
+    go _ = CastTy orig_ty co -- NB: orig_ty: preserve synonyms if possible
+
+{-
+Note [Using coreView in mk_cast_ty]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Invariants (EQ3) and (EQ4) of Note [Respecting definitional equality] in
+GHC.Core.TyCo.Rep must apply regardless of type synonyms. For instance,
+consider this example (#19742):
+
+   type EqSameNat = () |> co
+   useNatEq :: EqSameNat |> sym co
+
+(Those casts aren't visible in the user-source code, of course; see #19742 for
+what the user might write.)
+
+The type `EqSameNat |> sym co` looks as if it satisfies (EQ3), as it has no
+nested casts, but if we expand EqSameNat, we see that it doesn't.
+And then Bad Things happen.
+
+The solution is easy: just use `coreView` when establishing (EQ3) and (EQ4) in
+`mk_cast_ty`.
+-}
 
 tyConBindersTyCoBinders :: [TyConBinder] -> [TyCoBinder]
 -- Return the tyConBinders in TyCoBinder form
diff --git a/testsuite/tests/typecheck/should_compile/T19742.hs b/testsuite/tests/typecheck/should_compile/T19742.hs
new file mode 100644
index 0000000000..c6489976bd
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T19742.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+module T19742 where
+
+import Data.Kind
+
+type Id :: Type -> Type
+type family Id x where
+  Id x = x
+
+type EqSameNat :: Id Type
+type EqSameNat = ()
+
+useNatEq :: EqSameNat
+useNatEq = ()
+
+decCongS :: ()
+decCongS = case useNatEq of () -> ()
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index b02d64adcc..9b3753848f 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -783,3 +783,4 @@ test('T18467', normal, compile, [''])
 test('T19315', normal, compile, [''])
 
 test('T19535', normal, compile, [''])
+test('T19742', normal, compile, [''])