T14270.hs 3.45 KB
Newer Older
1 2 3 4 5 6 7 8 9
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
10
{-# LANGUAGE PolyKinds #-}
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78
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
79
withTypeable _ _ = undefined
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110

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