<div dir="ltr"><div><div><div><div><div><div><div><div>I mean if `insert :: a -> Container a -> Container a`, and I call it with `[e| insert 5 True |]`, the quote will fail.<br><br></div>The goal here is to generate `Fn f` patterns in the property lambda whenever the `UnboundVarE` is a function. For example, today if I am given this:<br><br></div><span style="font-family:monospace">[e| law "length/map" (length as == length (map f as)) |]</span><br><br></div>the generated code will be<br><br></div><span style="font-family:monospace">property $ \as f -> length as === length (map f as)</span><br><br></div>when I would prefer to generate<br><br></div><span style="font-family:monospace">property $ \as (Fn f) -> length as === length (map f as)</span><br><br></div>which will have significantly better UX. I'm willing to write a bad typechecker for `Exp`s, but really hoping I won't have to.<br><br></div>Thanks!<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Mar 18, 2020 at 1:04 AM Matthew Pickering <<a href="mailto:matthewtpickering@gmail.com">matthewtpickering@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Good morning Sandy, thanks for your email.<br>
<br>
I don't think that GHC will typecheck the quote until you splice it<br>
in. What exactly do you mean that it fails if `b` is replaced with<br>
something different?<br>
<br>
What are you hoping to do with this information?<br>
<br>
This reminds me a bit of the `qTypecheck` action I have implemented on<br>
another branch -<br>
<a href="https://gitlab.haskell.org/ghc/ghc/issues/17565#note_242199" rel="noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc/issues/17565#note_242199</a><br>
<br>
Cheers,<br>
<br>
Matt<br>
<br>
On Wed, Mar 18, 2020 at 1:56 AM Sandy Maguire <<a href="mailto:sandy@sandymaguire.me" target="_blank">sandy@sandymaguire.me</a>> wrote:<br>
><br>
> Hi all,<br>
><br>
> I'm writing some TH code that should generate property tests. For example, the expression:<br>
><br>
> $(generate [e| law "idempotent" (insert a (insert a b) == insert a b) |])<br>
><br>
> should generate the code<br>
><br>
> property $ \a b -> insert a (insert a b) === insert a b<br>
><br>
> I do this by looking for UnboundVarEs in the Exp returned by the [e| quote, and binding them in a lambda. All of this works.<br>
><br>
> However, now I'm trying to get the inferred types of `a` and `b` in the above. GHC clearly is typechecking the quote, since it will fail if I replace `b` with something nonsensical. Is there some existent way to get the inferred type of an UnboundVarE --- ideally without reimplementing the typechecker?<br>
><br>
> Thanks!<br>
> Sandy<br>
> _______________________________________________<br>
> ghc-devs mailing list<br>
> <a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>