{-# LANGUAGE TypeInType #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
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