Question about implementing `Typeable` (with kinds)

[Richard Eisenberg]

Thanks, Iavor, for doing this!

On Feb 7, 2015, at 3:11 PM, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:

>   1. Add a new filed to `TypeRep` that remembers _kind_ parameters:
> 
>       TypeRep Fingerprint TyCon [TypeRep]{-kinds-} [TypeRep]{-types-}

Perhaps change to use record syntax? With two `[TypeRep]` parameters, it could get confusing.

> 
>   2. Modify the constraint solver, to solve constraints like this:
>      - Kind-polymorphic type constructors don't get `Typeable` instances on their own
>      - GHC can solve `Typeable` constraints on  _concrete uses_ of polymorphic type constructors.
>       More precisely, GHC can solve constraints of the form `Typeable k (TC @ ks)`, as long as:
>        (1) `k` is not a forall kind,
>        (2) the `ks` are all concrete kinds (i.e., they have no free kind variables).
> 
> This all seems fairly straight-forward, but I got stuck on the actual implementation, in particular:
> 
> what `EvTerm` should I use when discharging a `Typeable` constraint?
> 
> I can create a an `HsSyn` value for the required method (i.e., a function of type `Proxy# t -> TypeRep`).
> I can also cast this into a `Typeable` dictionary value.
> The issue is that I am left with an `HsSyn` expression, and not an `EvTerm`.
> 
> So is there a way to treat an arbitrary expression as an `EvTerm`?
> 
> In the implementation of the type-lits, I just added custom evidence, but this does not scale well (also, in that case the evidence is just a simple value, while here
> it is a bit more complex).
> 
> Suggestions would be most appreciated!

Seems to me that adding another constructor of EvTerm is the way forward. I agree that the approach doesn't scale, but I think that any custom behavior in the solver is going to need some custom support. However, perhaps there is a better way, such as encoding either an HsExpr or a CoreExpr into an EvTerm somehow...

Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20150207/c5622b61/attachment-0001.html>