Haskell › Haskell - Glasgow-haskell-bugs

[GHC] #5910: Holes with other constraints

Classic

List

Threaded

24 messages Options

GHC

[GHC] #5910: Holes with other constraints

#5910: Holes with other constraints
-----------------------------------------------+----------------------------
Reporter: xnyhps | Owner:
Type: feature request | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: 7.5 | Keywords: holes
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: Incorrect warning at compile-time | Testcase:
Blockedby: | Blocking:
Related: |
-----------------------------------------------+----------------------------
Hello. As can be seen on http://hackage.haskell.org/trac/ghc/wiki/Holes
and http://www.haskell.org/pipermail/glasgow-haskell-
users/2012-January/021670.html, we've been working on adding holes to GHC.
I'm opening this ticket about a specific problem I've been having, and I
hope someone has a suggestion of how to do it correctly.

As holes work quite similarly to implicit parameters (see the wiki-page
for a comparison), we started out in the same way as implicit parameters.
Typechecking of a hole generates a constraint (a new type of constraint),
and the constraint solver will try to find the right type for each hole.
The difference is that hole constraints never show up in a type, but their
type is printed separately. This currently works correctly for simple
typechecking, but it has some problems when other constraints are
generated too. A simple example:

{{{
test :: String
test = show _h
}}}

Here, the {{{_h}}} denotes a hole named "h". If this function is defined
like this inside a module it will currently fail:

