Example:

-type tree(A) :: nil | {node, A, tree(A), tree(A)}.

This requires adding line numbers to constraint tuples

Types of

foo11(N) -> N = 3, foo12(N).
foo12(N) -> N.

are:

foo11 :: (integer)->integer
foo12 :: (integer)->integer

Moreover, this causes a type error (!) :

foo10(N) -> N = 3, foo12(N).
foo11(N) -> N = "", foo12(N).
foo12(N) -> N.

Make prettify return a string. This would be easier to format etc.

Currently the A is funt (A,B) -> {funt, A, B} is a parameter for one type, this needs to be changed to a list of types

Currently function types look like Haskell types, they need to look like "Erlang types"! That is: (a,b) -> a instead of a -> (b -> c)

Implement union of predicates instead of ++

Clause unification uses "pairwiseChunk" - this is ridiculous - and leads to an error. for example this will pass the type checker:

foo() -> 1.0;
foo() -> 1.0;
foo() -> true;
foo() -> false.

Instead, it should make a "chain" of unification constraints..

Requires implementation of (basic) type classes. Being able to type expressions like int + float depends on this.

Inferred type of lets(x,app(idterm(y),int(5)),X) is A !!

Trace:

Type of y = {tvar,#Ref<0.1275695646.2152202243.105277>}
Fresh Type of y = {tvar,#Ref<0.1275695646.2152202243.105277>}
App Type1 = {funt,[{tvar,#Ref<0.1275695646.2152202243.105277>}],
                  {tvar,#Ref<0.1275695646.2152202243.105277>}}
 Constraints1 = []
App Type2 = {bt,int}
 Constraints2 = []
LETX Type1 = {tvar,#Ref<0.1275695646.2152202243.105280>}
 Constraints1 = [{{funt,[{tvar,#Ref<0.1275695646.2152202243.105277>}],
                        {tvar,#Ref<0.1275695646.2152202243.105277>}},
                  {funt,[{bt,int}],
                        {tvar,#Ref<0.1275695646.2152202243.105280>}}}]
----------Env = []
Type of x = {forall,{tvar,#Ref<0.1275695646.2152202243.105280>},
                    {tvar,#Ref<0.1275695646.2152202243.105280>}}
Fresh Type of x = {tvar,#Ref<0.1275695646.2152202243.105286>}
LETX Type2 = {tvar,#Ref<0.1275695646.2152202243.105286>}
 Constraints2= []
A
Generated constraints are:
(B)->B :==: (int)->C
Inferred type: A

Do a pre-pass and assign a fresh type to each function in the environment before attempting to infer the types of each function

Currently, this program is rejected although it is semantically valid:

x() -> 
    if
      true -> X = 1;
      false -> X = 3
    end,
    X.    %%line 24

with error:

test.erl: error in parse transform 'etc': {"Type Error: 'X' not bound on line 24

already implemented by c438e15, but needs testing..

Currently, X=3 overshadows an X in scope. Instead, it should unify both the types if in scope, and extend environment otherwise.

Let the unifier continue unification in spite of failing to unify a constraint, and collect the problematic constraints separately. Printing the errors with "relevant bindings" and solved types (to the extent possible) could lead to a lot more readable errors.