/* --------------------------------------------------------------------------
 * subst.c:     Copyright (c) Mark P Jones 1991-1998.   All rights reserved.
 *              See NOTICE for details and conditions of use etc...
 *              Hugs version 1.3b, January 1998
 *
 * Part of type checker dealing with operations on current substitution.
 * ------------------------------------------------------------------------*/

static  List	   accumVars;		/* holds constrained vars between  */
					/* unification passes		   */
static  Int        lastTyvar;		/* last tyvar visited by postUnify()*/
static  List       lastBounds;		/* bounds of lastType              */

static  List	   skolVars;		/* Current list of skolemized vars */
static  List	   skolVars2;		/* Current list of local constr/sel vars */


static Void local checkVars();

static Void local emptySubstitution() {	/* clear current substitution	   */
    numTyvars   = 0;
#if !FIXED_SUBST
    if (maxTyvars!=NUM_TYVARS) {
	maxTyvars = 0;
	if (tyvars) {
	    free(tyvars);
	    tyvars = 0;
	}
    }
#endif
    nextGeneric = 0;
    genericVars = NIL;
    typeIs      = NIL;
    accumVars   = NIL;
    lastBounds  = NIL;
    lastTyvar   = 0;
}

static Void local expandSubst(n)	/* add further n type variables to */
Int n; {				/* current substituion		   */
#if FIXED_SUBST
    if (numTyvars+n>NUM_TYVARS) {
	ERRMSG(0) "Too many type variables in type checker"
	EEND;
    }
#else
    if (numTyvars+n>maxTyvars) {	/* need to expand substitution	   */
        Int   newMax = maxTyvars+NUM_TYVARS;
	Tyvar *newTvs;
	Int   i;

	if (numTyvars+n>newMax) {	/* safety precaution		   */
	    ERRMSG(0) "Substitution expanding too quickly"
	    EEND;
	}
	
	/* It would be better to realloc() here, but that isn't portable
	 * enough for calloc()ed arrays.  The following code could cause
	 * a space leak if an interrupt occurs while we're copying the
	 * array ... we won't worry about this for the time being because
	 * we don't expect to have to go through this process much (if at
	 * all) in normal use of the type checker.
	 */

	newTvs = (Tyvar *)calloc(newMax,sizeof(Tyvar));
	if (!newTvs) {
	    ERRMSG(0) "Too many variables (%d) in type checker", newMax
	    EEND;
	}
	for (i=0; i<numTyvars;++i) {		/* copy substitution	   */
	    newTvs[i].state = tyvars[i].state;
	    newTvs[i].offs  = tyvars[i].offs;
	    newTvs[i].bound = tyvars[i].bound;
	    newTvs[i].kind  = tyvars[i].kind;
	}
	maxTyvars = 0;				/* protection from SIGINT? */
	if (tyvars) free(tyvars);
	tyvars    = newTvs;
	maxTyvars = newMax;
    }
#endif
}

static Void local resetState(tyv)
Tyvar *tyv; {
    tyv->state = NORMAL;
    tyv->bound = NIL;
    tyv->offs  = UNUSED_GENERIC;
}

static Int local newTyvars(n)	        /* allocate new type variables	   */
Int n; {				/* all of kind STAR		   */
    Int beta = numTyvars;

    expandSubst(n);
    for (numTyvars+=n; n>0; n--) {
        resetState(tyvar(numTyvars-n));
	tyvars[numTyvars-n].kind  = STAR;
#ifdef DEBUG_TYPES
	printf("new type variable: _%d ::: ",numTyvars-n);
	printKind(stdout,tyvars[numTyvars-n].kind);
	putchar('\n');
#endif
    }
    return beta;
}

static Int local newKindedVars(k,inPat)	/* allocate new variables with	   */
Kind k;					/* specified kinds		   */
Bool inPat; {				/* if k = k0 -> k1 -> ... -> kn	   */
    Int beta = numTyvars;		/* then allocate n vars with kinds */
    for (; isPair(k); k=snd(k)) {	/* k0, k1, ..., k(n-1)		   */
	expandSubst(1);			/* Dealing with quantifiers, if nec*/
        resetState(tyvar(numTyvars));
	tyvars[numTyvars].kind  = fst(k);
#ifdef DEBUG_TYPES
	printf("new type variable: _%d ::: ",numTyvars);
	printKind(stdout,tyvars[numTyvars].kind);
	putchar('\n');
#endif
	numTyvars++;
    }
    return beta;
}

#define deRef(tyv,t,o)  while ((tyv=getTypeVar(t,o)) && isBound(tyv)) { \
                            t = tyv->bound;                             \
                            o = tyv->offs;                              \
                        }

static Tyvar *local getTypeVar(t,o)	/* get number of type variable	   */
Type t; 				/* represented by (t,o) [if any].  */
Int  o; {
    switch (whatIs(t)) {
	case INTCELL : return tyvar(intOf(t));
	case OFFSET  : return tyvar(o+offsetOf(t));
    }
    return ((Tyvar *)0);
}

static Void local tyvarType(vn)       	/* load type held in type variable */
Int vn; {			       	/* vn into (typeIs,typeOff)	   */
    Tyvar *tyv;

    while ((tyv=tyvar(vn)), isBound(tyv))
	switch(whatIs(tyv->bound)) {
	    case INTCELL : vn = intOf(tyv->bound);
			   break;

	    case OFFSET  : vn = offsetOf(tyv->bound)+(tyv->offs);
			   break;

	    default	 : typeIs  = tyv->bound;
			   typeOff = tyv->offs;
			   return;
	}
    typeIs  = var;
    typeOff = vn;
}

#define bindTyv(tyv,t,o)     tyv->bound = t; tyv->offs  = o

static Void local bindTv(vn,t,o)       	/* set type variable vn to (t,o)   */
Int  vn;
Type t;
Int  o; {
    Tyvar *tyv = tyvar(vn);
    if (!isNormal(tyv))
        internal("bindTv");
    bindTyv(tyv,t,o);
#ifdef DEBUG_TYPES
    printf("binding type variable: _%d to ",vn);
    printType(stdout,debugType(t,o));
    putchar('\n');
#endif
}

static Void local expandSyn(h,ar,at,ao)	/* Expand type synonym with:	   */
Tycon h;				/* head h			   */
Int   ar;				/* ar args (NB. ar>=tycon(h).arity)*/
Type  *at;				/* original expression (*at,*ao)   */
Int   *ao; {				/* expansion returned in (*at,*ao) */
    ar -= tycon(h).arity;		/* calculate surplus arguments	   */
    if (ar==0)
	expandSyn1(h,at,ao);
    else {				/* if there are more args than the */
	Type t    = *at;		/* arity, we have to do a little   */
	Int  o    = *ao;		/* bit of work to isolate args that*/
	Type args = NIL;		/* will not be changed by expansion*/
	Int  i;
	while (ar-- > 0) {		/* find part to expand, and the	   */
	    Tyvar *tyv;			/* unused arguments		   */
	    args = cons(arg(t),args);
	    t    = fun(t);
	    deRef(tyv,t,o);
	}
	expandSyn1(h,&t,&o);		/* do the expansion		   */
	bindTv((i=newTyvars(1)),t,o);	/* and embed the results back in   */
	tyvar(i)->kind = getKind(t,o);	/* (*at, *ao) as required	   */
	*at = applyToArgs(mkInt(i),args);
    }
}

