use myc::ast::environment::Environment;
use myc::ast::types::Value;

// ── Stage B: HM Let-Polymorphism ─────────────────────────────────────────────
//
// These tests verify that user-defined generic functions (e.g. `last`, `prev`)
// work correctly across multiple series element types without type conflicts.
//
// Before Stage B: TypeVars are unified once per call site. The optimizer
// hides failures by inlining, but diagnostics may report false conflicts and
// return types remain `Any` instead of the precise inferred type.
//
// After Stage B: `generalize` wraps function types in `Forall`; `instantiate`
// gives each call site fresh TypeVars. No conflicts, precise return types.
// ─────────────────────────────────────────────────────────────────────────────

/// A generic accessor function must compile without any type-conflict diagnostics
/// when called with two series of different element types.
///
/// This is the primary Stage B regression test. Before let-polymorphism, the
/// TypeVar from the first call may leak into the second, producing a spurious
/// type-conflict error.
#[test]
fn test_let_poly_no_conflict_diagnostic() {
    let env = Environment::new();
    let source = r#"
    (do
      (def last (fn [s] (s 0)))
      (def a (series 5))
      (push a 1.5)
      (def b (series 5))
      (push b "hello")
      (last a)
      (last b)
    )
    "#;
    let result = env.compile(source);
    assert!(
        !result.diagnostics.has_errors(),
        "Generic function used with two series types must not produce type errors: {}",
        result.diagnostics.format_errors()
    );
    let has_type_conflict = result
        .diagnostics
        .items
        .iter()
        .any(|d| d.message.contains("type") || d.message.contains("conflict") || d.message.contains("mismatch"));
    assert!(
        !has_type_conflict,
        "No type-conflict diagnostics expected for a polymorphic function: {:?}",
        result.diagnostics.items
    );
}

/// Runtime correctness: `last` retrieves the correct value from Float and Text series.
#[test]
fn test_let_poly_two_series_types_runtime() {
    let env = Environment::new();
    let source = r#"
    (do
      (def last (fn [s] (s 0)))
      (def a (series 5))
      (push a 1.5)
      (push a 2.5)
      (def b (series 5))
      (push b "hello")
      (push b "world")
      [(last a) (last b)]
    )
    "#;
    let result = env.run_script(source);
    match result {
        Ok(Value::Tuple(elems)) if elems.len() == 2 => {
            match (&elems[0], &elems[1]) {
                (Value::Float(f), Value::Text(t))
                    if (*f - 2.5).abs() < 1e-9 && t.as_ref() == "world" => {}
                other => panic!("Expected [Float(2.5), Text(\"world\")], got {:?}", other),
            }
        }
        other => panic!("Expected tuple result, got {:?}", other),
    }
}

/// A generic function works on record series as well as scalar series.
#[test]
fn test_let_poly_record_series() {
    let env = Environment::new();
    let source = r#"
    (do
      (def last (fn [s] (s 0)))
      (def prices (series 5))
      (push prices {:close 42.0 :vol 100})
      (def names (series 5))
      (push names {:name "Alice"})
      [
        ((.close prices) 0)
        ((.name names) 0)
      ]
    )
    "#;
    let result = env.run_script(source);
    match result {
        Ok(Value::Tuple(elems)) if elems.len() == 2 => {
            match (&elems[0], &elems[1]) {
                (Value::Float(f), Value::Text(t))
                    if (*f - 42.0).abs() < 1e-9 && t.as_ref() == "Alice" => {}
                other => panic!("Expected [Float(42.0), Text(\"Alice\")], got {:?}", other),
            }
        }
        other => panic!("Expected tuple result, got {:?}", other),
    }
}

/// Value restriction: a series binding must NOT be generalized.
/// Pushing incompatible types into the same series must remain a type error.
#[test]
fn test_let_poly_value_restriction_series() {
    let env = Environment::new();
    let source = r#"
    (do
      (def s (series 5))
      (push s 1.5)
      (push s "hello")
      (s 0)
    )
    "#;
    let result = env.compile(source);
    assert!(
        result.diagnostics.has_errors(),
        "Pushing incompatible types into the same series must produce a type error"
    );
}

