1 files changed, 28 insertions, 0 deletions
diff --git a/testsuite/tests/simplCore/should_compile/T14270a.hs b/testsuite/tests/simplCore/should_compile/T14270a.hs
new file mode 100644
index 0000000000..5054b43a2c
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T14270a.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE TypeApplications, ScopedTypeVariables, GADTs, RankNTypes,
+             PolyKinds, KindSignatures #-}
+{-# OPTIONS_GHC -O2 #-} -- We are provoking a bug in SpecConstr
+
+module T14270a where
+
+import Data.Kind
+import Data.Proxy
+
+data T a = T1 (T a) | T2
+
+data K (a :: k) where
+  K1 :: K (a :: Type)
+  K2 :: K a
+
+f :: T (a :: Type) -> Bool
+f (T1 x) = f x
+f T2     = True
+
+g :: forall (a :: k). K a -> T a -> Bool
+g kv x = case kv of
+            K1 -> f @a T2   -- f @a (T1 x) gives a different crash
+            k2 -> True
+
+-- The point here is that the call to f looks like
+--    f @(a |> co) (T2 @(a |> co))
+-- where 'co' is bound by the pattern match on K1
+-- See Note [SpecConstr and casts] in SpecConstr