Unmatchable type, following terminology from the paper. This is contrasted with a matchable type which is "injective" and "generative". Basically these unmatcha

Unmatchable type, following terminology from the paper. This is contrasted with a matchable type which is "injective" and "generative". Basically these unmatchable types are potentially ambiguous under certain operations, so it indicates to the type system limits to the transformations which can be done. So Maybe is * -> * means that if Maybe a is f a, then f is Maybe, and if Maybe a is Maybe b then a is b. If another type t is * ->> *, then the type checker can't make these assumptions.