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 <[email protected]> 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:[email protected]] > | > *Sent:* 07 February 2015 20:11 > | > *To:* Simon Peyton Jones; [email protected] > | > *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/ >
_______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
