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!
Simon 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
_______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
