diff --git a/evaluator.lua b/evaluator.lua index 32b7389..f154ec5 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -102,7 +102,7 @@ local function FunctionRelation(srel) srel, rctx, applied_use, - terms.constraintcause.lost("FunctionRelation inner", debug.traceback()) + terms.constraintcause.nested("FunctionRelation inner", cause) ) end), }, subtype_relation_mt) @@ -147,7 +147,7 @@ local function IndepTupleRelation(...) args[i].srel, rctx, use_elems[i], - terms.constraintcause.lost("tuple element constraint", debug.traceback()) + terms.constraintcause.nested("positive tuple element constraint", cause) ) else typechecker_state:queue_constrain( @@ -156,7 +156,7 @@ local function IndepTupleRelation(...) args[i].srel, lctx, val_elems[i], - terms.constraintcause.lost("tuple element constraint", debug.traceback()) + terms.constraintcause.nested("negative tuple element constraint", cause) ) end end @@ -262,7 +262,7 @@ enum_desc_srel = setmetatable({ val_type, rctx, use_variant --[[@as value -- please find a better approach]], - terms.constraintcause.lost("enum variant", debug.traceback()) + terms.constraintcause.nested("enum variant", cause) ) end end @@ -309,7 +309,7 @@ local TupleDescRelation = setmetatable({ tuple_types_val[i], rctx, tuple_types_use[i], - terms.constraintcause.lost("TupleDescRelation.constrain", debug.traceback()) + terms.constraintcause.nested("TupleDescRelation.constrain " .. tostring(i), cause) ) end end @@ -855,7 +855,7 @@ add_comparer("value.tuple_type", "value.tuple_type", function(lctx, a, rctx, b, TupleDescRelation, rctx, desc_b, - terms.constraintcause.lost("tuple type", debug.traceback()) + terms.constraintcause.nested("tuple type", cause) ) return true end) @@ -868,7 +868,7 @@ add_comparer("value.host_tuple_type", "value.host_tuple_type", function(lctx, a, TupleDescRelation, rctx, desc_b, - terms.constraintcause.lost("host tuple type", debug.traceback()) + terms.constraintcause.nested("host tuple type", cause) ) return true end) @@ -880,7 +880,7 @@ add_comparer("value.enum_desc_type", "value.enum_desc_type", function(lctx, a, r a_univ, rctx, b_univ, - terms.constraintcause.lost("enum desc universe covariance", debug.traceback()) + terms.constraintcause.nested("enum desc universe covariance", cause) ) return true end) @@ -893,7 +893,7 @@ add_comparer("value.enum_type", "value.enum_type", function(lctx, a, rctx, b, ca enum_desc_srel, rctx, b_desc, - terms.constraintcause.lost("enum type description", debug.traceback()) + terms.constraintcause.nested("enum type description", cause) ) return true end) @@ -949,7 +949,7 @@ add_comparer("value.enum_type", "value.tuple_desc_type", function(lctx, a, rctx, enum_desc_srel, rctx, value.enum_desc_value(construction_variants), - terms.constraintcause.lost("use enum construction as tuple desc", debug.traceback()) + terms.constraintcause.nested("use enum construction as tuple desc", cause) ) return true end) @@ -1005,7 +1005,7 @@ add_comparer("value.tuple_desc_type", "value.enum_type", function(lctx, a, rctx, enum_desc_srel, rctx, b_desc, - terms.constraintcause.lost("use tuple description as enum", debug.traceback()) + terms.constraintcause.nested("use tuple description as enum", nested) ) return true end) @@ -1034,7 +1034,7 @@ add_comparer("value.pi", "value.pi", function(lctx, a, rctx, b, cause) b_param_type, lctx, a_param_type, - terms.constraintcause.lost("pi function parameters", debug.traceback()) + terms.constraintcause.nested("pi function parameters", cause) ) --local unique_placeholder = terms.value.neutral(terms.neutral_value.free(terms.free.unique({}))) --local a_res = apply_value(a_result_type, unique_placeholder) @@ -1048,7 +1048,7 @@ add_comparer("value.pi", "value.pi", function(lctx, a, rctx, b, cause) FunctionRelation(UniverseOmegaRelation), rctx, b_result_type, - terms.constraintcause.lost("pi function results", debug.traceback()) + terms.constraintcause.nested("pi function results", cause) ) return true @@ -1072,7 +1072,7 @@ add_comparer("value.host_function_type", "value.host_function_type", function(lc b_param_type, lctx, a_param_type, - terms.constraintcause.lost("host function parameters", debug.traceback()) + terms.constraintcause.nested("host function parameters", cause) ) --local unique_placeholder = terms.value.neutral(terms.neutral_value.free(terms.free.unique({}))) --local a_res = apply_value(a_result_type, unique_placeholder) @@ -1086,7 +1086,7 @@ add_comparer("value.host_function_type", "value.host_function_type", function(lc FunctionRelation(UniverseOmegaRelation), rctx, b_result_type, - terms.constraintcause.lost("host function results", debug.traceback()) + terms.constraintcause.nested("host function results", cause) ) return true end) @@ -1122,9 +1122,9 @@ add_comparer("value.host_user_defined_type", "value.host_user_defined_type", fun value.host_value(rctx), value.host_value(value.tuple_value(b_args)), value.host_value( - terms.constraintcause.lost( + terms.constraintcause.nested( "host_user_defined_type compared against host_user_defined_type", - debug.traceback() + cause ) ) ) @@ -1156,13 +1156,7 @@ end add_comparer("value.srel_type", "value.srel_type", function(lctx, a, rctx, b, cause) local a_target = a:unwrap_srel_type() local b_target = b:unwrap_srel_type() - typechecker_state:queue_subtype( - lctx, - a_target, - rctx, - b_target, - terms.constraintcause.lost("srel target", debug.traceback()) - ) + typechecker_state:queue_subtype(lctx, a_target, rctx, b_target, terms.constraintcause.nested("srel target", cause)) return true end) @@ -1174,7 +1168,7 @@ add_comparer("value.variance_type", "value.variance_type", function(lctx, a, rct a_target, rctx, b_target, - terms.constraintcause.lost("variance target", debug.traceback()) + terms.constraintcause.nested("variance target", cause) ) return true end) @@ -1208,13 +1202,7 @@ end) add_comparer("value.host_wrapped_type", "value.host_wrapped_type", function(lctx, a, rctx, b, cause) local ua, ub = a:unwrap_host_wrapped_type(), b:unwrap_host_wrapped_type() - typechecker_state:queue_subtype( - lctx, - ua, - rctx, - ub, - terms.constraintcause.lost("wrapped type target", debug.traceback()) - ) + typechecker_state:queue_subtype(lctx, ua, rctx, ub, terms.constraintcause.nested("wrapped type target", cause)) --U.tag("check_concrete", { ua, ub }, check_concrete, ua, ub) return true end) @@ -1227,7 +1215,7 @@ add_comparer("value.singleton", "value.singleton", function(lctx, a, rctx, b, ca a_supertype, rctx, b_supertype, - terms.constraintcause.lost("singleton supertypes", debug.traceback()) + terms.constraintcause.nested("singleton supertypes", cause) ) if a_value == b_value then @@ -1245,7 +1233,7 @@ add_comparer("value.tuple_desc_type", "value.tuple_desc_type", function(lctx, a, a_universe, rctx, b_universe, - terms.constraintcause.lost("tuple_desc_type universes", debug.traceback()) + terms.constraintcause.nested("tuple_desc_type universes", cause) ) return true end) @@ -1260,7 +1248,7 @@ add_comparer("value.program_type", "value.program_type", function(lctx, a, rctx, effect_row_srel, rctx, b_eff, - terms.constraintcause.lost("program effects", debug.traceback()) + terms.constraintcause.nested("program effects", cause) ) return true end) @@ -1294,13 +1282,7 @@ function check_concrete(lctx, val, rctx, use, cause) local vnv = val:unwrap_neutral() if vnv:is_tuple_element_access_stuck() then local innerctx, bound = upcast(lctx, val) - typechecker_state:queue_subtype( - innerctx, - bound, - rctx, - use, - terms.constraintcause.lost("upcast", debug.traceback()) - ) + typechecker_state:queue_subtype(innerctx, bound, rctx, use, terms.constraintcause.nested("upcast", cause)) return true end end @@ -1328,27 +1310,15 @@ function check_concrete(lctx, val, rctx, use, cause) val_supertype, rctx, use, - terms.constraintcause.lost("singleton subtype", debug.traceback()) + terms.constraintcause.nested("singleton subtype", cause) ) return true end if val:is_union_type() then local vala, valb = val:unwrap_union_type() - typechecker_state:queue_subtype( - lctx, - vala, - rctx, - use, - terms.constraintcause.lost("union dissasembly", debug.traceback()) - ) - typechecker_state:queue_subtype( - lctx, - valb, - rctx, - use, - terms.constraintcause.lost("union dissasembly", debug.traceback()) - ) + typechecker_state:queue_subtype(lctx, vala, rctx, use, terms.constraintcause.nested("union dissasembly", cause)) + typechecker_state:queue_subtype(lctx, valb, rctx, use, terms.constraintcause.nested("union dissasembly", cause)) return true end @@ -1359,14 +1329,14 @@ function check_concrete(lctx, val, rctx, use, cause) val, rctx, usea, - terms.constraintcause.lost("intersection dissasembly", debug.traceback()) + terms.constraintcause.nested("intersection dissasembly", cause) ) typechecker_state:queue_subtype( lctx, val, rctx, useb, - terms.constraintcause.lost("intersection dissasembly", debug.traceback()) + terms.constraintcause.nested("intersection dissasembly", cause) ) return true end diff --git a/terms.lua b/terms.lua index 24547a0..883e2a1 100644 --- a/terms.lua +++ b/terms.lua @@ -506,6 +506,10 @@ constraintcause:define_enum("constraintcause", { "right", gen.builtin_number, "position", anchor_type, } }, + { "nested", { + "description", gen.builtin_string, + "inner", constraintcause, + } }, { "leftcall_discharge", { "call", gen.builtin_number, "constraint", gen.builtin_number, diff --git a/types/constraintcause.lua b/types/constraintcause.lua index 8b8c398..b294e8a 100644 --- a/types/constraintcause.lua +++ b/types/constraintcause.lua @@ -17,6 +17,12 @@ function constraintcause:unwrap_composition() end ---@return boolean, number, number, Anchor function constraintcause:as_composition() end ---@return boolean +function constraintcause:is_nested() end +---@return string, constraintcause +function constraintcause:unwrap_nested() end +---@return boolean, string, constraintcause +function constraintcause:as_nested() end +---@return boolean function constraintcause:is_leftcall_discharge() end ---@return number, number, Anchor function constraintcause:unwrap_leftcall_discharge() end @@ -39,6 +45,7 @@ function constraintcause:as_lost() end ---@field define_enum fun(self: constraintcauseType, name: string, variants: Variants): constraintcauseType ---@field primitive fun(description: string, position: any): constraintcause ---@field composition fun(left: number, right: number, position: Anchor): constraintcause +---@field nested fun(description: string, inner: constraintcause): constraintcause ---@field leftcall_discharge fun(call: number, constraint: number, position: Anchor): constraintcause ---@field rightcall_discharge fun(constraint: number, call: number, position: Anchor): constraintcause ---@field lost fun(unique_string: string, stacktrace: string, auxiliary: any): constraintcause