Typecheker, backed by Prolog embedded unification and `cyclic_term/1` predicate.

tc.prolog

% Type variable.
%
tvar(A)         :- var(A).

% Type application.
%
% The `forall` is forbidden as constructor name, arglist must be non-empty.
%
tapp(FX, F, Xs) :- FX =.. [F | Xs], F \= forall, F \= prod, F \= sum, Xs \= [].

% Some grounded type.
%
tcon(Con) :- atom(Con).

% Quantified type. Is instantiated on match.
%
tqua(forall(_, X), Y) :- copy_term(X, Y).

% Labelled tensor product of types.
%
% Will attempt to pull one component at a time.
%
% When tensor op is *, its a record of (field: type).
% When tensor op is +, its a disjoint sum of (variant: type).
%
ttensor(Cat, Src, F, Ty, Dst)
    :-  of(Cat, Src, R)
    ,   ttensorAux(R, F, Ty, R1)
    ,   of(Cat, Dst, R1)
    .

ttensorAux(R, Field, Ty, Rest)
    :-  (   R   = (Field: Ty, Rest)
        
        ;   R = (X, R1)
        ,   \+ var(X)
        ,   Rest = (X, Next)
        ,   ttensorAux(R1, Field, Ty, Next)
        )
    .

% Neutral element of corresponding tensor op.
%
ttensor0(Cat, Source) :- of(Cat, Source, -).

of(Cat, X, Y) :- X =.. [Cat, Y].

% Direct sum of types.
%
tsum(Source, Field, Ty, Dest) :- ttensor(sum,  Source, Field, Ty, Dest).

% Direct product of types (record).
%
tprod(Source, Field, Ty, Dest) :- ttensor(prod, Source, Field, Ty, Dest).

% Empty sum, `void` type, uninhabited.
%
tzero(Source) :- ttensor0(sum, Source).

% Empty product, `unit` type, inhabited by only one value.
%
tone(Source) :- ttensor0(prod, Source).

% Debug print (does nothing now).
%
debug(Msg).

unify(A, B)
    :-  debug(unify(A, B))

    ,   (   % If any of types is a typevar - merge structurally.
            %
           (tvar(A); tvar(B)) -> A = B
           
            % If both are type ctors - check equality.
            %
        ;   tcon(A), tcon(B)  -> A = B

            % If both are type expressions - recursively unify items.
            %
        ;   tapp(A, F, Xs)
        ,   tapp(B, G, Ys)
        ->  unify(F, G)
        ,   maplist(unify, Xs, Ys)
            
            % If any is quantified, instantiate and unify again.
            %
        ;   tqua(A, X) -> unify(X, B)
        ;   tqua(B, Y) -> unify(A, Y)
        
            % If nothing goes, complain.
            %
        ;   die(cannot_unify(A, B))
        )
    
            % [Occurs check] Check that type is not cyclic.
            %
    ,   (   cyclic_term(A) -> die(cyclic_term(A))
        ;   true           -> true
        )
    .

% Die with a message.
%
die(Msg) :- writeln(Msg), fail.