Do not bind coercion variables in SpecConstr rules

Trac #14270 showed that SpecConstr could cause nasty Lint failures
if it generates a RULE that binds coercion varables.  See

 * Note [SpecConstr and casts], and
 * the test simplCore/should_compile/T14270.

This doesn't feel like the final word to me, because somehow the
specialisation "ought" to work.  So I left in a debug WARN to yell if
the new check acutally fires.

Meanwhile, it stops the erroneous specialisation.

binding coercion

2 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..840b1e8436
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T14270a.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE TypeApplications, ScopedTypeVariables, GADTs, RankNTypes, TypeInType, 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
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index 7f21331cb1..28e26ed317 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -281,3 +281,4 @@ test('T14140',
      ['$MAKE -s --no-print-directory T14140'])
 
 test('T14272', normal, compile, [''])
+test('T14270a', normal, compile, [''])