When using forall in the type of a parameter of a returned function other types get confused

[snoble]

I've tried to simplify this a bunch. It's possible this could be related to #264, or I might have just come across this at the same time.

package SubsumeTest

def restructure(input: String, f: String -> TupleCons[String, TupleCons[(forall ss. List[ss] -> Int) -> Int, Unit]]) -> String:
  (output, _) = f(input)
  output

results in the error

in file: /home/steven/Code/bosatsu2/test_workspace/subsume_test_case.bosatsu, package SubsumeTest, type ?a
2|
3|def restructure(input: String, f: String -> TupleCons[String, TupleCons[(forall ss. List[ss] -> Int) -> Int, Unit]]) -> String:
4|  (output, _) = f(input)
                  ^^^^^^^^

does not subsume type forall ss. Bosatsu/Predef::List[ss] -> Bosatsu/Predef::Int
3|def restructure(input: String, f: String -> TupleCons[String, TupleCons[(forall ss. List[ss] -> Int) -> Int, Unit]]) -> String:
4|  (output, _) = f(input)
5|  output
    ^^^^^^

It looks like output is getting assigned the function that f returns instead of the string

[snoble]

If you don't mind I'll take a stab at trying to fix this. I assume this isn't the sort of thing a lot of people will stumble on if it takes me a little longer

[snoble]

of course if you see a bug in my bosatsu code I'd be interested

[johnynek]

Your code looks right but the explicit use of TupleCons makes it harder for me to read. This looks like a bug to me. Thanks for taking a look at fixing it. Finding that error message in the code is a good first step.

[snoble]

Oh, yeah. I switched to TupleCons to test if maybe it was the tuple syntax stuff

[johnynek]

is the function needed on this bug? Can you repro just with (String, (forall a. List[a] -> Int) -> Int) then matching on that?

If you do need a function, can you get rid of the String input and just call with a constant f("Hello").

[snoble]

I've reduced this to

package SubsumeTest
struct Wrap(y1)
def foo(cra_fn: (forall ss. List[ss]) -> Int):
  _ = Wrap(cra_fn)
  2

or

package SubsumeTest
struct Wrap(y1)
def foo(cra_fn: Wrap[(forall ss. List[ss]) -> Int]):
  Wrap(_) = cra_fn
  2

I think both are the same bug. It seems to have something to do with unifyFn will assign to a meta a Type.Fn with two more metas as parameters. But when that first parameter meta is unified it gets set to SkolemVar. But I can't tell how it could be any different since writeMeta has a comment that it's not supposed to write types with ForAlls. But weirdly this is not a problem if the second parameter to Type.Fn is a Type.ForAll

Definitely open to solutions if you can see it

[snoble]

If you just have a Let without the Wrap it also works

[johnynek]

In the second parameter in Fn it is covariant, which comes into play with skolemization IIRC. The first parameter is contravariant.

That seems like it’s probably related to the bug.

[snoble]

Oooooh. Good lead

[snoble]

Making sure I can reproduce without using structs at all

package SubsumeTest
def bar(var_fn: x -> Int) -> Int:
  2
def foo(cra_fn: (forall ssss. ssss -> String) -> Int) -> Int:
  y1 = bar(cra_fn)
  3

gives

in file: /home/steven/Code/bosatsu2/test_workspace/subsume_test_case3.bosatsu, package SubsumeTest, type ?a does not subsume type forall ssss. ssss -> Bosatsu/Predef::String
5|
6|def foo(cra_fn: (forall ssss. ssss -> String) -> Int) -> Int:
7|  y1 = bar(cra_fn)
             ^^^^^^

[johnynek]

Well that seems like a case the paper should cover. It would be interesting to take that example on the code before I added Variance support and see if it passed then.

[snoble]

I have a new hypothesis but my understanding isn't deep enough to verify yet.

My theory is that extendVarEnv might have some unstated invariant on the ty it is passed. The reason why I think this is that if you look at the comment in instSigma it is saying that t2 is in weak-prenex form and tcRho (Var v) exp_ty calls instSigma with pretty much anything that's in the variable env

