Question about implementing `Typeable` (with kinds)

[Iavor Diatchki]

Hello,

I started adding custom solving for `Typeable` constraints, to work around
the problem where kind parameters were missing from the representation of
types.

The idea is as follows:

  1. Add a new filed to `TypeRep` that remembers _kind_ parameters:

      TypeRep Fingerprint TyCon [TypeRep]{-kinds-} [TypeRep]{-types-}

  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!

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