Fix compose_2

alicorn-expressions.lua

@@ -440,16 +440,7 @@ local function speculate_pi_type(env, metaval)
 	local ok, res = evaluator.typechecker_state:speculate(function()
 		local param_mv = evaluator.typechecker_state:metavariable(env.typechecking_context)
 		local result_mv = evaluator.typechecker_state:metavariable(env.typechecking_context)
-		local pi = value.pi(
-			param_mv:as_value(),
-			param_info_implicit,
-			value.closure(
-				"#spec-pi",
-				typed_term.literal(result_mv:as_value()),
-				env.typechecking_context.runtime_context
-			),
-			result_info_pure
-		)
+		local pi = value.pi(param_mv:as_value(), param_info_implicit, result_mv:as_value(), result_info_pure)
 
 		U.tag(
 			"flow",
@@ -475,16 +466,7 @@ local function speculate_pi_type(env, metaval)
 	return evaluator.typechecker_state:speculate(function()
 		local param_mv = evaluator.typechecker_state:metavariable(env.typechecking_context)
 		local result_mv = evaluator.typechecker_state:metavariable(env.typechecking_context)
-		local pi = value.pi(
-			param_mv:as_value(),
-			param_info_explicit,
-			value.closure(
-				"#spec-pi",
-				typed_term.literal(result_mv:as_value()),
-				env.typechecking_context.runtime_context
-			),
-			result_info_pure
-		)
+		local pi = value.pi(param_mv:as_value(), param_info_explicit, result_mv:as_value(), result_info_pure)
 
 		U.tag(
 			"flow",

evaluator.lua

@@ -3750,16 +3750,21 @@ function TypeCheckerState:Visualize(diff)
 	end
 
 	for i, e in ipairs(self.graph.constrain_edges:all()) do
-		g = g .. "\n" .. e.left .. " -> " .. e.right .. " [arrowType=normal"
+		g = g .. "\n" .. e.left .. " -> " .. e.right .. " [arrowhead=normal"
 
 		if diff and diff.constrain_edges[i] and diff.constrain_edges[i].left == e.left and diff.constrain_edges[i].right == e.right then
-			g = g .. ', color="#cccccc"'
+			g = g .. ', fontcolor=\"#cccccc\", color="#cccccc"'
+		end
+
+		if e.rel.debug_name then
+			g = g .. ', label="'.. e.rel.debug_name .. '"'
 		end
+
 		g = g .. "]"
 	end
 
 	for i, e in ipairs(self.graph.leftcall_edges:all()) do
-		g = g .. "\n" .. e.left .. " -> " .. e.right .. " [arrowType=empty"
+		g = g .. "\n" .. e.left .. " -> " .. e.right .. " [arrowhead=empty"
 
 		if diff and diff.leftcall_edges[i] and diff.leftcall_edges[i].left == e.left and diff.leftcall_edges[i].right == e.right then
 			g = g .. ', color="#cccccc"'
@@ -3768,7 +3773,7 @@ function TypeCheckerState:Visualize(diff)
 	end
 
 	for i, e in ipairs(self.graph.rightcall_edges:all()) do
-		g = g .. "\n" .. e.left .. " -> " .. e.right .. " [arrowType=invempty"
+		g = g .. "\n" .. e.left .. " -> " .. e.right .. " [arrowhead=invempty"
 
 		if diff and diff.rightcall_edges[i] and diff.rightcall_edges[i].left == e.left and diff.rightcall_edges[i].right == e.right then
 			g = g .. ', color="#cccccc"'
@@ -4468,15 +4473,16 @@ function TypeCheckerState:constrain_leftcall_compose_2(edge, edge_id)
 					"Relations do not match! " .. tostring(l2.rel) .. " is not " .. tostring(FunctionRelation(edge.rel))
 				)
 			end
+			local lvalue, _, lctx = table.unpack(self.values[l2.left])
+			local l = self:check_value(apply_value(lvalue, edge.arg), TypeCheckerTag.VALUE, lctx)
 			U.append(
 				self.pending,
-				EdgeNotif.CallLeft(
-					edge.left,
-					edge.arg,
+				EdgeNotif.Constrain(
+					l,
 					edge.rel,
-					l2.right,
+					edge.right,
 					math.min(edge.shallowest_block, l2.shallowest_block),
-					compositecause("leftcall_discharge", edge_id, edge, i, l2, NIL_ANCHOR)
+					compositecause("composition", i, l2, edge_id, edge, NIL_ANCHOR)
 				)
 			)
 		end

terms.lua

@@ -350,7 +350,7 @@ checkable_term:define_enum("checkable", {
 -- inferrable terms can have their type inferred / don't need a goal type
 -- stylua: ignore
 inferrable_term:define_enum("inferrable", {
-	{ "bound_variable", { "index", gen.builtin_number, "debug", gen.builtin_string } },
+	{ "bound_variable", { "index", gen.builtin_number, "debug", gen.any_lua_type } },
 	{ "typed", {
 		"type",         value,
 		"usage_counts", array(gen.builtin_number),
@@ -582,7 +582,7 @@ local unique_id = gen.builtin_table
 -- typed terms have been typechecked but do not store their type internally
 -- stylua: ignore
 typed_term:define_enum("typed", {
-	{ "bound_variable", { "index", gen.builtin_number, "debug", gen.builtin_string  } },
+	{ "bound_variable", { "index", gen.builtin_number, "debug", gen.any_lua_type  } },
 	{ "literal", { "literal_value", value } },
 	{ "lambda", {
 		"param_name", gen.builtin_string,

types/inferrable.lua

@@ -7,11 +7,11 @@ inferrable = {}
 ---@return boolean
 function inferrable:is_bound_variable() end
 ---@return number index
----@return string debug
+---@return any debug
 function inferrable:unwrap_bound_variable() end
 ---@return boolean
 ---@return number index
----@return string debug
+---@return any debug
 function inferrable:as_bound_variable() end
 ---@return boolean
 function inferrable:is_typed() end
@@ -368,7 +368,7 @@ function inferrable:as_program_type() end
 
 ---@class (exact) inferrableType: EnumType
 ---@field define_enum fun(self: inferrableType, name: string, variants: Variants): inferrableType
----@field bound_variable fun(index: number, debug: string): inferrable
+---@field bound_variable fun(index: number, debug: any): inferrable
 ---@field typed fun(type: value, usage_counts: ArrayValue, typed_term: typed): inferrable
 ---@field annotated_lambda fun(param_name: string, param_annotation: inferrable, body: inferrable, start_anchor: Anchor, visible: visibility, pure: checkable): inferrable
 ---@field pi fun(param_type: inferrable, param_info: checkable, result_type: inferrable, result_info: checkable): inferrable