static Void local expandSyn1(h,at,ao)	/* Expand type synonym with:	   */
Tycon h;				/* head h, tycon(h).arity args,	   */
Type  *at;				/* original expression (*at,*ao)   */
Int   *ao; {				/* expansion returned in (*at,*ao) */
    Int   n = tycon(h).arity;
    Type  t = *at;
    Int   o = *ao;
    Tyvar *tyv;

    *at = tycon(h).defn;
    *ao = newKindedVars(tycon(h).kind,FALSE);
    for (; 0<n--; t=fun(t)) {
	deRef(tyv,t,o);
	if (tyv || !isAp(t))
	    internal("expandSyn1");
	bindTv(*ao+n,arg(t),o);
    }
}

static Cell local getDerefHead(t,o)	/* get value at head of type exp.  */
Type t;
Int  o; {
    Tyvar *tyv;
    argCount = 0;
    for (;;) {
	while (isAp(t)) {
	    argCount++;
	    t = fun(t);
	}
	if ((tyv=getTypeVar(t,o)) && isBound(tyv)) {
	    t = tyv->bound;
	    o = tyv->offs;
	}
	else
	    break;
    }
    if (isOffset(t))
        return mkInt(offsetOf(t)+o);
    else
        return t;
}

/* --------------------------------------------------------------------------
 * Skolemization:
 * ------------------------------------------------------------------------*/
 
static Void local skolemOffsetsAbove(n,t,o)
Int  n;
Type t;
Int  o; {
    switch(whatIs(t)) {
    	case AP      : skolemOffsetsAbove(n,fst(t),o);
    		       skolemOffsetsAbove(n,snd(t),o);
    		       break;
	case OFFSET  : if (offsetOf(t) >= n) {
	                   Tyvar *tyv = tyvar(o+offsetOf(t));
	                   if (isBound(tyv))
	                       internal("skolemOffsetsAbove");
	                   if (!isSkolem(tyv)) {
                               tyv->state = SKOLEM;
                               hd(skolVars2) = cons(mkInt(o+offsetOf(t)),hd(skolVars2));
                           }
                       }
	               break;
    }
}

static Void saveSkolem2() {
    skolVars2 = cons(NIL,skolVars2);
}

static Void local restoreSkolem2() {
    List vs = hd(skolVars2);
    for (; nonNull(vs); vs=tl(vs))
        deskolemTyvar(intOf(hd(vs)));
    skolVars2 = tl(skolVars2);
}

static Void local skolemTyvar(vn)	/* Skolemize type variable         */
Int vn; {
    Tyvar *tyv = tyvar(vn);
    if (isBound(tyv))
        skolemType(tyv->bound,tyv->offs);
    else if (isUnbound(tyv)) {
	tyv->state = SKOLEM;
    	hd(skolVars) = cons(mkInt(vn),hd(skolVars));
    }
}

static Void local skolemType(t,o)	/* Skolemize type	           */
Type t;
Int  o; {
    switch(whatIs(t)) {
    	case AP      : skolemType(fst(t),o);
    		       skolemType(snd(t),o);
    		       break;
	case OFFSET  : skolemTyvar(o+offsetOf(t));
	               break;
	case INTCELL : break;           /* Must be fresh, don't skolemize  */
    }
}

static Void local deskolemTyvar(vn)	/* Remove skolemization from tyvar */
Int vn; {
    Tyvar *tyv = tyvar(vn);
    if (!isSkolem(tyv))
        internal("deskolemTyvar");
    resetState(tyv);
}

static Void saveSkolem() {
    skolVars = cons(NIL,skolVars);
}

static Void local restoreSkolem() {
    List vs = hd(skolVars);
    for (; nonNull(vs); vs=tl(vs))
        deskolemTyvar(intOf(hd(vs)));
    skolVars = tl(skolVars);
}

/* --------------------------------------------------------------------------
 * Count tyvar references in accumulated bounds (used during unification).
 * ------------------------------------------------------------------------*/
 
static Int delta;

#define countWith(n,vn)	{delta = n; countTyvar(vn);}
#define countUp(vn)	countWith(1,vn)
#define countDown(vn)	countWith(-1,vn)

static Void local countTyvar(vn)
Int vn; {
    Tyvar *tyv = tyvar(vn);
    
    if (isBound(tyv))
        countType(tyv->bound,tyv->offs);
    else if (isCloned(tyv))
        internal("countTyvar");
    else if (!isSkolem(tyv)) {
	mkAccum(tyv);
    	tyv->offs += delta;
    	if (tyv->offs < 0)
    	    internal("refCount < 0");
    }
}

static Void local countType(t,o)
Type t;
Int  o; {
    switch(whatIs(t)) {
    	case AP      : countType(fst(t),o);
    		       countType(snd(t),o);
    		       break;
	case OFFSET  : countTyvar(o+offsetOf(t));
	               break;
	case INTCELL : countTyvar(intOf(t));
	               break;
    }
}

/* ----------------------------------------------------------------------
 * Accumulating bounds
 * ---------------------------------------------------------------------*/
 
static Void local mkAccum(tyv)
Tyvar *tyv; {
    if (!isAccum(tyv)) {
	if (!isUnbound(tyv))
	    internal("mkAccum");
        tyv->bound = NIL;
        tyv->state = ACCUM;
        tyv->offs  = 0;
        accumVars  = cons(mkInt(tyvNum(tyv)),accumVars);
    }
}

static Void accumBound(tyv,beta,z)
Tyvar *tyv;
Int   beta;
Int   z; {
    if (z != NONV) {
	mkAccum(tyv);
    	countUp(beta);
    	tyv->bound = cons(pair(mkInt(beta),mkInt(z)),tyv->bound);
    	checkVars();
    }
}

static Void local deAccum(tyv,decr)
Tyvar *tyv;
Bool decr; {
    if (isAccum(tyv)) {
	if (decr) {
	    List bs = tyv->bound;
            for (; nonNull(bs); bs=tl(bs))
            	countDown(intOf(fst(hd(bs))));
	}
	resetState(tyv);
	accumVars = removeCell(mkInt(tyvNum(tyv)),accumVars);
    }
}

/* --------------------------------------------------------------------------
 * Mark type expression, so that all variables are marked as unused generics
 * ------------------------------------------------------------------------*/

static Void local normState() {      	/* reset state for all unbound vars*/
    Int i;			
    for (i=0; i<numTyvars; ++i) {
        Tyvar *tyv = tyvar(i);
        if (!isNormal(tyv))
            resetState(tyv);
    }
}

