Incomplete rows can trigger an internal error

[dhil]

The following program triggers an internal error in the type checker (during the construction of an error message).

typename S(e::Eff) = () ~e~> ();

sig r : (S({ |e})) {R:(S( { R{_} |e})) => () | e}~> ()
fun r(x) { do R(x) }

The problem with this program is that the formal parameter type of r doesn't mention R. However, at the time of writing Links produces the following internal error when type checking this program (with effect_sugar=false).

Raised at Links_core__Types.extract_row in file "core/types.ml", line 1793, characters 5-201
Called from Links_core__TypeSugar.Gripers.do_operation in file "core/typeSugar.ml", line 692, characters 47-73
Called from Links_core__TypeSugar.type_check in file "core/typeSugar.ml", line 4293, characters 12-78
Called from Links_core__TypeSugar.type_check in file "core/typeSugar.ml", line 3849, characters 20-83
Called from Links_core__TypeSugar.type_binding in file "core/typeSugar.ml", line 4530, characters 21-72
Called from Links_core__TypeSugar.type_bindings.(fun) in file "core/typeSugar.ml", line 4932, characters 37-104
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Links_core__TypeSugar.type_bindings in file "core/typeSugar.ml", line 4930, characters 4-420
Called from Links_core__TypeSugar.Check.program in file "core/typeSugar.ml", line 5128, characters 32-60
Called from Links_core__Frontend.transform in file "core/frontend.ml", line 316, characters 4-64
Called from Dune__exe__Driver.Phases.whole_program in file "bin/driver.ml", line 165, characters 6-61
Called from Dune__exe__Repl.directives.(fun) in file "bin/repl.ml", line 201, characters 21-65
Called from CamlinternalLazy.force_lazy_block in file "camlinternalLazy.ml", line 31, characters 17-27
Re-raised at CamlinternalLazy.force_lazy_block in file "camlinternalLazy.ml", line 36, characters 4-11
Called from Links_core__Errors.display in file "core/errors.ml", line 218, characters 9-21
***: Error: Links_core.Types.TypeDestructionError("Internal error: attempt to extract a row from a datatype that is not a row container: (Types.Operation\n   ((Types.Record\n       (Types.Row\n          ({1 => (Types.Present\n                    (Types.Alias\n                       (CommonTypes.PrimaryKind.Type,\n                        (\"S\",\n                         [(CommonTypes.PrimaryKind.Row,\n                           (CommonTypes.Linearity.Unl,\n                            CommonTypes.Restriction.Effect))\n                           ],\n                         [(CommonTypes.PrimaryKind.Row,\n                           (Types.Row\n                              ({R => (Types.Meta\n                                        Point @ 0x7f8c832b2d58 (Types.Var\n                                                                  (7838,\n                                                                   (CommonTypes.PrimaryKind.Presence,\n                                                                    (\n                                                                    CommonTypes.Linearity.Unl,\n                                                                    CommonTypes.Restriction.Any)),\n                                                                   `Rigid)));\n                                },\n                               Point @ 0x7f8c832b35e0 (Types.Var\n                                                         (7837,\n                                                          (CommonTypes.PrimaryKind.Row,\n                                                           (CommonTypes.Linearity.Unl,\n                                                            CommonTypes.Restriction.Any)),\n                                                          `Rigid)),\n                               false)))\n                           ],\n                         false),\n                        (Types.Function\n                           ((Types.Record\n                               (Types.Row\n                                  ({}, Point @ 0x7f8c82a18940 Types.Closed,\n                                   false))),\n                            (Types.Row\n                               ({R => (Types.Meta\n                                         Point @ 0x7f8c832b2d58 (Types.Var\n                                                                   (7838,\n                                                                    (\n                                                                    CommonTypes.PrimaryKind.Presence,\n                                                                    (\n                                                                    CommonTypes.Linearity.Unl,\n                                                                    CommonTypes.Restriction.Any)),\n                                                                    `Rigid)));\n                                 wild => (Types.Present\n                                            (Types.Record\n                                               (Types.Row\n                                                  ({},\n                                                   Point @ 0x7f8c82a18940 Types.Closed,\n                                                   false))));\n                                 },\n                                Point @ 0x7f8c832b35e0 (Types.Var\n                                                          (7837,\n                                                           (CommonTypes.PrimaryKind.Row,\n                                                            (CommonTypes.Linearity.Unl,\n                                                             CommonTypes.Restriction.Any)),\n                                                           `Rigid)),\n                                false)),\n                            (Types.Record\n                               (Types.Row\n                                  ({}, Point @ 0x7f8c82a18940 Types.Closed,\n                                   false))))))));\n            },\n           Point @ 0x7f8c82a18940 Types.Closed, false))),\n    (Types.Record\n       (Types.Row ({}, Point @ 0x7f8c82a18940 Types.Closed, false)))))")