Incomplete rows can trigger an internal error #1164
Description
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)))))")