static Void local clearOffsTyvar(vn)
Int vn; {
    Tyvar *tyv = tyvar(vn);
    
    if (isBound(tyv))
        clearOffsType(tyv->bound,tyv->offs);
    else if (!isAccum(tyv))
	tyv->offs = NONV;		/* == UNUSED_GENERIC		   */
}

static Void local clearOffsType(t,o)
Type t;
Int  o; {
    switch (whatIs(t)) {
        case AP      : clearOffsType(fst(t),o);
        	       clearOffsType(snd(t),o);
        	       return;
        case OFFSET  : if (o >= 0) clearOffsTyvar(o+offsetOf(t));
        	       return;
        case INTCELL : clearOffsTyvar(intOf(t));
        	       return;
    }
}

static Void local clearMarks() {       	/* set all unbound type vars to	   */
    Int i;			       	/* unused generic variables	   */
    for (i=0; i<numTyvars; ++i) {
        Tyvar *tyv = tyvar(i);
	if (shouldMark(tyv))
	    tyv->offs = UNUSED_GENERIC;
    }
    nextGeneric = 0;
    genericVars = NIL;
}

static Void local resetGenericsFrom(n)	/* reset all generic vars to unused*/
Int n; {				/* for generics >= n		   */
    Int i;

    if (n==0)				/* reset generic variables list	   */
	genericVars = NIL;		/* most common case: reset to zero */
    else
	for (i=length(genericVars); i>n; i--)
	    genericVars = tl(genericVars);

    for (i=0; i<numTyvars; ++i)
	if (shouldMark(tyvar(i)) && tyvar(i)->offs>=GENERIC+n)
	    tyvar(i)->offs = UNUSED_GENERIC;
    nextGeneric = n;
}

static Void local markTyvar(vn)        	/* mark fixed vars in type bound to*/
Int vn; {			       	/* given type variable		   */
    Tyvar *tyv = tyvar(vn);

    if (isBound(tyv))
	markType(tyv->bound, tyv->offs);
    else if (isAccum(tyv))
        internal("markTyvar");
    else if (isCloned(tyv)) {
        List bs = tyv->bound;
        for (; nonNull(bs); bs=tl(bs))
            markTyvar(intOf(fst(hd(bs))));
	tyv->offs = FIXED_TYVAR;
    }
    else if (!isSkolem(tyv))
	tyv->offs = FIXED_TYVAR;
}

static Void local markType(t,o)        	/* mark fixed vars in type (t,o)   */
Type t;
Int  o; {
    Int w = whatIs(t);
    switch (w) {
	case TYCON   :
	case TUPLE   : return;

	case AP      : markType(fst(t),o);
		       markType(snd(t),o);
		       return;

	case OFFSET  : markTyvar(o+offsetOf(t));
		       return;

	case INTCELL : markTyvar(intOf(t));
		       return;

	default      : internal("markType");
    }
}

/* --------------------------------------------------------------------------
 * Copy type expression from substitution to make a single type expression:
 * ------------------------------------------------------------------------*/

static Type local copyTyvar(vn)        	/* calculate most general form of  */
Int vn; {			       	/* type bound to given type var	   */
    Tyvar *tyv = tyvar(vn);

    if (isBound(tyv))
	return copyType(tyv->bound,tyv->offs);

    if (!isNormal(tyv))
        return (mkInt(vn));
                
    switch (tyv->offs) {
	case FIXED_TYVAR    : return mkInt(vn);

	case UNUSED_GENERIC : (tyv->offs) = GENERIC + nextGeneric++;
			      if (nextGeneric>=NUM_OFFSETS) {
				  ERRMSG(0)
				      "Too many quantified type variables"
				  EEND;
			      }
			      genericVars = cons(mkInt(vn),genericVars);

	default 	    : return mkOffset(tyv->offs - GENERIC);
    }
}

static Type local copyType(t,o)        	/* calculate most general form of  */
Type t; 			       	/* type expression (t,o) 	   */
Int  o; {
    switch (whatIs(t)) {
	case AP      : {   Type l = copyType(fst(t),o);  /* ensure correct */
			   Type r = copyType(snd(t),o);  /* eval. order    */
			   return ap(l,r);
		       }
	case OFFSET  : return copyTyvar(o+offsetOf(t));
	case INTCELL : return copyTyvar(intOf(t));
    }

    return t;
}

static Type local genvarTyvar(vn,vs)	/* calculate list of generic vars  */
Int  vn;				/* thru variable vn, prepended to  */
List vs; {				/* list vs			   */
    Tyvar *tyv = tyvar(vn);

    if (isBound(tyv))
	return genvarType(tyv->bound,tyv->offs,vs);
    else if (!isNormal(tyv))
        return vs;
    else if (tyv->offs == UNUSED_GENERIC) {
	tyv->offs = GENERIC + nextGeneric++;
        return cons(mkInt(vn),vs);
    }
    else if (tyv->offs>=GENERIC && !intIsMember(vn,vs))
	return cons(mkInt(vn),vs);
    else
	return vs;
}

static List local genvarType(t,o,vs)    /* calculate list of generic vars  */
Type t; 			       	/* in type expression (t,o) 	   */
Int  o;					/* results are prepended to vs	   */
List vs; {
    switch (whatIs(t)) {
	case AP      : return genvarType(snd(t),o,genvarType(fst(t),o,vs));
	case OFFSET  : return genvarTyvar(o+offsetOf(t),vs);
	case INTCELL : return genvarTyvar(intOf(t),vs);
    }
    return vs;
}

#ifdef DEBUG_TYPES
static Type local debugTyvar(vn)	/* expand type structure in full   */
Int vn; {				/* detail			   */
    Tyvar *tyv = tyvar(vn);

    if (isBound(tyv))
	return debugType(tyv->bound,tyv->offs);
    return mkInt(vn);
}

static Type local debugType(t,o)
Type t;
Int  o; {
    switch (whatIs(t)) {
	case AP      : {   Type l = debugType(fst(t),o);
			   Type r = debugType(snd(t),o);
			   return ap(l,r);
		       }
	case OFFSET  : return debugTyvar(o+offsetOf(t));
	case INTCELL : return debugTyvar(intOf(t));
    }

    return t;
}
#endif /*DEBUG_TYPES*/

/* --------------------------------------------------------------------------
 * Compute variance information
 * -------------------------------------------------------------------------*/

static Cell local getVariance(h,n)
Type h;
Int  n; {
    if (isTycon(h))
        return skipOver(length(tycon(h).arity)-n,tycon(h).variance);
    else if (isTuple(h))
        return mkInt(POSV);
    else if (isInt(h) || isOffset(h))
        return mkInt(INV);		/* higer order variance assumption */
    else
        internal("getVariance");
}

static Int local thisVariance(z)
Cell z; {
    if (isPair(z))
        return intOf(hd(z));
    else if (isInt(z))
        return intOf(z);
    else
        internal("thisVariance");
}

static Cell local nextVariance(z)
Cell z; {
    if (isPair(z))
        return tl(z);
    else if (isInt(z))
        return z;
    else
        internal("nextVariance");
}

