// -----------------------------------------------------------------------------

// PassTyping - Public Interface

// -----------------------------------------------------------------------------

type InferNodeIndex = usize;

enum DefinitionType{

    Component(ComponentDefinitionId),

    Function(FunctionDefinitionId),

}

struct InferenceNode {

    expr_type: InferenceType,       // result type from expression

    expr_id: ExpressionId,          // expression that is evaluated

    inference_rule: InferenceRule,

    parent_index: Option<InferNodeIndex>,

    field_or_monomorph_index: i32,    // index of field

    type_id: TypeId,                // when applicable indexes into type table

}

/// Inferencing rule to apply. Some of these are reasonably generic. Other ones

/// require so much custom logic that we'll not try to come up with an

/// abstraction.

/// that all expressions have the appropriate types.

pub(crate) struct PassTyping {

    // Current definition we're typechecking.

    reserved_type_id: TypeId,

    definition_type: DefinitionType,

    poly_vars: Vec<ConcreteType>,

    parent_index: Option<InferNodeIndex>,

    // Buffers for iteration over various types

    var_buffer: ScopedBuffer<VariableId>,

    expr_buffer: ScopedBuffer<ExpressionId>,

    stmt_buffer: ScopedBuffer<StatementId>,

    bool_buffer: ScopedBuffer<bool>,

    index_buffer: ScopedBuffer<usize>,

    // Mapping from parser type to inferred type. We attempt to continue to

    // specify these types until we're stuck or we've fully determined the type.

    var_types: HashMap<VariableId, VarData>,            // types of variables

    infer_nodes: Vec<InferenceNode>,                     // will be transferred to type table at end

    // Keeping track of which expressions need to be reinferred because the

    // expressions they're linked to made progression on an associated type

    expr_queued: DequeSet<i32>,

}

    definition_id: DefinitionId, // the definition, only used for user feedback

    poly_vars: Vec<InferenceType>,

    returned: InferenceType,

}

    fn default() -> Self {

            definition_id: DefinitionId::new_invalid(),

            poly_vars: Vec::new(),

            returned: InferenceType::default(),

        }

    }

}

struct VarData {

    /// Type of the variable

    var_type: InferenceType,

    /// VariableExpressions that use the variable

    used_at: Vec<ExpressionId>,

    /// For channel statements we link to the other variable such that when one

            var_buffer: ScopedBuffer::with_capacity(BUFFER_INIT_CAP_LARGE),

            expr_buffer: ScopedBuffer::with_capacity(BUFFER_INIT_CAP_LARGE),

            stmt_buffer: ScopedBuffer::with_capacity(BUFFER_INIT_CAP_LARGE),

            bool_buffer: ScopedBuffer::with_capacity(BUFFER_INIT_CAP_SMALL),

            var_types: HashMap::new(),

            infer_nodes: Vec::new(),

            expr_queued: DequeSet::new(),

        }

    }

    pub(crate) fn queue_module_definitions(ctx: &mut Ctx, queue: &mut ResolveQueue) {

        debug_assert_eq!(ctx.module().phase, ModuleCompilationPhase::ValidatedAndLinked);

    fn reset(&mut self) {

        self.reserved_type_id = TypeId::new_invalid();

        self.definition_type = DefinitionType::Function(FunctionDefinitionId::new_invalid());

        self.poly_vars.clear();

        self.var_types.clear();

        self.infer_nodes.clear();

        self.expr_queued.clear();

    }

}

// -----------------------------------------------------------------------------

