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:[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
