...  ...  @@ 319,15 +319,17 @@ Conclusion: make `TypeRep` abstract. But then how can we patternmatch on it? 


### Trusted computing base









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



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.






```wiki



TTyCon a  abstract type



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



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



tyConKind :: TTyCon (a :: k) > TTypeRep (k :: *)



```






**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?






Note that `TTyCon` represents type constructors already applied to any kind arguments. Even with kind equalities, we have no way of creating a representation for `Proxy :: forall k. k > *`, as that would require an impredicative kind for the implicit kind argument to `TTyCon`.






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




...  ...  @@ 335,6 +337,9 @@ eqTyCon :: forall k1 k2. forall (a :: k1) (b :: k2). 


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



```









Implementing the "fast comparison" idea above will require putting more code in the TCB because of interaction with fingerprints. But the functions above are morally the only ones that need be trusted.






### What about structure information?







...  ...  @@ 345,68 +350,65 @@ Related but different issue: [ https://ghc.haskell.org/trac/ghc/ticket/7897](htt 


## Step by step









We can do steps 1 and 2 without kind equalities, although the



implementation of `decomposeFun` will use `unsafeCoerce` and will be part of the TCB.



We can do steps 1 and 2 (and probably 3) without kind equalities, although the



implementation of `decomposeFun` will use `unsafeCoerce` and will be part of the TCB. However, this will all likely happen after merging with kind equalities.






## Proposed API









This assumes heterogeneous equality (that is, with kind equalities). If you really want to see this with homogeneous equality, look through the history of this page, before April 29, 2015.






```wiki



data TTypeRep (a :: k)  abstract



data TTyCon (a :: k)  abstract






tyConKind :: forall k (a :: k). TTyCon a > TTypeRep k






 Costructors



trCon :: forall k (a :: k). TTyCon a > TTypeRep a  in TCB



trCon :: forall k (a :: k). TTyCon a > TTypeRep a



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



TTypeRep a > TTypeRep b > TTypeRep (a b)  in TCB



TTypeRep a > TTypeRep b > TTypeRep (a b)






 Destructors



pattern type TRCon :: forall k (a :: k). TyCon a > TTypeRep a



pattern type TRApp :: forall k. exists k1 (a :: k1 > k) (b :: k1).



TTypeRep a > TTypeRep b > TTypeRep (a b)



pattern type TRFun :: TTypeRep arg



> TTypeRep res



> TypeRep (TTypeRep (arg>res))









 For now, homogeneous equalities



eqTyCon :: forall k (a :: k) (b :: k).



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



eqTT :: forall k (a :: k) (b :: k).



TTypeRep a >T TypeRep b > Maybe (a :~: b)



```









When we get kind equalities, we can generalise `eqTyCon` and `eqTT`:






```wiki



 this definition to go into Data.Type.Equality



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



HRefl :: a :~~: a






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



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



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






 the following definitions can be defined on top of the interface



 above, but would be included for convenience



pattern type TRFun :: TTypeRep arg > TTypeRep res



> TTypeRep (arg > res)






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



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






 can now implement TRFun in terms of TRApp, outside of TCB



typeRepKind :: forall k (a :: k). TTypeRep a > TTypeRep k






class forall k (a :: k). Typeable k => Typeable a where



tTypeRep :: TTypeRep a



```






**SLPJ**: Do we need both `:~:` and `:~~:`?









Some of this design is motivated by the desire to allow flexibility in the implementation to allow for fingerprinting for fast equality comparisons. Naturally, the fingerprints have to be in the TCB. If it weren't for them, though, the `TypeRep` type could be exported concretely.



**RAE**: I don't think it's strictly necessary, but keeping the distinction might be useful. `:~:` will unify the kinds of its arguments during type inference, and that might be what the programmer wants. I don't feel strongly here.









Could we simplify this a bit by removing `TyCon`?



Some of this design is motivated by the desire to allow flexibility in the implementation to allow for fingerprinting for fast equality comparisons. Naturally, the fingerprints have to be in the TCB. If it weren't for them, though, the `TypeRep` type could be exported concretely.









Can we get the representation of a Kind from a TyCon? I.e. should we have something like



Could we simplify this a bit by removing `TyCon`? **RAE**: No.






```wiki



getKind :: forall k. TTCon (a :: k) > TTypeRep (k :: *)



```






The class declaration for `Typeable` is highly suspect, as it is manifestly cyclic. However, (forgetting about implementation) this doesn't cause a problem here, because all kinds have kind `*`. Thus, we know the cycle terminates. Implementation is an open question, but I (RAE) surmise that this barrier is surmountable.






Seems like this would be a good thing to add, but it is not clear.



**RAE:** How can we get a `TTyCon` for a knownatcompiletime tycon? I want something like `tyConRep @(>)` that will give something of type `TTyCon (>)`. The problem is that the type argument to `tyConRep` might not be a bare type constructor... but I would hate to have such a function return a `Maybe`, as it would be very annoying in practice, and it could be checked at compile time. I almost wonder if a new highlymagical language primitive would be helpful here.






## Kindpolymorphism




...  ...  