On 09/02/15 13:20, Simon Peyton Jones wrote:
I think just add a new constructor to EvTerm.
Yes, it’s special-purpose, but the **solver* *is special-purpose too. And it does mean that we know exactly what forms of evidence we can generate!
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. 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@gmail.com] *Sent:* 07 February 2015 20:11 *To:* Simon Peyton Jones; ghc-devs@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/