From 57c11b0d257e399220eb1d42fb4c7e909c07b347 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simon.peytonjones@gmail.com>
Date: Sat, 28 Jan 2023 22:12:35 +0000
Subject: Treat existentials correctly in dubiousDataConInstArgTys

Consider (#22849)

 data T a where
   MkT :: forall k (t::k->*) (ix::k). t ix -> T @k a

Then dubiousDataConInstArgTys MkT [Type, Foo] should return
        [Foo (ix::Type)]
NOT     [Foo (ix::k)]

A bit of an obscure case, but it's an outright bug, and the fix is easy.
---
 compiler/GHC/Core/Opt/WorkWrap/Utils.hs            | 25 +++++++++++++++-------
 testsuite/tests/simplCore/should_compile/T22849.hs | 14 ++++++++++++
 testsuite/tests/simplCore/should_compile/all.T     |  3 ++-
 3 files changed, 33 insertions(+), 9 deletions(-)
 create mode 100644 testsuite/tests/simplCore/should_compile/T22849.hs

diff --git a/compiler/GHC/Core/Opt/WorkWrap/Utils.hs b/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
index f599975355..488eeaf5f4 100644
--- a/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
+++ b/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
@@ -707,7 +707,7 @@ Worker/wrapper will unbox
        * is an algebraic data type (not a newtype)
        * is not recursive (as per 'isRecDataCon')
        * has a single constructor (thus is a "product")
-       * that may bind existentials
+       * that may bind existentials (#18982)
      We can transform
      > data D a = forall b. D a b
      > f (D @ex a b) = e
@@ -1272,16 +1272,25 @@ also unbox its components. That is governed by the `usefulSplit` mechanism.
 -}
 
 -- | Exactly 'dataConInstArgTys', but lacks the (ASSERT'ed) precondition that
--- the 'DataCon' may not have existentials. The lack of cloning the existentials
--- compared to 'dataConInstExAndArgVars' makes this function \"dubious\";
--- only use it where type variables aren't substituted for!
+-- the 'DataCon' may not have existentials. The lack of cloning the
+-- existentials this function \"dubious\"; only use it where type variables
+-- aren't substituted for!  Why may the data con bind existentials?
+--    See Note [Which types are unboxed?]
 dubiousDataConInstArgTys :: DataCon -> [Type] -> [Type]
 dubiousDataConInstArgTys dc tc_args = arg_tys
   where
-    univ_tvs = dataConUnivTyVars dc
-    ex_tvs   = dataConExTyCoVars dc
-    subst    = extendSubstInScopeList (zipTvSubst univ_tvs tc_args) ex_tvs
-    arg_tys  = map (GHC.Core.Type.substTy subst . scaledThing) (dataConRepArgTys dc)
+    univ_tvs        = dataConUnivTyVars dc
+    ex_tvs          = dataConExTyCoVars dc
+    univ_subst      = zipTvSubst univ_tvs tc_args
+    (full_subst, _) = substTyVarBndrs univ_subst ex_tvs
+    arg_tys         = map (substTy full_subst . scaledThing) $
+                      dataConRepArgTys dc
+    -- NB: use substTyVarBndrs on ex_tvs to ensure that we
+    --     substitute in their kinds.  For example (#22849)
+    -- Consider data T a where
+    --            MkT :: forall k (t::k->*) (ix::k). t ix -> T @k a
+    -- Then dubiousDataConInstArgTys MkT [Type, Foo] should return
+    --        [Foo (ix::Type)], not [Foo (ix::k)]!
 
 findTypeShape :: FamInstEnvs -> Type -> TypeShape
 -- Uncover the arrow and product shape of a type
diff --git a/testsuite/tests/simplCore/should_compile/T22849.hs b/testsuite/tests/simplCore/should_compile/T22849.hs
new file mode 100644
index 0000000000..a4c5179251
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T22849.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE GADTs #-}
+
+module T22849 where
+
+data Foo a where
+  Foo :: Foo Int
+
+data Bar a = Bar a (Foo a)
+
+data Some t = forall ix. Some (t ix)
+
+instance Show (Some Bar) where
+  show (Some (Bar v t)) = case t of
+    Foo -> show v
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index 927ac191f6..1a2ac5f7d0 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -453,7 +453,7 @@ test('T22375', normal, compile, ['-O -ddump-simpl -dsuppress-uniques -dno-typeab
 test('T21851_2', [grep_errmsg(r'wwombat') ], multimod_compile, ['T21851_2', '-O -dno-typeable-binds -dsuppress-uniques'])
 # Should not inline m, so there shouldn't be a single YES
 test('T22317', [grep_errmsg(r'ANSWER = YES') ], compile, ['-O -dinline-check m -ddebug-output'])
-
+test('T22849', normal, compile, ['-O'])
 test('T22634', normal, compile, ['-O -fcatch-nonexhaustive-cases'])
 test('T22494', [grep_errmsg(r'case') ], compile, ['-O -ddump-simpl -dsuppress-uniques'])
 test('T22491', normal, compile, ['-O2'])
@@ -472,3 +472,4 @@ test('T22611', [when(wordsize(32), skip), grep_errmsg(r'\$salterF') ], compile,
 test('T22715_2', normal, multimod_compile, ['T22715_2', '-v0 -O -fspecialise-aggressively'])
 test('T22802', normal, compile, ['-O'])
 test('T15205', normal, compile, ['-O -ddump-simpl -dno-typeable-binds -dsuppress-uniques'])
+
-- 
cgit v1.2.1