static Void local markVarianceTyvar(vn,z)	  /* mark variance in tyvar */
Int vn;
Int z; {
    Tyvar *tyv = tyvar(vn);

    if (isBound(tyv))
	markVarianceType(tyv->bound, tyv->offs, z);
    else if (!isAccum(tyv))
	tyv->offs |= z;
}

static Void local markVarianceType(t,o,z)	  /* mark variance in type  */
Type t;
Int  o;
Int  z; {
    switch (whatIs(t)) {
        case AP      : {    Cell z1;
        		    Type h = getHead(t);
        		    
        		    if (isInt(h) || (isOffset(h) && o >= 0))
        		        h = getDerefHead(t,o);
        		    z1 = getVariance(h,argCount);
        		 
        		    while (isAp(t)) {
        		        Tyvar *tyv;
        		        markVarianceType(arg(t),o,multv(z,thisVariance(z1)));
        		        t = fun(t);
        		        if (isInt(t) || (isOffset(t) && o >= 0))
        		            deRef(tyv,t,o);
        		        z1 = nextVariance(z1);
        		    }
        		    markVarianceType(t,o,z);
        	       }
        	       break;
	
        case OFFSET  : if (o >= 0)
        		   markVarianceTyvar(o+offsetOf(t),z);
	               break;

        case INTCELL : markVarianceTyvar(intOf(t),z);
        	       break;
    }
}

/* --------------------------------------------------------------------------
 * Clone type expression by replacing each tyvar occurrence with a fresh 
 * copy, and append each new tyvar to the bounds of its origin.
 * ------------------------------------------------------------------------*/

static Type local cloneTyvar(vn,z)
Int vn;
Int z; {
    Tyvar *tyv = tyvar(vn);
    
    if (isBound(tyv))
        return cloneType(tyv->bound,tyv->offs,z);
    else {
        Int beta;
        if (isNormal(tyv)) {
            tyv->state = CLONED;
        }
        if (!isCloned(tyv))		/* Never clone skolemized tyvars */
            return mkInt(vn);
        else {
	    beta = newTyvars(1);	/* invalidates tyv */
	    tyv = tyvar(vn);	
	    tyvar(beta)->kind = tyv->kind;
	    tyv->bound = cons(pair(mkInt(beta),mkInt(z)),tyv->bound);
	    return fst(hd(tyv->bound));
	}
    }
}

static Type local cloneType(t,o,z)
Type t;
Int  o;
Int  z; {
    switch (whatIs(t)) {
	case TYCON   :
	case TUPLE   : return t;
	case AP      : {    Cell z1;
		       	    List args = NIL;
        		    Type h = getHead(t);
        		    
        		    if (isInt(h) || (isOffset(h) && o >= 0))
        		        h = getDerefHead(t,o);
        		    z1 = getVariance(h,argCount);
        		 
        		    while (isAp(t)) {
        		        Tyvar *tyv;
        		        args = cons(cloneType(arg(t),o,multv(z,thisVariance(z1))),args);
        		        t = fun(t);
        		        if (isInt(t) || (isOffset(t) && o >= 0))
        		            deRef(tyv,t,o);
        		        z1 = nextVariance(z1);
        		    }
        		    t = cloneType(t,o,z);
        		    while (nonNull(args)) {
        		        t = ap(t,hd(args));
        		        args = tl(args);
        		    }
        		    return t;
        	       }
	case OFFSET  : return (o<0) ? t : cloneTyvar(o+offsetOf(t),z);
	case INTCELL : return cloneTyvar(intOf(t),z);
	default      : internal("cloneType");
    }
}

static Type local clone(t,o,z)
Type t;
Int  z; {
    return cloneType(t,o,z);
}

static Int cloneTv(vn,z)
Int vn;
Int z; {
    Type t = clone(var,vn,z);
    if (isInt(t))
        return intOf(t);
    else {
        Int beta = newTyvars(1);
        bindTv(beta,t,0);
        return beta;
    }
}

/* --------------------------------------------------------------------------
 * Convert a CLONED tyvar to an ACCUM one, i.e. essentially remove the 
 * tyvars from its bounds and prepare for postunify.
 * ------------------------------------------------------------------------*/

static Bool local doAccum(vn)
Int vn; {
    Tyvar *tyv = tyvar(vn);
    List bs = tyv->bound;
    Int saveLastTyvar = lastTyvar;
    List saveLastBounds = lastBounds;

    resetState(tyv);
    lastTyvar  = vn;
    lastBounds = appendOnto(bs,lastBounds);
    for (; nonNull(bs) && bs!=saveLastBounds; bs=tl(bs)) {
        Int beta = intOf(fst(hd(bs)));
        Int z    = intOf(snd(hd(bs)));
        if (!accumClonedTyvar(beta,FALSE))
            return FALSE;
        if (!preUnify(var,beta,var,vn,z))
            return FALSE;
    }
    lastTyvar  = saveLastTyvar;
    lastBounds = saveLastBounds;
    return TRUE;
}

static Bool local accumClonedTyvar(vn,skip)
Int vn;
Bool skip; {
    Tyvar *tyv = tyvar(vn);
    
    if (isBound(tyv))
        return accumClonedType(tyv->bound,tyv->offs,skip);
    else if (isCloned(tyv)) {
        if (skip && tyv->offs == FIXED_TYVAR)	/* Skip these, since they are reachable   */
            return TRUE;		/* from some other cloned tyvar that will */
        else				/* be resolved later.                     */
	    return doAccum(vn);
    }
    return TRUE;
}

static Bool local accumClonedType(t,o,skip)
Type t;
Int  o;
Bool skip; {
    switch (whatIs(t)) {
        case AP      : if (!accumClonedType(fst(t),o,skip))
        		   return FALSE;
        	       return accumClonedType(snd(t),o,skip);
        case INTCELL : return accumClonedTyvar(intOf(t),skip);
        case OFFSET  : if (o>=0) 
        		   return accumClonedTyvar(o+offsetOf(t),skip);
    }
    return TRUE;
}

static Bool local accumClonedPolyType(t,skip)
Type t;
Bool skip; {
    if (isPolyType(t))
        t = monoTypeOf(t);
    if (whatIs(t) == QUAL)
        t = snd(snd(t));
    return accumClonedType(t,-1,skip);
}

/* --------------------------------------------------------------------------
 * Occurs check:
 * ------------------------------------------------------------------------*/

static Tyvar *lookingFor;	       	/* var to look for in occurs check */

static Bool local occursIn(t,o)   	/* Return TRUE if var lookingFor   */
Type t; 			       	/* is referenced in (t,o)	   */
Int o; {
    Tyvar *tyv;

    for (;;) {
	deRef(tyv,t,o);
	if (tyv)			/* type variable		   */
	    return tyv==lookingFor;
        else if (isAp(t)) {		/* application			   */
	    if (occursIn(snd(t),o))
		return TRUE;
	    else
		t = fst(t);
	}
	else                            /* no variable found		   */
	    break;
    }
    return FALSE;
}

