Holes with other constraints

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.

Trac metadata

Trac field	Value
Version	7.5
Type	FeatureRequest
TypeOfFailure	IncorrectWarning
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture