[GHC] #5910: Holes with other constraints

[GHC]

#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