static Bool local occurs(tyv,t,o)
Tyvar *tyv;
Type  t;
Int  o; {
    lookingFor = tyv;
    return occursIn(t,o);
}

static Bool local offsetsBetween(lo,hi,t)
Int lo, hi;
Type t; {
    switch (whatIs(t)) {
	case TYCON   :
	case TUPLE   : return FALSE;
	case AP      : return offsetsBetween(lo,hi,fun(t)) || offsetsBetween(lo,hi,arg(t));
	case OFFSET  : return lo < offsetOf(t) && offsetOf(t) <= hi;
	default      : internal("offsetsBetween");
    }
}

/* --------------------------------------------------------------------------
 * Unification algorithm:
 * ------------------------------------------------------------------------*/

static char *unifyFails = 0;		/* unification error message	   */
static Bool matchMode	= FALSE;	/* set to TRUE to prevent binding  */
					/* during matching process	   */
static Bool local failure(str)
String str; {
    unifyFails = str;
    checkVars();
    return FALSE;
}

static Bool solveAccum(tyv,t,o)		/* bind tyv to (t,o) and preUnify  */
Tyvar *tyv;				/* with accumulated bounds         */
Type  t;
Int   o; {
    List bs = NIL;
    Int  n  = 0;
    Type h;
    
    if (occurs(tyv,t,o))
        return failure("unification would give infinite type");
    if (isAccum(tyv)) {
    	bs = tyv->bound;
	n = tyv->offs;
	deAccum(tyv,TRUE);
    }
    bindTyv(tyv,t,o);
    if (n > 0)
	countWith(n,tyvNum(tyv));
    for (; nonNull(bs); bs=tl(bs))
	if (!preUnify(var,intOf(fst(hd(bs))),t,o,intOf(snd(hd(bs)))))
	    return FALSE;
    return TRUE;
}

static Bool local varToVarBind(tyv1,tyv2,z)   /* Make binding tyv1 := tyv2 */
Tyvar *tyv1;
Tyvar *tyv2;
Int z; {
    checkVars();
    if (tyv1!=tyv2) {
	if (matchMode)
	    return failure("types do not match");
        if (isCloned(tyv1) || isCloned(tyv2))
            internal("clones in varToVarBind");
	if (!eqKind(tyv1->kind,tyv2->kind))
	    return failure("constructor variable kinds do not match");
	if (!isSkolem(tyv1)) {
	    if (!isSkolem(tyv2)) {
		/* equivalent:  return solveAccum(tyv1,var,tyvNum(tyv2));  */
		if (isAccum(tyv1)) {
		    mkAccum(tyv2);
		    tyv2->bound = appendOnto(tyv1->bound,tyv2->bound);
		    tyv2->offs  = tyv1->offs + tyv2->offs;   /* ref-counts */
		    deAccum(tyv1,FALSE);
		}
		bindTyv(tyv1,var,tyvNum(tyv2));
		checkVars();
	    }
	    else
		return varToTypeAccum(tyv1,var,tyvNum(tyv2),negv(z));
	}
	else {
	    if (!isSkolem(tyv2))
	    	return varToTypeAccum(tyv2,var,tyvNum(tyv1),z);
	    else {
	        // Insert subtyping extension here...
	        return failure("quantified variable prevents unification");
	    }
	}
    }
    checkVars();
    return TRUE;
}

static Bool local varToTypeAccum(tyv,t,o,z) /* Accumulate tyv < (t,o)       */
Tyvar *tyv;
Type  t;			/* guaranteed not bo be a variable, or to  */
Int   o;			/* have synonym as outermost constr        */
Int   z; {			/* Can assume t==mkInt() => t skolemized   */
    Type h;
    checkVars();
    if (matchMode)
	return failure("types do not match");
    if (isCloned(tyv))
        internal("clone in varToTypeAccum");
    if (!eqKind(tyv->kind,getKind(t,o)))
	return failure("kinds do not match");
    if (isSkolem(tyv)) {
        h = getDerefHead(t,o);
        // Insert subtyping extension here...
        return failure("quantified variable prevents unification");
    }
    else {					  /* var to type bind      */
        Int alpha = tyvNum(tyv);
	Int beta  = newTyvars(1);		  /* invalidates tyv       */
	tyv = tyvar(alpha);
	bindTv(beta,t,o);
	accumBound(tyv,beta,z);
	return TRUE;
    }
    return FALSE; /* not reached */
}

#define lub(ts) bestBounds(ts,0,POSV)
#define glb(ts) bestBounds(ts,0,NEGV)
#define raiseArity(tc,a,z) bestBounds(singleton(tc),a,z)

