Lambda the Ultimate

I'm working on a constraint based hybrid type system. The idea is to use a constraint as the type of all the value that it could be bound to. For example a finite domain range constraint like 1..7 would be the type of integers between 1 and 7. By default this test would be done at runtime, but as there are some fairly strong ties between type inference and checking, and constraint propagation I think that it should be posible to move a lot of the checking to compile time.

But the problem is that 1..7 would not ony have integers as members but also other ranges like 2..4, and most importantly, it would be a member of it self. Actually as any value could be considerd as a constraint, every term vould be a type (and a kind) and a member of itself. This would wreck havoc on the Curry Howard Isomorphism, as every proposition would be a prof of itself, and thats a rather meaningless logic language.

But im not that good at type theory so I wonder exactly what do I lose by not being able to use CHI and other type theoretical works based on it?

Is there a generic term for deriving lower-order concept form a higher-order concept? I'll illustrate this question with the following example:

A language has concept of class. A class is 'defined' by notion:

class myclass ...;

A class is instantiated by notion

myclass myvar = new myclass();

Instance of a class is an object and it appears to be a first-order concept. A particular class is a second-order concept, and 'class' as a notion of a class concept is a third-order concept.

In MPS their are giving ability to "define" (?) third-order concepts with notion of fourth-order concept noted as "concept", e.g.:

concept class;

Thus, we may say that in each of these examples a lower-order concept is "derived" from a higher-order concept.

What is the right term for this act?