module HM

let rec loop x = loop x
let mk_dno x = loop loop

let assert_same_type a b =
    (fun f -> // manually desuget let to avoid let-polymorphism
        let _ = f a in
        let _ = f b in
        mk_dno loop
    ) (fun x -> mk_dno loop)

let assert_different_types a b =
    assert_same_type a (b a)

let test_unification t1 t2 =
    let _ = assert_different_types t1 t2 in
    let force_t1 p = p (fun f s -> assert_same_type f t1) in
    let force_t2 p = p (fun f s -> assert_same_type s t2) in
    (fun p ->
        let _ = force_t1 p in
        let _ = force_t2 p in
        p
    ) (mk_dno loop)