1 files changed, 110 insertions, 0 deletions
diff --git a/testsuite/tests/polykinds/T14270.hs b/testsuite/tests/polykinds/T14270.hs
new file mode 100644
index 0000000000..3eed83c657
--- /dev/null
+++ b/testsuite/tests/polykinds/T14270.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE PolyKinds #-}
+module T14270 (pattern App) where
+
+import Data.Kind (Type)
+import GHC.Fingerprint (Fingerprint, fingerprintFingerprints)
+import GHC.Types (RuntimeRep, TYPE, TyCon)
+
+data (a :: k1) :~~: (b :: k2) where
+  HRefl :: a :~~: a
+
+data TypeRep (a :: k) where
+    TrTyCon :: {-# UNPACK #-} !Fingerprint -> !TyCon -> [SomeTypeRep]
+            -> TypeRep (a :: k)
+
+    TrApp   :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
+               {-# UNPACK #-} !Fingerprint
+            -> TypeRep (a :: k1 -> k2)
+            -> TypeRep (b :: k1)
+            -> TypeRep (a b)
+
+    TrFun   :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
+                      (a :: TYPE r1) (b :: TYPE r2).
+               {-# UNPACK #-} !Fingerprint
+            -> TypeRep a
+            -> TypeRep b
+            -> TypeRep (a -> b)
+
+data SomeTypeRep where
+    SomeTypeRep :: forall k (a :: k). !(TypeRep a) -> SomeTypeRep
+
+typeRepFingerprint :: TypeRep a -> Fingerprint
+typeRepFingerprint = undefined
+
+mkTrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
+           TypeRep (a :: k1 -> k2)
+        -> TypeRep (b :: k1)
+        -> TypeRep (a b)
+mkTrApp rep@(TrApp _ (TrTyCon _ con _) (x :: TypeRep x)) (y :: TypeRep y)
+  | con == funTyCon  -- cheap check first
+  , Just (IsTYPE (rx :: TypeRep rx)) <- isTYPE (typeRepKind x)
+  , Just (IsTYPE (ry :: TypeRep ry)) <- isTYPE (typeRepKind y)
+  , Just HRefl <- withTypeable x $ withTypeable rx $ withTypeable ry
+                  $ typeRep @((->) x :: TYPE ry -> Type) `eqTypeRep` rep
+  = undefined
+mkTrApp a b = TrApp fpr a b
+  where
+    fpr_a = typeRepFingerprint a
+    fpr_b = typeRepFingerprint b
+    fpr   = fingerprintFingerprints [fpr_a, fpr_b]
+
+pattern App :: forall k2 (t :: k2). ()
+            => forall k1 (a :: k1 -> k2) (b :: k1). (t ~ a b)
+            => TypeRep a -> TypeRep b -> TypeRep t
+pattern App f x <- (splitApp -> Just (IsApp f x))
+  where App f x = mkTrApp f x
+
+data IsApp (a :: k) where
+    IsApp :: forall k k' (f :: k' -> k) (x :: k'). ()
+          => TypeRep f -> TypeRep x -> IsApp (f x)
+
+splitApp :: forall k (a :: k). ()
+         => TypeRep a
+         -> Maybe (IsApp a)
+splitApp (TrApp _ f x)     = Just (IsApp f x)
+splitApp rep@(TrFun _ a b) = Just (IsApp (mkTrApp arr a) b)
+  where arr = bareArrow rep
+splitApp (TrTyCon{})       = Nothing
+
+withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r
+withTypeable = undefined
+
+eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
+             TypeRep a -> TypeRep b -> Maybe (a :~~: b)
+eqTypeRep = undefined
+
+typeRepKind :: TypeRep (a :: k) -> TypeRep k
+typeRepKind = undefined
+
+bareArrow :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
+                    (a :: TYPE r1) (b :: TYPE r2). ()
+          => TypeRep (a -> b)
+          -> TypeRep ((->) :: TYPE r1 -> TYPE r2 -> Type)
+bareArrow = undefined
+
+data IsTYPE (a :: Type) where
+    IsTYPE :: forall (r :: RuntimeRep). TypeRep r -> IsTYPE (TYPE r)
+
+isTYPE :: TypeRep (a :: Type) -> Maybe (IsTYPE a)
+isTYPE = undefined
+
+class Typeable (a :: k) where
+
+typeRep :: Typeable a => TypeRep a
+typeRep = undefined
+
+funTyCon :: TyCon
+funTyCon = undefined
+
+instance (Typeable f, Typeable a) => Typeable (f a)
+instance Typeable ((->) :: TYPE r -> TYPE s -> Type)
+instance Typeable TYPE