Question about implementing `Typeable` (with kinds)

[Iavor Diatchki]

Hello,

Like Adam, I think it'd be nice to allow for general HsSyn (or, perhaps,
Core) in EvTerm.  In the meantime, I'll add another  constructor specific
for `Typeable`, and deal with it in the desugarer.

-Iavor

On Mon, Feb 9, 2015 at 5:45 AM, Simon Peyton Jones <simonpj at microsoft.com>
wrote:

> |  Is there any problem in principle with allowing arbitrary HsExprs
> |  inside an EvTerm? Hopefully that would subsume the type-lits, Typeable
> |  and possible future cases.
>
> I don't think there is an objection in principle.  But maybe it should be
> Core not HsSyn?  And it's a bit tiresome for the type checker to be
> generating syntax trees ... it is for the desugarer to, well, desugar them.
>
> But I suggest that for the #9858 stuff we stick the current story
>
> S
>
>  The grand plan with typechecker plugins is
> |  to make it possible to implement such special-purpose constraint
> |  solvers outside GHC itself; at the moment we can do that for equality
> |  constraints, but not very easily for other sorts of constraints (like
> |  Typeable).
> |
> |  Adam
> |
> |
> |  >
> |  > *From:*Iavor Diatchki [mailto:iavor.diatchki at gmail.com]
> |  > *Sent:* 07 February 2015 20:11
> |  > *To:* Simon Peyton Jones; ghc-devs at haskell.org
> |  > *Subject:* Question about implementing `Typeable` (with kinds)
> |  >
> |  >
> |  >
> |  > 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
> |
> |
> |  --
> |  Adam Gundry, Haskell Consultant
> |  Well-Typed LLP, http://www.well-typed.com/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20150209/4bc93d59/attachment.html>