Ambiguous hyperkind
From The Twelf Project
An ambiguous hyperkind occurs in pathological cases like this:
a : type. b = a : _ _ .
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)a : type. Error: Ambiguous reconstruction Inferred: {x:`%A1%} kind Omitted term has ambiguous hyperkind Error: 1 error found
%% ABORT %%