wiki:Typeable/BenGamari

A plan for type-indexed type representations

This is Ben Gamari's plan for moving ahead with the type-indexed Typeable scheme, described most recently in A reflection on types.

Status

A branch with the current state of things can be found here. There is also an intermittently-updated Phabricator differential, Phab:D2010. It's still rather preliminary however it does give you a working stage2 compiler with functional type-indexed type representations and what I believe is a pretty reasonable set of interfaces, described below.

There are a number of tasks outstanding. These involve only Ben,

  • The representation of tycon kinds needs work
  • Fix representation pretty-printer to correctly handle tuples, lists, arrows, and precedence
  • Examine performance changes (even some improvements, perplexingly)
  • Look at testsuite failures involving stack overflows: T10294, plugins01, T5550, annrun01, ann01, annth_make
  • Evaluate whether we want to try harder to preserve the re-exports that have been dropped from Data.Dynamic.
  • Some of the new naming choices should be revisited (e.g. TRFun)
  • Typeable fingerprints need to be made more robust (#7897)
  • When, if at all, should the Show instance produce kind signatures?
    • Should show (typeRep @Int) produce Int or Int :: *?
    • Should show (typeRep @(Proxy Int#) produce Proxy or Proxy :: *?
    • Should show (typeRep @(Proxy :: # -> *) produce Proxy or Proxy :: # -> *?
  • Performance:
    • Carefully check Data.Typeable for deviations from the previous interface and fill in gaps where possible
    • Examine whether the primitive TypeReps (e.g. trTYPE, trArrow) should be INLINEABLE; we perform a number of runtime checks during serialization/deserialization so being able to inline these fingerprints may be helpful.
    • Perhaps generated TyCons should also be inlined (or generate rules to inline just fingerprints)
    • Perhaps it would be worth offering unsafe deserialization interface without runtime checks?

These are issues that need to be addressed elsewhere in the compiler,

  • #11736: Core Lint rejects unsaturated applications of unlifted types; it's not clear whether this is actually a safe thing to do
  • #11714: kind of (->) is overly-restrictive consequently T11120 testcase fails
  • #11722: need a representation for unboxed types; closely related to #11736
  • #11715: TypeOf fails due to the fact that Constraint and * are indistinguishable in Core
  • #12670: RuntimeRep polymorphism check is too strict (needed to implement TrFun described below)

Immediate next steps

  • Fix #11714
  • Move things to a richer TypeRep representation to make user serialization implementations safer.

Representing tycon kinds

In order to provide typeRepKind we must have some way of getting a kind from a TrTyCon TypeRep node. There are two ways of doing this,

  1. Making the TrTyCon carry its kind
  2. Making the TrTyCon carry the instantiations of its kind variables and ensuring that we have a way of conjuring the final kind from these variables (e.g. encoding a representation of the type's uninstantiated kind in its TyCon)

In many ways (1) is easier but has a few unfortunate disadvantages,

  • several types has recursive kind relationships (e.g. Type :: Type)
  • it increases the size of all TypeReps to allow for the rather uncommon case of kind polymorphism

On the other hand, (2) lacks these disadvantages but presents a few challenges,

  • TyCons become much larger, potentially blowing up compilation time for modules not using Typeable
  • TyCons need to refer to TypeRep dictionaries, potentially complicating evidence generation

The need for kind representations

While typeRepKind may seem like a non-essential feature, it ends up being quite important in the presence of representationally polymorphic arrow lest we may produce ill-kinded type representations. Consider, for a moment, that we have a function, mkApp, which attempts to construct an application type from two SomeTypeReps. It might look like,

mkApp :: SomeTypeRep -> SomeTypeRep -> Maybe SomeTypeRep
mkApp (SomeTypeRep f) (SomeTypeRep x) = do
    FunTy a b <- pure f
    Refl <- a `eqTypeRep` typeRepKind x
    return (App f x)

Note that before we can apply x to f we must prove to GHC that the kind of x is compatible with that expected by f. I haven't proven to myself that omitting this check will result in unsafety, but I'm fairly confident that someone with enough time to read through #9858 would be able to find a way.

Encoding kind instantiations

One approach would be,

type KindBndr = Int
data KindRep = KindTyCon TyCon
             | KindVar !KindBndr
             | KindApp KindRep KindRep

data TyCon = TyCon { tyConName :: String, ...
                   , tyConKindRep :: KindRep
                   }
data TypeRep (a :: k) where
  TrCon :: TyCon -> [SomeTypeRep] -> TypeRep a
  TrApp :: TypeRep a -> TypeRep b -> TypeRep (a b)

data SomeTypeRep where
    SomeTypeRep :: forall k (a :: k). TypeRep a -> SomeTypeRep

However this has the unfortunate side-effect of making the production of TyCons (and hence all data types) significantly more expensive due to the need to produce KindRep.

An alternative to this would be to push the KindRep out of TyCon and into evidence generation,

type KindBndr = Int
data KindRep = KindTyCon TyCon
             | KindVar !KindBndr
             | KindApp KindRep KindRep

data TyCon = TyCon { tyConName :: String, ...
                   }

data TypeRep (a :: k) where
  TrCon :: TyCon -> KindRep -> [SomeTypeRep] -> TypeRep a
  TrApp :: TypeRep a -> TypeRep b -> TypeRep (a b)

data SomeTypeRep where
    SomeTypeRep :: forall k (a :: k). TypeRep a -> SomeTypeRep

This has the advantage of only inflicting the cost of KindRep generation on users of Typeable. However, this means we lose sharing of KindReps.

Another alternative would be to drop KindRep entirely and instead capture kinds through constraints,

data TyCon = TyCon { tyConName :: String, ...
                   }

data TypeRep (a :: k) where
  TrCon :: TyCon -> [SomeTypeRep] -> TypeRep a
  TrApp :: TypeRep a -> TypeRep b -> TypeRep (a b)

class Typeable k => Typeable (a :: k) where
  typeRep :: TypeRep a

-- Which has slight consequences on withTypeable,
withTypeable :: Typeable k => TypeRep (a :: k) -> (Typeable a => r) -> r

-- and SomeTypeRep
data SomeTypeRep where
    SomeTypeRep :: forall k (a :: k). Typeable k => TypeRep a -> SomeTypeRep

Notes from meeting with Simon (5 Oct. 2016)

Next step,

  1. Introduce special case in TypeRep for functions (TrFun)
  2. Encode instantiated kind variables in TrTyCon instead of full kind
  3. GHC: Try failing in splitTyConApp when splitting (->) application that has unlifted kind
  4. Introduce FunCo coercion
  5. Generalize (->) kind

Encoding instantiated kind variables

Instead of encoding the kind of a constructor in TrTyCon let's encode its instantiated kind variables. This has two advantages,

  1. It's more concise: most tycons are not kind polymorphic
  2. It's easier: we avoid having to represent kind loops

This slightly complicates the implementation of typeRepKind, however. We will need some way of moving from the list of kind variable instantiations to the resulting kind of a tycon. This will need to be encoded with the TyCon in a manner than can serialized. For instance,

data TyCon = Tc String [String] TyConKindRep
data TyConKindRep = Var String | TyConApp TyCon [TyConKindRep]

This unfortunately bloats the TyCon bindings produced by the compiler with every datatype.

Tickets

Use Keyword = Typeable to ensure that a ticket ends up on these lists.

Open Tickets:

#10770
Typeable solver has strange effects
#11251
isInstance does not work on Typeable with base-4.8 anymore
#11349
[TypeApplications] Create Proxy-free alternatives of functions in base
#11715
Constraint vs *
#12451
TemplateHaskell and Data.Typeable - tcIfaceGlobal (local): not found
#13261
Consider moving Typeable evidence generation wholly back to solver
#13276
Unboxed sums are not Typeable
#13647
Tidy up TcTypeable
#13933
Support Typeable instances for types with coercions
#14190
Typeable imposes seemingly redundant constraints on polykinded instances
#14255
Type-indexed type fingerprints
#14270
GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal
#14337
typeRepKind can perform substantial amounts of allocation
#14341
Show instance for TypeReps is a bit broken
#14401
Add a test ensuring that TypeReps can be stored in compact regions
#14480
Clean up tyConTYPE
#14582
Review and improve the Typeable API
#14663
Deriving Typeable for enumerations seems expensive
#15322
`KnownNat` does not imply `Typeable` any more when used with plugin
#15862
Panic with promoted types that Typeable doesn't support

Closed Tickets:

#3480
Easily make Typeable keys pure, so that Typeable can be handled efficiently across communications
#8931
The type defaulting in GHCi with Typeable
#9639
Remove OldTypeable
#9707
(Try to) restructure `base` to allow more use of `AutoDeriveTypeable`
#10163
Export typeRepKinds in Data.Typeable
#10343
Make Typeable track kind information better
#11011
Add type-indexed type representations (`TypeRep a`)
#11120
Missing type representations
#11714
Kind of (->) type constructor is overly constrained
#11722
No TypeRep for unboxed tuples
#11736
Allow unsaturated uses of unlifted types in Core
#12082
Typeable on RealWorld fails
#12123
GHC crashes when calling typeRep on a promoted tuple
#12409
Unboxed tuples have no type representations
#12670
Representation polymorphism validity check is too strict
#12905
Core lint failure with pattern synonym and levity polymorphism
#13197
Perplexing levity polymorphism issue
#13333
Typeable regression in GHC HEAD
#13871
GHC panic in 8.2 only: typeIsTypeable(Coercion)
#13872
Strange Typeable error message involving TypeInType
#13915
GHC 8.2 regression: "Can't find interface-file declaration" for promoted data family instance
#14199
Document Type.Reflection better (Fun and Con')
#14254
The Binary instance for TypeRep smells a bit expensive
#14925
Non-ASCII type names get garbled when their `TypeRep` is shown
#15067
When Typeable and unboxed sums collide, GHC panics

Type.Reflection

The new type-indexed typeable machinery will be exposed via a new module (Type.Reflection is chosen here, although this name is still up in the air; Reflection in particular has an unfortunate conflict with Edward Kmett's reflection library). The user-visible interface of Type.Reflection will look like this,

-- The user-facing interface
module Type.Reflection where

class Typeable (a :: k)

-- This is how we get the representation for a type
typeRep :: forall (a :: k). Typeable a => TypeRep a 

-- This is merely a record of some metadata about a type constructor.
-- One of these is produced for every type defined in a module during its
-- compilation.
--
-- This should also carry a fingerprint; to address #7897 this fingerprint
-- should hash not only the name of the tycon, but also the structure of its
-- data constructors
data TyCon

tyConPackage :: TyCon -> String
tyConModule :: TyCon -> String
tyConName :: TyCon -> String

-- A runtime type representation with O(1) access to a fingerprint.
data TypeRep (a :: k)

instance Show (TypeRep a)

-- Since TypeRep is indexed by its type and must be a singleton we can trivially
-- provide these
instance Eq (TypeRep a)  where (==) _ _    = True
instance Ord (TypeRep a) where compare _ _ = EQ

-- While TypeRep is abstract, we can pattern match against it.
-- This can be a bi-directional pattern (using mkTrApp for construction).
pattern TRApp :: forall k2 (fun :: k2). ()
              => forall k1 (a :: k1 -> k2) (b :: k1). (fun ~ a b)
              => TypeRep a -> TypeRep b -> TypeRep fun

-- Open question: Should this pattern include the kind of the constructor?
-- In practice you often need it when you need the TyCon
pattern TRCon :: forall k (a :: k). TyCon -> TypeRep a

-- Decompose functions, also bidirectional
pattern TRFun :: forall fun. ()
              => forall arg res. (fun ~ (arg -> res))
              => TypeRep arg
              -> TypeRep res
              -> TypeRep fun

-- We can also request the kind of a type
typeRepKind :: TypeRep (a :: k) -> TypeRep k

-- and compare types
eqTypeRep  :: forall k (a :: k) (b :: k).
              TypeRep a -> TypeRep b -> Maybe (a :~: b)
eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2).
              TypeRep a -> TypeRep b -> Maybe (a :~~: b)

-- it can also be useful to quantify over the type such that we can, e.g.,
-- index a map on a type
data TypeRepX where
    TypeRepX :: forall a. TypeRep a -> TypeRepX

-- these have some useful instances
instance Eq TypeRepX
instance Ord TypeRepX
instance Show TypeRepX

-- A `TypeRep a` gives rise to a `Typeable a` instance without loss of
-- confluence.
withTypeable :: TypeRep a -> (Typeable a => b) -> b
withTypeable = undefined

-- We can also allow the user to build up his own applications
mkTrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
           TypeRep (a :: k1 -> k2)
        -> TypeRep (b :: k1)
        -> TypeRep (a b)

-- However, we can't (easily) allow instantiation of TyCons since we have
-- no way of producing the kind of the resulting type...
--mkTrCon :: forall k (a :: k). TyCon -> [TypeRepX] -> TypeRep a

Preserving compatibility with Data.Typeable

Note how above we placed the new type-indexed Typeable machinery in an entirely new module. The goal of this is to preserve compatibility with the old Data.Typeable. Notice how the old Data.Typeable.TypeRep is essentially TypeRepX under the new scheme. This gives us a very nice compatibility story (thanks due to Richard Eisenberg for first proposing this),

module Data.Typeable
    ( -- We can use the same Typeable class
      I.Typeable
    , I.TyCon
    , I.tyConPackage
    , I.tyConModule
    , I.tyConName
    , (:~:)(Refl)
    , module Data.Typeable
    ) where

import Type.Reflection as I
import Data.Type.Equality

-- Merely expose TypeRepX opaquely under the old name
type TypeRep = I.TypeRepX

typeOf :: forall a. Typeable a => a -> TypeRep
typeOf _ = I.typeRepX (Proxy :: Proxy a)

typeRep :: forall proxy a. Typeable a => proxy a -> TypeRep
typeRep = I.typeRepX

cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast x
  | Just HRefl <- ta `I.eqTypeRep` tb = Just x
  | otherwise                         = Nothing
  where
    ta = I.typeRep :: I.TypeRep a
    tb = I.typeRep :: I.TypeRep b

eqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT
  | Just HRefl <- ta `I.eqTypeRep` tb = Just Refl
  | otherwise                         = Nothing
  where
    ta = I.typeRep :: I.TypeRep a
    tb = I.typeRep :: I.TypeRep b

funResultTy :: TypeRep -> TypeRep -> Maybe TypeRep
funResultTy (I.TypeRepX f) (I.TypeRepX x)
  | Just HRefl <- (I.typeRep :: I.TypeRep Type) `I.eqTypeRep` I.typeRepKind f
  , I.TRFun arg res <- f
  , Just HRefl <- arg `I.eqTypeRep` x
  = Just (I.TypeRepX res)
  | otherwise
  = Nothing

typeRepTyCon :: TypeRep -> TyCon

-- the old typeOfN exports from the pre-PolyKinds days can
-- also be trivially provided.

The representation serialization problem

Serialization of type representations is a bit tricky in this new world. Let's say that we want to serialize (say, using the binary package), for instance, a type-indexed map,

data TMap a
lookup :: TypeRepX -> TMap a -> Maybe a
insert :: TypeRepX -> a -> TMap a -> TMap a

-- we want to support these operations...
getTMap :: Binary a => Get (TMap a)
putTMap :: Binary a => TMap a -> Put

This is the sort of usage we might see in, for instance, the Shake build system.

Serializing TypeRep

Of course in order to provide getTMap and putTMap we need to be able to both serialize and deserialize TypeRepXs. Serialization poses no particular issue. For instance, we might write,

instance Binary TyCon

putTypeRep :: TypeRep a -> Put
putTypeRep tr@(TRCon tc) = do put 0
                              put tc
                              putTypeRep (typeRepKind tr) 
putTypeRep (TRApp f x)   = do put 1
                              putTypeRep f
                              putTypeRep x

putTypeRepX :: TypeRepX -> Put
putTypeRepX (TypeRepX rep) = putTypeRep rep

That was easy.

Now let's try deserialization.

Deserialization

First, we need to define how deserialization should behave. For instance, defining

getTypeRep :: Get (TypeRep a)

is a non-starter as we have no way to verify that the representation that we deserialize plausibly represents the type a that the user requests.

Instead, let's first consider TypeRepX (thanks to Adam Gundry for his guidance),

getTypeRepX :: Get TypeRepX
getTypeRepX = do
    tag <- get :: Get Word8
    case tag of
        0 -> do con <- get :: Get TyCon
                TypeRepX rep_k <- getTypeRepX
                case rep_k `eqTypeRep` (typeRep :: TypeRep Type) of
                    Just HRefl -> pure $ TypeRepX $ mkTrCon con rep_k
                    Nothing    -> fail "getTypeRepX: Kind mismatch"

        1 -> do TypeRepX f <- getTypeRepX
                TypeRepX x <- getTypeRepX
                case typeRepKind f of
                    TRFun arg _ | Just HRefl <- arg `eqTypeRep` x ->
                      pure $ TypeRepX $ mkTrApp f x
                    _ -> fail "getTypeRepX: Kind mismatch"
        _ -> fail "getTypeRepX: Invalid TypeRepX"

Note how we need to invoke type equality here to ensure,

  • in the case of a tycon: that the tycon's kind is Type (as all kinds must be in the TypeInType scheme)
  • in the case of applications f x:
    • that the type f is indeed an arrow
    • that the type f is applied at the type x that it expects

Given this we can easily implement TypeRep a given a representation of the expected a,

getTypeRep :: Typeable a => Get (TypeRep a)
getTypeRep = do
   TypeRepX rep <- getTypeRepX
   case rep `eqTypeRep` (typeRep :: TypeRep a) of
       Just HRefl -> pure rep
       Nothing    -> fail "Binary: Type mismatch"

Alternative: Through static data?

One might have the idea that the solution here may be to avoid encoding representations at all: instead use GHC's existing support for static data, e.g. add TypeRep a entries to the static pointer table for every known type. One will quickly realize, however, that this is unrealistic: we have no way of enumerating the types that must be considered and even if we did, there would be very many of them.

Alternative: Type-indexed TyCons?

Under the above proposal TyCon is merely a record of static metadata; it has no type information and consequently the user is quite limited in what they can do with it. Another point in the design space would be to add a type index to TyCon,

-- metadata describing a tycon
data TyConMeta = TyConMeta { tyConPackage :: String
                           , tyConModule  :: String
                           , tyConName    :: String
                           }
newtype TyCon (a :: k) = TyCon TyConMeta

pattern TRCon :: TyCon a -> TypeRep a

-- which allows us to provide
mkTyCon :: TyCon a -> TypeRep a

While this is something that we could do, I have yet to see a compelling reason why we should do it. The only way you can produce a TyCon is from a TypeRep, so ultimately you should be able to accomplish everything you can with type-index TyCons by just not destructuring the TypeRep from which it arose.

Data.Dynamic

Dynamic doesn't really change,

module Data.Dynamic where

-- Dynamic itself no longer needs to be abstract
data Dynamic where
    Dynamic :: TypeRep a -> a -> Dynamic

-- Construction
toDynR :: TypeRep a -> a -> Dynamic
toDyn  :: Typeable a => a -> Dynamic

-- Elimination
fromDynamicR :: TypeRep a -> Dynamic -> Maybe a
fromDynamic  :: Typeable a => Dynamic -> Maybe a

-- 
fromDynR :: TypeRep a -> Dynamic -> a -> a
fromDyn  :: Typeable a => Dynamic -> a -> a

-- Application
dynApp   :: Dynamic -> Dynamic -> Dynamic  -- Existing function; calls error on failure
                                           -- I think this should be deprecated
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic

Ben Pierce also suggested this variant of Dynamic, which models a value of dynamic type "inside" of a known functor. He p

data SDynamic s where
    SDynamic :: TypeRep a -> s a -> SDynamic s

toSDynR :: TypeRep a -> s a -> SDynamic s
toSDyn :: Typeable a => s a -> SDynamic s
fromSDynamicR :: TypeRep a -> SDynamic s -> Maybe (s a)
fromSDynamic :: Typeable a => SDynamic s -> Maybe (s a)
fromSDynR :: TypeRep a -> SDynamic s -> s a -> s a
fromSDyn :: Typeable a => SDynamic s -> s a -> s a

Implementation notes

The implementation of the above plan shares a great deal with the previous Typeable implementation. As we did before, we split the generation of Typeable representations into two halves,

  1. At time of type definition: When compiling a type definition we emit a TyCon binding describing its type constructor
  1. When solving for a Typeable constraint: We produce a dictionary referring to TyCon binding associated with the type for which Typeable is needed.

Step (1) is essentially unchanged from the previous implementation. There's nothing particularly interesting here other than some tiresome details regarding generating representations for primitive types, which doesn't really change (see Note [The Grand Typeable Story] in TcTypeable for details).

Step (2), however, changes slightly in that it needs to produce evidence for the kind of type.

Typeable evidence is merely a TypeRep,

data TypeRep (a :: k) where
    TrTyCon :: !Fingerprint -> !TyCon -> TypeRep k -> TypeRep (a :: k)

    TrApp   :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
               !Fingerprint
            -> TypeRep a
            -> TypeRep b
            -> TypeRep (a b)

Note that a Fingerprint is included in each node for O(1) comparison.

Dealing with recursive kinds

The fact that we now have the ability to reflect on kinds poses an interesting challenge (especially in the TypeInType world) as we now have to worry about recursive kind relationships during evidence generation. Thankfully there are only a few types which we need to worry about,

TYPE               :: RuntimeRep -> TYPE 'PtrRepLifted
RuntimeRep         :: TYPE 'PtrRepLifted
'PtrRepLifted      :: RuntimeRep
(->)               :: TYPE 'PtrRepLifted -> TYPE 'PtrRepLifted -> Type 'PtrRepLifted
TYPE 'PtrRepLifted :: TYPE 'PtrRepLifted

While in principle we could generate knot-tied dictionaries for these in the typechecker, this would be quite tiresome; moreover these types are ubiquitous and it would be wasteful to replicate representations for them. Instead, the implementation manually defines representations for these types in Data.Typeable.Internal and using these definitions instead of generated bindings.

Alternative: Richer TypeRep

Another approach would be to to encode these special cases in the TypeRep type itself

data TypeRep (a :: k) where
    TrTyCon :: !Fingerprint -> !TyCon -> TypeRep k -> TypeRep (a :: k)

    TrApp   :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
               !Fingerprint
            -> TypeRep a
            -> TypeRep b
            -> TypeRep (a b)

    TrArrow :: forall k1 k2.
               !Fingerprint
            -> TypeRep k1
            -> TypeRep k2
            -> TypeRep ((->) :: k1 -> k2 -> *)

    TrTYPE  :: TypeRep TYPE
    TrType  :: TypeRep (TYPE 'PtrRepLifted)

    TrRuntimeRep    :: TypeRep RuntimeRep
    Tr'PtrRepLifted :: TypeRep 'PtrRepLifted

(although TrArrow won't quite work yet due to #11714)

With this we can easily write typeRepKind,

typeRepKind :: forall k (a :: k). TypeRep a -> TypeRep k
-- these cases are unchanged...
typeRepKind (TrTyCon _ _ k) = k
typeRepKind (TrApp _ f _)   = case typeRepKind f of TRFun _arg res -> res

-- these are new...
typeRepKind (TrArrow x y)   = mkTrApp (mkTrApp (TrArrow TrType TrType) x) y
typeRepKind TrTYPE          = mkTrApp TrRuntimeRep TrType
typeRepKind TrType          = TrType
typeRepKind TrRuntimeRep    = TrType
typeRepKind Tr'PtrRepLifted = TrRuntimeRep

Although providing pattern synonyms to allow decomposition of, e.g., TYPE 'PtrTypeLifted becomes a bit trickier,

-- Just as above, we can decompose applications but we
-- now need to define it in terms of the splitApp helper,
pattern TRApp :: forall k2 (t :: k2). ()
              => forall k1 (a :: k1 -> k2) (b :: k1). (t ~ a b)
              => TypeRep a -> TypeRep b -> TypeRep t
pattern TRApp x y = (splitApp -> Just (App x y))

data AppResult (t :: k) where
    App :: TypeRep a -> TypeRep b -> AppResult (a b)

splitApp :: TypeRep a -> Maybe (AppResult a)
splitApp (TrTyCon _ _ _) = Nothing
splitApp (TrApp _ f x)   = Just $ App f x
splitApp (TrArrow _ x y) = Just $ App (mkTrApp (TrArrow (typeRepKind x) (typeRepKind y)) x) y
splitApp TrTYPE          = Nothing
splitApp TrType          = Just $ App TrTYPE Tr'PtrRepLifted
splitApp TrRuntimeRep    = Nothing
splitApp Tr'PtrRepLifted = Nothing

Pretty much everything else follows from this. For instance TRFun,

pattern TRFun :: forall fun. ()
              => forall arg res. (fun ~ (arg -> res))
              => TypeRep arg
              -> TypeRep res
              -> TypeRep fun
pattern TRFun arg res <- TRApp _ (TRApp _ (TrArrow _ _) arg) res where
    TRFun arg res = mkTrApp (mkTrApp trArrow arg) res

This approach trades some user-code complexity for a more complex representation type. I'm not yet certain whether it would be an improvement over the current state of affairs. It has the disadvantage that the implementation needs to take care to normalize representations that it builds (e.g. prefer TrType to TrApp TrTYPE Tr'PtrRepLifted). That being said, it may be a bit more efficient for the compiler to produce dictionaries in this form.

mkApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
mkApp TrTYPE Tr'PtrRepLifted = TrType
mkApp TrTYPE 
Last modified 21 months ago Last modified on May 26, 2017 12:11:14 PM