Question about implementing `Typeable` (with kinds)
Simon Peyton Jones
simonpj at microsoft.com
Mon Feb 9 13:45:37 UTC 2015
| 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/
More information about the ghc-devs
mailing list