So my hypothesis would be that when the bosatsu code calls extendEnv while going through the top level Lets (https://github.com/johnynek/bosatsu/blob/0984ec5976f61c106e8971ce2039d23a2332ede3/core/src/main/scala/org/bykn/bosatsu/rankn/Infer.scala#L1183) that this unstated invariant isn't satisfied.

I've clumsily written some code such that typeCheckMeta returns a tuple of its original result as well as the direct output of inferSigmaMeta and then called extendEnv with the latter. That produced a lot of failed tests and failed on the Predef, so it was less than successful.

[johnynek]

ahh, this is very interesting.... yes, this does look like a place where the invariant is failed...

MOAR TYPES!!!

We probably need tests and maybe types that track weak-prenex form...

That said... maybe this isn't a real problem, because the type we are adding is an inferred type, and maybe all the inferred type are in weak-prenex form?

In any case, it would could write a function which the paper calls pr to put things in weak-prenex form, and do that as we add the lets.

[johnynek]

we could also just add a thing to assert that we are in weak-prenex form, and then see what tests fail (or try to make some fail).

[snoble]

Something that supports this theory (but not as cleanly as I would like) is when I type check

package SubsumeTest

def wrap(k: int):
  def bar(var_fn: ttt -> Int) -> Int:
    2

  def foo(cra_fn: (forall ssss. ssss -> String) -> Int) -> Int:
    y1 = bar(cra_fn)
    3
  k

I get a different type error than previously. Now I get

in file: /home/steven/Code/bosatsu2/test_workspace/subsume_test_case3.bosatsu, package SubsumeTest, type $ttt2 does not unify with type ?a -> ?b
6|
7|  def foo(cra_fn: (forall ssss. ssss -> String) -> Int) -> Int:
8|    y1 = bar(cra_fn)
               ^^^^^^

The change in error is that bar in the environment now has type

TyApply(TyApply(TyConst(Defined(PackageName(NonEmptyList(Bosatsu, Predef)),TypeName(Constructor(Fn)))),TyApply(TyApply(TyConst(Defined(PackageName(NonEmptyList(Bosatsu, Predef)),TypeName(Constructor(Fn)))),TyVar(Skolem(ttt,2))),TyConst(Defined(PackageName(NonEmptyList(Bosatsu, Predef)),TypeName(Constructor(Int)))))),TyConst(Defined(PackageName(NonEmptyList(Bosatsu, Predef)),TypeName(Constructor(Int)))))

vs

ForAll(NonEmptyList(Bound(a)),TyApply(TyApply(TyConst(Defined(PackageName(NonEmptyList(Bosatsu, Predef)),TypeName(Constructor(Fn)))),TyApply(TyApply(TyConst(Defined(PackageName(NonEmptyList(Bosatsu, Predef)),TypeName(Constructor(Fn)))),TyVar(Bound(a))),TyConst(Defined(PackageName(NonEmptyList(Bosatsu, Predef)),TypeName(Constructor(Int)))))),TyConst(Defined(PackageName(NonEmptyList(Bosatsu, Predef)),TypeName(Constructor(Int))))))

That is, when it is nested the Bound is Skolem and we lose the ForAll... which is essentially skolemized?

[johnynek]

https://github.com/johnynek/bosatsu/blob/0984ec5976f61c106e8971ce2039d23a2332ede3/core/src/main/scala/org/bykn/bosatsu/rankn/Infer.scala#L1149

actually, wouldn't that only create types in weak-prenex form? We only ever add a top-level forall. Seems like it should... but maybe not...

We could assert at that point or convert at that point.

[johnynek]

okay, that's a good kind of test. We expect them to give the same errors (or at least fail in the same places).

This is also an area the paper does not cover: how to handle syntactic issues. The whole, skolemizeFreeVars is something I cooked up. So, that is a definitely place to look for invariant violations.

[snoble]

Oh interesting. I'll look for pr.

I don't really understand weak-prenex enough. Is there a relationship between weak-prenex and rho?

[snoble]

I guess the question is, is it ok to have unbound Metas in the environment? Or should they be skolems (which... of course causes me a different error)

[snoble]

Oh, nevermind. You don't have unbound Metas in there. That's the whole point of the outer ForAll and replacing them with Bounds

[snoble]

ok, back to the same error if I do

package SubsumeTest

def wrap(k: Int):
  (bar: forall ttt. (ttt -> String) -> Int) = \fn -> 2

  def foo(cra_fn: (forall ssss. ssss -> String) -> Int) -> Int:
    y1 = bar(cra_fn)
    3
  k

I get

in file: /home/steven/Code/bosatsu2/test_workspace/subsume_test_case3.bosatsu, package SubsumeTest, type ?a does not subsume type forall ssss. ssss -> Bosatsu/Predef::String
5|
6|  def foo(cra_fn: (forall ssss. ssss -> String) -> Int) -> Int:
7|    y1 = bar(cra_fn)
               ^^^^^^

It keeps coming back to what to do when testing if an unbound Meta subsumes something that contains a ForAll

[johnynek]

those are two different types. Do you mean that? the parens are in different places. If you make them exactly the same type, does it pass?

That said, those two types maybe should be the same, since (a -> b) -> c is covariant in a, so I think we should be able to lift the forall out... unless I'm wrong about that...

[johnynek]

wait, no, we can't lift the forall out of the first parameter, so it gets stuck there, they are different.

[snoble]

The more I try to come up with applications that this bug restricts I keep coming back to this comment https://github.com/johnynek/bosatsu/pull/269#issuecomment-497995921

Even this example that has no constructors, has the type Fn[a,b], and is trying to create one with a polytype for a.

I originally ran into this problem because I had a function that returned multiple values, one of which is a polymorphic function, and I was being lazy and was returning them via a tuple. If I created a return value struct I think this problem goes away

The other example I tried to cook up using an Option is really the same thing

package SubsumeTest

def lengths(l1: List[Int], l2: List[String], maybeFn: Option[forall tt. List[tt] -> Int]):
  match maybeFn:
    Some(fn: forall tt. List[tt]): fn(l1).add(fn(l2))
    None: 0

I'm starting to think this bug is really just a matter of having a better error message

[snoble]

I think you'd probably solve the previous with

package SubsumeTest

struct LengthFunction(lf: forall tt. List[tt] -> Int)
def length(LengthFunction(fn), x: List[t]): fn(x)

def lengths(l1: List[Int], l2: List[String], maybeFn: Option[LengthFunction]):
  match maybeFn:
    Some(lf): lf.length(l1).add(lf.length(l2))
    None: 0

It means users can end up with weird errors with weird solutions if they are trying to push the limits of the type system

[snoble]

Even this example that has no constructors, has the type Fn[a,b], and is trying to create one with a polytype for a.

This statement isn't quite right. You can obviously have a Fn[a,b] where a is polymorphic. I'm guessing the struct free example is a case of the underlying predicativity constraint

[snoble]

and to totally close the loop, the original example could be refactored to this

package SubsumeTest

struct ReturnStruct[shape](str: String, fn: (forall ss. shape[ss] -> Int) -> Int)

def restructure(input: String, f: String -> ReturnStruct[shape]) -> String:
  ReturnStruct(output, _) = f(input)
  output

[snoble]

Thinking a bit about work arounds. We've seen we can't do

(fn: forall k. k -> Option[k]) = \x -> Some(x)
foo = Some(fn)

but we can do

struct Wrap(fn: forall k. k -> Option[k])
(fn: forall k. k -> Option[k]) = \x -> Some(x)
foo = Some(Wrap(fn))

and we probably even do

struct Wrap[t](fn: forall k. k -> t[k])
(fn: forall k. k -> Option[k]) = \x -> Some(x)
foo = Some(Wrap(fn))

plus we can make

def applyWrap(Wrap(fn), x):
  fn(x)

which would let us do

struct Wrap[t](fn: forall k. k -> t[k])

def higherOrder(g: String -> Option[String]):
  g("bar")
(fn: forall k. k -> Option[k]) = \x -> Some(x)
foo = Some(Wrap(fn))

def applyWrap(Wrap(fn), x):
  fn(x)

main = match foo:
  case None: None
  case Some(wrapped): higherOrder(wrapped.applyWrap)

The tricky question is could we remove Wrap and applyWrap from the code and infer when they are needed? Alternatively, if they can't be inferred, can there be syntax for them that feels natural?

I also wonder if we can do struct Wrap[t1, t2](fn: forall k. t1[k] -> t2[k])

[johnynek]

okay, I poked at a couple of these examples. At least some of the examples are actual flaws in the paper's type system.

I think #650 is an algorithm that at least partially addresses it.