hm.fs

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)

hm.hs

loop x = loop x
dno = loop loop

assert_same_type a b = 
    (\f -> -- manually desuget let to avoid let-polymorphism    
        let _ = f a in
        let _ = f b in
        dno
    ) (\x -> dno)

assert_different_types a b = 
    assert_same_type a (b a)

test_unification t1 t2 = 
    let _ = assert_different_types t1 t2 in
    let force_t1 p = p (\f s -> assert_same_type f t1) in
    let force_t2 p = p (\f s -> assert_same_type s t2) in
    (\p -> 
        let _ = force_t1 p in
        let _ = force_t2 p in
        p
    ) dno


main = print "hello"