HaRe and incremental type checking / type inference

[AlanKim Zimmerman]

I am working with HsSyn Name, resulting from calling.typecheckModule from
the GHC API.

This seems to give a workable balance between the ParsedSource which is
lexically close to the original source but lacks grouping of related
elements, and the TypecheckedSource which has had the type information
reduced to the type checker output.

I am not sure which of the two type signatures is the "right" one for a
refactorer. The commented out one preserves that the original baz returns
an Int, and splices in the xx signature, the uncommented one is as
generated by GHC 7.6.3 when using the :i command in ghci.

The API calls I would like to make would be something like

reTypecheckModule  :: GhcMonad
<http://www.haskell.org/ghc/docs/7.6.3/html/libraries/ghc-7.6.3/GHC.html#t:GhcMonad>
m => ParsedModule
<http://www.haskell.org/ghc/docs/7.6.3/html/libraries/ghc-7.6.3/GHC.html#t:ParsedModule>
-> m TypecheckedModule
<http://www.haskell.org/ghc/docs/7.6.3/html/libraries/ghc-7.6.3/GHC.html#t:TypecheckedModule>

which would take a modified ParsedModule (or RenamedSource, or whatever
context is required), restore the original type checking environment, and
redo the type checking phase.

This would then allow a query something like the existing getInfo call to
retrieve the inferred type.

Alternatively, explicitly putting a typed hole in for the required
signature as part of the changes going in to the call to reTypecheckModule
and then processing the returned warnings would work just as well.

But I suspect I should poke around in the internals a bit more to clarify
my question by trying to actually do it.

Alan




On Sun, Jul 13, 2014 at 10:41 PM, Richard Eisenberg <eir at cis.upenn.edu>
wrote:

> Sorry -- I'm still not sure what you mean.
>
> What AST are you working with? HsSyn RdrName? HsSyn Name? HsSyn Id? Core?
> And, in your original example, there is a commented-out type signature and
> then an uncommented-out one. Which are you trying to generate? Would the
> recent partial type signature work help you? (I don't think it's in HEAD
> yet.)
>
> Perhaps give the type of a function in the GHC API that you would like to
> have...
>
> Richard
>
> On Jul 13, 2014, at 4:31 PM, AlanKim Zimmerman <alan.zimm at gmail.com>
> wrote:
>
> Basically I want to be able to make a few small changes to an already type
> checked AST and then query the type system, similar to what is possible
> with typed holes.
>
> So in my example I would like to move baz to the top level, and then
> invoke the type checker to get the required signature, without having to
> convert the partial result back to source and re-run the entire compilation.
>
> Alan
>
>
>
>
>
> On Sun, Jul 13, 2014 at 10:21 PM, Richard Eisenberg <eir at cis.upenn.edu>
> wrote:
>
>> Hello Alan,
>>
>> It's not clear what you're asking for here. What's keeping you from
>> "accessing the full power of the GHC type system"?
>>
>> Richard
>>
>> On Jul 9, 2014, at 4:35 PM, AlanKim Zimmerman <alan.zimm at gmail.com>
>> wrote:
>>
>> > I have hit a problem in HaRe when lifting a declaration from e.g. a
>> where clause of a function to the top level, where there is a type
>> signature of any complexity.
>> >
>> > e.g lifting 'baz' from function 'foo' below
>> >
>> > --------------------------
>> > foo a = baz
>> >   where
>> >     baz :: Int
>> >     baz = xx 1 a
>> >
>> >     xx :: (Num t) => t -> t -> t
>> >     xx p1 p2 = p1 + p2
>> > --------------------------------------
>> >
>> > becomes
>> >
>> > ---------------------------------------------
>> > foo a = (baz xx a)
>> >   where
>> >     xx :: (Num t) => t -> t -> t
>> >     xx p1 p2 = p1 + p2
>> >
>> > -- baz:: (forall t. Num t => t -> t -> t) -> Int ->Int
>> > baz :: Num a => (a -> t1 -> t) -> t1 -> t
>> > baz xx a= xx 1 a
>> > -----------------------------------------------
>> >
>> > For a very small subset this can be calculated easily, but for full
>> generality it would be great to access the full power of the GHC type
>> system.
>> >
>> > So before diving in too deeply, I thought I would test the waters as to
>> the feasibility of doing something like this. I was hoping that perhaps the
>> effort at an external constraint solver might be making the interfacing
>> slightly simpler.
>> >
>> > Regards
>> >  Alan
>> >
>> > _______________________________________________
>> > ghc-devs mailing list
>> > ghc-devs at haskell.org
>> > http://www.haskell.org/mailman/listinfo/ghc-devs
>>
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140713/af57a06c/attachment.html>