...  ...  @@ 24,112 +24,7 @@ The names of functions and type constructors is totally up for grabs. 





# Status









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












Open Tickets:






<table><tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/10770">#10770</a></th>



<td>Typeable solver has strange effects</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/11251">#11251</a></th>



<td>isInstance does not work on Typeable with base4.8 anymore</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/11349">#11349</a></th>



<td>[TypeApplications] Create Proxyfree alternatives of functions in base</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/11715">#11715</a></th>



<td>Constraint vs *</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/12451">#12451</a></th>



<td>TemplateHaskell and Data.Typeable  tcIfaceGlobal (local): not found</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/13261">#13261</a></th>



<td>Consider moving Typeable evidence generation wholly back to solver</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/13276">#13276</a></th>



<td>Unboxed sums are not Typeable</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/13647">#13647</a></th>



<td>Tidy up TcTypeable</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/13933">#13933</a></th>



<td>Support Typeable instances for types with coercions</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14190">#14190</a></th>



<td>Typeable imposes seemingly redundant constraints on polykinded instances</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14255">#14255</a></th>



<td>Typeindexed type fingerprints</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14270">#14270</a></th>



<td>GHC HEAD's ghcstage1 panics on Data.Typeable.Internal</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14337">#14337</a></th>



<td>typeRepKind can perform substantial amounts of allocation</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14341">#14341</a></th>



<td>Show instance for TypeReps is a bit broken</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14401">#14401</a></th>



<td>Add a test ensuring that TypeReps can be stored in compact regions</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14480">#14480</a></th>



<td>Clean up tyConTYPE</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14582">#14582</a></th>



<td>Review and improve the Typeable API</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14663">#14663</a></th>



<td>Deriving Typeable for enumerations seems expensive</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/15322">#15322</a></th>



<td>`KnownNat` does not imply `Typeable` any more when used with plugin</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/15862">#15862</a></th>



<td>Panic with promoted types that Typeable doesn't support</td></tr></table>















Closed Tickets:






<table><tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/3480">#3480</a></th>



<td>Easily make Typeable keys pure, so that Typeable can be handled efficiently across communications</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/8931">#8931</a></th>



<td>The type defaulting in GHCi with Typeable</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/9639">#9639</a></th>



<td>Remove OldTypeable</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/9707">#9707</a></th>



<td>(Try to) restructure `base` to allow more use of `AutoDeriveTypeable`</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/10163">#10163</a></th>



<td>Export typeRepKinds in Data.Typeable</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/10343">#10343</a></th>



<td>Make Typeable track kind information better</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/11011">#11011</a></th>



<td>Add typeindexed type representations (`TypeRep a`)</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/11120">#11120</a></th>



<td>Missing type representations</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/11714">#11714</a></th>



<td>Kind of (>) type constructor is overly constrained</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/11722">#11722</a></th>



<td>No TypeRep for unboxed tuples</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/11736">#11736</a></th>



<td>Allow unsaturated uses of unlifted types in Core</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/12082">#12082</a></th>



<td>Typeable on RealWorld fails</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/12123">#12123</a></th>



<td>GHC crashes when calling typeRep on a promoted tuple</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/12409">#12409</a></th>



<td>Unboxed tuples have no type representations</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/12670">#12670</a></th>



<td>Representation polymorphism validity check is too strict</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/12905">#12905</a></th>



<td>Core lint failure with pattern synonym and levity polymorphism</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/13197">#13197</a></th>



<td>Perplexing levity polymorphism issue</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/13333">#13333</a></th>



<td>Typeable regression in GHC HEAD</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/13871">#13871</a></th>



<td>GHC panic in 8.2 only: typeIsTypeable(Coercion)</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/13872">#13872</a></th>



<td>Strange Typeable error message involving TypeInType</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/13915">#13915</a></th>



<td>GHC 8.2 regression: "Can't find interfacefile declaration" for promoted data family instance</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14199">#14199</a></th>



