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)))))")
The following program triggers an internal error in the type checker (during the construction of an error message).
The problem with this program is that the formal parameter type of
rdoesn't mentionR. However, at the time of writing Links produces the following internal error when type checking this program (witheffect_sugar=false).