DesugarInners cannot supply proper type args for calls to mutually recursive, polymorphic functions

[frank-emrich]

Consider the following program:

mutual {
  fun f1() {
    ()
  }

  fun f2() {
    f1()
  }
}

This translates to the following, ill-typed IR:

  (Ir.Rec
     [{ Ir.fn_binder =
        (229, (forall 362::Row.() ~362~> (), "f1", Var.Scope.Global));
        fn_tyvars =
        [(362,
          (CommonTypes.PrimaryKind.Row,
           (CommonTypes.Linearity.Unl, CommonTypes.Restriction.Any)))
          ];
        fn_params = []; fn_body = ([], (Ir.Return (Ir.Extend ({}, None))));
        fn_closure = None; fn_location = CommonTypes.Location.Unknown;
        fn_unsafe = false };
       { Ir.fn_binder =
         (228, (forall 362::Row.() ~362~> (), "f2", Var.Scope.Global));
         fn_tyvars =
         [(362,
           (CommonTypes.PrimaryKind.Row,
            (CommonTypes.Linearity.Unl, CommonTypes.Restriction.Any)))
           ];
         fn_params = [];
         fn_body =
         ([], (Ir.Apply ((Ir.TApp ((Ir.Variable 229), [{ |%363 }])), [])));     (* <-- bug here  *)
         fn_closure = None; fn_location = CommonTypes.Location.Unknown;
         fn_unsafe = false }
       ])

This is ill-typed because in type application Ir.TApp ((Ir.Variable 229), [{ |%363 }]) we supply a fresh flexible variable in place for f1's effects, which means that the subsequent call fails due to mismatching effects.

The problem is DesugarInners, which supplies type arguments to recursive functions. However, this only seems to work if a recursive function calls itself. Otherwise, DesugarInners uses fresh flexible variables in place for the necessary type arguments. This leads to ill-typed program above and is documented in a comment on add_extras in DesugarInners.

It seems that in the current design, at the point when we reach DesugarInners, the necessary information about what arguments to supply does not exist in the AST.

[kwanghoon]

@frank-emrich Maybe I am lost, but the example is successfully IR-typechecked in my run.

(Ir.Rec
     [{ Ir.fn_binder =
        (229, (forall 460::Row.() ~460~> (), "f1", Var.Scope.Global));
        fn_tyvars =
        [(460,
          (CommonTypes.PrimaryKind.Row,
           (CommonTypes.Linearity.Unl, CommonTypes.Restriction.Any)))
          ];
        fn_params = []; fn_body = ([], (Ir.Return (Ir.Extend ({}, None))));
        fn_closure = None; fn_location = CommonTypes.Location.Unknown;
        fn_unsafe = false };
       { Ir.fn_binder =
         (228, (forall 461::Row.() ~461~> (), "f2", Var.Scope.Global));
         fn_tyvars =
         [(461,
           (CommonTypes.PrimaryKind.Row,
            (CommonTypes.Linearity.Unl, CommonTypes.Restriction.Any)))
           ];
         fn_params = [];
         fn_body =
         ([], (Ir.Apply ((Ir.TApp ((Ir.Variable 229), [{ |461 }])), []))); (* <-- Isn't this what you want?  *)
         fn_closure = None; fn_location = CommonTypes.Location.Unknown;
         fn_unsafe = false }
       ])

The source code I am using is

commit 761c6935d4549af6176fc3ead7fcf85a9a80d222 (origin/master)
Author: Daniel Hillerström <1827113+dhil@users.noreply.github.com>
Date:   Thu Jun 3 09:45:21 2021 +0100

[frank-emrich]

Thanks for looking into this! :)

It looks like your IR snippet indeed doesn't have this bug, which is quite mysterious. I'm using the same commit 761c6935d, using the following config file, with no other options set:

prelude=tests/empty_prelude.links
typecheck_ir=true
fail_on_ir_type_error=true

show_raw_type_vars=true
hide_fresh_type_vars=false
show_flavours=true
show_quantifiers=true
show_compiled_ir=true

Further, I'm executing the program above as a file (i.e., not calling links with -e, not executing it from the REPL).

[kwanghoon]

Here is my configuration for my run. (I got this somewhere in IR typing discussion.)

