Fix #15725 with an extra Sym

Summary:
We were adding a `Sym` to one argument in the `InstCo`
case of `optCoercion` but not another, leading to the two arguments
to misaligned when combined via `Trans`. This fixes the issue with
a well targeted use of `wrapSym`.

Test Plan: make test TEST=T15725

Reviewers: goldfire, ningning, bgamari

Reviewed By: goldfire, ningning

Subscribers: rwbarton, carter

GHC Trac Issues: #15725

Differential Revision: https://phabricator.haskell.org/D5217

3 files changed, 97 insertions, 11 deletions

diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index 8a44b86f7e..1d48ed05b5 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -377,9 +377,9 @@ opt_co4 env sym rep r (InstCo co1 arg)
     -- forall over type...
   | Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1
   = opt_co4_wrap (extendLiftingContext env tv
-                    (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) arg'))
-                   -- kind_co :: k1 ~ k2
-                   -- arg' :: (t1 :: k1) ~ (t2 :: k2)
+                    (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) sym_arg))
+                   -- mkSymCo kind_co :: k1 ~ k2
+                   -- sym_arg :: (t1 :: k1) ~ (t2 :: k2)
                    -- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1)
                  sym rep r co_body
 
@@ -396,23 +396,34 @@ opt_co4 env sym rep r (InstCo co1 arg)
     -- forall over type...
   | Just (tv', kind_co', co_body') <- splitForAllCo_ty_maybe co1'
   = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
-                    (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co') arg'))
+                    (mkCoherenceRightCo Nominal t2' (mkSymCo kind_co') arg'))
             False False r' co_body'
 
     -- forall over coercion...
   | Just (cv', kind_co', co_body') <- splitForAllCo_co_maybe co1'
-  , CoercionTy h1 <- t1
-  , CoercionTy h2 <- t2
-  = let new_co = mk_new_co cv' kind_co' h1 h2
+  , CoercionTy h1' <- t1'
+  , CoercionTy h2' <- t2'
+  = let new_co = mk_new_co cv' kind_co' h1' h2'
     in opt_co4_wrap (extendLiftingContext (zapLiftingContext env) cv' new_co)
                     False False r' co_body'
 
   | otherwise = InstCo co1' arg'
   where
-    co1' = opt_co4_wrap env sym rep r co1
-    r'   = chooseRole rep r
-    arg' = opt_co4_wrap env sym False Nominal arg
-    Pair t1 t2 = coercionKind arg'
+    co1'    = opt_co4_wrap env sym rep r co1
+    r'      = chooseRole rep r
+    arg'    = opt_co4_wrap env sym False Nominal arg
+    sym_arg = wrapSym sym arg'
+
+    -- Performance note: don't be alarmed by the two calls to coercionKind
+    -- here, as only one call to coercionKind is actually demanded per guard.
+    -- t1/t2 are used when checking if co1 is a forall, and t1'/t2' are used
+    -- when checking if co1' (i.e., co1 post-optimization) is a forall.
+    --
+    -- t1/t2 must come from sym_arg, not arg', since it's possible that arg'
+    -- might have an extra Sym at the front (after being optimized) that co1
+    -- lacks, so we need to use sym_arg to balance the number of Syms. (#15725)
+    Pair t1  t2  = coercionKind sym_arg
+    Pair t1' t2' = coercionKind arg'
 
     mk_new_co cv kind_co h1 h2
       = let -- h1 :: (t1 ~ t2)
diff --git a/testsuite/tests/dependent/should_compile/T15725.hs b/testsuite/tests/dependent/should_compile/T15725.hs
new file mode 100644
index 0000000000..a5f259ea9e
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15725.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T15725 where
+
+import Data.Functor.Identity (Identity(..))
+import Data.Kind (Type)
+import GHC.Exts (Any)
+
+-----
+-- The important bits
+-----
+
+type instance Meth (x :: Identity a) = GenericMeth x
+instance SC Identity
+
+-------------------------------------------------------------------------------
+
+data family Sing :: forall k. k -> Type
+data instance Sing :: forall a. Identity a -> Type where
+  SIdentity :: Sing x -> Sing ('Identity x)
+
+newtype Par1 p = Par1 p
+data instance Sing :: forall p. Par1 p -> Type where
+  SPar1 :: Sing x -> Sing ('Par1 x)
+
+type family Rep1 (f :: Type -> Type) :: Type -> Type
+
+class PGeneric1 (f :: Type -> Type) where
+  type From1 (z :: f a)      :: Rep1 f a
+  type To1   (z :: Rep1 f a) :: f a
+
+class SGeneric1 (f :: Type -> Type) where
+  sFrom1 :: forall (a :: Type) (z :: f a).      Sing z -> Sing (From1 z)
+  sTo1   :: forall (a :: Type) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)
+
+type instance Rep1 Identity = Par1
+
+instance PGeneric1 Identity where
+  type From1 ('Identity x) = 'Par1 x
+  type To1   ('Par1 x)     = 'Identity x
+
+instance SGeneric1 Identity where
+  sFrom1 (SIdentity x) = SPar1 x
+  sTo1 (SPar1 x) = SIdentity x
+
+type family GenericMeth (x :: f a) :: f a where
+  GenericMeth x = To1 (Meth (From1 x))
+
+type family Meth (x :: f a) :: f a
+
+class SC f where
+  sMeth         :: forall a (x :: f a).
+                   Sing x -> Sing (Meth x)
+  default sMeth :: forall a (x :: f a).
+                   ( SGeneric1 f, SC (Rep1 f)
+                   , Meth x ~ GenericMeth x
+                   )
+                => Sing x -> Sing (Meth x)
+  sMeth sx = sTo1 (sMeth (sFrom1 sx))
+
+  dummy :: f a -> ()
+  dummy _ = ()
+
+type instance Meth (x :: Par1 p) = x
+instance SC Par1 where
+  sMeth x = x
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 5f6e901dcf..1bf6cc7142 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -55,3 +55,4 @@ test('T15346', normal, compile, [''])
 test('T15419', normal, compile, [''])
 test('T14066h', normal, compile, [''])
 test('T15666', normal, compile, [''])
+test('T15725', normal, compile, [''])