<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Thanks, Iavor, for doing this!</div><div><br></div><div><div>On Feb 7, 2015, at 3:11 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com">iavor.diatchki@gmail.com</a>> wrote:</div><br><blockquote type="cite"><div dir="ltr"><div> 1. Add a new filed to `<font face="monospace, monospace">TypeRep</font>` that remembers _kind_ parameters:</div><div><br></div><div> <font face="monospace, monospace">TypeRep Fingerprint TyCon [TypeRep]{-kinds-} [TypeRep]{-types-}</font></div></div></blockquote><div><br></div><div>Perhaps change to use record syntax? With two `[TypeRep]` parameters, it could get confusing.</div><br><blockquote type="cite"><div dir="ltr"><div><br></div><div> 2. Modify the constraint solver, to solve constraints like this:</div><div> - Kind-polymorphic type constructors don't get `<font face="monospace, monospace">Typeable</font>` instances on their own</div><div> - GHC can solve `<font face="monospace, monospace">Typeable</font>` constraints on _<i>concrete uses</i>_ of polymorphic type constructors.</div><div> More precisely, GHC can solve constraints of the form `<font face="monospace, monospace">Typeable k (TC @ ks)</font>`, as long as:</div><div> (1) `<font face="monospace, monospace">k</font>` is not a forall kind,</div><div> (2) the `<font face="monospace, monospace">ks</font>` are all concrete kinds (i.e., they have no free kind variables).</div></div></blockquote><blockquote type="cite"><div dir="ltr"><div><br></div><div>This all seems fairly straight-forward, but I got stuck on the actual implementation, in particular:</div><div><br></div><div><b>what `<font face="monospace, monospace">EvTerm</font>` should I use when discharging a `<font face="monospace, monospace">Typeable</font>` constraint?</b></div><div><br></div><div>I can create a an `<font face="monospace, monospace">HsSyn</font>` value for the required method (i.e., a function of type `<font face="monospace, monospace">Proxy# t -> TypeRep</font>`).</div><div>I can also cast this into a `<font face="monospace, monospace">Typeable</font>` dictionary value.</div><div>The issue is that I am left with an `<font face="monospace, monospace">HsSyn</font>` expression, and not an `<font face="monospace, monospace">EvTerm</font>`.</div><div><br></div><div>So is there a way to treat an arbitrary expression as an `EvTerm`?</div><div><br></div><div>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</div><div>it is a bit more complex).</div><div><br></div><div>Suggestions would be most appreciated!</div></div></blockquote><div><br></div><div>Seems to me that adding another constructor of EvTerm is the way forward. I agree that the approach doesn't scale, but I think that any custom behavior in the solver is going to need some custom support. However, perhaps there is a better way, such as encoding either an HsExpr or a CoreExpr into an EvTerm somehow...</div></div><br><div>Richard</div></body></html>