Spurious ability check failure here

[pchiusano]

foo : forall g . ('{g} () ->{g} ()) -> Nat
foo g = todo g

wat : ('{IO} () ->{IO} ()) ->{} Nat
wat f = foo f

  The expression in red

                needs the abilities: {IO}
    but was assumed to only require: {}

  This is likely a result of using an un-annotated function as an argument with concrete abilities. Try adding an annotation to the function definition whose body is red.

     10 | wat f = foo f
                      ^-- error here

There seems to be no workaround (I tried putting annotations on f at the call site to no avail)

[pchiusano]

Some notes:

synthesizeWanted tm@(Term.Apps' f args) = do
  -- ->EEEEE
  (ft, fwant) <- synthesize f
  ctx <- getContext
  (vs, ft) <- ungeneralize' ft -- Is this line correct? Seems unnecessary, since synthesizeApp will unroll the forall
  (at, awant) <-
    scope (InFunctionCall vs f ft args) $
      synthesizeApps tm (apply ctx ft) args 
  (at,) <$> coalesceWanted awant fwant

The other thing is we will presumably end up here in synthesizeApp:

    go (Type.Arrow' i o0) = do
      -- ->App
      let (es, o) = Type.stripEffect o0
      (o,) <$> checkWantedScoped ((Just fun,) <$> es) arg i

Where we'll have f : ('{IO} () ->{IO} ()) and i will be ('{g} () ->{g} ()) for a fresh existential g.

This seems like it reduces to '{IO} () ->{IO} () <: '{g} () ->{g} (), which should typecheck with g solved to IO.

[dolio]

So, here's what I think is going on.

Eventually we do something like:

subtype ('{IO} () ->{IO} ()) ('{g} () ->{g} ())

This then eventually does two subtype calls:

subtype {g} {IO}
subtype {IO} {g}

in that order. The first one triggers defaulting g to the empty set, which is done in cases like this to prune 'slack' variables, I think. For instance, if we ran things in the opposite order, then I think the subtype {IO} {g} would turn g into {IO, g'}, then the other check would prune off the g'. But, in this case, the second check just fails after the first one gets pruned.

So, you might think, "just do the checks in the opposite order." But I think that just means you get the same error in the opposite scenario. Also, before anyone suggests {g} < {IO} => g = {IO}, that's exactly the sort of rule that the rewrite was supposed to eliminate.

One thing that might be possible is to delay ability subtyping until after the subtyping of the rest of the structure. Just collect up all the ability subtyping problems, and try to take advantage of having them all together. That way we could see that both {g} < {IO} and {IO} < {g} are desired, and just do g = {IO}. There are probably situations that aren't part of a single subtyping call that that wouldn't solve, but it might solve this one.

Edit: BTW, the above is only relatively easy for a single subtype check, I think. Some type checking does not go through a single subtype check, though. For instance, if the problem involved types like ('{g} () ->{g} ()) ->{g} T, but was otherwise similar, then the last of those g occurrences won't get processed in the same subtype check as the others, because it gets handled as part of checking the application foo f. I think this is less likely to cause problems, though.

[pchiusano]

Dan and I talked about this on a recent call. At first I was thinking "let's get rid of the slack variables" and instead do #3753. But @dolio pointed out that repeated subtype checks are fairly common and it's nice to come up with the "right" row type via incremental refinement.

My other idea which we didn't really get to explore is to have "open" row types be more of a first class concept in the typechecker. Right now, we have only "closed" row types, with the "openness" represented using slack variables. This leads to proliferation of slack variables, which we try to clean up, but then that causes problems in cases like this ticket.

If however, an "open" row type is represented explicitly, we could have a typing judgement which says that that open row types can be extended by a subtype check, if there are no matches in the existing set. Thus, you never create slack variables in a row type, only solved type variables. It's possible this will be better behaved, but needs more exploration.