I mean if `insert :: a -> Container a -> Container a`, and I call it with `[e| insert 5 True |]`, the quote will fail. 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: [e| law "length/map" (length as == length (map f as)) |] the generated code will be property $ \as f -> length as === length (map f as) when I would prefer to generate property $ \as (Fn f) -> length as === length (map f as) 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. Thanks! On Wed, Mar 18, 2020 at 1:04 AM Matthew Pickering < matthewtpickering@gmail.com> wrote:

Good morning Sandy, thanks for your email.

I don't think that GHC will typecheck the quote until you splice it in. What exactly do you mean that it fails if `b` is replaced with something different?

What are you hoping to do with this information?

This reminds me a bit of the `qTypecheck` action I have implemented on another branch - https://gitlab.haskell.org/ghc/ghc/issues/17565#note_242199

Cheers,

Matt

On Wed, Mar 18, 2020 at 1:56 AM Sandy Maguire wrote:

...

Hi all,

I'm writing some TH code that should generate property tests. For

example, the expression:

...

$(generate [e| law "idempotent" (insert a (insert a b) == insert a b) |])

should generate the code

property $ \a b -> insert a (insert a b) === insert a b

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.

...

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?

...

Thanks! Sandy _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

I'm also generating code at the same time, and might have gotten confused by that interaction :) In the meantime I guess I'll implement HM. The world will be a much better place when TTG is finished and we have ghc-as-an-easy-to-use-library :) On Thu, Mar 19, 2020 at 2:51 AM Richard Eisenberg wrote:

Good to see you around, Sandy!

On Mar 18, 2020, at 6:54 PM, Sandy Maguire wrote:

I mean if `insert :: a -> Container a -> Container a`, and I call it with `[e| insert 5 True |]`, the quote will fail.

I don't observe this. Specifically, when I compile

{-# LANGUAGE TemplateHaskellQuotes #-}

module Bug where

import Prelude ( Bool(..), undefined )

data Container a

insert :: a -> Container a -> Container a insert = undefined

quote = [e| insert 5 True |]

GHC happily succeeds.

I think what you want, though, is reasonable: you want the ability to send an expression through GHC's type-checker. I think we'd need to extend TH to be able to support this, and it will be hard to come up with a good design, I think. (Specifically, I'm worried about interactions with top-level defined entities, whose types might not really be known by the time of splice processing.) This might all be worthwhile -- singletons would be able to be improved with this, for example -- but it's not cheap, sadly.

Richard