<div dir="ltr">Hello,<div><br></div><div>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.</div><div><br></div><div>-Iavor </div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Feb 9, 2015 at 5:45 AM, Simon Peyton Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">|  Is there any problem in principle with allowing arbitrary HsExprs<br>
|  inside an EvTerm? Hopefully that would subsume the type-lits, Typeable<br>
|  and possible future cases.<br>
<br>
</span>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.<br>
<br>
But I suggest that for the #9858 stuff we stick the current story<br>
<span class="HOEnZb"><font color="#888888"><br>
S<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
 The grand plan with typechecker plugins is<br>
|  to make it possible to implement such special-purpose constraint<br>
|  solvers outside GHC itself; at the moment we can do that for equality<br>
|  constraints, but not very easily for other sorts of constraints (like<br>
|  Typeable).<br>
|<br>
|  Adam<br>
|<br>
|<br>
|  ><br>
|  > *From:*Iavor Diatchki [mailto:<a href="mailto:iavor.diatchki@gmail.com">iavor.diatchki@gmail.com</a>]<br>
|  > *Sent:* 07 February 2015 20:11<br>
|  > *To:* Simon Peyton Jones; <a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
|  > *Subject:* Question about implementing `Typeable` (with kinds)<br>
|  ><br>
|  ><br>
|  ><br>
|  > Hello,<br>
|  ><br>
|  ><br>
|  ><br>
|  > I started adding custom solving for `Typeable` constraints, to work<br>
|  > around the problem where kind parameters were missing from the<br>
|  > representation of types.<br>
|  ><br>
|  ><br>
|  ><br>
|  > The idea is as follows:<br>
|  ><br>
|  ><br>
|  ><br>
|  >   1. Add a new filed to `TypeRep` that remembers _kind_ parameters:<br>
|  ><br>
|  ><br>
|  ><br>
|  >       TypeRep Fingerprint TyCon [TypeRep]{-kinds-} [TypeRep]{-types-<br>
|  }<br>
|  ><br>
|  ><br>
|  ><br>
|  >   2. Modify the constraint solver, to solve constraints like this:<br>
|  ><br>
|  >      - Kind-polymorphic type constructors don't get `Typeable`<br>
|  > instances on their own<br>
|  ><br>
|  >      - GHC can solve `Typeable` constraints on  _/concrete uses/_ of<br>
|  > polymorphic type constructors.<br>
|  ><br>
|  >       More precisely, GHC can solve constraints of the form<br>
|  `Typeable<br>
|  > k (TC @ ks)`, as long as:<br>
|  ><br>
|  >        (1) `k` is not a forall kind,<br>
|  ><br>
|  >        (2) the `ks` are all concrete kinds (i.e., they have no free<br>
|  > kind variables).<br>
|  ><br>
|  ><br>
|  ><br>
|  > This all seems fairly straight-forward, but I got stuck on the<br>
|  actual<br>
|  > implementation, in particular:<br>
|  ><br>
|  ><br>
|  ><br>
|  > *what `**EvTerm` should I use when discharging a `**Typeable`<br>
|  > constraint?*<br>
|  ><br>
|  ><br>
|  ><br>
|  > I can create a an `HsSyn` value for the required method (i.e., a<br>
|  > function of type `Proxy# t -> TypeRep`).<br>
|  ><br>
|  > I can also cast this into a `Typeable` dictionary value.<br>
|  ><br>
|  > The issue is that I am left with an `HsSyn` expression, and not an<br>
|  `EvTerm`.<br>
|  ><br>
|  ><br>
|  ><br>
|  > So is there a way to treat an arbitrary expression as an `EvTerm`?<br>
|  ><br>
|  ><br>
|  ><br>
|  > In the implementation of the type-lits, I just added custom<br>
|  evidence,<br>
|  > but this does not scale well (also, in that case the evidence is<br>
|  just<br>
|  > a simple value, while here<br>
|  ><br>
|  > it is a bit more complex).<br>
|  ><br>
|  ><br>
|  ><br>
|  > Suggestions would be most appreciated!<br>
|  ><br>
|  ><br>
|  ><br>
|  > -Iavor<br>
|<br>
|<br>
|  --<br>
|  Adam Gundry, Haskell Consultant<br>
|  Well-Typed LLP, <a href="http://www.well-typed.com/" target="_blank">http://www.well-typed.com/</a><br>
</div></div></blockquote></div><br></div>