Holes with other constraints

changed weight to 5

added Tfeature request Trac import error messages typechecker labels

Attached file patch.diff (download).

Patch with my current changes.

Trac metadata

Trac field	Value
CC	→ leather@cs.uu.nl

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.
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.
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.
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.

So I think you can make your implementation able to do more, and yet have less code!

Simon

Replying to [ticket:5910#comment:59972 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!

Replying to [ticket:5910#comment:60020 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.

Replying to [ticket:5910#comment:60104 simonpj]:

Replying to [ticket:5910#comment:60020 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.

Thanks for the advice, I've been working on implementing this, and it is indeed a good way to report handle the compilation of holes. Instead of using -fdefer-type-errors, I've changed it so that holes are always deferred (maybe it's just me, but using ghci with -fdefer-type-errors on got annoying quite quickly, like having to print everything because otherwise it has a warning that the result is not in IO).

However, there's a one problem with this approach. The code that handles prioritization of errors and the code that handles deferring type erros to runtime, as far as I can tell, do different things to handle multiple errors: when -fdefer-type-errors is on, every error is reported and no prioritization is done. This also means that when just holes are deferred, the class ambiguity errors I initially had still happen. Do you have a suggestion on how to avoid this, other than always deferring all type errors?

Btw, I'm attaching an updated patch against a more recent version of HEAD. Some things were changed in the constraint solver that have been updated, the deferring to runtime works, and I changed the syntax to _?a for a hole named "a", _a was giving too many collisions with FFI generated code. It should now be possible to build stage1, stage2 and all libraries with it.

Attached file patch3.diff (download).

Replying to [ticket:5910#comment:60743 xnyhps]:

However, there's a one problem with this approach. The code that handles prioritization of errors and the code that handles deferring type erros to runtime, as far as I can tell, do different things to handle multiple errors: when -fdefer-type-errors is on, every error is reported and no prioritization is done. This also means that when just holes are deferred, the class ambiguity errors I initially had still happen. Do you have a suggestion on how to avoid this, other than always deferring all type errors?

Can you give me a concrete example, showing the behaviour you get, and the behaviour you want?

Do you have a separate flag to enable holes? I assume so.

Thanks. I’m pretty sure your proposed implementation is more complex than necessary. In particular, I don’t think you need all the mkHoleName and HoleTyCon stuff at all. This machinery is needed for implicit parameters for one reason only, namely so that

	f :: (?x :: Int) => Int -> Int

really has a different type to

	f :: Int -> Int -> Int

Functions in GHC have one type, the Core type, so we need to have enough, robust information in that type to recover the Haskell type. Hence (?x::Int) is a different type to Int, and we explicitly cast between them.

None of this is necessary for holes. They are not part of the Haskell language, and we do not abstract over them. So

The expression _?a really can have type alpha where alpha is a fresh unification variable.
You don't need HolePred in PredTree
You don't need any changes in TyCon, nor any of th complex stuff in mkHoleName.
You do still need CHoleCan; it's generated when you meet a hole _?a expression.

Would you like to try that simplification? That is, do NOT take implicit parameters as your guide!

I agree that you don't want -fdefer-type-errors just because you have holes. Just -XHoles should do, no?

Simon

Sorry for the delay.

Replying to [ticket:5910#comment:60748 simonpj]:

Replying to [ticket:5910#comment:60743 xnyhps]:

However, there's a one problem with this approach. The code that handles prioritization of errors and the code that handles deferring type erros to runtime, as far as I can tell, do different things to handle multiple errors: when -fdefer-type-errors is on, every error is reported and no prioritization is done. This also means that when just holes are deferred, the class ambiguity errors I initially had still happen. Do you have a suggestion on how to avoid this, other than always deferring all type errors?

Can you give me a concrete example, showing the behaviour you get, and the behaviour you want?

Do you have a separate flag to enable holes? I assume so.

This is still the example I'm working with:

test = show _?a

With -fdefer-type-errors, I see:

[1 of 1] Compiling Main             ( test.hs, interpreted )

test.hs:1:8: Warning:
    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)
    Note: there are several potential instances:
      instance Show Double -- Defined in `GHC.Float'
      instance Show Float -- Defined in `GHC.Float'
      instance Show () -- Defined in `GHC.Show'
      ...plus 24 others
    In the expression: show (_?a)
    In an equation for `test': test = show (_?a)

test.hs:1:13: Warning:
    Found hole _?a with type a0
    In the first argument of `show', namely `_?a'
    In the expression: show (_?a)
    In an equation for `test': test = show (_?a)
Ok, modules loaded: Main.

Makes sense. There's a hole, and a show for which it can not figure out what instance to use. Trying to run it will throw an exception with the first error. That's all good.

Without -fdefer-type-errors (but holes still get deferred):

[1 of 1] Compiling Main             ( test.hs, interpreted )

test.hs:1: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)
    Note: there are several potential instances:
      instance Show Double -- Defined in `GHC.Float'
      instance Show Float -- Defined in `GHC.Float'
      instance Show () -- Defined in `GHC.Show'
      ...plus 24 others
    In the expression: show (_?a)
    In an equation for `test': test = show (_?a)
Failed, modules loaded: none.

So the hole gets deferred, but all other type errors still exist and the prioritization of errors therefore does not remove this one. Somehow prioritizing first, and then deferring would also not be ideal, as then unrelated type errors in completely different could become hidden.

There is currently no flag yet to enable them, they're always on, but I do plan to add one. However, I'm hoping my changes to the core are noninvasive enough when not using holes that it would suffice to only use the flag to turn off the parsing of holes.

Replying to [ticket:5910#comment:60798 simonpj]:

Would you like to try that simplification? That is, do NOT take implicit parameters as your guide!

I'm going to look into this, thanks!

It seems to me that ambiguous types are the key problem here. We've been working on this a bit at UHac, but we haven't yet reached a solution.

Thijs has already mentioned the problem with:

show _?x

Paolo has also pointed out the following:

data Foo a = Foo a
data Bar1 = Bar1
data Bar2 = Bar2

instance Show (Foo Bar1) where
instance Show (Foo Bar2) where

test = show (Foo _?y)

What type do we get for the type of _?y? It appears unknowable.

Perhaps we can solve only part of the problem.

You might have to treat ambiguity errors in a special way. They can still be deferred with -fdefer-type-errors, and the error message adequately says there are two possible instances:

    No instance for (Show (Foo 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)
    Note: there are several potential instances:
      instance Show (Foo Bar1) -- Defined at Holes.hs:7:11
      instance Show (Foo Bar2) -- Defined at Holes.hs:8:11
    Possible fix: add an instance declaration for (Show (Foo a0))
    In the expression: show (Foo undefined)
    In an equation for `test': test = show (Foo undefined)

So maybe you could use this in the feedback for holes with an ambiguous type.

Do send a new patch with the simpler implementation I describe above.

Concernign this ambiguity stuff, what is the behaviour you want? A good way to articulate this woudl be to write the manual section for holes.

I imagine that what you want is:

A hole is always reported
A hole is treated like a type error; that is, reported as an error unless you use -fdefer-type-errors in which case you get a warning and a run-time error.
If there is a hole you probably want to suppress ambiguity errors; this prioritisation is done in TcErrors.reportInsolsAndFlats.

If you can say waht you want I think it'll be easy enough to achieve.

Simon

If -XHoles is set, we want the following:

The program should be type-checked as if every hole _?h is replaced by undefined, except:

* If type-checking would fail due to unsolved constraints that could be solved by giving a type to a hole.
If the program is well-typed, then:

* The types of all holes should be reported.

* Reporting the hole types should not cause type-checking (or compiling in general) to stop (in error).
(optional) If the program is ill-typed, then:

* The types of all holes should be reported.

The above should hold true with and without the monomorphism restriction. In particular, if an undefined somewhere in a program type-checked with the monomorphism restriction would cause type-checking to fail, then a hole in that same position should also cause type-checking to fail.

The type of a hole should be the resolved type with minimum constraints. That is, the type of a hole should only have constraints that have not be solved but are either inferred from the context (e.g. show _?h) or given in a type annotation/signature (e.g. _?h :: Show a => a.

Trac metadata

Trac field	Value
TypeOfFailure	IncorrectWarning → OtherFailure

I have transferred your proposed design to the Wiki page Holes.

But can you clarify? Under (2), are you saying that if I write

f x = _?foo

then you want the program to typecheck and run, even though it is incomplete? Isn't that what -fdefer-type-errors is for?

About the monomorphism restriction, can you give an example?

Ideally answer the questions by amplifying the spec on Holes, and adding examples to illustrate.

About the simpler implementation:

HoleName was unnecessary, I agree (right now a hole name includes the "_?", so it can never collide with the name of a variable). I've removed it.
I've thought about this a lot, and went through the code, but I'm still not sure about your advice about HolePred and HoleTyCon. Right now, tcExpr emits a constraint (which is just a Type) when encountering a hole. Without HoleTyCon, I'm not sure how to find out a constraint was a hole-constraint, which is needed for it to turn into an CHoleCan. classifyPredType will reduce anything it doesn't recognize to a IrredPred, in which case it never solves anything. canEvVar (with canHole) needs to see a HolePred to make it an CHoleCan.

(Do you perhaps mean: generate a fresh tyvar for every hole, and every time a hole is encountered, emit an Eq constraint between this tyvar and the type it needs at that location? In that case, a lot of what's added could be removed, even CHoleCan would not be needed anymore, but it would need a new way of reporting the holes as they are no longer separate constraints.)

About the original problem of ambiguous constraints:

We currently have a solution that uses tyVarsOfCt to find out which class-ambiguity errors apply to tyvars that also occur in hole-"errors", and automatically defers those as well. I'm not sure this is a very robust solution, but it seems to solve the problem.

Replying to [ticket:5910#comment:61250 simonpj]:

I have transferred your proposed design to the Wiki page Holes.

Good idea. Thanks!

About the monomorphism restriction, can you give an example?

Ideally answer the questions by amplifying the spec on Holes, and adding examples to illustrate.

We have revised the wiki page and added an example.

We have revised our statement about ambiguous types and the monomorphism restriction on Holes. I hope it is clear now.

Replying to [ticket:5910#comment:61373 xnyhps]:

I've thought about this a lot, and went through the code, but I'm still not sure about your advice about HolePred and HoleTyCon. Right now, tcExpr emits a constraint (which is just a Type) when encountering a hole. Without HoleTyCon, I'm not sure how to find out a constraint was a hole-constraint, which is needed for it to turn into an CHoleCan. classifyPredType will reduce anything it doesn't recognize to a IrredPred, in which case it never solves anything. canEvVar (with canHole) needs to see a HolePred to make it an CHoleCan.

No, I mean something very simple, roughly like this:

tcExpr (HoleExpr hole_name _) res_ty
 = do { loc <- getCtLoc (HoleOrigin hole_name)
      ; emitFlat (CHoleCan res_ty loc)
      ; return (HoleExpr hole_name res_ty) }

What is happening here is this:

We are type-checking a hole, expecting it to have type res_ty
Fine! We assume it does have that type (that is, no unification or whatnot)
But we emit a CHoleCan constraint which will later (in TcErrors) report that the hole _?x should have type res_ty.

And that's about all really. No messing with TyCons, no special predicates, nothing.

Now it is true that these hole constraints are a bit unusual in that they don't have evidence, and there isn't a PredType. But I don't think that will be hard: in the solver you just want to put them in the "frozen errors" set; indeed you can put them there right away. Currently we have emitFlat and emitImplication; just add emitInsoluble which adds to the wc_insol field of the WantedConstraints.

I think it's all delightfully simple. But of course I coudld be wrong.

I've added some questions to the wiki page

How hard would it be to implement a -fdefer-undefined-errors that would treat all undefined symbols as holes?

Then when you hit Ctrl+R to resolve them in Leksah we could include an option to add the missing function to the module (currently it will only add an import if the function is defined in a some other module). User types...

main = putStrLn hello

Which results in a warning that hello is undefined. They then they hit Ctrl+R and we would add...

hello :: String
hello = undefined

and select the word undefined in the above so they can start typing.

The problem with _? is we won't know when to include it until it is too late. We could just add _? to whatever the user is typing, but for all we know there could be a "hello" in scope and we might just be breaking valid code. Also what if the user deletes an existing function we have no way to know to add _? to the calling site to get a suitable type for the now missing function.

If we need the type for autocomplete we will get it if the symbol is undefined (because it will be treated as a hole). If it is defined we probably don't want to autocomplete, but if the user presses Ctrl+Space we can change "hello" to "hello_Leksah_Autocomplete" to get it.

mentioned in commit 8a9a7a8c

changed milestone to %7.8.1

changed weight to 7

Trac metadata

Trac field	Value
Priority	normal → high

OK, so holes are now in HEAD.

They lack

documentation
tests of any kind

Two more actions:

Sean or Thijs, could you add documentation and tests?
I think the idea of allowing undefined variables to turn into holes is a good one; so I'll leave the ticket open for that too.

changed milestone to %7.10.1

Bumping priority down (these tickets haven't been closely followed or fixed in 7.4), and moving out to 7.10 and out of 7.8.3.

Replying to [ticket:5910#comment:65198 simonpj]:

OK, so holes are now in HEAD.

They lack

documentation

tests of any kind

Two more actions:

Sean or Thijs, could you add documentation and tests?

I think the idea of allowing undefined variables to turn into holes is a good one; so I'll leave the ticket open for that too.

Did those tests ever get added? What is left to do here? See also #9091.

changed weight to 5

Trac metadata

Trac field	Value
Priority	high → normal

removed milestone

Moving to 7.12.1

mentioned in issue #10569 (closed)

changed milestone to %8.0.1

Milestone renamed

added typed holes label

added Pnormal label

It does not seem like this ticket is relevant anymore? I tried parsing through the messages and as far as I can see constraints are handled properly nowadays?

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

Holes with other constraints

Child items 0

Activity