<td>Document Type.Reflection better (Fun and Con')</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14254">#14254</a></th>



<td>The Binary instance for TypeRep smells a bit expensive</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/14925">#14925</a></th>



<td>NonASCII type names get garbled when their `TypeRep` is shown</td></tr>



<tr><th><a href="https://gitlab.haskell.org/ghc/ghc/issues/15067">#15067</a></th>



<td>When Typeable and unboxed sums collide, GHC panics</td></tr></table>












See the ~typeable ticket for tickets.









## Goal

...  ...  @@ 139,7 +34,7 @@ Closed Tickets: 


Consider `Dynamic`:









```



```haskell



data Dynamic where



Dyn :: TypeRep > a > Dynamic



```

...  ...  @@ 148,7 +43,7 @@ data Dynamic where 


We'd like to write `dynApply`:









```



```haskell



dynApply :: Dynamic > Dynamic > Maybe Dynamic



```




...  ...  @@ 156,7 +51,7 @@ dynApply :: Dynamic > Dynamic > Maybe Dynamic 


which succeeds only when the application is type correct. But how? Let's try









```



```haskell



dynApply (Dyn tf f) (Dyn tx x) = ???



```




...  ...  @@ 168,7 +63,7 @@ We need some way to decompose `tf` (the type representation for `f`), ask if it 


But at the moment we don't have any *typesafe* way to decompose `TypeRep`. Indeed `dynApply` is defined like this right now:









```



```haskell



dynApply (Dyn tf f) (Dyn tx x)



= case funResultTy tf tx of



Just tr > Just (Dyn tr (unsafeCoerce f x))

...  ...  @@ 192,7 +87,7 @@ So **our main goal is to be able to write `dynApply` in a typesafe way** so tha 


The first obvious thing is that we must make a connection between the typerep arg of `Dyn` and the value itself. Something like this:









```



```haskell



data Dynamic where



Dyn :: TTypeRep a > a > Dynamic



```

...  ...  @@ 205,7 +100,7 @@ Here we are using a *typeindexed* type representation, `TTypeRep`. Now the con 


We can redefine the `Typeable` class and `TypeRep` thus:









```



```haskell



class Typeable a where



tTypeRep :: TTypeRep a  No need for a proxy argument!




...  ...  @@ 228,7 +123,7 @@ We can get from `Typeable a` to `TTypeRep` by using the class method `tTypeRep`. 


We need to add the following primitive:









```



```haskell



withTypeable :: TTypeRep a > (Typeable a => b) > b



```




...  ...  @@ 240,7 +135,7 @@ withTypeable :: TTypeRep a > (Typeable a => b) > b 


We can also compare two `TTypeReps` to give a staticallyusable proof of equality:









```



```haskell



eqTT :: TTypeRep a > TTypeRep b > Maybe (a :~: b)



eqT :: (Typeable a, Typeable b) => Maybe (a :~: b)




...  ...  @@ 260,7 +155,7 @@ data a :~: b where  Defined in Data.Typeable.Equality 


If we want to decompose `TTypable`, at least in the function arrow case, we need a function like this:









```



```haskell



decomposeFun :: TTypeRep fun



> r



> (forall arg res. (fun ~ (arg>res))

...  ...  @@ 279,7 +174,7 @@ This function is part of `Typeable`, and replaces `funResultTy`. 


Now we can write `dynApply`, in a completely typesafe way, outside the TCB:









```



```haskell



dynApply :: Dynamic > Dynamic > Maybe Dynamic



dynApply (Dyn tf f) (Dyn tx x)



= decomposeFun tf Nothing $ \ ta tr >

...  ...  @@ 292,7 +187,7 @@ dynApply (Dyn tf f) (Dyn tx x) 


**Pattern synonyms**. An alternative, rather nicer interface for `decomoposeFun` would use a [pattern synonym](patternsynonyms) instead of continuationpassing style. Here is the signature for the pattern synonym:









```



```haskell



pattern TRFun :: fun ~ (arg > res)



=> TTypeRep arg



> TTypeRep res

...  ...  @@ 303,7 +198,7 @@ pattern TRFun :: fun ~ (arg > res) 


which looks (by design) very like the signature for a GADT data constructor. Now we can use `TRFun` in a pattern, thus:









```



```haskell



dynApply :: Dynamic > Dynamic > Maybe Dynamic



dynApply (Dyn (TRFun ta tr) f) (Dyn tx x)



= case eqTT ta tx of

...  ...  @@ 324,7 +219,7 @@ Suppose we have a `TTypeRep (a :: k)`. It might be nice to get a `TTypeRep (k :: 


out of it. (Here, we assume `* :: *`, but the idea actually works without that assumption.) An example is an attempt to typecheck the *expression*









```



```haskell



typeOf :: Typeable (a :: k) => Proxy a > TypeRep



```




...  ...  @@ 336,7 +231,7 @@ where `typeOf :: Typeable a => a > TypeRep` is a longstanding part of the `Typ 


So, we now include









```



```haskell



kindRep :: TTypeRep (a :: k) > TTypeRep k



```




...  ...  @@ 355,7 +250,7 @@ It is all very well being able to decompose functions, but what about decomposin 


To do this it is natural to regard types as built from type constructors and binary application, like this:









```



```haskell



data TTypeRep (a :: k) :: * where



TRApp :: TTypeRep a > TTypeRep b > TTypeRep (a b)



TRCon :: TTyCon a > TTypeRep a

...  ...  @@ 373,7 +268,7 @@ data TTypeRep (a :: k) :: * where 


While this GADT is expressible in GHC now (note the existential kind in TRApp), **it is not very useful without kind equalities**. (GHC does not currently support kind equalities, but Richard Eisenberg is working that very question.) Why? Here is the type of `TRApp` in its full glory, with normallyinvisible kind args in angle brackets:









```



```haskell



TRApp :: forall k1 k2. forall (a :: k1 > k2) (b :: k1).



TTypeRep <k1>k2> a > TTypeRep <k1> b > TTypeRep <k2> (a b)



```

...  ...  @@ 382,7 +277,7 @@ TRApp :: forall k1 k2. forall (a :: k1 > k2) (b :: k1). 


Or, to be really explicit about the existentials:









```



```haskell



TRApp :: forall k2 (c:k2).  Universal



forall k1 (a :: k1 > k2) (b :: k1).  Existential



(c ~ a b)

...  ...  @@ 395,7 +290,7 @@ TRApp :: forall k2 (c:k2).  Universal 


Now suppose we want to implement `decomposeFun`. We should be able to do this outside the TCB, i.e. without `unsafeCoerce`:









```



```haskell



arrowCon :: TTyCon (>)  The type rep for (>)






decomposeFun :: TTypeRep fun

...  ...  @@ 415,7 +310,7 @@ decomposeFun tr def kont 


But look at the arguments of `eqTyCon`:









```



```haskell



arrowCon :: TTyCon <*>*>*> (>)



c :: TTyCon <k1>k2>*> tc



```

...  ...  @@ 428,7 +323,7 @@ where `k1` and `k2` are existential kinds bound by the two nested `TRApp` constr 


The real work is done by `eqTyCon`:









```



```haskell



eqTyCon :: forall (k1 k2 :: *).



forall (a :: k1) (b :: k2).



TTyCon <k1> a > TTyCon <k2> b > Maybe (a :~~: b)

...  ...  @@ 438,7 +333,7 @@ eqTyCon :: forall (k1 k2 :: *). 


where `:~~:` is a *kindheterogeneous* version of `:~:`:









```



```haskell



data (a::k1) :~~: (b::k2) where



HRefl :: forall (a::k). a :~~: a



```

...  ...  @@ 447,7 +342,7 @@ data (a::k1) :~~: (b::k2) where 


Or, to write the type of `HRefl` with its constraints explicit:









```



```haskell



HRefl :: forall k1 k2. forall (a::k1) (b::k2).



(k1 ~ k2, a ~ b)



=> a :~~: b

...  ...  @@ 478,7 +373,7 @@ Conclusion: make `TypeRep` abstract. But then how can we patternmatch on it? 


With all of this, what is left in the TCB? The `TTyCon` type is a new abstract type, and the comparison (based on fingerprints) must be in the TCB.









```



```haskell



TTyCon a  abstract type



eqTyCon :: forall k1 k2. forall (a :: k1) (b :: k2).



TTyCon a > TTyCon b > Maybe (a :~~: b)

...  ...  @@ 493,7 +388,7 @@ Note that `TTyCon` represents type constructors already applied to any kind argu 


`withTypeable` could be written in core (and perhaps could be generalized to other constraints) but not in source Haskell:









```



```haskell



withTypeable :: TypeRep a > (Typeable a => b) > b



```




...  ...  @@ 523,7 +418,7 @@ implementation of `decomposeFun` will use `unsafeCoerce` and will be part of the 


This version assumes homoegeneous equality (as GHC is today, July 2, 2015). Below is the version with heterogeneous equality.









```



```haskell



data TTypeRep (a :: k)  abstract



data TTyCon (a :: k)  abstract




...  ...  @@ 552,7 +447,7 @@ eqTT :: forall k (a :: k) (b :: k). 


This assumes heterogeneous equality (that is, with kind equalities).









```



```haskell



data TTypeRep (a :: k)  abstract



data TTyCon (a :: k)  abstract




...  ...  @@ 621,7 +516,7 @@ As painfully demonstrated (painful in the conclusion, not the demonstration!) in 


Drawing this out somewhat: we allow only `Typeable` instances for unapplied constructors. That is, we have









```



```haskell



deriving instance Typeable Maybe



```




...  ...  @@ 629,7 +524,7 @@ deriving instance Typeable Maybe 


never









```



```haskell



deriving instance Typeable (Maybe Int)



```




...  ...  @@ 637,7 +532,7 @@ deriving instance Typeable (Maybe Int) 


However, what if we have









```



```haskell



data PK (a :: k)



```




...  ...  @@ 646,7 +541,7 @@ data PK (a :: k) 


when we write









```



```haskell



deriving instance Typeable PK



```




...  ...  @@ 668,7 +563,7 @@ The "obvious" answer  don't supply the `k` here  doesn't work. The instance 


One (somewhat unpleasant) way forward is to allow kind parameters to be supplied in `Typeable` instances, but still restrict type parameters. So, we would have









```



```haskell



deriving instance Typeable (PK :: * > *)



deriving instance Typeable (PK :: (* > *) > *)



```

...  ...  @@ 706,7 +601,7 @@ Some drawbacks: 


We actually don't have a good longterm solution available. We thought that `* :: *` and kind equalities would fix this, but they don't. To see why, let's examine the type of `trApp`:









```



```haskell



trApp :: forall k k1 (a :: k1 > k) (b :: k1).



TTypeRep a > TTypeRep b > TTypeRep (a b)



```

...  ...  @@ 715,7 +610,7 @@ trApp :: forall k k1 (a :: k1 > k) (b :: k1). 


In the `* :: *` world, it would be reasonable to have `TTypeRep`s for kinds, assuming we have `TTypeRep`s always take explicit kind parameters. So, we might imagine having a `TTypeRep` for `PK` (call it `pkRep`) and a `TTypeRep` for `Bool` (call it `boolRep`). Does `pkRep `trApp` boolRep`` typecheck? Unfortunately, no. We have









```



```haskell



pkRep :: TTypeRep <forall k. k > *> PK



boolRep :: TTypeRep <*> Bool



```

...  ...  @@ 724,7 +619,7 @@ boolRep :: TTypeRep <*> Bool 


but `trApp` says that `a` must have type `k1 > k` for some `k1` and `k`. Here `PK` would be the value for `a`, but `PK`'s kind is `forall k. k > *`, which doesn't fit `k1 > k` at all! We would need to generalize `trApp` to









```



```haskell



trApp2 :: forall (k1 :: *) (k :: k1 > *)



(a :: pi (b :: k1). k b) (b :: k1).



TTypeRep <pi (b :: k1). k b> a > TTypeRep <k1> b

...  ...  