static Bool local preUnify(t1,o1,t2,o2,z) /* break down constraint into a  */
Type t1,t2;				  /* set of simple constraints on  */
Int  o1,o2;				  /* variables (result is stored   */
Int  z; {				  /* in 'accumVars') 	           */
    Tyvar *tyv1, *tyv2;

    checkVars();
    unifyFails = 0;
    if (z==NONV)
	return TRUE;
        
    deRef(tyv1,t1,o1);
    deRef(tyv2,t2,o2);

un: if (tyv1)
	if (tyv2)
	    return varToVarBind(tyv1,tyv2,z);	    /* t1, t2 variables    */
	else {
	    Cell h2 = getDerefHead(t2,o2);	    /* t1 variable, t2 not */
	    if (isSynonym(h2) && argCount>=tycon(h2).arity) {
		expandSyn(h2,argCount,&t2,&o2);
		deRef(tyv2,t2,o2);
		checkVars();
		goto un;
	    }
	    return varToTypeAccum(tyv1,t2,o2,negv(z));
	}
    else
	if (tyv2) {
	    Cell h1 = getDerefHead(t1,o1);	    /* t2 variable, t1 not */
	    if (isSynonym(h1) && argCount>=tycon(h1).arity) {
		expandSyn(h1,argCount,&t1,&o1);
		deRef(tyv1,t1,o1);
		checkVars();
		goto un;
	    }
	    return varToTypeAccum(tyv2,t1,o1,z);
	}
	else {					    /* t1, t2 not vars	   */
	    Type h1 = getDerefHead(t1,o1);
	    Int  a1 = argCount;
	    Type h2 = getDerefHead(t2,o2);
	    Int  a2 = argCount;
	    checkVars();

#ifdef DEBUG_TYPES
	    printf("tt unifying types: ");
	    printType(stdout,debugType(t1,o1));
	    printf(" with ");
	    printType(stdout,debugType(t2,o2));
	    putchar('\n');
#endif

	    if (isOffset(h1) || isInt(h1)) h1=NIL;  /* represent var by NIL*/
	    if (isOffset(h2) || isInt(h2)) h2=NIL;

	    if (nonNull(h1) && h1==h2) {
	        Cell z1 = getVariance(h1,a1);
	        
		if (a1!=a2)
		    return failure("incompatible constructors");
		while (isAp(t1)) {
		    if (!preUnify(arg(t1),o1,arg(t2),o2,multv(z,thisVariance(z1))))
			return FALSE;
		    checkVars();
		    t1 = fun(t1);
		    deRef(tyv1,t1,o1);
		    t2 = fun(t2);
		    deRef(tyv2,t2,o2);
		    z1 = nextVariance(z1);
		}
		return TRUE;
	    }

	    /* Types do not match -- look for type synonyms to expand */

	    if (isSynonym(h1) && a1>=tycon(h1).arity) {
		expandSyn(h1,a1,&t1,&o1);
		deRef(tyv1,t1,o1);
		checkVars();
		goto un;
	    }
	    if (isSynonym(h2) && a2>=tycon(h2).arity) {
		expandSyn(h2,a2,&t2,&o2);
		deRef(tyv2,t2,o2);
		checkVars();
		goto un;
	    }
	    checkVars();

	    /* See if h1 and h2 are related by subtyping */
	    
	    if (!matchMode && z != INV &&
	        isTycon(h1) && isTycon(h2) && tycon(h1).what==tycon(h2).what) {
	        static String ho_err = "higher order subtyping axiom cannot be derived";
	        Type ax=NIL,s1,s2,t;
	        Int  o, n, hi, lo;
	        
		if ((tycon(h1).what==DATATYPE) == (z==POSV)) {
	            if (nonNull(ax = findAxiom(h2,h1))) {
	                instantiate(ax,&s1,&o,0);
	                s2 = satTycon(h2);
	                hi = tycon(h2).arity-1;
	                if (tcMode!=EXPRESSION)
	                    skolemOffsetsAbove(tycon(h2).arity,s1,o);
	            }
	        }
	        else {
	            if (nonNull(ax = findAxiom(h1,h2))) {
	                instantiate(ax,&s2,&o,0);
	                s1 = satTycon(h1);
	                hi = tycon(h1).arity-1;
	                if (tcMode!=EXPRESSION)
	                    skolemOffsetsAbove(tycon(h1).arity,s2,o);
	            }
	        }
	        if (isNull(ax) || (n=(tycon(h1).arity-a1)) != (tycon(h2).arity-a2))
	            return failure(0);
	            
	        /* If n > 0, try to derive a higher-order subtyping axiom */
	        
		lo = hi-n;
	        for (; n>0; n--, s1=fun(s1), s2=fun(s2))
	            if (!isOffset(arg(s1)) || arg(s1) != arg(s2))
	                return failure(ho_err);
	        if (offsetsBetween(lo,hi,s1) || offsetsBetween(lo,hi,s2))
		    return failure(ho_err);
		        
		/* Check axiom against original types */
		
		return preUnify(t1,o1,s1,o,z) &&
		       preUnify(s2,o,t2,o2,z);
	    }
	    
	    if ((isNull(h1) && a1<=a2) ||       /* last attempt -- maybe   */
		(isNull(h2) && a2<=a1))	{	/* one head is a variable? */
		Cell z1 = nonNull(h1) ? getVariance(h1,a1) 
				      : (nonNull(h2) ? getVariance(h2,a2)
				      		     : mkInt(INV));
		for (;;) {
		    deRef(tyv1,t1,o1);
		    deRef(tyv2,t2,o2);
		    checkVars();

		    if (tyv1)				/* unify heads!	   */
			if (tyv2)
			    return varToVarBind(tyv1,tyv2,z);
			else
			    return varToTypeAccum(tyv1,t2,o2,negv(z));
		    else if (tyv2)
			return varToTypeAccum(tyv2,t1,o1,z);

		    /* at this point, neither t1 nor t2 is a variable. In  */
		    /* addition, they must both be APs unless one of the   */
		    /* head variables has been bound during unification of */
		    /* the arguments.					   */

		    checkVars();
		    if (!isAp(t1) || !isAp(t2))		/* might not be APs*/
			return (t1==t2) ? TRUE : failure(0);
							/*must be APs      */
		    if (!preUnify(arg(t1),o1,arg(t2),o2,multv(z,thisVariance(z1))))
			return FALSE;
		    t1 = fun(t1);
		    t2 = fun(t2);
		    z1 = nextVariance(z1);
		}
	    }
	    
	    if (matchMode || z==INV)
	        return failure(0);
	        
	    /* One final attempt: handle arity mismatches.  Check if a      */
	    /* unique suptyping axiom can be determined on basis of the     */
	    /* arity requirements.  One typical example is the subtyping    */
	    /* problem Action < m a, which can be solved by utilizing the   */
	    /* axiom Action < Cmd ()  (in preference over Action < O s ())  */
	    	    
	    /* Todo: handle higher kinds here? */
	    
	    if (isTycon(h1) && isNull(h2) && a2>0) {
	    	List tcs = raiseArity(h1,a2,z);
	    	if (nonNull(tcs) && isNull(tl(tcs))) {
	    	    Type t;
	    	    Int  o;
	    	    instantiate(findAxiom(h1,hd(tcs)),&t,&o,0);
	    	    return preUnify(t1,o1,t,o,z) && preUnify(t,o,t2,o2,z);
	    	}
	    }
	    if (isTycon(h2) && isNull(h1) && a1>0) {
	        List tcs = raiseArity(h2,a1,negv(z));
	        if (nonNull(tcs) && isNull(tl(tcs))) {
	            Type t;
	            Int  o;
	            instantiate(findAxiom(h2,hd(tcs)),&t,&o,0);
	            return preUnify(t1,o1,t,o,z) && preUnify(t,o,t2,o2,z);
	        }
	    }
	}
    return failure(0);
}

static Int local varianceInGoal(tyv)	/* variance of tyv in current goal */
Tyvar *tyv; {
    Tyvar saved = *tyv;
    Int  z;
    List gs;
    resetState(tyv);
    if (isNull(goalStack))
        internal("varianceInGoal");
    for (gs=hd(goalStack); nonNull(gs); gs=tl(gs))
        markVarianceTyvar(intOf(hd(gs)),POSV);
    z = tyv->offs;
    *tyv = saved;
    return z;
}

static Bool local allSubtypes(ts,t,z)
List ts;
Type t;
Int  z; {
    for (; nonNull(ts); ts=tl(ts))
        if (!isSubtype(hd(ts),t,z))
            break;
    return isNull(ts);
}

