Lamdu's new type system

ExampleOut.hs

(\id -> id) (\x -> x) :: forall a2. a2 -> a2
((\id -> id{3}){2} (\x -> x{5}){4}){1}
    1 = a2 -> a2
    2 = (a2 -> a2) -> a2 -> a2
    3 = a2 -> a2
    4 = a2 -> a2
    5 = a2
(\id -> id id) (\x -> x)
Occurs check fails: a1 vs. a1 -> a2
(\id -> id id) (\x -> (\y -> y) x)
Occurs check fails: a1 vs. a1 -> a2
(\id -> id id 2) (\x -> (\y -> y) x)
Occurs check fails: a1 vs. a1 -> a3
(\id -> id) (\x -> x x)
Occurs check fails: a2 vs. a2 -> a3
\m -> (\y -> (\x -> x) (y 3)) m :: forall a1. (Int -> a1) -> a1
(\m -> ((\y -> ((\x -> x{6}){5} (y{8} 3{9}){7}){4}){3} m{10}){2}){1}
    1 = (Int -> a1) -> a1
    2 = a1
    3 = (Int -> a1) -> a1
    4 = a1
    5 = a1 -> a1
    6 = a1
    7 = a1
    8 = Int -> a1
    9 = Int
    10 = Int -> a1
2 2
Types do not unify Int vs. Int -> a0
\a -> (\x -> x 3) (\b -> (\y -> y 2) (\c -> a 1)) :: forall a1. (Int -> a1) -> a1
(\a -> ((\x -> (x{5} 3{6}){4}){3} (\b -> ((\y -> (y{11} 2{12}){10}){9} (\c -> (a{15} 1{16}){14}){13}){8}){7}){2}){1}
    1 = (Int -> a1) -> a1
    2 = a1
    3 = (Int -> a1) -> a1
    4 = a1
    5 = Int -> a1
    6 = Int
    7 = Int -> a1
    8 = a1
    9 = (Int -> a1) -> a1
    10 = a1
    11 = Int -> a1
    12 = Int
    13 = Int -> a1
    14 = a1
    15 = Int -> a1
    16 = Int
\a -> \b -> b (a (a b))
Occurs check fails: a3 vs. a3 -> a2
\vec -> { newX = vec.x, { newY = vec.y, V{} } } :: forall a1 a3 r5. {x y} ∉ r5 => { x : a1, y : a3, r5... } -> { newX : a1, newY : a3 }
(\vec -> { newX = (vec{4}.x){3}, { newY = (vec{7}.y){6}, V{}{8} }{5} }{2}){1}
    1 = { x : a1, y : a3, r5... } -> { newX : a1, newY : a3 }
    2 = { newX : a1, newY : a3 }
    3 = a1
    4 = { x : a1, y : a3, r5... }
    5 = { newY : a3 }
    6 = a3
    7 = { x : a1, y : a3, r5... }
    8 = T{}
(\vec -> vec.x) { x = 5, { y = 7, V{} } } :: Int
((\vec -> (vec{4}.x){3}){2} { x = 5{6}, { y = 7{8}, V{}{9} }{7} }{5}){1}
    1 = Int
    2 = { x : Int, y : Int } -> Int
    3 = Int
    4 = { x : Int, y : Int }
    5 = { x : Int, y : Int }
    6 = Int
    7 = { y : Int }
    8 = Int
    9 = T{}
(\vec -> vec.z) { x = 5, { y = 7, V{} } }
Incompatible composite types { z : a2, r3... } vs. { x : Int, y : Int }
\x -> { prev = x.cur, x } :: forall a1 r2. {cur prev} ∉ r2 => { cur : a1, r2... } -> { prev : a1, cur : a1, r2... }
(\x -> { prev = (x{4}.cur){3}, x{5} }{2}){1}
    1 = { cur : a1, r2... } -> { prev : a1, cur : a1, r2... }
    2 = { prev : a1, cur : a1, r2... }
    3 = a1
    4 = { cur : a1, r2... }
    5 = { cur : a1, r2... }
{ x = 2, { x = 3, V{} } }
Added field x but already in record { x : Int }
(\r -> { x = 2, r }) { x = 3, V{} }
Field x forbidden in var r2 from record { x : Int }
(\f -> f { x = 2, V{} }) (\r -> { x = 3, r })
Field x forbidden in var r4 from record { x : Int }