/// Higher-order function: `apply-f` passes a generic function to different series.
/// Both calls must compile cleanly and return the correct values.
#[test]
fn test_let_poly_higher_order() {
    let env = Environment::new();
    let source = r#"
    (do
      (def last (fn [s] (s 0)))
      (def apply-f (fn [f s] (f s)))
      (def a (series 5))
      (push a 1.5)
      (push a 2.5)
      (def b (series 5))
      (push b "hello")
      (push b "world")
      [(apply-f last a) (apply-f last b)]
    )
    "#;
    let result = env.run_script(source);
    match result {
        Ok(Value::Tuple(elems)) if elems.len() == 2 => {
            match (&elems[0], &elems[1]) {
                (Value::Float(f), Value::Text(t))
                    if (*f - 2.5).abs() < 1e-9 && t.as_ref() == "world" => {}
                other => panic!("Expected [Float(2.5), Text(\"world\")], got {:?}", other),
            }
        }
        other => panic!("Expected tuple result, got {:?}", other),
    }
}

/// When a generic function returns `Any` (because its TypeVar is not resolved),
/// pushing the result into a new series leaves that series with an unresolved
/// element type. Field access on `Series(TypeVar)` then fails because the type
/// checker cannot find the record layout.
///
/// After Stage B + call-site unification: the return type of `(get-first prices)`
/// is correctly inferred as `Record({:price Float})`, the pushed series gets
/// `Series(Record({:price Float}))`, and field access works.
#[test]
fn test_let_poly_generic_return_used_in_field_series() {
    let env = Environment::new();
    let source = r#"
    (do
      (def get-first (fn [s] (s 0)))
      (def prices (series 5))
      (push prices {:price 42.0})
      (def out (series 3))
      (push out (get-first prices))
      ((.price out) 0)
    )
    "#;
    let result = env.run_script(source);
    match result {
        Ok(Value::Float(v)) if (v - 42.0).abs() < 1e-9 => {}
        other => panic!("Expected Float(42.0), got {:?}", other),
    }
}

/// Regression: when a generic function indexes the same TypeVar parameter twice —
/// `(s 0)` and `(s 1)` — both result TypeVars must share the same element type.
///
/// Before the fix, Step 9 overwrote `index_constraints[n]` on the second call,
/// leaving the first result TypeVar unbound (`Any`). This caused false negatives
/// when the first-call result was pushed into a typed series.
///
/// After the fix, the second call unifies its fresh TypeVar with the existing one
/// so all index results on the same parameter resolve together.
#[test]
fn test_let_poly_multi_index_all_results_typed() {
    let env = Environment::new();
    let source = r#"
    (do
      (def tricky (fn [s]
        (do
          (def a (s 0))
          (def b (s 1))
          a
        )
      ))
      (def texts (series 5))
      (push texts "hello")
      (def check (series 5))
      (push check (tricky texts))
      (push check 1.0)
    )
    "#;
    let result = env.compile(source);
    assert!(
        result.diagnostics.has_errors(),
        "Multi-index: (s 0) result must be Text, not Any; \
         pushing Float into a Text-derived series must produce a type error: {}",
        result.diagnostics.format_errors()
    );
}

/// Regression test: passing a non-series callable to a generic `last` function
/// must NOT produce a type error. Before the index-constraint fix, Step 9 would
/// eagerly unify `TypeVar = Series(elem)`, making `last` Series-only and causing
/// a spurious conflict when a Function-typed variable was passed.
///
/// After the fix, `last` is inferred as `∀α β. fn(α) → β` with a lazy constraint:
/// only when `α` resolves to `Series(inner)` does `β` also resolve to `inner`.
/// For any other callable, `β` stays unbound and the return type is `Any`.
#[test]
fn test_let_poly_non_series_callable_no_false_positive() {
    let env = Environment::new();
    let source = r#"
    (do
      (def f (fn [n] (n)))
      (def last (fn [s] (s 0)))
      (last f)
    )
    "#;
    let result = env.compile(source);
    assert!(
        !result.diagnostics.has_errors(),
        "Passing a non-series callable to a generic function must not produce a type error: {}",
        result.diagnostics.format_errors()
    );
}