static List local bestBounds(ts,a,z)
List ts;
Int  a;
Int  z; {
    List ts1;
    
    if (isNull(ts))
        return ts;
    if (isNull(tl(ts)) && a == 0)		/* trivial case			*/
        return ts;
    for (ts1=ts; nonNull(ts1); ts1=tl(ts1)) {	/* case ts contains the bound	*/
        Type h = hd(ts1);
        if (isTuple(h))
            return NIL;
        if (isInt(h))
            break;
        if (allSubtypes(ts,h,z) && tycon(h).arity >= a) {
            tl(ts1) = NIL;
            return ts1;
        }
    }
    if (nonNull(ts1)) {				/* case ts contains a skolem var*/
        if (ts1==ts && isNull(tl(ts)) && a <= length(tyvar(intOf(hd(ts)))->kind))
            return ts;
        return NIL;                             /* todo: search its bounds      */
    }
    else {					/* full search is needed	*/
        Int   w   = tycon(hd(ts)).what;
	List  bds = NIL;
	Tycon tc;
	if ((w==DATATYPE) == (z==POSV)) {
	    Tycon tc2 = lastTycon();
	    for (tc=TYCMIN; tc<=tc2; tc++)
	        if (tycon(tc).what == w && tycon(tc).arity >= a) {
		    for (ts1=ts; nonNull(ts1); ts1=tl(ts1))
		        if (!findAxiom(tc,hd(ts1)))
		            break;
		    if (isNull(ts1))
		        bds = cons(tc,bds);
		}
	}
	else {
	    for (ts1=tycon(hd(ts)).axioms; nonNull(ts1); ts1=tl(ts1)) {
	        tc = getHead(monoType(hd(ts1)));
	        if (allSubtypes(ts,tc,z) && tycon(tc).arity >= a)
	            bds = cons(tc,bds);
	    }
	}
	for (ts1=bds; nonNull(ts1); ts1=tl(ts1))
	    if (allSubtypes(bds,hd(ts1),negv(z))) {
	        tl(ts1) = NIL;
	        return ts1;
	    }
	return bds;
    }
}

static List local matchingArities(ts,loArity,hiArity)
List ts;
Int loArity;
Int hiArity; {
    List matching = NIL;
    
    for (; nonNull(ts); ts=tl(ts)) {
    	Type t = hd(ts);
    	if (isInt(t)) {		/* must be a skolemvar */
    	    Int arity = length(tyvar(intOf(t))->kind);
    	    if (loArity <= arity && hiArity <= arity)
    	    	matching = cons(t,matching);
    	    else {
    	    	/* Todo: search its bounds */
    	    }
    	} else if (isTuple(t)) {
            Int arity = tupleOf(t);
            if (loArity <= arity && hiArity <= arity)
                matching = cons(t, matching);
        } else {
    	    Int w = tycon(t).what;
    	    Int quickArity = (w==DATATYPE) ? loArity : hiArity;
    	    Int slowArity  = (w==DATATYPE) ? hiArity : loArity;
    	    Bool mismatch = FALSE;
    	    if (quickArity > tycon(t).arity) {
    	        List ts1 = tycon(t).axioms;
    	        for (; nonNull(ts1); ts1=tl(ts1))
    	            if (quickArity <= tycon(getHead(monoType(hd(ts1)))).arity)
    	            	break;
    	        if (isNull(ts1))
    	            mismatch = TRUE;
    	    }
    	    if (!mismatch && slowArity > tycon(t).arity) {
    	    	Tycon tc = TYCMIN, tc2 = lastTycon();
    	    	for (; tc <= tc2; tc++)
    	    	    if (tycon(tc).what==w && slowArity <= tycon(tc).arity && findAxiom(tc,t))
    	    	        break;
    	    	if (tc > tc2)
    	    	    mismatch = TRUE;
    	    }
    	    if (!mismatch)
    	        matching = cons(t,matching);
        }
    }
    return matching;
}

static Bool local isSubtype(t1,t2,z)
Type t1;
Type t2;
Int  z; {
    if (t1==t2)
        return TRUE;
    switch (whatIs(t1)) {
        case TUPLE   : return FALSE;
        
        case INTCELL : /* insert skolem constraint check here */ return FALSE;
        
        case TYCON   : if (isInt(t2)) {
        	           /* insert skolem constraint check here */ return FALSE;
        	       }
        	       else if ((tycon(t1).what==DATATYPE) == (z==POSV))
        		   return nonNull(findAxiom(t2,t1));
        	       else
        	           return nonNull(findAxiom(t1,t2));
    }
    internal("isSubtype");
}

static Bool local mergeBounds(tyv,t,o)		        /* Result is (*t,*o) */
Tyvar *tyv;
Type  *t;
Int   *o; {
    List bs, lo=NIL, hi=NIL;
    Int  loArity = 0, hiArity = 0;
    List bds;
    Int  n,i;
    Kind k0 = tyv->kind;
    Kind k, loKind = STAR, hiKind = STAR;
    
    if (!isAccum(tyv))
        internal("mergeBounds");
        
    for (bs=tyv->bound; nonNull(bs); bs=tl(bs)) {
	Type b = fst(hd(bs));
	Int  z = intOf(snd(hd(bs)));
	Type h = getDerefHead(b,0);
        if (isInt(h) && !isSkolem(tyvar(intOf(h)))) {
            if ((z & POSV) && argCount > loArity) {
                loArity = argCount;
                loKind = tyvar(intOf(h))->kind;
            }
            if ((z & NEGV) && argCount > hiArity) {
                hiArity = argCount;
                hiKind = tyvar(intOf(h))->kind;
            }
            continue;
        }
	if ((z & POSV) && !cellIsMember(h,lo))
	    lo = cons(h,lo);
	if ((z & NEGV) && !cellIsMember(h,hi))
	    hi = cons(h,hi);
    }

    if (isNull(lo) && isNull(hi)) {
        Int alpha = newTyvars(1);
        tyvar(alpha)->kind = hiArity > loArity ? hiKind : loKind;
        bds = singleton(mkInt(alpha));
    } else if (isNull(lo))
        bds = glb(hi);
    else if (isNull(hi))
        bds = lub(lo);
    else {
        hi = glb(hi);
        lo = lub(lo);
        bds = NIL;
        if (nonNull(lo) && nonNull(hi)) {
	    if (varianceInGoal(tyv) == NEGV) {
		for (; nonNull(hi); hi=tl(hi))
		    if (allSubtypes(lo,hd(hi),POSV))
			bds = cons(hd(hi),bds);
		if (length(bds) > 1 && length(lo) == 1)
		    bds = lo;
	    }
	    else {
		for (; nonNull(lo); lo=tl(lo))
		    if (allSubtypes(hi,hd(lo),NEGV))
			bds = cons(hd(lo),bds);
		if (length(bds) > 1 && length(hi) == 1)
		    bds = hi;
	    }
	}
    }
    
    bds = matchingArities(bds,loArity,hiArity);

    if (isNull(bds))
        return failure("variable has conflicting bounds");
    else if (nonNull(tl(bds)))
        return failure("variable has ambiguous bounds");
    *t = hd(bds);
    switch (whatIs(*t)) {
        case TYCON   : k = tycon(*t).kind;
    		       break;
    		     
        case TUPLE   : k = simpleKind(tupleOf(*t));
                       break;
                     
        case INTCELL : k = tyvar(intOf(*t))->kind;
        	       break;
        	       
        default      : internal("mergeBounds");
    }
    *o = newTyvars(0);
    for (n=0; isPair(k); k=snd(k),n++) {
        if (eqKind(k,k0))
            break;
    	tyvar(newTyvars(1))->kind = fst(k);
    }
    if (k==STAR && k0!=STAR)
        return failure("kind error in higher-order bound");
    for (i=0; i<n; ++i)
	*t = ap(*t,mkOffset(i));
    return TRUE;
}

