Ambiguous hyperkind

From The Twelf Project
Jump to: navigation, search

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 %%