[GHC] #5910: Holes with other constraints

[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