// PassTyping - Visitor-like implementation

                expr_ids.forget();

                let element_indices = expr_indices.into_vec();

                // Assign rule and extra data index to inference node

                let extra_index = self.insert_initial_struct_polymorph_data(ctx, id);

                let node = &mut self.infer_nodes[self_index];

                node.inference_rule = InferenceRule::LiteralStruct(InferenceRuleLiteralStruct{

                    element_indices,

                });

            },

            Literal::Enum(_) => {

                // Enumerations do not carry any subexpressions, but may still

                // have a user-defined polymorphic marker variable. For this 

                // reason we may still have to apply inference to this 

                // polymorphic variable

                let extra_index = self.insert_initial_enum_polymorph_data(ctx, id);

                let node = &mut self.infer_nodes[self_index];

                node.inference_rule = InferenceRule::LiteralEnum(InferenceRuleLiteralEnum{

                });

            },

            Literal::Union(literal) => {

                // May carry subexpressions and polymorphic arguments

                    expr_indices.push(expr_index);

                }

                expr_ids.forget();

                let element_indices = expr_indices.into_vec();

                let node = &mut self.infer_nodes[self_index];

                node.inference_rule = InferenceRule::LiteralUnion(InferenceRuleLiteralUnion{

                    element_indices,

                });

            },

            Literal::Array(expressions) | Literal::Tuple(expressions) => {

                let expr_ids = self.expr_buffer.start_section_initialized(expressions.as_slice());

                    expr_indices.push(expr_index);

                }

                expr_ids.forget();

                let element_indices = expr_indices.into_vec();

                let node = &mut self.infer_nodes[self_index];

                node.inference_rule = InferenceRule::LiteralArray(InferenceRuleLiteralArray{

                    element_indices,

                })

            }

        }

            expr_indices.push(expr_index);

        }

        expr_ids.forget();

        let argument_indices = expr_indices.into_vec();

        let node = &mut self.infer_nodes[self_index];

        node.inference_rule = InferenceRule::CallExpr(InferenceRuleCallExpr{

            argument_indices,

        });

        self.parent_index = old_parent;

        self.progress_call_expr(ctx, id)

            // Expression is fine, check if any extra data is attached

            if infer_expr.extra_data_idx < 0 { continue; }

            // Extra data is attached, perform typechecking and transfer

            // resolved information to the expression

            // Note that only call and literal expressions need full inference.

            // Select expressions also use `extra_data`, but only for temporary

            // storage of the struct type whose field it is selecting.

            match &ctx.heap[extra_data.expr_id] {

                Expression::Call(expr) => {

                    }

                    // Insert the initial data needed to infer polymorphic

                    // fields

                    let extra_index = self.insert_initial_select_polymorph_data(ctx, node_index, definition_id);

                    let node = &mut self.infer_nodes[node_index];

                },

                Ok(None) => {

                    // We don't know what to do yet, because we don't know the

                    // subject type yet.

                    return Ok(())

                },

            }

        }

        // If here then the field index is known, hence we can start inferring

        // the type of the selected field

        let node = &self.infer_nodes[node_index];

        let mut poly_progress = HashSet::new(); // TODO: @Performance

        // Apply to struct's type

        let subject_type: *mut _ = &mut self.infer_nodes[subject_expr_idx as usize].expr_type;

        let (_, progress_subject) = Self::apply_equal2_signature_constraint(

            ctx, upcast_id, Some(subject_id), poly_data, &mut poly_progress,

            signature_type, 0, subject_type, 0

        )?;

        let signature_type: *mut _ = &mut poly_data.returned;

        let expr_type: *mut _ = &mut self.infer_nodes[expr_idx as usize].expr_type;

        let (_, progress_expr) = Self::apply_equal2_signature_constraint(

            ctx, upcast_id, None, poly_data, &mut poly_progress,

            signature_type, 0, expr_type, 0

        if progress_expr {

            if let Some(parent_id) = ctx.heap[upcast_id].parent_expr_id() {

                let parent_idx = ctx.heap[parent_id].get_unique_id_in_definition();

                self.expr_queued.push_back(parent_idx);

            }

        }

        // Reapply progress in polymorphic variables to struct's type

        let subject_type: *mut _ = &mut self.infer_nodes[subject_expr_idx as usize].expr_type;

        let progress_subject = Self::apply_equal2_polyvar_constraint(

            poly_data, &poly_progress, signature_type, subject_type

        );

                    }

                }

                // If here then field index is known, and the referenced struct type

                // information is inserted into `extra_data`. Check to see if we can

                // do some mutual inference.

                let mut poly_progress = HashSet::new(); // TODO: @Performance

                // Apply to struct's type

                let subject_type: *mut _ = &mut self.infer_nodes[subject_expr_idx as usize].expr_type;

                let (_, progress_subject) = Self::apply_equal2_signature_constraint(

                    ctx, upcast_id, Some(subject_id), poly_data, &mut poly_progress,

                    signature_type, 0, subject_type, 0

                )?;

                        let parent_idx = ctx.heap[parent_id].get_unique_id_in_definition();

                        self.expr_queued.push_back(parent_idx);

                    }

                }

                // Reapply progress in polymorphic variables to struct's type

                let subject_type: *mut _ = &mut self.infer_nodes[subject_expr_idx as usize].expr_type;

                let progress_subject = Self::apply_equal2_polyvar_constraint(

                    poly_data, &poly_progress, signature_type, subject_type

                );

                self.apply_forced_constraint(ctx, upcast_id, &CHARACTER_TEMPLATE)?

            },

            Literal::String(_) => {

                self.apply_forced_constraint(ctx, upcast_id, &STRING_TEMPLATE)?

            },

            Literal::Struct(data) => {

                for _poly in &extra.poly_vars {

                    debug_log!(" * Poly: {}", _poly.display_name(&ctx.heap));

                }

                let mut poly_progress = HashSet::new();

                debug_log!(" * During (inferring types from fields and struct type):");

                // Mutually infer field signature/expression types

                for (field_idx, field) in data.fields.iter().enumerate() {

                    let field_expr_id = field.value;

                    let field_expr_idx = ctx.heap[field_expr_id].get_unique_id_in_definition();

                    let field_type: *mut _ = &mut self.infer_nodes[field_expr_idx as usize].expr_type;

                    let (_, progress_arg) = Self::apply_equal2_signature_constraint(

                        ctx, upcast_id, Some(field_expr_id), extra, &mut poly_progress,

                        signature_type, 0, field_type, 0

                    )?;

                // Check which expressions use the polymorphic arguments. If the

                // polymorphic variables have been progressed then we try to 

                // progress them inside the expression as well.

                debug_log!(" * During (reinferring from progressed polyvars):");

                // For all field expressions

                    // Note: fields in extra.embedded are in the same order as

                    // they are specified in the literal. Whereas

                    // `data.fields[...].field_idx` points to the field in the

                    // struct definition.

                    let field_expr_id = data.fields[field_idx].value;

                    let field_expr_idx = ctx.heap[field_expr_id].get_unique_id_in_definition();

                    let field_type: *mut _ = &mut self.infer_nodes[field_expr_idx as usize].expr_type;

                    let progress_arg = Self::apply_equal2_polyvar_constraint(

                        extra, &poly_progress, signature_type, field_type

                    extra, &poly_progress, signature_type, expr_type

                );

                progress_expr

            },

            Literal::Enum(_) => {

                for _poly in &extra.poly_vars {

                    debug_log!(" * Poly: {}", _poly.display_name(&ctx.heap));

                }

                let mut poly_progress = HashSet::new();

                debug_log!(" * During (inferring types from return type)");

                    extra, &poly_progress, signature_type, expr_type

                );

                progress_expr

            },

            Literal::Union(data) => {

                for _poly in &extra.poly_vars {

                    debug_log!(" * Poly: {}", _poly.display_name(&ctx.heap));

                }

                let mut poly_progress = HashSet::new();

                debug_log!(" * During (inferring types from variant values and union type):");

                // Mutually infer union variant values

                for (value_idx, value_expr_id) in data.values.iter().enumerate() {

                    let value_expr_id = *value_expr_id;

                    let value_expr_idx = ctx.heap[value_expr_id].get_unique_id_in_definition();

                    let value_type: *mut _ = &mut self.infer_nodes[value_expr_idx as usize].expr_type;

                    let (_, progress_arg) = Self::apply_equal2_signature_constraint(

                        ctx, upcast_id, Some(value_expr_id), extra, &mut poly_progress,

                        signature_type, 0, value_type, 0 

                    )?;

                    }

                }

                debug_log!(" * During (reinferring from progress polyvars):");

                // For all embedded values of the union variant

                    let value_expr_id = data.values[value_idx];

                    let value_expr_idx = ctx.heap[value_expr_id].get_unique_id_in_definition();

                    let value_type: *mut _ = &mut self.infer_nodes[value_expr_idx as usize].expr_type;

                    let progress_arg = Self::apply_equal2_polyvar_constraint(

                        extra, &poly_progress, signature_type, value_type

        debug_log!("Call expr '{}': {}", ctx.heap[expr.definition].identifier().value.as_str(), upcast_id.index);

        debug_log!(" * Before:");

        debug_log!("   - Expr type: {}", self.debug_get_display_name(ctx, upcast_id));

        debug_log!(" * During (inferring types from arguments and return type):");

        // Check if we can make progress using the arguments and/or return types

        // while keeping track of the polyvars we've extended

        let mut poly_progress = HashSet::new();

        for (call_arg_idx, arg_id) in expr.arguments.clone().into_iter().enumerate() {

            let arg_expr_idx = ctx.heap[arg_id].get_unique_id_in_definition();

            let argument_type: *mut _ = &mut self.infer_nodes[arg_expr_idx as usize].expr_type;

            let (_, progress_arg) = Self::apply_equal2_signature_constraint(

                ctx, upcast_id, Some(arg_id), extra, &mut poly_progress,

                signature_type, 0, argument_type, 0

            )?;

        for (_poly_idx, _poly_var) in extra.poly_vars.iter().enumerate() {

            debug_log!("   - Poly {} | sig: {}", _poly_idx, _poly_var.display_name(&ctx.heap));

        }

        // TODO: @performance If the algorithm is changed to be more "on demand

        //  argument re-evaluation", instead of "all-argument re-evaluation",

        //  then this is no longer true

            let arg_expr_id = expr.arguments[arg_idx];

            let arg_expr_idx = ctx.heap[arg_expr_id].get_unique_id_in_definition();

            let arg_type: *mut _ = &mut self.infer_nodes[arg_expr_idx as usize].expr_type;

            let progress_arg = Self::apply_equal2_polyvar_constraint(

                extra, &poly_progress,

            return Err(self.construct_arg_type_error(ctx, node_index, arg1_index, arg2_index));

        }

        Ok((infer_res.modified_lhs(), infer_res.modified_rhs()))

    }

    /// Applies an equal2 constraint between a signature type (e.g. a function

    /// argument or struct field) and an expression whose type should match that

    /// expression. If we make progress on the signature, then we try to see if

    /// any of the embedded polymorphic types can be progressed.

    ///

    /// `outer_expr_id` is the main expression we're progressing (e.g. a 

    /// function call), while `expr_id` is the embedded expression we're 

    /// matching against the signature. `expression_type` and 

    /// `expression_start_idx` belong to `expr_id`.

    fn apply_equal2_signature_constraint(

        ctx: &Ctx, outer_expr_id: ExpressionId, expr_id: Option<ExpressionId>,

        signature_type: *mut InferenceType, signature_start_idx: usize,

        expression_type: *mut InferenceType, expression_start_idx: usize

    ) -> Result<(bool, bool), ParseError> {

        // Safety: all pointers distinct

        // Infer the signature and expression type

        let infer_res = unsafe { 

            InferenceType::infer_subtrees_for_both_types(

                signature_type, signature_start_idx,

                expression_type, expression_start_idx

        };

        if infer_res == DualInferenceResult::Incompatible {

            // TODO: Check if I still need to use this

            let outer_span = ctx.heap[outer_expr_id].full_span();

            let (span_name, span) = match expr_id {

    /// progressed as far as possible by calling 

    /// `apply_equal2_signature_constraint`. As such, we expect to not encounter

    /// any errors.

    ///

    /// This function returns true if the expression's type has been progressed

    fn apply_equal2_polyvar_constraint(

        signature_type: *mut InferenceType, expr_type: *mut InferenceType

    ) -> bool {

        // Safety: all pointers should be distinct

        //         polymorph_data containers may not be modified

        let signature_type = unsafe{&mut *signature_type};

        let expr_type = unsafe{&mut *expr_type};

        return Ok(infer_index);

    }

    fn insert_initial_call_polymorph_data(

        &mut self, ctx: &mut Ctx, call_id: CallExpressionId

        // Note: the polymorph variables may be partially specified and may

        // contain references to the wrapping definition's (i.e. the proctype

        // we are currently visiting) polymorphic arguments.

        //

        // The arguments of the call may refer to polymorphic variables in the

        // definition of the function we're calling, not of the wrapping

            },

            Some(returned) => {

                self.determine_inference_type_from_parser_type_elements(&returned.elements, false)

            }

        };

            expr_id: call_id.upcast(),

            definition_id: call.definition,

            poly_vars: poly_args,

            returned: return_type

        });

        return extra_data_idx

    }

    fn insert_initial_struct_polymorph_data(

        &mut self, ctx: &mut Ctx, lit_id: LiteralExpressionId,

        use InferenceTypePart as ITP;

        let literal = ctx.heap[lit_id].value.as_struct();

        // Handle polymorphic arguments

        let num_embedded = literal.parser_type.elements[0].variant.num_embedded();

        let mut total_num_poly_parts = 0;

            parts.extend(poly_var.parts.iter().cloned());

        }

        debug_assert_eq!(parts.len(), parts_reserved);

        let return_type = InferenceType::new(!poly_args.is_empty(), return_type_done, parts);

            expr_id: lit_id.upcast(),

            definition_id: literal.definition,

            poly_vars: poly_args,

            returned: return_type,

        });

        return extra_data_index

    }

    /// Inserts the extra polymorphic data struct for enum expressions. These

    /// can never be determined from the enum itself, but may be inferred from

    /// the use of the enum.

    fn insert_initial_enum_polymorph_data(

        &mut self, ctx: &Ctx, lit_id: LiteralExpressionId

        use InferenceTypePart as ITP;

        let literal = ctx.heap[lit_id].value.as_enum();

        // Handle polymorphic arguments to the enum

        let num_poly_args = literal.parser_type.elements[0].variant.num_embedded();

        let mut total_num_poly_parts = 0;

            parts.extend(poly_var.parts.iter().cloned());

        }

        debug_assert_eq!(parts.len(), parts_reserved);

        let enum_type = InferenceType::new(!poly_args.is_empty(), enum_type_done, parts);

            expr_id: lit_id.upcast(),

            definition_id: literal.definition,

            poly_vars: poly_args,

            returned: enum_type,

        });

        return extra_data_index;

    }

    /// Inserts the extra polymorphic data struct for unions. The polymorphic

    /// arguments may be partially determined from embedded values in the union.

    fn insert_initial_union_polymorph_data(

        &mut self, ctx: &Ctx, lit_id: LiteralExpressionId

        use InferenceTypePart as ITP;

        let literal = ctx.heap[lit_id].value.as_union();

        // Construct the polymorphic variables

        let num_poly_args = literal.parser_type.elements[0].variant.num_embedded();

        let mut total_num_poly_parts = 0;

            parts.extend(poly_var.parts.iter().cloned());

        }

        debug_assert_eq!(parts_reserved, parts.len());

        let union_type = InferenceType::new(!poly_args.is_empty(), union_type_done, parts);

            expr_id: lit_id.upcast(),

            definition_id: literal.definition,

            poly_vars: poly_args,

            returned: union_type

        });

        return extra_data_index;

    }

    /// Inserts the extra polymorphic data struct. Assumes that the select

    /// expression's referenced (definition_id, field_idx) has been resolved.

    fn insert_initial_select_polymorph_data(

        &mut self, ctx: &Ctx, node_index: InferNodeIndex, struct_def_id: DefinitionId

        use InferenceTypePart as ITP;

        let definition = ctx.heap[struct_def_id].as_struct();

        let node = &self.infer_nodes[node_index];

        let field_index = node.field_or_monomorph_index as usize;

        }

        debug_assert_eq!(struct_parts.len(), struct_parts_reserved);

        // Generate initial field type

        let field_type = self.determine_inference_type_from_parser_type_elements(&definition.fields[field_index].parser_type.elements, false);

            definition_id: struct_def_id,

            poly_vars,

            returned: field_type

        });

        return extra_data_index;

    }

    ///

    /// So we find this pair and construct the error using it.

    ///

    /// We assume that the expression is a function call or a struct literal,

    /// and that an actual error has occurred.

    fn construct_poly_arg_error(

    ) -> ParseError {

        // Helper function to check for polymorph mismatch between two inference

        // types.

        fn has_poly_mismatch<'a>(type_a: &'a InferenceType, type_b: &'a InferenceType) -> Option<(u32, &'a [InferenceTypePart], &'a [InferenceTypePart])> {

            if !type_a.has_marker || !type_b.has_marker {

                return None

            let func_name = definition.identifier().value.as_str();

            (poly_var, func_name)

        }

        // Helper function to construct initial error

            match expr {

                Expression::Call(expr) => {

                    let (poly_var, func_name) = get_poly_var_and_definition_name(ctx, poly_var_idx, poly_data.definition_id);

                    return ParseError::new_error_at_span(

                        &ctx.module().source, expr.func_span, format!(

                            "Conflicting type for polymorphic variable '{}' of '{}'",

                        InferenceType::partial_display_name(&ctx.heap, section_b)

                    )

                );

        }

        // - check arguments with each other argument and with return type

                if arg_b_idx > arg_a_idx {

                    break;

                }

                if let Some((poly_idx, section_a, section_b)) = has_poly_mismatch(&arg_a, &arg_b) {

                    let error = construct_main_error(ctx, poly_data, poly_idx, expr);

                    );

            }

        }

        // Now check against the explicitly specified polymorphic variables (if

        // any).

            if let Some((poly_idx, poly_section, arg_section)) = has_explicit_poly_mismatch(&poly_data.poly_vars, arg) {

                let arg = &ctx.heap[expr_args[arg_idx]];

                return construct_main_error(ctx, poly_data, poly_idx, expr)

                    .with_info_at_span(

                        &ctx.module().source, arg.full_span(), format!(

                            "The polymorphic variable has type '{}' (which might have been partially inferred) while the argument inferred it to '{}'",