Typeable meeting

[Richard Eisenberg]

> On Oct 6, 2016, at 1:15 PM, Ben Gamari <ben at smart-cactus.org> wrote:
>>> 1. Currently saturated (->) is treated differently to unsaturated
>>> (->), as witnessed by the special kinding rule for FunTy. The
>>> shortest path for TypeRep is to do the same: add TrFunTy.
>> 
>> Will this be changed after Ben's work to generalize the kind of (->)?
> 
> I suspect not; I think we'll want TrFunTy regardless of the kind of
> (->). If nothing else it makes common TypeReps a bit more compact.

So this will just be an optimization, then? May be worth thinking about how to measure whether this is actually an improvement. I was also under the impression that TypeReps would carry fingerprints for efficiency.... perhaps this will make TypeReps smaller in memory, but I don't foresee gobs and gobs of TypeReps filling up a lot of memory, so I'm not convinced this compression will be worth its weight.

I do agree that we need TrFunTy now (because of the weird kind of (->)), but I'm unconvinced that we need it in the future.
> 
>>> 
>>> 4. Under (3) at what kinds is ((->) ?? LiftedPtrRep (Ord Int) Char)
>>> called? If we continue to distinguish * from Constraint, we'd need to
>>> instantiate ?? with ConstraintRep, and define
>>> 	type Constraint = TYPE ConstraintRep
>>> Orthogonally, one might wonder about combining * and Constraint, but
>>> we don't yet know how to do that well.
>> 
>> Urgh. This gives me the willies. The whole point of representation
>> polymorphism is to common up things with the same representation. And
>> here we're specifically taking two things with the same rep -- Type
>> and Constraint -- and separating them. What's wrong with ((->)
>> LiftedPtrRep LiftedPtrRep (Ord Int) Char)? Recall that `eqType
>> Constraint Type` says `True`. It's only `tcEqType` that distinguishes
>> between Constraint and Type.
>> 
> Indeed this seems to be one of the possible conclusions of #11715.
> 
> However, I think the point of the approach Simon describes is that we
> want to handle the Constraint ~ Type issue separately from Typeable (and
> the variety of other issues that it has dragged in). Introducing another
> RuntimeRep is merely a way of maintaining the status quo (where
> Constraint /~ Type) until we want to consider unifying the two. 

I believe that **right now**, if you say (eqType Constraint Type), you get True. So they're already unified! A problem is that this equality is not universally respected. If you try to splitAppTy Type, you get TYPE and LiftedPtrRep. If you try to splitAppTy Constraint, you fail. Perhaps the short-term thing is just to fix, e.g., splitAppTy.... much like we already special-case FunTy to be splittable, we can special-case Constraint to be splittable. I'm sure that the problem extends past just splitAppTy, but a scan through Type.hs, Kind.hs, and TcType.hs should hopefully show up all the problem sites.

> 
> 
> Also, Simon didn't mention another conclusion from our meeting:
> 
> 5. TrTyCon should somehow carry the TyCon's kind variable
> instantiations, not the final kind of the type.

Why? Will we want to decompose this? (I suppose we will. But do we have a use-case?) Why not carry both the kind instantiations and the final kind? That seems much simpler than the scheme below.

> That is, currently we
> have,
> 
>    TrTyCon :: TyCon -> TypeRep k -> TypeRep (a :: k)
> 
> What we want, however, is something closer to,
> 
>    TrTyCon :: TyCon -> [SomeTypeRep] -> TypeRep (a :: k)

To be concrete, I'm proposing

TrTyCon :: TyCon -> [SomeTypeRep] -> TypeRep k -> TypeRep (a :: k)

> 
> This carries a complication, however, since typeRepKind needs to somehow
> reconstruct the kind `k` from the information carried by the TrTyCon.
> TyCon must carry additional information to make this feasible. The naive
> approach would be,
> 
>    data TyCon = TyCon { tyConName :: String
>                       , tyConKind :: [SomeTypeRep] -> SomeTypeRep
>                       }
> 
> This, however, suffers from the fact that it can no longer be
> serialized. Consequently we'll need to use something like,
> 
>    type KindBinder = Int
> 
>    data TyConKindRep = TyConKindVar KindBinder
>                      | TyConKindApp TyCon [TyConKindRep]
> 
>    data TyCon = TyCon { tyConName :: String
>                       , tyConKindRep :: TyConKindRep
>                       }
> 
>    tyConKind :: TyCon -> [SomeTypeRep] -> SomeTypeRep

I'm afraid this isn't quite sophisticated enough, because kind quantification isn't necessarily prenex anymore. For example:

data (:~~:) :: forall k1. k1 -> forall k2. k2 -> Type

Your TyConKindRep doesn't have any spot for kind quantification, so I'm assuming your plan is just to quantify everything up front... but that won't quite work, I think. Argh.

Richard