Type Hole Inference (post merge)

[RaefM]

No description provided.

[RaefM]

Not sure what this cursor inspector message means?

That text pops up when the occurs check fails (so whenever a pts is a proper subset of itself, eg being solved as T and Int -> T)
I'm definitely open to other text there, I figured 'occurs check failed' doesn't tell all that much and had gone with 'inferred type refers to self' to indicate the solution set recurses on itself and is thus not valid

Can we show the two possibilities here? Why is it only showing Int -> T?

Sorry for the wall of text; tldr, fixed with new behavior illustrated below

So after unification, it's solved as pts = {?, T, Int ->(pts)}. The occurs check as implemented makes it so that becomes {?, T, Int -> ?} and the general filtering rule for making suggestions out of ptses is to prefer 'non-nodes' over nodes if possible (which is anything that isn't a plain var or hole)- that filters it down to Int -> ?

The 'solution' in this case would be the set {T, Int -> T, Int -> Int -> T, ...}. Our filtering rules reads to Int -> T, where the issue is detected, and replaces T with ?.

Before ADTs were added, so when the occurs failure could only happen on holes (eg ? or Int -> ?), saying ? was always useless so we'd just suggest Int -> ? while marking occurs failing ptses as unsolved. With type variables, (T vs Int -> T) the two possibilities are each valid suggestions as they are inconsistent with one another.

To facilitate this, changing the filtering so that when it comes to type variables, keep at least one when filtering the pts if the occurs check has failed. When occurs hasn't failed, still filtering all type variables is non hole/var alternatives exist (eg Z, Int -> T will have the suggestion Int -> T, and A, Int will have the suggestion Int)

Some suggestions based on this handling:

[cyrus-]

@RaefM @anandrav this needs a merge with dev

[cyrus-]

Seems to be a bug here:

[cyrus-]

Possibly downstream of above bug, but was expecting this to be [Int], not an error.

[cyrus-]

Probably also related but this should be a conflict but it's solving it as [?]:

[cyrus-]

When I Tab-expand on this I get [] which is a syntax error rather than [?]:

[cyrus-]

@RaefM I think there must be a bug in your recent fixes -- the following should certainly not infer [T], as neither A nor B are used anywhere!

Also still seeing this issue where there isn't a conflict arising from the conflicted patterns:

[cyrus-]

Another probably related one that is behaving weirdly:

[thomasporter522]

After re-uploading, Cyrus's identified errors are mostly solved. The exceptions are:

• Tab-expanding the suggestion here still produces [], which is a syntax error.

• ADTs appear to be converted into binary sums at some point, which are wrongly displayed and suggested to the user.

[thomasporter522]

Here's another odd bug:

[thomasporter522]

Also maybe we don't want to offer this suggestion.

[thomasporter522]

Adding constructor names was easy, thanks to the well-factored code. This works fine:

And this gives an inconsistency, as desired.

However, the error information is wrong. The ? constructors are my own doing, as a placeholder.

[thomasporter522]

I understand why this is the error message we give, but I think it's unintuitive. Is there a better way to convey this? Either just having the type holes in the message be red, or actually showing the two different arrow types? The latter would allow the user to select which one they want and resume bidirectional checking.

There is also the potentially appealing possibility of displaying potential type sets in full, as nested lists of options. For example, if the PTS is {Num , Arrow({Num, Bool}, {Num, Bool})}, the user could hover over any element listed between a pair of {...}, including the sublists, rather than inconsistent sublists being displayed as a hole.

There are a couple of issues with this. The first is that if the user selects a sub-option, like the second "Num" in the text example, it is not determinate what entire type they are selecting. Do they mean Arrow(Num, Num) or Arrow(Num, Bool)? Should we just treat it as Arrow(Num, Hole)? What if the user wants to specify both sides? Maybe we could have a tree of drop downs, but that's surely far too complex.

The second issue is that a PTS is in fact a lossy representation of the set of potential types for a hole. In the image example, the two constrained fillings for the type hole are {Arrow(Num,Bool), Arrow(Bool,Num)}, and if this is collapsed to Arrow({Num, Bool}, {Num, Bool}), the original possibilities may not be recovered, without also including Arrow(Num,Num) and Arrow(Bool,Bool).

In light of these two issues, might it be better to forgo merging inconsistent potential types? The principal disadvantage would be the loss of compactness, and now we reach an empirical matter, but I think that merging only consistent types (which needs further specification since consistency isn't transitive) would recover much of the compactness of the general scheme, and that remaining examples would probably produce moderately sized sets most of the time. To the first point, the example of a combinatorically explosive set of types in the old draft consists of six pairwise consistent types: and thus they could be compressed to one inconsistency-free type. To the second, the number of potential types grows multiplicatively, but only upon the inclusion of other type holes, and only by the number of different type constructors as which these type holes are used.

I don't doubt that it is easy to construct cases in which this "consistent representation" is too big a set. Maybe we could pragmatically compute both the compact and the consistent representations, and display the consistent one preferentially, and the compact one if the consistent one is larger than some predefined limit and larger than the compact one.

This was a bit of a ramble, sorry. Thoughts welcome.