[jhc] explanation of FrontEnd.KindInfer.constrain

[Samuel Bronson]

On 3/18/08, John Meacham <john at repetae.net> wrote:
> On Tue, Mar 18, 2008 at 06:52:04PM -0400, Samuel Bronson wrote:
> > On 3/18/08, John Meacham <john at repetae.net> wrote:
> >
> > > 'constrain' refines a type subject to constraints, kindCombine actually
> > > returns what the unification of the kinds are. constrain works on
> > > constraints, combine works on kinds. constraints don't necessarily map
> > > to kinds, though currently most have an analog.
> >
> > Eh? Doesn't KindInfer run before typechecking begins?
>
> excuse me, I meant 'kind', not 'type'. this terminology is real
> trickylike... At least I made sure that jhc core's axioms allowed a
> stratified type system so 'term','type','kind','superkind' all are
> distinct sets and have no cyclic dependencies... though, I am not sure
> if there are practical languages where that is not the case.. though
> wacky type systems are fun to play with.

Well, it seems like constrain doesn't really have any choice but to
throw an error when asked to constrain a KBase KQuest with a
KindSimple constraint... it has no way of indicating that the result
should be a KBase KStar!