...  ...  @@ 176,7 +176,32 @@ Is that not beautiful? The second equation for `dynApply` is needed in case the 












## Step 3: Decomposing arbitrary types



## Step 3: Extracting kind equalities









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*






```wiki



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



```









where `typeOf :: Typeable a => a > TypeRep` is a longstanding part of the `Typeable` API. To typecheck that expression, we need a `Typeable (Proxy a)` dictionary. Of course, to build such a thing, we need `Typeable k`, which we have no way of getting.









So, we now include






```wiki



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



```









in the API. I (Richard) conjecture that this is all possible without kind equalities, but would be rather awkward due to GHC's insistence that kind parameters be implicit. See [\#10343](https://gitlab.haskell.org//ghc/ghc/issues/10343), which inspired this bit.













## Step 4: Decomposing arbitrary types









It is all very well being able to decompose functions, but what about decomposing other types, like `Maybe Int`?

...  ...  @@ 286,7 +311,7 @@ So Step 3 (allowing `TypeRep` to be fully decomposed in a type safe way) absolut 


### Fast comparison of `TypeRep`









The current implementation of `TypeRep` allows constanttype comparison based on fingerprints. To support this in the new scheme we would want to add a fingerprint to every `TypeRep` node. But we would not want clients to see those fingerprints, lest they forge them.



The current implementation of `TypeRep` allows constanttime comparison based on fingerprints. To support this in the new scheme we would want to add a fingerprint to every `TypeRep` node. But we would not want clients to see those fingerprints, lest they forge them.









Conclusion: make `TypeRep` abstract. But then how can we patternmatch on it? Pattern synonyms seem to be exactly what we need.

...  ...  @@ 302,6 +327,8 @@ eqTyCon :: forall k1 k2. forall (a :: k1) (b :: k2). 


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



```






**RAE stuck:** We have `data TTyCon (a :: k) = ...`, but how is that used to represent polykinded tycons? If we want a representation of `Proxy`, it would have to be `TTyCon <forall k. k > *> Proxy`, writing in the kind argument explicitly. And that's impredicative! Or do `TTyCon`s store type constructors applied to all dependent (i.e. kind) arguments?






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






```wiki

...  ...  @@ 422,6 +449,8 @@ we actually supply a kind parameter `k0`. GHC tries to find a value for `k0`, fa 





### A stopgap solution






**NB:** This was not implemented. The "mediumterm solution" below was, as of 7.10.1.






[comment:16:ticket:9858](https://gitlab.haskell.org//ghc/ghc/issues/9858) is a demonstration that the boat is taking on water! Fix the leak, fast!







...  ...  @@ 439,12 +468,14 @@ deriving instance Typeable (PK :: (* > *) > *) 


which would yield instances `Typeable <* > *> (PK <*>)` and `Typeable <(* > *) > *> (PK <* > *>)`  two separate instances with different, and distinguishable `TypeRep`s. What's painful here is that, clearly, there are an *infinite* number of such instantiations of `PK`. We could maybe provide a handful of useful ones, but we could never provide them all.









That, then, is the current plan of attack. `Typeable` instance heads must include concrete instantiations of all kind parameters but no type parameters. `base` will provide several instantiations for polykinded datatypes, but users may have to write orphan instances to get others. `AutoDeriveTypeable` will ignore polykinded datatype definitions  users must write explicit instances if they want to.



That, then, is the current plan of attack. (**No, it's not.**) `Typeable` instance heads must include concrete instantiations of all kind parameters but no type parameters. `base` will provide several instantiations for polykinded datatypes, but users may have to write orphan instances to get others. `AutoDeriveTypeable` will ignore polykinded datatype definitions  users must write explicit instances if they want to.






**Question:** With this design, orphan instances will be unavoidable. Given that two different authors may introduce the same orphan instances, would it work to mark every `Typeable` instance as `{# INCOHERENT #}`? For this to work out, we would need a guarantee that the fingerprints of the instances are the same regardless of originating module.






### Mediumterm solution






**This is implemented in 7.10.**









Although it is impossible to create all necessary `Typeable` instances for polykinded constructors at the definition site (there's an infinite number), it *is* possible to create `Typeable` "instances" on demand at use sites. The idea (originally proposed in [comment:20:ticket:9858](https://gitlab.haskell.org//ghc/ghc/issues/9858)) is to add some custom logic to the solver to invent `Typeable` evidence on demand. Then, whenever the solver needs to satisfy a `Typeable` constraint, it will just recur down to the type's leaves and invent evidence there.




...  ...  