{{{
test2.hs:2:8:
No instance for (Show a0)
arising from a use of `show'
The type variable `a0' is ambiguous
Possible fix: add a type signature that fixes these type variable(s)
In the expression: show (_h)
In an equation for `test': test = show (_h)
Failed, modules loaded: none.
}}}

The problem is that the {{{Show}}} constraint is still there. If the type
signature is omitted and the monomorphism restriction off, we can see that
the types found are:

{{{
Found the following holes:
_h :: GHC.Show.Show a => a
...
test :: Show a => String
}}}

The problem is the {{{Show a}}} that is irrelevant to the actual type of
{{{test}}}, but nevertheless it's there.

How do other approaches handle this?

'''undefined''':
{{{
test :: String
test = show undefined
}}}

Gives the same ambiguity error, even if the signature is omitted.

'''Implicit parameters''':
{{{
test = show ?h
}}}

This works, but generates the following type signature:

{{{
test :: (Show a, ?h::a) => String
}}}

So, as I'd want to use it, this is wrong. It has the right ingredients,
but I'd want:

{{{
test :: (?h :: (Show a) => a) => String
}}}

For implicit parameters the difference doesn't matter too much, as
implicit parameters are still parameters: they still show up in the type
signature. A hole is not required to be a parameter, so it's more
important that every constraint only shows up where it's necessary.

So the problem is that I don't know how to select from the constraints
only those that are applicable to the expression/function itself, and
those that apply to which of the holes. I've tried typechecking all of the
holes first, but I don't know how to determine how to change the
constraint set after that. If you need more information about how it
currently works, or have any feedback on this approach, please let me
know. I'm still quite unfamiliar with the architecture of GHC. :)

----

I'm attaching a patch against the master branch on git with my current
work in case someone is interested in trying it. Note that the code
generation is pretty much a stub and it will panic if you try to run a
function with a hole. It will print the holes of an expression if you
invoke {{{:t}}} (it doesn't currently print the holes when loading a
module, but it should still print them with {{{:t}}} on a function from
the module). Also, I do not recommend building stage 1 with this, as some
packages have some issues. Easiest is to build stage 1 and the packages
without these changes and then applying the patch and then building only
stage 2.

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5910>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #5910: Holes with other constraints

GHC

Re: [GHC] #5910: Holes with other constraints

In reply to this post by GHC

GHC

Re: [GHC] #5910: Holes with other constraints

In reply to this post by GHC

#5910: Holes with other constraints
----------------------------------------+-----------------------------------
Reporter: xnyhps | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.5
Keywords: holes | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: Incorrect warning at compile-time
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
----------------------------------------+-----------------------------------

Comment(by xnyhps):

Replying to [comment:2 simonpj]:
> Some brief responses. We may want a Skype chat.
>
> * I think the Right Way to do this is to add a new form of constraint,
as you have done.
>
> * I do not see why you need `tcl_holes` in the `TcLclEnv`.

Sorry, this was a relic from an earlier attempt. I thought I still needed
it, but I don't. I'll update the patch (I want to make sure it can build
stage1 as well).

>
> * The place to report the unsolved holes is '''not''' in `TcRnDriver`,
but rather in `TcErrors`. It is a thing of beauty. The constraint solver
tries to solve the constraints, ''returning an unsolved constraint''. The
latter is passed to `reportUnsolved` and '''that''' is the place to report
any unsolved holes.
>

The `TcRnDriver` stuff is definitely a placeholder, most of the stuff
there should actually be a part of GHCi instead.

> * Moreover, `TcErrors` ''already has'' a kind of error prioritisation:
it does not report ambiguity errors if it any more important errors (such
as holes) happen first: see `tryReporters` in `reportInsolsAndFlats`. So
that will deal nicely with the problem you describe.
>

Hmm. My intent was to allow typechecking to continue when there are holes
(so compiling them, similar to {{{undefined}}}, to something like
{{{throw#}}}). If I understand your suggestion correctly, we should abort
compilation and show the hole's type as errors when an unresolved hole is
found.

But maybe what I want it unfeasible to do "correctly" with classes. I
suppose that to compile {{{show _h}}} (where {{{_h}}} is a hole) the
compiler wants to have a concrete function to use as the show, but the
{{{Show}}} constraint is still ambiguous due to it being on a hole
therefore it can't find any instance to use.

It seems useful to me to be able to test different parts of your code when
you put in a hole. I see the holes as TODOs in the code, for parts you
need to finish later while you work on other stuff first (though maybe it
could be combined with the deferring of type errors to runtime? Haven't
experimented with that myself, I just noticed it in the code).

> * Finally, here's a fresh idea. If you store the `TcTypeEnv` in the
`CtOrigin` of the hole, then when you report the hole as an error you can
look at the type environment (better zonk it first) and print the types of
all locally bound identifiers. Or some. Or whatever.
>

That sounds like a very interesting idea, I will definitely look more at
this later. Thanks!

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5910#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Simon Peyton-Jones

RE: [GHC] #5910: Holes with other constraints

Replying by email because I'm on a train.

Dear xnyhps

Hmm. My intent was to allow typechecking to continue when there are holes (so compiling them, similar to {{{undefined}}}, to something like {{{throw#}}}). If I understand your suggestion correctly, we should abort compilation and show the hole's type as errors when an unresolved hole is found.

No, not at all. Your new stuff will integrate beautifully with -fdefer-type-errors. With this flag, TcErrors will build an error thunk for any unsolved constraints, thereby deferring the error until runtime just as you wanted. So you can use the holes as to-dos. Look at TcErrors.reportTidyWanteds, and note the call to deferToRuntime.

If you want to defer only *holes*, but not other type errors, until runtime, you’d need another flag, but I think as a first cut deferring *all* type errors (including holes) would do. Or alternatively you could by-default defer holes but not other errors. But then you’d still want a flag to say “don’t defer holes”.

I strongly urge you to use the TcErrors stuff. It does precisely what you want. If you don’t see how, ask more.

Simon

| -----Original Message-----

| From: [hidden email] [mailto:glasgow-haskell-bugs-

| [hidden email]] On Behalf Of GHC

| Sent: 05 March 2012 14:19

| Cc: [hidden email]

| Subject: Re: [GHC] #5910: Holes with other constraints

| #5910: Holes with other constraints

| ----------------------------------------+-----------------------------------

| Reporter: xnyhps | Owner:

| Type: feature request | Status: new

| Priority: normal | Milestone:

| Component: Compiler (Type checker) | Version: 7.5

| Keywords: holes | Os: Unknown/Multiple

| Architecture: Unknown/Multiple | Failure: Incorrect warning at compile-

| time

| Difficulty: Unknown | Testcase:

| Blockedby: | Blocking:

| Related: |

| ----------------------------------------+-----------------------------------

| Comment(by xnyhps):

| Replying to [comment:2 simonpj]:

| > Some brief responses. We may want a Skype chat.

| >

| > * I think the Right Way to do this is to add a new form of constraint,

| as you have done.

| >

| > * I do not see why you need `tcl_holes` in the `TcLclEnv`.

| Sorry, this was a relic from an earlier attempt. I thought I still needed

| it, but I don't. I'll update the patch (I want to make sure it can build

| stage1 as well).

| >

| > * The place to report the unsolved holes is '''not''' in `TcRnDriver`,

| but rather in `TcErrors`. It is a thing of beauty. The constraint solver

| tries to solve the constraints, ''returning an unsolved constraint''. The

| latter is passed to `reportUnsolved` and '''that''' is the place to report

| any unsolved holes.

| >

| The `TcRnDriver` stuff is definitely a placeholder, most of the stuff

| there should actually be a part of GHCi instead.

| > * Moreover, `TcErrors` ''already has'' a kind of error prioritisation:

| it does not report ambiguity errors if it any more important errors (such

| as holes) happen first: see `tryReporters` in `reportInsolsAndFlats`. So

| that will deal nicely with the problem you describe.

| >

| Hmm. My intent was to allow typechecking to continue when there are holes

| (so compiling them, similar to {{{undefined}}}, to something like

| {{{throw#}}}). If I understand your suggestion correctly, we should abort

| compilation and show the hole's type as errors when an unresolved hole is

| found.

| But maybe what I want it unfeasible to do "correctly" with classes. I

| suppose that to compile {{{show _h}}} (where {{{_h}}} is a hole) the

| compiler wants to have a concrete function to use as the show, but the

| {{{Show}}} constraint is still ambiguous due to it being on a hole

| therefore it can't find any instance to use.

| It seems useful to me to be able to test different parts of your code when

| you put in a hole. I see the holes as TODOs in the code, for parts you

| need to finish later while you work on other stuff first (though maybe it

| could be combined with the deferring of type errors to runtime? Haven't

| experimented with that myself, I just noticed it in the code).

| > * Finally, here's a fresh idea. If you store the `TcTypeEnv` in the

| `CtOrigin` of the hole, then when you report the hole as an error you can

| look at the type environment (better zonk it first) and print the types of

| all locally bound identifiers. Or some. Or whatever.

| >

| That sounds like a very interesting idea, I will definitely look more at

| this later. Thanks!

| --

| Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5910#comment:3>

| GHC <http://www.haskell.org/ghc/>

| The Glasgow Haskell Compiler

In reply to this post by GHC