typecheck_ir=true
fail_on_ir_type_error=true
prelude=../links/tests/empty_prelude.links
optimise=false
debug=true
print_types_pretty=true
recheck_frontend_transformations=true
hide_fresh_type_vars=false
show_flavours=true
show_quantifiers=true
show_raw_type_vars=true

[dhil]

Using the same commit, I get the same result as Frank's output

./links -d --set=show_compiled_ir=true --set=prelude=empty.links --set=show_flavours=true --set=show_raw_type_vars=true --set=hide_fresh_type_vars=false --set=show_quantifiers=true frank.links
registering driver for null
([], (Ir.Return (Ir.Extend ({}, None))))
Finishing process MAIN
([(Ir.Rec
     [{ Ir.fn_binder =
        (229, (forall 362::Row.() ~362~> (), "f1", Var.Scope.Global));
        fn_tyvars =
        [(362,
          (CommonTypes.PrimaryKind.Row,
           (CommonTypes.Linearity.Unl, CommonTypes.Restriction.Any)))
          ];
        fn_params = []; fn_body = ([], (Ir.Return (Ir.Extend ({}, None))));
        fn_closure = None; fn_location = CommonTypes.Location.Unknown;
        fn_unsafe = false };
       { Ir.fn_binder =
         (228, (forall 362::Row.() ~362~> (), "f2", Var.Scope.Global));
         fn_tyvars =
         [(362,
           (CommonTypes.PrimaryKind.Row,
            (CommonTypes.Linearity.Unl, CommonTypes.Restriction.Any)))
           ];
         fn_params = [];
         fn_body =
         ([], (Ir.Apply ((Ir.TApp ((Ir.Variable 229), [{ |%363 }])), [])));
         fn_closure = None; fn_location = CommonTypes.Location.Unknown;
         fn_unsafe = false }
       ])
   ],
 (Ir.Return (Ir.Extend ({}, None))))
Finishing process MAIN
() : ()

[dhil]

When I enable recheck_frontend_transformations, then I get the same result as @kwanghoon

./links -d --set=show_compiled_ir=true --set=prelude=empty.links --set=show_flavours=true --set=show_raw_type_vars=true --set=hide_fresh_type_vars=false --set=show_quantifiers=true --set=recheck_frontend_transformations=true frank.links
registering driver for null
([], (Ir.Return (Ir.Extend ({}, None))))
Finishing process MAIN
([(Ir.Rec
     [{ Ir.fn_binder =
        (229, (forall 460::Row.() ~460~> (), "f1", Var.Scope.Global));
        fn_tyvars =
        [(460,
          (CommonTypes.PrimaryKind.Row,
           (CommonTypes.Linearity.Unl, CommonTypes.Restriction.Any)))
          ];
        fn_params = []; fn_body = ([], (Ir.Return (Ir.Extend ({}, None))));
        fn_closure = None; fn_location = CommonTypes.Location.Unknown;
        fn_unsafe = false };
       { Ir.fn_binder =
         (228, (forall 461::Row.() ~461~> (), "f2", Var.Scope.Global));
         fn_tyvars =
         [(461,
           (CommonTypes.PrimaryKind.Row,
            (CommonTypes.Linearity.Unl, CommonTypes.Restriction.Any)))
           ];
         fn_params = [];
         fn_body =
         ([], (Ir.Apply ((Ir.TApp ((Ir.Variable 229), [{ |461 }])), [])));
         fn_closure = None; fn_location = CommonTypes.Location.Unknown;
         fn_unsafe = false }
       ])
   ],
 (Ir.Return (Ir.Extend ({}, None))))
Finishing process MAIN
() : ()

[kwanghoon]

I ran with a command with a file as

• links --config=./config_example ./desugarinners.links

[dhil]

If I recall correctly, recheck_frontend_transformations=true causes the type checker to be run multiple times. I am guessing that during one of the subsequent runs the flexible variable gets generalised.

[jamescheney]

I think we already encountered situations where type checking/inference is not idempotent (cf #732), i.e. rerunning it on something gives different results, and there is discussion that it would be desirable to have a separate typechecker that just typechecks using the inferred annotations (and maybe other invariants) without doing any inference or unification per se. This would be (a) faster than rerunning type inference many times when recheck_frontend_transformations=true and (b) helpful as a separate specification of what we expect type inference to do. We don't currently have an issue for this but perhaps it could be a fun larger project for an enterprising intern.