:- set_prolog_flag(verbose,silent).
:- prompt(_, '').
:- use_module(library(readutil)).

:- set_prolog_flag(occurs_check,true).
:- op(500,yfx,$).

kind(KC,var(Z),K1) :- first(Z:K,KC), instantiate(K,K1).
kind(KC,F $ G, K2) :- kind(KC,F,K1 -> K2), kind(KC,G,K1).
kind(KC,A -> B,o)  :- kind(KC,A,o), kind(KC,B,o).

type(KC,C,var(X),     T1) --> { first(X:T,C) }, inst_type(KC,T,T1).
type(KC,C,lam(X,E), A->B) --> type(KC,[X:mono(A)|C],E,B), [kind(KC,A->B,o)].
type(KC,C,X $ Y,       B) --> type(KC,C,X,A->B), type(KC,C,Y,A).
type(KC,C,let(X=E0,E1),T) --> type(KC,C,E0,A), type(KC,[X:poly(C,A)|C],E1,T).

first(X:T,[X1:T1|_]) :- X = X1, T = T1.
first(X:T,[X1:_|Zs]) :- X\==X1, first(X:T, Zs).

instantiate(mono(T),T).
instantiate(poly(C,T),T1) :- copy_term(t(C,T),t(C,T1)).

inst_type(KC,poly(C,T),T2) -->
  { copy_term(t(C,T),t(C,T1)), 
    free_variables(T,Xs), free_variables(T1,Xs1) }, % Xs and Xs1 are same length
  samekinds(KC,Xs,Xs1), { T1=T2 }. %% unify T1 T2 later (T2 might not be var)
inst_type(_ ,mono(T),T) --> [].

samekinds(KC,[X|Xs],[Y|Ys]) --> { X\==Y }, [kind(KC,X,K),kind(KC,Y,K)],
                                samekinds(KC,Xs,Ys).
samekinds(KC,[X|Xs],[X|Ys]) --> [], samekinds(KC,Xs,Ys).
samekinds(_ ,[],[]) --> [].

variablize(var(X)) :- gensym(t,X).

main:-
	process,
	halt.

type_and_print(KC,C,E,T) :-
  phrase(type(KC,C,E,T),Gs),
  (bagof(Ty, X^Y^member(kind(X,Ty,Y),Gs), Tys); Tys=[]),
  free_variables(Tys,Xs), maplist(variablize,Xs), maplist(call,Gs),
  write("kind ctx instantiated as: "), print(KC), nl, print(E : T), nl.

process:-
	/* your code goes here */
	type_and_print(_,[],lam(x,var(x)),_), nl,
	type_and_print(_,[],lam(x,lam(y,var(y)$var(x))),_), nl,
	type_and_print(_,[],let(id=lam(x,var(x)),var(id)$var(id)),_), nl,
	KC0 =
	 [ 'Nat':mono(o)
     , 'List':mono(o->o)
     ],
	Nat = var('Nat'), List = var('List'),
    C0 =
     [ 'Zero':mono(Nat)
     , 'Succ':mono(Nat -> Nat)
     , 'Nil' :poly([], List$A)
     , 'Cons':poly([], A->((List$A)->(List$A)))
     ],
    append(KC0,_,KC1),
    type_and_print(KC1,C0,lam(x,lam(n,var(x)$var('Succ')$var(n))),_),
	true.

%% haven't really shown examples of type constructor polymorphsim or
%% kind polymorphism here but you get the idea what strucutural extensions
%% to HM are needed to support type constructor and kind polymoprhisms

:- main.