IR Typing: IR Translation of concatMap is unsound, misses type application

[frank-emrich]

The IR typechecker caught the following problem:

The IR version of concatMap from the Links prelude is as follows. Here, 234 is the variable bound to the function, which has the polymorphic type forall a::(Any,Any),b::Row,c.((a::Any) ~b~> [c], [a::Any]) ~b~> [c]

`Rec ([((234,
           (forall a::(Any,Any),b::Row,c.((a::Any) ~b~> [c], [a::Any]) ~b~> [c],
            "concatMap", `Global)),
          ([(655, (`Any, `Any), `Type (...));
             (662, (`Unl, `Any), `Row (...));
             (663, (`Unl, `Any), `Type (...))],
           [(232, ((_::Any) ~> [_], "", `Local));
             (233, ([_::Any], "", `Local))],
           ([`Let (((230, ([_::Any], "l", `Local)),
                    ([], `Return (`Variable (233)))));
              `Let (((231, ((_::Any) ~> [_], "f", `Local)),
                     ([], `Return (`Variable (232)))));
              `Let (((237, ([_::Any], "", `Local)),
                     ([], `Return (`Variable (230)))))
              ],
            `If ((`ApplyPure ((`TApp ((`Variable (13),
                                       [`Type (`MetaTypeVar (...));
                                         `Row (({}, ..., false))])),
                               [`Variable (237);
                                 `TApp ((`Variable (55),
                                         [`Type (`MetaTypeVar (...))]))
                                 ])),
                  ([],
                   `Return (`TApp ((`Variable (55),
                                    [`Type (`MetaTypeVar (...))])))),
                  ([`Let (((238, (_::Any, "", `Local)),
                           ([],
                            `Apply ((`TApp ((`Variable (58),
                                             [`Type (`MetaTypeVar (...));
                                               `Row (({}, ..., false))])),
                                     [`Variable (237)])))));
                     `Let (((239, ([_::Any], "", `Local)),
                            ([],
                             `Apply ((`TApp ((`Variable (59),
                                              [`Type (`MetaTypeVar (...));
                                                `Row (({}, ..., false))])),
                                      [`Variable (237)])))));
                     `Let (((236, ([_::Any], "tl", `Local)),
                            ([], `Return (`Variable (239)))));
                     `Let (((235, (_::Any, "hd", `Local)),
                            ([], `Return (`Variable (238)))));
                     `Let (((241, ([_], "", `Local)),
                            ([],
                             `Apply ((`Variable (231), [`Variable (235)])))));
                     `Let (((240, ([_], "", `Local)),
                            ([],
                             `Apply ((`Variable (234),
                                      [`Variable (231); `Variable (236)])))))
                     ],
                   `Return (`ApplyPure ((`TApp ((`Variable (57),
                                                 [`Type (`MetaTypeVar (...));
                                                   `Row (({}, ..., false))])),
                                         [`Variable (241); `Variable (240)])))))))),
None, `Unknown)]);

The erroneous part is

`Apply ((`Variable (234),
           [`Variable (231); `Variable (236)]))

denoting the recursive call in concatMap.
Since the function is polymorphic, there must be a type application happening beforehand.

[jamescheney]

Might be easier to localize the problem in typechecking/desugaring by deleting parts of concatMap until the error goes away. E.g. does

fun concatMap'(f, l) {
  switch (l) {
    case hd::tl -> concatMap'(f, tl)
  }
}

have the same problem? If so, what about

fun concatMap''(f, l) {
  concatMap''(f, tl)
}

(or indeed why doesn't any other recursive function have the same problem?)

[frank-emrich]

Good call. Actually, even

fun foo(f) { foo(f) }

has the same problem. Howver, it's not the case that we never emit type applications. I'll investigate it further.

[jstolarek]

Test added in 9a2880c. Closing.