[GHC] #5910: Holes with other constraints

[Simon Peyton-Jones]

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: glasgow-haskell-bugs-bounces at haskell.org [mailto:glasgow-haskell-bugs-

|  bounces at haskell.org] On Behalf Of GHC

|  Sent: 05 March 2012 14:19

|  Cc: glasgow-haskell-bugs at haskell.org

|  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

|

|  _______________________________________________

|  Glasgow-haskell-bugs mailing list

|  Glasgow-haskell-bugs at haskell.org

|  http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-bugs/attachments/20120306/cf487bb7/attachment-0001.htm>