static Bool local postUnify() {		/* solve accumulated constraints   */

    while (nonNull(accumVars)) {
        Tyvar *tyv;
	List  vs,bs;
	Type  t;
	Int   o;
	
	checkVars();
	for (vs=accumVars; nonNull(vs); vs=tl(vs)) {/* find unreferenced var */
	    if (tyvar(intOf(hd(vs)))->offs == 0)
	        break;
	}
	        
	lastTyvar = intOf(hd(nonNull(vs) ? vs : accumVars));
	tyv = tyvar(lastTyvar);
	if (!isAccum(tyv))
	    internal("postUnify");
	bs = lastBounds = tyv->bound;

	/* If vs==NIL we have a pending infinite type error, but we */
	/* continue until we have a directly recursive constraint   */
	/* for the sake of a more readable error message.           */

	if (vs==NIL) {
	    for (; nonNull(bs); bs=tl(bs))
	        if (occurs(tyv,var,intOf(fst(hd(bs)))))
	            return failure("constraints are recursive");
	    bs = lastBounds;
	}
	    
	if (isNull(bs)) {	   /* short-circuit empty or single bounds */
	    if (nonNull(vs))
		deAccum(tyv,TRUE);
	    else
		accumVars = tl(accumVars);
	    continue;
	} else if (isNull(tl(bs))) {
	    countDown(intOf(fst(hd(bs))));
	    tyv->bound = NIL;
	    if (!solveAccum(tyv,var,intOf(fst(hd(bs)))))
	        return FALSE;
	    continue;
	}
	
	if (!mergeBounds(tyv,&t,&o))	  /* general case, result is (t,o) */
	    return FALSE;
	if (!solveAccum(tyvar(lastTyvar),t,o))
	    return FALSE;
	checkVars();
    }
    return TRUE;
}

static Bool local unify(t1,o1,t2,o2)	/* Main unification routine	   */
Type t1,t2;				/* unify (t1,o1) with (t2,o2)	   */
Int  o1,o2; {
    lastTyvar  = 0;
    lastBounds = NIL;
    if (!preUnify(t1,o1,t2,o2,POSV))
        return FALSE;
    return postUnify();
}

static Bool local sameType(t1,o1,t2,o2)   /* Compare types without binding */
Type t1,t2;
Int  o1,o2; {
    Bool result;
    matchMode = TRUE;
    result    = unify(t1,o1,t2,o2);
    matchMode = FALSE;
    return result;
}

/* --------------------------------------------------------------------------
 * Unify kind expressions:
 * ------------------------------------------------------------------------*/

static Bool local kvarToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2	   */
Tyvar *tyv1, *tyv2; {			  /* for kind variable bindings	   */
    if (tyv1!=tyv2) {
	tyv1->bound = var;
	tyv1->offs  = tyvNum(tyv2);
    }
    return TRUE;
}

static Bool local kvarToTypeBind(tyv,t,o)/* Make binding tyv := (t,o)	   */
Tyvar *tyv;				/* for kind variable bindings	   */
Type  t;				/* guaranteed not to be a v'ble or */
Int   o; {				/* have synonym as outermost constr*/
    if (occurs(tyv,t,o))
	return failure("unification would give infinite kind");
    tyv->bound = t;
    tyv->offs  = o;
    return TRUE;
}

static Bool local kunify(k1,o1,k2,o2)	/* Unify kind expr (k1,o1) with	   */
Kind k1,k2;				/* (k2,o2)			   */
Int  o1,o2; {
    Tyvar *kyv1, *kyv2;

    deRef(kyv1,k1,o1);
    deRef(kyv2,k2,o2);

    if (kyv1)
        if (kyv2)
	    return kvarToVarBind(kyv1,kyv2);	    /* k1, k2 variables    */
        else
	    return kvarToTypeBind(kyv1,k2,o2);	    /* k1 variable, k2 not */
    else
        if (kyv2)
	    return kvarToTypeBind(kyv2,k1,o1);	    /* k2 variable, k1 not */
	else
	    if (k1==STAR && k2==STAR)		    /* k1, k2 not vars	   */
		return TRUE;
	    else if (isAp(k1) && isAp(k2))
		return kunify(fst(k1),o1,fst(k2),o2) &&
		       kunify(snd(k1),o1,snd(k2),o2);
    return failure(0);
}

/*-------------------------------------------------------------------------*/

static Void local checkVars() {
#if 0
    List vs, bs;
    Tyvar *tyv, *tyv1, *tyv2;
    Int lenBs, beta, beta1, p, z, len = length(accumVars);
    
    for (vs=accumVars; nonNull(vs); vs=tl(vs)) {
        beta = intOf(hd(vs));
        tyv  = tyvar(beta);
        if (cellIsMember(hd(vs),tl(vs)))
            internal("duplicates in accumVars");
        if (!isAccum(tyv))
            internal("no accum");
        lenBs = length(tyv->bound);
        if (tyv->offs < 0)
            internal("negative refcount");
        for (bs=tyv->bound; nonNull(bs); bs=tl(bs)) {
            p = hd(bs);
            z = intOf(snd(p));
            beta1 = intOf(fst(p));
            tyv1 = tyvar(beta1);
            if (isAccum(tyv1))
                internal("bound has accum");
            if ((tyv2=getTypeVar(tyv1->bound,tyv1->offs)) && !isSkolem(tyv2))
                internal("var at head");
            countDown(beta1);
        }
    }
    for (vs=accumVars; nonNull(vs); vs=tl(vs)) {
        beta = intOf(hd(vs));
        tyv = tyvar(beta);
        if (tyv->offs != 0)
            internal("refCount mismatch");
    }
    for (vs=accumVars; nonNull(vs); vs=tl(vs)) {
        beta = intOf(hd(vs));
        tyv = tyvar(beta);
        for (bs=tyv->bound; nonNull(bs); bs=tl(bs)) {
            p = hd(bs);
            z = intOf(snd(p));
            beta1 = intOf(fst(p));
            tyv1 = tyvar(beta1);
            countUp(beta1);
        }
    }
    for (vs=skolVars; nonNull(vs); vs=tl(vs)) {
        List vs1;
        for (vs1=hd(vs); nonNull(vs1); vs1=tl(vs1)) {
	    beta = intOf(hd(vs1));
            tyv = tyvar(beta);
            if (!isSkolem(tyv))
                internal("no skolem");
        }
    }
    for (vs=skolVars2; nonNull(vs); vs=tl(vs)) {
        List vs1;
        for (vs1=hd(vs); nonNull(vs1); vs1=tl(vs1)) {
	    beta = intOf(hd(vs1));
            tyv = tyvar(beta);
            if (!isSkolem(tyv))
                internal("no skolem");
        }
    }
#endif
}