ghc/interpreter/subst.c

   1
   2 /* --------------------------------------------------------------------------
   3  * Provides an implementation for the `current substitution' used during
   4  * type and kind inference in both static analysis and type checking.
   5  *
   6  * The Hugs 98 system is Copyright (c) Mark P Jones, Alastair Reid, the
   7  * Yale Haskell Group, and the Oregon Graduate Institute of Science and
   8  * Technology, 1994-1999, All rights reserved.  It is distributed as
   9  * free software under the license in the file "License", which is
  10  * included in the distribution.
  11  *
  12  * $RCSfile: subst.c,v $
  13  * $Revision: 1.17 $
  14  * $Date: 2000/03/23 14:54:21 $
  15  * ------------------------------------------------------------------------*/
  16
  17 #include "hugsbasictypes.h"
  18 #include "storage.h"
  19 #include "connect.h"
  20 #include "errors.h"
  21
  22
  23 /*#define DEBUG_TYPES*/
  24
  25 static Int numTyvars;                   /* no. type vars currently in use  */
  26 static Int maxTyvars = 0;
  27 static Int nextGeneric;                 /* number of generics found so far */
  28
  29 Tyvar  *tyvars = 0;                     /* storage for type variables      */
  30 Int    typeOff;                         /* offset of result type           */
  31 Type   typeIs;                          /* skeleton of result type         */
  32 Int    typeFree;                        /* freedom in instantiated type    */
  33 List   predsAre;                        /* list of predicates in type      */
  34 List   genericVars;                     /* list of generic vars            */
  35 List   btyvars = NIL;                   /* explicitly scoped type vars     */
  36
  37 /* --------------------------------------------------------------------------
  38  * local function prototypes:
  39  * ------------------------------------------------------------------------*/
  40
  41 static Void local expandSubst           ( Int );
  42 static Int  local findBtyvsInt          ( Text );
  43 static Type local makeTupleType         ( Int );
  44 static Kind local makeSimpleKind        ( Int );
  45 static Kind local makeVarKind           ( Int );
  46 static Void local expandSyn1            ( Tycon, Type *, Int * );
  47 static List local listTyvar             ( Int,List );
  48 static List local listTyvars            ( Type,Int,List );
  49 static Cell local dupTyvar              ( Int,List );
  50 static Cell local dupTyvars             ( Cell,Int,List );
  51 static Pair local copyNoMark            ( Cell,Int );
  52 static Type local dropRank1Body         ( Type,Int,Int );
  53 static Type local liftRank1Body         ( Type,Int );
  54 static Bool local matchTypeAbove        ( Type,Int,Type,Int,Int );
  55
  56 static Bool local varToVarBind          ( Tyvar *,Tyvar * );
  57 static Bool local varToTypeBind         ( Tyvar *,Type,Int );
  58 #if TREX
  59 static Bool local inserter              ( Type,Int,Type,Int );
  60 static Int  local remover               ( Text,Type,Int );
  61 static Int  local tailVar               ( Type,Int );
  62 #endif
  63
  64 static Bool local improveAgainst        ( Int,List,Cell,Int );
  65 static Bool local instImprove           ( Int,Class,Cell,Int );
  66 static Bool local pairImprove           ( Int,Class,Cell,Int,Cell,Int,Int );
  67 #if IPARAM
  68 static Bool local ipImprove             ( Int,Cell,Int,Cell,Int );
  69 #endif
  70
  71 static Bool local kvarToVarBind         ( Tyvar *,Tyvar * );
  72 static Bool local kvarToTypeBind        ( Tyvar *,Type,Int );
  73
  74 /* --------------------------------------------------------------------------
  75  * The substitution, types, and kinds:
  76  *
  77  * In early versions of Gofer, the `substitution' data structure was only
  78  * used by the type checker, so it made sense to include support for it in
  79  * type.c.  This changed when kinds and kind inference where introduced,
  80  * which required access to the substitution during static analysis.  The
  81  * links between type.c and static.c that were intially used to accomplish
  82  * this have now been avoided by making the substitution visible as an
  83  * independent data structure in storage.c.
  84  *
  85  * In the same way that values have types, type constructors (and more
  86  * generally, expressions built from such constructors) have kinds.
  87  * The syntax of kinds in the current implementation is very simple:
  88  *
  89  *        kind ::= STAR         -- the kind of types
  90  *              |  kind => kind -- constructors
  91  *              |  variables    -- either INTCELL or OFFSET
  92  *
  93  * For various reasons, this implementation uses structure sharing, instead
  94  * of a copying approach.  In principal, this is fast and avoids the need to
  95  * build new type expressions.  Unfortunately, this implementation will not
  96  * be able to handle *very* large expressions.
  97  *
  98  * The substitution is represented by an array of type variables each of
  99  * which is a triple:
 100  *      bound   a (skeletal) type expression, or NIL if the variable
 101  *              is not bound, or SKOLEM for a Skolem constant (i.e., an
 102  *              uninstantiable variable).
 103  *      offs    offset of skeleton in bound.  If isNull(bound), then offs is
 104  *              used to indicate whether that variable is generic (i.e. free
 105  *              in the current assumption set) or fixed (i.e. bound in the
 106  *              current assumption set).  Generic variables are assigned
 107  *              offset numbers whilst copying type expressions (t,o) to
 108  *              obtain their most general form.
 109  *      kind    kind of value bound to type variable (`type variable' is
 110  *              rather inaccurate -- `constructor variable' would be better).
 111  * ------------------------------------------------------------------------*/
 112
 113 Void emptySubstitution() {              /* clear current substitution      */
 114     numTyvars   = 0;
 115     if (maxTyvars!=NUM_TYVARS) {
 116         maxTyvars = 0;
 117         if (tyvars) {
 118             free(tyvars);
 119             tyvars = 0;
 120         }
 121     }
 122     nextGeneric = 0;
 123     genericVars = NIL;
 124     typeIs      = NIL;
 125     predsAre    = NIL;
 126     btyvars     = NIL;
 127 }
 128
 129 static Void local expandSubst(n)        /* add further n type variables to */
 130 Int n; {                                /* current substituion             */
 131     if (numTyvars+n>maxTyvars) {        /* need to expand substitution     */
 132         Int   newMax = maxTyvars+NUM_TYVARS;
 133         Tyvar *newTvs;
 134         Int   i;
 135
 136         if (numTyvars+n>newMax) {       /* safety precaution               */
 137             ERRMSG(0) "Substitution expanding too quickly"
 138             EEND;
 139         }
 140
 141         /* It would be better to realloc() here, but that isn't portable
 142          * enough for calloc()ed arrays.  The following code could cause
 143          * a space leak if an interrupt occurs while we're copying the
 144          * array ... we won't worry about this for the time being because
 145          * we don't expect to have to go through this process much (if at
 146          * all) in normal use of the type checker.
 147          */
 148
 149         newTvs = (Tyvar *)calloc(newMax,sizeof(Tyvar));
 150         if (!newTvs) {
 151             ERRMSG(0) "Too many variables (%d) in type checker", newMax
 152             EEND;
 153         }
 154         for (i=0; i<numTyvars;++i) {            /* copy substitution       */
 155             newTvs[i].offs  = tyvars[i].offs;
 156             newTvs[i].bound = tyvars[i].bound;
 157             newTvs[i].kind  = tyvars[i].kind;
 158         }
 159         maxTyvars = 0;                          /* protection from SIGINT? */
 160         if (tyvars) free(tyvars);
 161         tyvars    = newTvs;
 162         maxTyvars = newMax;
 163     }
 164 }
 165
 166 Int newTyvars(n)                        /* allocate new type variables     */
 167 Int n; {                                /* all of kind STAR                */
 168     Int beta = numTyvars;
 169
 170     expandSubst(n);
 171     for (numTyvars+=n; n>0; n--) {
 172         tyvars[numTyvars-n].offs  = UNUSED_GENERIC;
 173         tyvars[numTyvars-n].bound = NIL;
 174         tyvars[numTyvars-n].kind  = STAR;
 175 #ifdef DEBUG_TYPES
 176         Printf("new type variable: _%d ::: ",numTyvars-n);
 177         printKind(stdout,tyvars[numTyvars-n].kind);
 178         Putchar('\n');
 179 #endif
 180     }
 181     return beta;
 182 }
 183
 184 Int newKindedVars(k)                    /* allocate new variables with     */
 185 Kind k; {                               /* specified kinds                 */
 186     Int beta = numTyvars;               /* if k = k0 -> k1 -> ... -> kn    */
 187     for (; isPair(k); k=snd(k)) {       /* then allocate n vars with kinds */
 188         expandSubst(1);                 /* k0, k1, ..., k(n-1)             */
 189         tyvars[numTyvars].offs  = UNUSED_GENERIC;
 190         tyvars[numTyvars].bound = NIL;
 191         tyvars[numTyvars].kind  = fst(k);
 192 #ifdef DEBUG_TYPES
 193         Printf("new type variable: _%d ::: ",numTyvars);
 194         printKind(stdout,tyvars[numTyvars].kind);
 195         Putchar('\n');
 196 #endif
 197         numTyvars++;
 198     }
 199     return beta;
 200 }
 201
 202 Void instantiate(type)                  /* instantiate type, if nonNull    */
 203 Type type; {
 204     predsAre = NIL;
 205     typeIs   = type;
 206     typeFree = 0;
 207
 208     if (nonNull(typeIs)) {             /* instantiate type expression ?    */
 209
 210         if (isPolyType(typeIs)) {      /* Polymorphic type scheme ?        */
 211             Kinds ks = polySigOf(typeIs);
 212             typeOff  = newKindedVars(ks);
 213             typeIs   = monotypeOf(typeIs);
 214             for (; isAp(ks); ks=arg(ks))
 215                 typeFree++;
 216         }
 217
 218         if (isQualType(typeIs)) {    /* Qualified type?                    */
 219             predsAre = fst(snd(typeIs));
 220             typeIs   = snd(snd(typeIs));
 221         }
 222     }
 223 }
 224
 225 /* --------------------------------------------------------------------------
 226  * Bound type variables:
 227  * ------------------------------------------------------------------------*/
 228
 229 Pair findBtyvs(t)                       /* Look for bound tyvar            */
 230 Text t; {
 231     List bts = btyvars;
 232     for (; nonNull(bts); bts=tl(bts)) {
 233         List bts1 = hd(bts);
 234         for (; nonNull(bts1); bts1=tl(bts1))
 235             if (t==textOf(fst(hd(bts1))))
 236                 return hd(bts1);
 237     }
 238     return NIL;
 239 }
 240
 241 static Int local findBtyvsInt(t)        /* Look for bound type variable    */
 242 Text t; {                               /* expecting to find an integer    */
 243     Pair p = findBtyvs(t);
 244     if (isNull(p))
 245         internal("findBtyvsInt");
 246     return intOf(snd(p));
 247 }
 248
 249 Void markBtyvs() {                      /* Mark explicitly scoped vars     */
 250     List bts = btyvars;
 251     for (; nonNull(bts); bts=tl(bts)) {
 252         List bts1 = hd(bts);
 253         for (; nonNull(bts1); bts1=tl(bts1))
 254             markTyvar(intOf(snd(hd(bts1))));
 255     }
 256 }
 257
 258 Type localizeBtyvs(t)                   /* Localize type to eliminate refs */
 259 Type t; {                               /* to explicitly scoped vars       */
 260     switch (whatIs(t)) {
 261         case RANK2    :
 262         case POLYTYPE : snd(snd(t)) = localizeBtyvs(snd(snd(t)));
 263                         break;
 264
 265         case QUAL     : fst(snd(t)) = localizeBtyvs(fst(snd(t)));
 266                         snd(snd(t)) = localizeBtyvs(snd(snd(t)));
 267                         break;
 268
 269         case AP       : fst(t) = localizeBtyvs(fst(t));
 270                         snd(t) = localizeBtyvs(snd(t));
 271                         break;
 272
 273         case VARIDCELL:
 274         case VAROPCELL: return mkInt(findBtyvsInt(textOf(t)));
 275     }
 276     return t;
 277 }
 278
 279 /* --------------------------------------------------------------------------
 280  * Dereference or bind types in subsitution:
 281  * ------------------------------------------------------------------------*/
 282
 283 Tyvar *getTypeVar(t,o)                  /* get number of type variable     */
 284 Type t;                                 /* represented by (t,o) [if any].  */
 285 Int  o; {
 286     switch (whatIs(t)) {
 287         case INTCELL   : return tyvar(intOf(t));
 288         case OFFSET    : return tyvar(o+offsetOf(t));
 289         case VARIDCELL :
 290         case VAROPCELL : return tyvar(findBtyvsInt(textOf(t)));
 291     }
 292     return ((Tyvar *)0);
 293 }
 294
 295 Void tyvarType(vn)                      /* load type held in type variable */
 296 Int vn; {                               /* vn into (typeIs,typeOff)        */
 297     Tyvar *tyv;
 298
 299     while ((tyv=tyvar(vn)), isBound(tyv))
 300         switch(whatIs(tyv->bound)) {
 301             case INTCELL   : vn = intOf(tyv->bound);
 302                              break;
 303
 304             case OFFSET    : vn = offsetOf(tyv->bound)+(tyv->offs);
 305                              break;
 306
 307             case VARIDCELL :
 308             case VAROPCELL : vn = findBtyvsInt(textOf(tyv->bound));
 309                              break;
 310
 311             default        : typeIs  = tyv->bound;
 312                              typeOff = tyv->offs;
 313                              return;
 314         }
 315     typeIs  = aVar;
 316     typeOff = vn;
 317 }
 318
 319 Void bindTv(vn,t,o)                     /* set type variable vn to (t,o)   */
 320 Int  vn;
 321 Type t;
 322 Int  o; {
 323     Tyvar *tyv = tyvar(vn);
 324     tyv->bound = t;
 325     tyv->offs  = o;
 326 #ifdef DEBUG_TYPES
 327     Printf("binding type variable: _%d to ",vn);
 328     printType(stdout,debugType(t,o));
 329     Putchar('\n');
 330 #endif
 331 }
 332
 333 Cell getDerefHead(t,o)                  /* get value at head of type exp.  */
 334 Type t;
 335 Int  o; {
 336     Tyvar *tyv;
 337     argCount = 0;
 338     for (;;) {
 339         while (isAp(t)) {
 340             argCount++;
 341             t = fun(t);
 342         }
 343         if ((tyv=getTypeVar(t,o)) && isBound(tyv)) {
 344             t = tyv->bound;
 345             o = tyv->offs;
 346         }
 347         else
 348             break;
 349     }
 350     return t;
 351 }
 352
 353 /* --------------------------------------------------------------------------
 354  * Expand type synonyms:
 355  * ------------------------------------------------------------------------*/
 356
 357 Void expandSyn(h,ar,at,ao)              /* Expand type synonym with:       */
 358 Tycon h;                                /* head h                          */
 359 Int   ar;                               /* ar args (NB. ar>=tycon(h).arity)*/
 360 Type  *at;                              /* original expression (*at,*ao)   */
 361 Int   *ao; {                            /* expansion returned in (*at,*ao) */
 362     ar -= tycon(h).arity;               /* calculate surplus arguments     */
 363     if (ar==0)
 364         expandSyn1(h,at,ao);
 365     else {                              /* if there are more args than the */
 366         Type t    = *at;                /* arity, we have to do a little   */
 367         Int  o    = *ao;                /* bit of work to isolate args that*/
 368         Type args = NIL;                /* will not be changed by expansion*/
 369         Int  i;
 370         while (ar-- > 0) {              /* find part to expand, and the    */
 371             Tyvar *tyv;                 /* unused arguments                */
 372             args = cons(arg(t),args);
 373             t    = fun(t);
 374             deRef(tyv,t,o);
 375         }
 376         expandSyn1(h,&t,&o);            /* do the expansion                */
 377         bindTv((i=newTyvars(1)),t,o);   /* and embed the results back in   */
 378         tyvar(i)->kind = getKind(t,o);  /* (*at, *ao) as required          */
 379         *at = applyToArgs(mkInt(i),args);
 380     }
 381 }
 382
 383 static Void local expandSyn1(h,at,ao)   /* Expand type synonym with:       */
 384 Tycon h;                                /* head h, tycon(h).arity args,    */
 385 Type  *at;                              /* original expression (*at,*ao)   */
 386 Int   *ao; {                            /* expansion returned in (*at,*ao) */
 387     Int   n = tycon(h).arity;
 388     Type  t = *at;
 389     Int   o = *ao;
 390     Tyvar *tyv;
 391
 392     *at = tycon(h).defn;
 393     *ao = newKindedVars(tycon(h).kind);
 394     for (; 0<n--; t=fun(t)) {
 395         deRef(tyv,t,o);
 396         if (tyv || !isAp(t))
 397             internal("expandSyn1");
 398         bindTv(*ao+n,arg(t),o);
 399     }
 400 }
 401
 402 /* --------------------------------------------------------------------------
 403  * Marking fixed variables in type expressions:
 404  * ------------------------------------------------------------------------*/
 405
 406 Void clearMarks() {                     /* Set all unbound type vars to    */
 407     Int i;                              /* unused generic variables        */
 408     for (i=0; i<numTyvars; ++i)
 409         if (!isBound(tyvar(i)))
 410             tyvar(i)->offs = UNUSED_GENERIC;
 411     genericVars = NIL;
 412     nextGeneric = 0;
 413 }
 414
 415 Void markAllVars() {                    /* Set all unbound type vars to    */
 416     Int i;                              /* be fixed vars                   */
 417     for (i=0; i<numTyvars; ++i)
 418         if (!isBound(tyvar(i)))
 419             tyvar(i)->offs = FIXED_TYVAR;
 420     genericVars = NIL;
 421     nextGeneric = 0;
 422 }
 423
 424 Void resetGenerics() {                  /* Reset all generic vars to unused*/
 425     Int i;
 426     for (i=0; i<numTyvars; ++i)
 427         if (!isBound(tyvar(i)) && tyvar(i)->offs>=GENERIC)
 428             tyvar(i)->offs = UNUSED_GENERIC;
 429     genericVars = NIL;
 430     nextGeneric = 0;
 431 }
 432
 433 Void markTyvar(vn)                      /* mark fixed vars in type bound to*/
 434 Int vn; {                               /* given type variable             */
 435     Tyvar *tyv = tyvar(vn);
 436
 437     if (isBound(tyv))
 438         markType(tyv->bound, tyv->offs);
 439     else
 440         (tyv->offs) = FIXED_TYVAR;
 441 }
 442
 443 Void markType(t,o)                      /* mark fixed vars in type (t,o)   */
 444 Type t;
 445 Int  o; {
 446     STACK_CHECK
 447     switch (whatIs(t)) {
 448         case POLYTYPE  :
 449         case QUAL      :
 450 #if TREX
 451         case EXT       :
 452 #endif
 453         case TYCON     :
 454         case TUPLE     : return;
 455
 456         case AP        : markType(fst(t),o);
 457                          markType(snd(t),o);
 458                          return;
 459
 460         case OFFSET    : markTyvar(o+offsetOf(t));
 461                          return;
 462
 463         case INTCELL   : markTyvar(intOf(t));
 464                          return;
 465
 466         case VARIDCELL :
 467         case VAROPCELL : markTyvar(findBtyvsInt(textOf(t)));
 468                          return;
 469
 470         case RANK2     : markType(snd(snd(t)),o);
 471                          return;
 472
 473         default        : internal("markType");
 474     }
 475 }
 476
 477 Void markPred(pi)                       /* Marked fixed type vars in pi    */
 478 Cell pi; {
 479     Cell cl = fst3(pi);
 480     Int  o  = intOf(snd3(pi));
 481
 482     for (; isAp(cl); cl=fun(cl))
 483         markType(arg(cl),o);
 484 }
 485
 486 /* --------------------------------------------------------------------------
 487  * Copy type expression from substitution to make a single type expression:
 488  * ------------------------------------------------------------------------*/
 489
 490 Type copyTyvar(vn)                      /* calculate most general form of  */
 491 Int vn; {                               /* type bound to given type var    */
 492     Tyvar *tyv = tyvar(vn);
 493
 494     if ((tyv->bound)==SKOLEM) {
 495         return mkInt(vn);
 496     } else if (tyv->bound) {
 497         return copyType(tyv->bound,tyv->offs);
 498     }
 499
 500     switch (tyv->offs) {
 501         case FIXED_TYVAR    : return mkInt(vn);
 502
 503         case UNUSED_GENERIC : (tyv->offs) = GENERIC + nextGeneric++;
 504                               if (nextGeneric>=(OFF_MAX-OFF_MIN+1)) {
 505                                   ERRMSG(0)
 506                                       "Too many quantified type variables"
 507                                   EEND;
 508                               }
 509                               genericVars = cons(mkInt(vn),genericVars);
 510
 511         default             : return mkOffset(tyv->offs - GENERIC);
 512     }
 513 }
 514
 515 Type copyType(t,o)                      /* calculate most general form of  */
 516 Type t;                                 /* type expression (t,o)           */
 517 Int  o; {
 518     STACK_CHECK
 519     switch (whatIs(t)) {
 520         case AP        : {   Type l = copyType(fst(t),o);/* ensure correct */
 521                              Type r = copyType(snd(t),o);/* eval. order    */
 522                              return ap(l,r);
 523                          }
 524         case OFFSET    : return copyTyvar(o+offsetOf(t));
 525         case INTCELL   : return copyTyvar(intOf(t));
 526         case VARIDCELL :
 527         case VAROPCELL : return copyTyvar(findBtyvsInt(textOf(t)));
 528     }
 529
 530     return t;
 531 }
 532
 533 Cell copyPred(pi,o)                     /* Copy single predicate (or part  */
 534 Cell pi;                                /* thereof) ...                    */
 535 Int  o; {
 536     if (isAp(pi)) {
 537         Cell temp = copyPred(fun(pi),o);/* to ensure correct order of eval.*/
 538         return ap(temp,copyType(arg(pi),o));
 539     }
 540     else
 541         return pi;
 542 }
 543
 544 Type zonkTyvar(vn)      /* flatten type by chasing all references          */
 545 Int vn; {               /* and collapsing OFFSETS to absolute indexes      */
 546     Tyvar *tyv = tyvar(vn);
 547
 548     if (tyv->bound)
 549         return zonkType(tyv->bound,tyv->offs);
 550     else
 551         return mkInt(vn);
 552 }
 553
 554 Type zonkType(t,o)      /* flatten type by chasing all references          */
 555 Type t;                 /* and collapsing OFFSETS to absolute indexes      */
 556 Int  o; {
 557     STACK_CHECK
 558     switch (whatIs(t)) {
 559         case AP        : {   Type l = zonkType(fst(t),o);/* ensure correct */
 560                              Type r = zonkType(snd(t),o);/* eval. order    */
 561                              return ap(l,r);
 562                          }
 563         case OFFSET    : return zonkTyvar(o+offsetOf(t));
 564         case INTCELL   : return zonkTyvar(intOf(t));
 565     }
 566
 567     return t;
 568 }
 569
 570 #ifdef DEBUG_TYPES
 571 Type debugTyvar(vn)                     /* expand type structure in full   */
 572 Int vn; {                               /* detail                          */
 573     Tyvar *tyv = tyvar(vn);
 574
 575     if (isBound(tyv))
 576         return debugType(tyv->bound,tyv->offs);
 577     return mkInt(vn);
 578 }
 579
 580 Type debugType(t,o)
 581 Type t;
 582 Int  o; {
 583     STACK_CHECK
 584     switch (whatIs(t)) {
 585         case AP        : {   Type l = debugType(fst(t),o);
 586                              Type r = debugType(snd(t),o);
 587                              return ap(l,r);
 588                          }
 589         case OFFSET    : return debugTyvar(o+offsetOf(t));
 590         case INTCELL   : return debugTyvar(intOf(t));
 591         case VARIDCELL :
 592         case VAROPCELL : return debugTyvar(findBtyvsInt(textOf(t)));
 593     }
 594
 595     return t;
 596 }
 597 List debugContext(ps)
 598 List ps; {
 599     Cell p;
 600     List qs = NIL;
 601     for (; nonNull(ps); ps=tl(ps)) {
 602         p = debugPred(fst3(hd(ps)),intOf(snd3(hd(ps))));
 603         qs = cons(p,qs);
 604     }
 605     return rev(qs);
 606 }
 607
 608 Cell debugPred(pi,o)
 609 Cell pi;
 610 Int  o; {
 611     if (isAp(pi)) {
 612         return pair(debugPred(fun(pi),o),debugType(arg(pi),o));
 613     }
 614     return pi;
 615 }
 616 #endif /*DEBUG_TYPES*/
 617
 618 Kind copyKindvar(vn)                    /* build kind attatched to variable*/
 619 Int vn; {
 620     Tyvar *tyv = tyvar(vn);
 621     if (tyv->bound)
 622         return copyKind(tyv->bound,tyv->offs);
 623     return STAR;                        /* any unbound variable defaults to*/
 624 }                                       /* the kind of all types           */
 625
 626 Kind copyKind(k,o)                      /* build kind expression from      */
 627 Kind k;                                 /* given skeleton                  */
 628 Int  o; {
 629     switch (whatIs(k)) {
 630         case AP      : {   Kind l = copyKind(fst(k),o);  /* ensure correct */
 631                            Kind r = copyKind(snd(k),o);  /* eval. order    */
 632                            return ap(l,r);
 633                        }
 634         case OFFSET  : return copyKindvar(o+offsetOf(k));
 635         case INTCELL : return copyKindvar(intOf(k));
 636     }
 637     return k;
 638 }
 639
 640 /* --------------------------------------------------------------------------
 641  * Copy type expression from substitution without marking:
 642  * ------------------------------------------------------------------------*/
 643
 644 static List local listTyvar(vn,ns)
 645 Int  vn;
 646 List ns; {
 647     Tyvar *tyv = tyvar(vn);
 648
 649     if (isBound(tyv)) {
 650         return listTyvars(tyv->bound,tyv->offs,ns);
 651     } else if (!intIsMember(vn,ns)) {
 652         ns = cons(mkInt(vn),ns);
 653     }
 654     return ns;
 655 }
 656
 657 static List local listTyvars(t,o,ns)
 658 Cell t;
 659 Int  o;
 660 List ns; {
 661     switch (whatIs(t)) {
 662         case AP        : return listTyvars(fst(t),o,
 663                                  listTyvars(snd(t),o,
 664                                   ns));
 665         case OFFSET    : return listTyvar(o+offsetOf(t),ns);
 666         case INTCELL   : return listTyvar(intOf(t),ns);
 667         default        : break;
 668     }
 669     return ns;
 670 }
 671
 672 static Cell local dupTyvar(vn,ns)
 673 Int  vn;
 674 List ns; {
 675     Tyvar *tyv = tyvar(vn);
 676
 677     if (isBound(tyv)) {
 678         return dupTyvars(tyv->bound,tyv->offs,ns);
 679     } else {
 680         Int i = 0;
 681         for (; nonNull(ns) && vn!=intOf(hd(ns)); ns=tl(ns)) {
 682             i++;
 683         }
 684         return mkOffset(i);
 685     }
 686 }
 687
 688 static Cell local dupTyvars(t,o,ns)
 689 Cell t;
 690 Int  o;
 691 List ns; {
 692     switch (whatIs(t)) {
 693         case AP        : {   Type l = dupTyvars(fst(t),o,ns);
 694                              Type r = dupTyvars(snd(t),o,ns);
 695                              return ap(l,r);
 696                          }
 697         case OFFSET    : return dupTyvar(o+offsetOf(t),ns);
 698         case INTCELL   : return dupTyvar(intOf(t),ns);
 699     }
 700     return t;
 701 }
 702
 703 static Cell local copyNoMark(t,o)       /* Copy a type or predicate without*/
 704 Cell t;                                 /* changing marks                  */
 705 Int  o; {
 706     List ns     = listTyvars(t,o,NIL);
 707     Cell result = pair(ns,dupTyvars(t,o,ns));
 708     for (; nonNull(ns); ns=tl(ns)) {
 709         hd(ns) = tyvar(intOf(hd(ns)))->kind;
 710     }
 711     return result;
 712 }
 713
 714 /* --------------------------------------------------------------------------
 715  * Droping and lifting of type schemes that appear in rank 2 position:
 716  * ------------------------------------------------------------------------*/
 717
 718 Type dropRank2(t,alpha,n)               /* Drop a (potentially) rank2 type */
 719 Type t;
 720 Int  alpha;
 721 Int  n; {
 722     if (whatIs(t)==RANK2) {
 723         Cell r  = fst(snd(t));
 724         Int  i  = intOf(r);
 725         Type as = NIL;
 726         for (t=snd(snd(t)); i>0; i--) {
 727             Type a = arg(fun(t));
 728             if (isPolyType(a))
 729                 a = dropRank1(a,alpha,n);
 730             as = fn(a,as);
 731             t  = arg(t);
 732         }
 733         t = ap(RANK2,pair(r,revOnto(as,t)));
 734     }
 735     return t;
 736 }
 737
 738 Type dropRank1(t,alpha,n)               /* Copy rank1 argument type t to   */
 739 Type t;                                 /* make a rank1 type scheme        */
 740 Int  alpha;
 741 Int  n; {
 742     if (n>0 && isPolyType(t))
 743         t = mkPolyType(polySigOf(t),dropRank1Body(monotypeOf(t),alpha,n));
 744     return t;
 745 }
 746
 747 static Type local dropRank1Body(t,alpha,n)
 748 Type t;
 749 Int  alpha;
 750 Int  n; {
 751     switch (whatIs(t)) {
 752         case OFFSET   : {   Int m = offsetOf(t);
 753                             return (m>=n) ? mkOffset(m-n) : mkInt(alpha+m);
 754                         }
 755
 756         case POLYTYPE : return mkPolyType(polySigOf(t),
 757                                           dropRank1Body(monotypeOf(t),alpha,n));
 758
 759         case QUAL     : return ap(QUAL,dropRank1Body(snd(t),alpha,n));
 760
 761         case RANK2    : return ap(RANK2,pair(fst(snd(t)),
 762                                              dropRank1Body(snd(snd(t)),
 763                                                            alpha,
 764                                                            n)));
 765
 766         case AP       : return ap(dropRank1Body(fun(t),alpha,n),
 767                                   dropRank1Body(arg(t),alpha,n));
 768
 769         default       : return t;
 770     }
 771 }
 772
 773 Void liftRank2Args(as,alpha,m)
 774 List as;
 775 Int  alpha;
 776 Int  m; {
 777     Int i = 0;
 778     for (; i<m; i++)
 779         copyTyvar(alpha+i);
 780     for (m=nextGeneric; nonNull(as); as=tl(as)) {
 781         Type ta = arg(fun(as));
 782         ta      = isPolyType(ta) ? liftRank1Body(ta,m) : copyType(ta,alpha);
 783         arg(fun(as))
 784                 = ta;
 785     }
 786 }
 787
 788 Type liftRank2(t,alpha,m)
 789 Type t;
 790 Int  alpha;
 791 Int  m; {
 792     if (whatIs(t)==RANK2) {
 793         Cell r  = fst(snd(t));
 794         Int  i  = 0;
 795         Type as = NIL;
 796         for (; i<m; i++)
 797             copyTyvar(alpha+i);
 798         m = nextGeneric;
 799         t = snd(snd(t));
 800         for (i=intOf(r); i>0; i--) {
 801             Type a = arg(fun(t));
 802             a      = isPolyType(a) ? liftRank1Body(a,m) : copyType(a,alpha);
 803             as     = fn(a,as);
 804             t      = arg(t);
 805         }
 806         t = ap(RANK2,pair(r,revOnto(as,copyType(t,alpha))));
 807     }
 808     else
 809         t = copyType(t,alpha);
 810     return t;
 811 }
 812
 813 Type liftRank1(t,alpha,m)
 814 Type t;
 815 Int  alpha;
 816 Int  m; {
 817     if (m>0 && isPolyType(t)) {
 818         Int i = 0;
 819         resetGenerics();
 820         for (; i<m; i++)
 821             copyTyvar(alpha+i);
 822         t = liftRank1Body(t,nextGeneric);
 823     }
 824     return t;
 825 }
 826
 827 static Type local liftRank1Body(t,n)
 828 Type t;
 829 Int  n; {
 830     switch (whatIs(t)) {
 831         case OFFSET    : return mkOffset(n+offsetOf(t));
 832
 833         case INTCELL   : return copyTyvar(intOf(t));
 834
 835         case VARIDCELL :
 836         case VAROPCELL : return copyTyvar(findBtyvsInt(textOf(t)));
 837
 838         case POLYTYPE  : return mkPolyType(polySigOf(t),
 839                                            liftRank1Body(monotypeOf(t),n));
 840
 841         case QUAL      : return ap(QUAL,liftRank1Body(snd(t),n));
 842
 843         case RANK2     : return ap(RANK2,pair(fst(snd(t)),
 844                                               liftRank1Body(snd(snd(t)),n)));
 845
 846         case AP        : return ap(liftRank1Body(fun(t),n),
 847                                    liftRank1Body(arg(t),n));
 848
 849         default        : return t;
 850     }
 851 }
 852
 853 /* --------------------------------------------------------------------------
 854  * Support for `kind preserving substitutions' from unification:
 855  * ------------------------------------------------------------------------*/
 856
 857 Bool eqKind(k1,k2)                      /* check that two (mono)kinds are  */
 858 Kind k1, k2; {                          /* equal                           */
 859     return k1==k2
 860            || (isPair(k1) && isPair(k2)
 861               && eqKind(fst(k1),fst(k2))
 862               && eqKind(snd(k1),snd(k2)));
 863 }
 864
 865 Kind getKind(c,o)                       /* Find kind of constr during type */
 866 Cell c;                                 /* checking process                */
 867 Int  o; {
 868     if (isAp(c))                                        /* application     */
 869         return snd(getKind(fst(c),o));
 870     switch (whatIs(c)) {
 871         case TUPLE     : return simpleKind(tupleOf(c)); /*(,)::* -> * -> * */
 872         case OFFSET    : return tyvar(o+offsetOf(c))->kind;
 873         case INTCELL   : return tyvar(intOf(c))->kind;
 874         case VARIDCELL :
 875         case VAROPCELL : return tyvar(findBtyvsInt(textOf(c)))->kind;
 876         case TYCON     : return tycon(c).kind;
 877 #if TREX
 878         case EXT    : return extKind;
 879 #endif
 880     }
 881 #ifdef DEBUG_KINDS
 882     Printf("getKind c = %d, whatIs=%d\n",c,whatIs(c));
 883 #endif
 884     internal("getKind");
 885     return STAR;/* not reached */
 886 }
 887
 888 /* --------------------------------------------------------------------------
 889  * Find generic variables in a type:
 890  * ------------------------------------------------------------------------*/
 891
 892 Type genvarTyvar(vn,vs)                 /* calculate list of generic vars  */
 893 Int  vn;                                /* thru variable vn, prepended to  */
 894 List vs; {                              /* list vs                         */
 895     Tyvar *tyv = tyvar(vn);
 896
 897     if (isBound(tyv))
 898         return genvarType(tyv->bound,tyv->offs,vs);
 899     else if (tyv->offs == UNUSED_GENERIC) {
 900         tyv->offs += GENERIC + nextGeneric++;
 901         return cons(mkInt(vn),vs);
 902     }
 903     else if (tyv->offs>=GENERIC && !intIsMember(vn,vs))
 904         return cons(mkInt(vn),vs);
 905     else
 906         return vs;
 907 }
 908
 909 List genvarType(t,o,vs)                 /* calculate list of generic vars  */
 910 Type t;                                 /* in type expression (t,o)        */
 911 Int  o;                                 /* results are prepended to vs     */
 912 List vs; {
 913     switch (whatIs(t)) {
 914         case AP        : return genvarType(snd(t),o,genvarType(fst(t),o,vs));
 915         case OFFSET    : return genvarTyvar(o+offsetOf(t),vs);
 916         case INTCELL   : return genvarTyvar(intOf(t),vs);
 917         case VARIDCELL :
 918         case VAROPCELL : return genvarTyvar(findBtyvsInt(textOf(t)),vs);
 919     }
 920     return vs;
 921 }
 922
 923 /* --------------------------------------------------------------------------
 924  * Occurs check:
 925  * ------------------------------------------------------------------------*/
 926
 927 Bool doesntOccurIn(lookFor,t,o)         /* Return TRUE if var lookFor      */
 928 Tyvar *lookFor;                         /* isn't referenced in (t,o)       */
 929 Type  t;
 930 Int   o; {
 931     Tyvar *tyv;
 932
 933     STACK_CHECK
 934     for (;;) {
 935         deRef(tyv,t,o);
 936         if (tyv)                        /* type variable                   */
 937             return tyv!=lookFor;
 938         else if (isAp(t)) {             /* application                     */
 939             if (doesntOccurIn(lookFor,snd(t),o))
 940                 t = fst(t);
 941             else
 942                 return FALSE;
 943         }
 944         else                            /* no variable found               */
 945             break;
 946     }
 947     return TRUE;
 948 }
 949
 950 /* --------------------------------------------------------------------------
 951  * Unification algorithm:
 952  * ------------------------------------------------------------------------*/
 953
 954 char   *unifyFails   = 0;               /* Unification error message       */
 955 static Int bindAbove = 0;               /* Used to restrict var binding    */
 956
 957 #define bindOnlyAbove(beta)     bindAbove=beta
 958 #define noBind()                bindAbove=MAXPOSINT
 959 #define unrestrictBind()        bindAbove=0
 960
 961 static Bool local varToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2      */
 962 Tyvar *tyv1, *tyv2; {
 963     if (tyv1!=tyv2) {                   /* If vars are same, nothing to do!*/
 964
 965         /* Check that either tyv1 or tyv2 is in allowed range for binding  */
 966         /* and is not a Skolem constant, and swap vars if nec. so we can   */
 967         /* bind to tyv1.                                                   */
 968
 969         if (tyvNum(tyv1)<bindAbove || tyv1->bound==SKOLEM) {
 970             if (tyvNum(tyv2)<bindAbove || tyv2->bound==SKOLEM) {
 971                 unifyFails = "types do not match";
 972                 return FALSE;
 973             }
 974             else {
 975                 Tyvar *tyv = tyv1;
 976                 tyv1       = tyv2;
 977                 tyv2       = tyv;
 978             }
 979         }
 980         if (!eqKind(tyv1->kind,tyv2->kind)) {
 981             unifyFails = "constructor variable kinds do not match";
 982             return FALSE;
 983         }
 984         tyv1->bound = aVar;
 985         tyv1->offs  = tyvNum(tyv2);
 986 #ifdef DEBUG_TYPES
 987         Printf("vv binding tyvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
 988 #endif
 989     }
 990     return TRUE;
 991 }
 992
 993 static Bool local varToTypeBind(tyv,t,o)/* Make binding tyv := (t,o)       */
 994 Tyvar *tyv;
 995 Type  t;                                /* guaranteed not to be a v'ble or */
 996 Int   o; {                              /* have synonym as outermost constr*/
 997     if (tyvNum(tyv)<bindAbove) {        /* Check that tyv is in range      */
 998         unifyFails = "types do not match";
 999         return FALSE;
1000     }
1001     else if (tyv->bound == SKOLEM) {    /* Check that it is not Skolemized */
1002         unifyFails = "cannot instantiate Skolem constant";
1003         return FALSE;
1004     }
1005     else if (!doesntOccurIn(tyv,t,o))   /* Carry out occurs check          */
1006         unifyFails = "unification would give infinite type";
1007     else if (!eqKind(tyv->kind,getKind(t,o)))
1008         unifyFails = "kinds do not match";
1009     else {
1010         tyv->bound = t;
1011         tyv->offs  = o;
1012 #ifdef DEBUG_TYPES
1013         Printf("vt binding type variable: _%d to ",tyvNum(tyv));
1014         printType(stdout,debugType(t,o));
1015         Putchar('\n');
1016 #endif
1017         return TRUE;
1018     }
1019     return FALSE;
1020 }
1021
1022 Bool unify(t1,o1,t2,o2)                 /* Main unification routine        */
1023 Type t1,t2;                             /* unify (t1,o1) with (t2,o2)      */
1024 Int  o1,o2; {
1025     Tyvar *tyv1, *tyv2;
1026
1027     STACK_CHECK
1028     deRef(tyv1,t1,o1);
1029     deRef(tyv2,t2,o2);
1030
1031 un: if (tyv1) {
1032         if (tyv2)
1033             return varToVarBind(tyv1,tyv2);         /* t1, t2 variables    */
1034         else {
1035             Cell h2 = getDerefHead(t2,o2);          /* t1 variable, t2 not */
1036             if (isSynonym(h2) && argCount>=tycon(h2).arity) {
1037                 expandSyn(h2,argCount,&t2,&o2);
1038                 deRef(tyv2,t2,o2);
1039                 goto un;
1040             }
1041             return varToTypeBind(tyv1,t2,o2);
1042         }
1043     }
1044     else
1045         if (tyv2) {
1046             Cell h1 = getDerefHead(t1,o1);          /* t2 variable, t1 not */
1047             if (isSynonym(h1) && argCount>=tycon(h1).arity) {
1048                 expandSyn(h1,argCount,&t1,&o1);
1049                 deRef(tyv1,t1,o1);
1050                 goto un;
1051             }
1052             return varToTypeBind(tyv2,t1,o1);
1053         }
1054         else {                                      /* t1, t2 not vars     */
1055             Type h1 = getDerefHead(t1,o1);
1056             Int  a1 = argCount;
1057             Type h2 = getDerefHead(t2,o2);
1058             Int  a2 = argCount;
1059
1060 #ifdef DEBUG_TYPES
1061             Printf("tt unifying types: ");
1062             printType(stdout,debugType(t1,o1));
1063             Printf(" with ");
1064             printType(stdout,debugType(t2,o2));
1065             Putchar('\n');
1066 #endif
1067             if (isOffset(h1) || isInt(h1)) h1=NIL;  /* represent var by NIL*/
1068             if (isOffset(h2) || isInt(h2)) h2=NIL;
1069
1070 #if TREX
1071             if (isExt(h1) || isExt(h2)) {
1072                 if (a1==2 && isExt(h1) && a2==2 && isExt(h2)) {
1073                     if (extText(h1)==extText(h2)) {
1074                         return unify(arg(fun(t1)),o1,arg(fun(t2)),o2) &&
1075                                 unify(arg(t1),o1,arg(t2),o2);
1076                     } else {
1077                         return inserter(t1,o1,t2,o2) &&
1078                                   unify(arg(t1),o1,aVar,
1079                                      remover(extText(h1),t2,o2));
1080                     }
1081                 } else {
1082                     unifyFails = "rows are not compatible";
1083                     return FALSE;
1084                 }
1085             }
1086 #endif
1087             if (nonNull(h1) && h1==h2) {/* Assuming well-formed types, both*/
1088                 if (a1!=a2) {           /* t1, t2 must have same no of args*/
1089                     unifyFails = "incompatible constructors";
1090                     return FALSE;
1091                 }
1092                 while (isAp(t1)) {
1093                     if (!unify(arg(t1),o1,arg(t2),o2))
1094                         return FALSE;
1095                     t1 = fun(t1);
1096                     deRef(tyv1,t1,o1);
1097                     t2 = fun(t2);
1098                     deRef(tyv2,t2,o2);
1099                 }
1100                 unifyFails = 0;
1101                 return TRUE;
1102             }
1103
1104             /* Types do not match -- look for type synonyms to expand */
1105
1106             if (isSynonym(h1) && a1>=tycon(h1).arity) {
1107                 expandSyn(h1,a1,&t1,&o1);
1108                 deRef(tyv1,t1,o1);
1109                 goto un;
1110             }
1111             if (isSynonym(h2) && a2>=tycon(h2).arity) {
1112                 expandSyn(h2,a2,&t2,&o2);
1113                 deRef(tyv2,t2,o2);
1114                 goto un;
1115             }
1116
1117             if ((isNull(h1) && a1<=a2) ||       /* last attempt -- maybe   */
1118                 (isNull(h2) && a2<=a1)) {       /* one head is a variable? */
1119                 for (;;) {
1120                     deRef(tyv1,t1,o1);
1121                     deRef(tyv2,t2,o2);
1122
1123                     if (tyv1) {                         /* unify heads!    */
1124                         if (tyv2)
1125                             return varToVarBind(tyv1,tyv2);
1126                         else
1127                             return varToTypeBind(tyv1,t2,o2);
1128                     }
1129                     else if (tyv2)
1130                         return varToTypeBind(tyv2,t1,o1);
1131
1132                     /* at this point, neither t1 nor t2 is a variable. In  */
1133                     /* addition, they must both be APs unless one of the   */
1134                     /* head variables has been bound during unification of */
1135                     /* the arguments.                                      */
1136
1137                     if (!isAp(t1) || !isAp(t2)) {       /* might not be APs*/
1138                         unifyFails = 0;
1139                         return t1==t2;
1140                     }
1141                     if (!unify(arg(t1),o1,arg(t2),o2))  /* o/w must be APs */
1142                         return FALSE;
1143                     t1 = fun(t1);
1144                     t2 = fun(t2);
1145                 }
1146             }
1147         }
1148     unifyFails = 0;
1149     return FALSE;
1150 }
1151
1152 #if TREX
1153 static Bool local inserter(r1,o1,r,o)   /* Insert first field in (r1,o1)   */
1154 Type r1;                                /* into row (r,o), both of which   */
1155 Int  o1;                                /* are known to begin with an EXT  */
1156 Type r;
1157 Int  o; {
1158     Text labt = extText(fun(fun(r1)));  /* Find the text of the label      */
1159 #ifdef DEBUG_TYPES
1160     Printf("inserting ");
1161     printType(stdout,debugType(r1,o1));
1162     Printf(" into ");
1163     printType(stdout,debugType(r,o));
1164     Putchar('\n');
1165 #endif
1166     for (;;) {
1167         Tyvar *tyv;
1168         deRef(tyv,r,o);
1169         if (tyv) {
1170             Int beta;                   /* Test for common tail            */
1171             if (tailVar(arg(r1),o1)==tyvNum(tyv)) {
1172                 unifyFails = "distinct rows have common tail";
1173                 return FALSE;
1174             }
1175             beta = newTyvars(1);        /* Extend row with new field       */
1176             tyvar(beta)->kind = ROW;
1177             return varToTypeBind(tyv,ap(fun(r1),mkInt(beta)),o1);
1178         }
1179         else if (isAp(r) && isAp(fun(r)) && isExt(fun(fun(r)))) {
1180             if (labt==extText(fun(fun(r))))/* Compare existing fields      */
1181                 return unify(arg(fun(r1)),o1,extField(r),o);
1182             r = extRow(r);              /* Or skip to next field           */
1183         }
1184         else {                          /* Nothing else will match         */
1185             unifyFails = "field mismatch";
1186             return FALSE;
1187         }
1188     }
1189 }
1190
1191 static Int local remover(l,r,o)         /* Make a new row by copying (r,o) */
1192 Text l;                                 /* but removing the l field (which */
1193 Type r;                                 /* MUST exist)                     */
1194 Int  o; {
1195     Tyvar *tyv;
1196     Int    beta       = newTyvars(1);
1197     tyvar(beta)->kind = ROW;
1198 #ifdef DEBUG_TYPES
1199     Printf("removing %s from",textToStr(l));
1200     printType(stdout,debugType(r,o));
1201     Putchar('\n');
1202 #endif
1203     deRef(tyv,r,o);
1204     if (tyv || !isAp(r) || !isAp(fun(r)) || !isExt(fun(fun(r))))
1205         internal("remover");
1206     if (l==extText(fun(fun(r))))
1207         r = extRow(r);
1208     else
1209         r = ap(fun(r),mkInt(remover(l,extRow(r),o)));
1210     bindTv(beta,r,o);
1211     return beta;
1212 }
1213
1214
1215 static Int local tailVar(r,o)           /* Find var at tail end of a row   */
1216 Type r;
1217 Int  o; {
1218     for (;;) {
1219         Tyvar *tyv;
1220         deRef(tyv,r,o);
1221         if (tyv) {
1222             return tyvNum(tyv);
1223         }
1224         else if (isAp(r) && isAp(fun(r)) && isExt(fun(fun(r)))) {
1225             r = extRow(r);
1226         }
1227         else {
1228             return (-1);
1229         }
1230     }
1231 }
1232 #endif
1233
1234
1235 Bool typeMatches(type,mt)               /* test if type matches monotype mt*/
1236     Type type, mt; {                    /* imported from STG Hugs          */
1237     Bool result;
1238      if (isPolyOrQualType(type))
1239         return FALSE;
1240     emptySubstitution();
1241     noBind();
1242     result = unify(mt,0,type,0);
1243     unrestrictBind();
1244     emptySubstitution();
1245     return result;
1246 }
1247
1248 Bool isProgType(ks,type)                /* Test if type is of the form     */
1249 List ks;                                /* IO t for some t.                */
1250 Type type; {
1251     Bool result;
1252     Int  alpha;
1253     Int  beta;
1254     emptySubstitution();
1255     alpha  = newKindedVars(ks);
1256     beta   = newTyvars(1);
1257     bindOnlyAbove(beta);
1258     result = unify(type,alpha,typeProgIO,beta);
1259     unrestrictBind();
1260     emptySubstitution();
1261     return result;
1262 }
1263
1264 /* --------------------------------------------------------------------------
1265  * Matching predicates:
1266  *
1267  * There are (at least) four situations where we need to match up pairs
1268  * of predicates:
1269  *
1270  *   1) Testing to see if two predicates are the same (ignoring differences
1271  *      caused by the use of type synonyms, for example).
1272  *
1273  *   2) Matching a predicate with the head of its class so that we can
1274  *      find the corresponding superclass predicates.  If the predicates
1275  *      have already been kind-checked, and the classes are known to be
1276  *      the same, then this should never fail.
1277  *
1278  *   3) Matching a predicate against the head of an instance to see if
1279  *      that instance is applicable.
1280  *
1281  *   4) Matching two instance heads to see if there is an overlap.
1282  *
1283  * For (1), we need a matching process that does not bind any variables.
1284  * For (2) and (3), we need to use one-way matching, only allowing
1285  * variables in the class or instance head to be instantiated.  For
1286  * (4), we need two-way unification.
1287  *
1288  * Another situation in which both one-way and two-way unification might
1289  * be used is in an implementation of improvement.  Here, a one-way match
1290  * would be used to determine applicability of a rule for improvement
1291  * that would then be followed by unification with another predicate.
1292  * One possible syntax for this might be:
1293  *
1294  *     instance P => pi [improves pi'] where ...
1295  *
1296  * The intention here is that any predicate matching pi' can be unified
1297  * with pi to get more accurate types.  A simple example of this is:
1298  *
1299  *   instance Collection [a] a improves Collection [a] b where ...
1300  *
1301  * As soon as we know what the collection type is (in this case, a list),
1302  * we will also know what the element type is.  To ensure that the rule
1303  * for improvement is valid, the compilation system will also need to use
1304  * a one-way matching process to ensure that pi is a (substitution) instance
1305  * of pi'.  Another extension would be to allow more than one predicate pi'
1306  * in an improving rule.  Read the paper on simplification and improvement
1307  * for technical background.  Watch this space for implementation news!
1308  * ------------------------------------------------------------------------*/
1309
1310 Bool samePred(pi1,o1,pi,o)              /* Test to see if predicates are   */
1311 Cell pi1;                               /* the same, with no binding of    */
1312 Int  o1;                                /* the variables in either one.    */
1313 Cell pi;                                /* Assumes preds are kind correct  */
1314 Int  o; {                               /* with the same class.            */
1315     Bool result;
1316     noBind();
1317     result = unifyPred(pi1,o1,pi,o);
1318     unrestrictBind();
1319     return result;
1320 }
1321
1322 Bool matchPred(pi1,o1,pi,o)             /* One way match predicate (pi1,o1)*/
1323 Cell pi1;                               /* against (pi,o), allowing only   */
1324 Int  o1;                                /* vars in 2nd pred to be bound.   */
1325 Cell pi;                                /* Assumes preds are kind correct  */
1326 Int  o; {                               /* with the same class and that no */
1327     Bool result;                        /* vars have been alloc'd since o. */
1328     bindOnlyAbove(o);
1329     result = unifyPred(pi1,o1,pi,o);
1330     unrestrictBind();
1331     return result;
1332 }
1333
1334 Bool unifyPred(pi1,o1,pi,o)             /* Unify two predicates            */
1335 Cell pi1;                               /* Assumes preds are kind correct  */
1336 Int  o1;                                /* with the same class.            */
1337 Cell pi;
1338 Int  o; {
1339   for (; isAp(pi1); pi1=fun(pi1), pi=fun(pi)) {
1340         if (!isAp(pi) || !unify(arg(pi1),o1,arg(pi),o))
1341             return FALSE;
1342   }
1343   /* pi1 has exhausted its argument chain, we also need to check that
1344      pi has no remaining arguments.  However, under this condition,
1345      the pi1 == pi will always return FALSE, giving the desired
1346      result. */
1347
1348 #if IPARAM
1349     if (isIP(pi1) && isIP(pi))
1350         return textOf(pi1)==textOf(pi);
1351     else
1352 #endif
1353     return pi1==pi;
1354 }
1355
1356 #if TREX
1357 static Cell trexShow = NIL;             /* Used to test for show on records*/
1358 static Cell trexEq   = NIL;             /* Used to test for eq on records  */
1359 #endif
1360
1361 Inst findInstFor(pi,o)                  /* Find matching instance for pred */
1362 Cell  pi;                               /* (pi,o), or otherwise NIL.  If a */
1363 Int   o; {                              /* match is found, then tyvars from*/
1364     Class c = getHead(pi);              /* typeOff have been initialized to*/
1365     List  ins;                          /* allow direct use of specifics.  */
1366     Cell  kspi = NIL;
1367
1368     if (!isClass(c))
1369         return NIL;
1370
1371     for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins)) {
1372         Inst in   = hd(ins);
1373         Int  beta = newKindedVars(inst(in).kinds);
1374         if (matchPred(pi,o,inst(in).head,beta)) {
1375             typeOff = beta;
1376             return in;
1377         }
1378         else {
1379             numTyvars = beta;
1380             if (allowOverlap) {
1381                 Int alpha = newKindedVars(inst(in).kinds);
1382                 if (isNull(kspi)) {
1383                     kspi = copyNoMark(pi,o);
1384                 }
1385                 beta = newKindedVars(fst(kspi));
1386                 if (matchPred(inst(in).head,alpha,snd(kspi),beta)) {
1387                     numTyvars = alpha;
1388                     return NIL;
1389                 }
1390                 numTyvars = alpha;
1391             }
1392         }
1393     }
1394     unrestrictBind();
1395
1396 #if TREX
1397     {   Bool wantShow   = (c==findQualClass(trexShow));
1398         Bool wantEither = wantShow || (c==findQualClass(trexEq));
1399
1400         if (wantEither) {                       /* Generate instances of   */
1401             Type  t = arg(pi);                  /* ShowRecRow and EqRecRow */
1402             Tyvar *tyv;                         /* on the fly              */
1403             Cell  e;
1404             deRef(tyv,t,o);
1405             e = getHead(t);
1406             if (isExt(e)) {
1407                 Inst in = NIL;
1408                 for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins))
1409                     if (getHead(arg(inst(hd(ins)).head))==e) {
1410                         in = hd(ins);
1411                         break;
1412                     }
1413                 if (isNull(in))
1414                     in = (wantShow ? addRecShowInst(c,e) : addRecEqInst(c,e));
1415                 typeOff = newKindedVars(extKind);
1416                 bindTv(typeOff,arg(fun(t)),o);
1417                 bindTv(typeOff+1,arg(t),o);
1418                 return in;
1419             }
1420         }
1421     }
1422 #endif
1423
1424     return NIL;
1425 }
1426
1427 #if MULTI_INST
1428 List findInstsFor(pi,o)                 /* Find matching instance for pred */
1429 Cell  pi;                               /* (pi,o), or otherwise NIL.  If a */
1430 Int   o; {                              /* match is found, then tyvars from*/
1431     Class c = getHead(pi);              /* typeOff have been initialized to*/
1432     List  ins;                          /* allow direct use of specifics.  */
1433     List  res = NIL;
1434
1435     if (!isClass(c))
1436         return NIL;
1437
1438     for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins)) {
1439         Inst in   = hd(ins);
1440         Int  beta = newKindedVars(inst(in).kinds);
1441         if (matchPred(pi,o,inst(in).head,beta)) {
1442             res = cons (pair (beta, in), res);
1443             continue;
1444         }
1445         else
1446             numTyvars = beta;
1447     }
1448     if (res == NIL) {
1449         unrestrictBind();
1450     }
1451
1452     return rev(res);
1453 }
1454 #endif
1455
1456 /* --------------------------------------------------------------------------
1457  * Improvement:
1458  * ------------------------------------------------------------------------*/
1459
1460 Void improve(line,sps,ps)               /* Improve a list of predicates    */
1461 Int  line;
1462 List sps;
1463 List ps; {
1464     Bool improved;
1465     List ps1;
1466     do {
1467         improved = FALSE;
1468         for (ps1=ps; nonNull(ps1); ps1=tl(ps1)) {
1469             Cell pi = fst3(hd(ps1));
1470             Int  o  = intOf(snd3(hd(ps1)));
1471             Cell c  = getHead(pi);
1472             if ((isClass(c) && nonNull(cclass(c).xfds)) || isIP(c)) {
1473                 improved |= improveAgainst(line,sps,pi,o);
1474                 if (!isIP(c))
1475                     improved |= instImprove(line,c,pi,o);
1476                 improved |= improveAgainst(line,tl(ps1),pi,o);
1477             }
1478         }
1479     } while (improved);
1480 }
1481
1482 Void improve1(line,sps,pi,o)            /* Improve a single predicate      */
1483 Int  line;
1484 List sps;
1485 Cell pi;
1486 Int o; {
1487     Bool improved;
1488     Cell c  = getHead(pi);
1489     do {
1490         improved = FALSE;
1491         if ((isClass(c) && nonNull(cclass(c).xfds)) || isIP(c)) {
1492             improved |= improveAgainst(line,sps,pi,o);
1493             if (!isIP(c))
1494                 improved |= instImprove(line,c,pi,o);
1495         }
1496     } while (improved);
1497 }
1498
1499 Bool improveAgainst(line,ps,pi,o)
1500 Int line;
1501 List ps;
1502 Cell pi;
1503 Int o; {
1504     Bool improved = FALSE;
1505     Cell h = getHead(pi);
1506     for (; nonNull(ps); ps=tl(ps)) {
1507         Cell pr = hd(ps);
1508         Cell pi1 = fst3(pr);
1509         Int o1 = intOf(snd3(pr));
1510         Cell h1 = getHead(pi1);
1511         /* it would be nice to optimize for the common case
1512            where h == h1 */
1513         if (isClass(h) && isClass(h1)) {
1514             improved |= pairImprove(line,h,pi,o,pi1,o1,numTyvars);
1515             if (h != h1)
1516                 improved |= pairImprove(line,h1,pi1,o1,pi,o,numTyvars);
1517         }
1518 #if IPARAM
1519         else if (isIP(h1) && textOf(h1) == textOf(h))
1520             improved |= ipImprove(line,pi,o,pi1,o1);
1521 #endif
1522     }
1523     return improved;
1524 }
1525 /* should emulate findInsts behavior of shorting out if the
1526    predicate would match a more general signature... */
1527
1528 Bool instImprove(line,c,pi,o)
1529 Int line;
1530 Class c;
1531 Cell pi;
1532 Int o; {
1533     Bool improved = FALSE;
1534     List ins      = cclass(c).instances;
1535     for (; nonNull(ins); ins=tl(ins)) {
1536         Cell in   = hd(ins);
1537         Int alpha = newKindedVars(inst(in).kinds);
1538         improved |= pairImprove(line,c,pi,o,inst(in).head,alpha,alpha);
1539     }
1540     return improved;
1541 }
1542
1543 #if IPARAM
1544 Bool ipImprove(line,pi,o,pi1,o1)
1545 Int line;
1546 Cell pi;
1547 Int o;
1548 Cell pi1;
1549 Int o1; {
1550     Type t  = arg(pi);
1551     Type t1 = arg(pi1);
1552     if (!sameType(t,o,t1,o1)) {
1553         if (!unify(t,o,t1,o1)) {
1554             ERRMSG(line) "Mismatching uses of implicit parameter\n"
1555             ETHEN
1556             ERRTEXT "\n***  "
1557             ETHEN ERRPRED(copyPred(pi1,o1));
1558             ERRTEXT "\n***  "
1559             ETHEN ERRPRED(copyPred(pi,o));
1560             ERRTEXT "\n"
1561             EEND;
1562         }
1563         return TRUE;
1564     }
1565     return FALSE;
1566 }
1567 #endif
1568
1569 Bool pairImprove(line,c,pi1,o1,pi2,o2,above)    /* Look for improvement of (pi1,o1)*/
1570 Int   line;                             /* against (pi2,o2)                */
1571 Class c;
1572 Cell  pi1;
1573 Int   o1;
1574 Cell  pi2;
1575 Int   o2;
1576 Int above; {
1577     Bool improved = FALSE;
1578     List xfds     = cclass(c).xfds;
1579     for (; nonNull(xfds); xfds=tl(xfds)) {
1580         Cell xfd = hd(xfds);
1581         Cell hs  = fst(xfd);
1582         Int alpha;
1583         for (; nonNull(hs); hs=tl(hs)) {
1584             Cell h  = hd(hs);
1585             Class d = getHead(h);
1586             alpha = newKindedVars(cclass(d).kinds);
1587             if (matchPred(pi2,o2,h,alpha))
1588                 break;
1589             numTyvars = alpha;
1590         }
1591         if (nonNull(hs)) {
1592             List fds = snd(xfd);
1593             for (; nonNull(fds); fds=tl(fds)) {
1594                 List as   = fst(hd(fds));
1595                 Bool same = TRUE;
1596                 for (; same && nonNull(as); as=tl(as)) {
1597                     Int n = offsetOf(hd(as));
1598                     same &= matchTypeAbove(nthArg(n,pi1),o1,
1599                                            mkOffset(n),alpha,above);
1600                 }
1601                 if (isNull(as) && same) {
1602                     for (as=snd(hd(fds)); same && nonNull(as); as=tl(as)) {
1603                         Int  n    = offsetOf(hd(as));
1604                         Type t1   = nthArg(n,pi1);
1605                         Type t2   = mkOffset(n);
1606                         if (!matchTypeAbove(t1,o1,t2,alpha,above)) {
1607                             same &= unify(t1,o1,t2,alpha);
1608                             improved = TRUE;
1609                         }
1610                     }
1611                     if (!same) {
1612                         ERRMSG(line)
1613                           "Constraints are not consistent with functional dependency"
1614                         ETHEN
1615                         ERRTEXT "\n*** Constraint       : "
1616                         ETHEN ERRPRED(copyPred(pi1,o1));
1617                         ERRTEXT "\n*** And constraint   : "
1618                         ETHEN ERRPRED(copyPred(pi2,o2));
1619                         ERRTEXT "\n*** For class        : "
1620                         ETHEN ERRPRED(cclass(c).head);
1621                         ERRTEXT "\n*** Break dependency : "
1622                         ETHEN ERRFD(hd(fds));
1623                         ERRTEXT "\n"
1624                         EEND;
1625                     }
1626                 }
1627             }
1628             numTyvars = alpha;
1629         }
1630     }
1631     return improved;
1632 }
1633
1634 /* --------------------------------------------------------------------------
1635  * Compare type schemes:
1636  * ------------------------------------------------------------------------*/
1637
1638 Bool sameSchemes(s,s1)                  /* Test to see whether two type    */
1639 Type s;                                 /* schemes are the same            */
1640 Type s1; {
1641     Int  o   = 0;
1642     Int  m   = 0;
1643     Int  nr2 = 0;
1644     Bool b   = isPolyType(s);           /* Check quantifiers are the same  */
1645     Bool b1  = isPolyType(s1);
1646     if (b || b1) {
1647         if (b && b1 && eqKind(polySigOf(s),polySigOf(s1))) {
1648             Kind k = polySigOf(s);
1649             s      = monotypeOf(s);
1650             s1     = monotypeOf(s1);
1651             o      = newKindedVars(k);
1652             for (; isAp(k); k=arg(k))
1653                 m++;
1654         }
1655         else
1656             return FALSE;
1657     }
1658
1659     b  = (whatIs(s)==QUAL);             /* Check that contexts are the same*/
1660     b1 = (whatIs(s1)==QUAL);
1661     if (b || b1) {
1662         if (b && b1) {
1663             List ps  = fst(snd(s));
1664             List ps1 = fst(snd(s1));
1665             noBind();
1666             while (nonNull(ps) && nonNull(ps1)) {
1667                 Cell pi  = hd(ps);
1668                 Cell pi1 = hd(ps1);
1669                 if (getHead(pi)!=getHead(pi1)
1670                         || !unifyPred(pi,o,pi1,o))
1671                     break;
1672                 ps  = tl(ps);
1673                 ps1 = tl(ps1);
1674             }
1675             unrestrictBind();
1676             if (nonNull(ps) || nonNull(ps1))
1677                 return FALSE;
1678             s  = snd(snd(s));
1679             s1 = snd(snd(s1));
1680         }
1681         else
1682             return FALSE;
1683     }
1684
1685     b  = (whatIs(s)==RANK2);            /* Check any rank 2 annotations    */
1686     b1 = (whatIs(s1)==RANK2);
1687     if (b || b1) {
1688         if (b && b1 && intOf(fst(snd(s)))==intOf(fst(snd(s1)))) {
1689             nr2 = intOf(fst(snd(s)));
1690             s   = snd(snd(s));
1691             s1  = snd(snd(s1));
1692         }
1693         else
1694             return FALSE;
1695     }
1696
1697     for (; nr2>0; nr2--) {              /* Deal with rank 2 arguments      */
1698         Type t  = arg(fun(s));
1699         Type t1 = arg(fun(s1));
1700         b       = isPolyOrQualType(t);
1701         b1      = isPolyOrQualType(t1);
1702         if (b || b1) {
1703             if (b && b1) {
1704                 t  = dropRank1(t,o,m);
1705                 t1 = dropRank1(t1,o,m);
1706                 if (!sameSchemes(t,t1))
1707                     return FALSE;
1708             }
1709             else
1710                 return FALSE;
1711         }
1712         else {
1713             if (!sameType(t,o,t1,o)) {
1714                 return FALSE;
1715             }
1716         }
1717
1718         s  = arg(s);
1719         s1 = arg(s1);
1720     }
1721
1722     return sameType(s,o,s1,o);          /* Ensure body types are the same  */
1723 }
1724
1725 Bool sameType(t1,o1,t,o)                /* Test to see if types are        */
1726 Type t1;                                /* the same, with no binding of    */
1727 Int  o1;                                /* the variables in either one.    */
1728 Cell t;                                 /* Assumes types are kind correct  */
1729 Int  o; {                               /* with the same kind.             */
1730     Bool result;
1731     noBind();
1732     result = unify(t1,o1,t,o);
1733     unrestrictBind();
1734     return result;
1735 }
1736
1737 Bool matchType(t1,o1,t,o)               /* One way match type (t1,o1)      */
1738 Type t1;                                /* against (t,o), allowing only    */
1739 Int  o1;                                /* vars in 2nd type to be bound.   */
1740 Type t;                                 /* Assumes types are kind correct  */
1741 Int  o; {                               /* and that no vars have been      */
1742     Bool result;                        /* alloc'd since o.                */
1743     bindOnlyAbove(o);
1744     result = unify(t1,o1,t,o);
1745     unrestrictBind();
1746     return result;
1747 }
1748
1749 static Bool local matchTypeAbove(t1,o1,t,o,a)   /* match, allowing only vars */
1750 Type t1;                                /* allocated since `a' to be bound   */
1751 Int  o1;                                /* this is deeply hacky, since it    */
1752 Type t;                                 /* relies on careful use of the      */
1753 Int  o;                                 /* substitution stack                */
1754 Int  a; {
1755     Bool result;
1756     bindOnlyAbove(a);
1757     result = unify(t1,o1,t,o);
1758     unrestrictBind();
1759     return result;
1760 }
1761
1762 /* --------------------------------------------------------------------------
1763  * Unify kind expressions:
1764  * ------------------------------------------------------------------------*/
1765
1766 static Bool local kvarToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2     */
1767 Tyvar *tyv1, *tyv2; {                     /* for kind variable bindings    */
1768     if (tyv1!=tyv2) {
1769         tyv1->bound = aVar;
1770         tyv1->offs  = tyvNum(tyv2);
1771 #ifdef DEBUG_KINDS
1772         Printf("vv binding kvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
1773 #endif
1774     }
1775     return TRUE;
1776 }
1777
1778 static Bool local kvarToTypeBind(tyv,t,o)/* Make binding tyv := (t,o)      */
1779 Tyvar *tyv;                             /* for kind variable bindings      */
1780 Type  t;                                /* guaranteed not to be a v'ble or */
1781 Int   o; {                              /* have synonym as outermost constr*/
1782     if (doesntOccurIn(tyv,t,o)) {
1783         tyv->bound = t;
1784         tyv->offs  = o;
1785 #ifdef DEBUG_KINDS
1786         Printf("vt binding kind variable: _%d to ",tyvNum(tyv));
1787         printType(stdout,debugType(t,o));
1788         Putchar('\n');
1789 #endif
1790         return TRUE;
1791     }
1792     unifyFails = "unification would give infinite kind";
1793     return FALSE;
1794 }
1795
1796 Bool kunify(k1,o1,k2,o2)                /* Unify kind expr (k1,o1) with    */
1797 Kind k1,k2;                             /* (k2,o2)                         */
1798 Int  o1,o2; {
1799     Tyvar *kyv1, *kyv2;
1800
1801     deRef(kyv1,k1,o1);
1802     deRef(kyv2,k2,o2);
1803
1804     if (kyv1) {
1805         if (kyv2)
1806             return kvarToVarBind(kyv1,kyv2);        /* k1, k2 variables    */
1807         else
1808             return kvarToTypeBind(kyv1,k2,o2);      /* k1 variable, k2 not */
1809     }
1810     else
1811         if (kyv2)
1812             return kvarToTypeBind(kyv2,k1,o1);      /* k2 variable, k1 not */
1813         else {
1814 #ifdef DEBUG_KINDS
1815             Printf("unifying kinds: ");
1816             printType(stdout,debugType(k1,o1));
1817             Printf(" with ");
1818             printType(stdout,debugType(k2,o2));
1819             Putchar('\n');
1820 #endif
1821             if (k1==STAR && k2==STAR)               /* k1, k2 not vars     */
1822                 return TRUE;
1823 #if TREX
1824             else if (k1==ROW && k2==ROW)
1825                 return TRUE;
1826 #endif
1827             else if (isAp(k1) && isAp(k2))
1828                 return kunify(fst(k1),o1,fst(k2),o2) &&
1829                        kunify(snd(k1),o1,snd(k2),o2);
1830         }
1831     unifyFails = 0;
1832     return FALSE;
1833 }
1834
1835 /* --------------------------------------------------------------------------
1836  * Tuple type constructors: are generated as necessary.  The most common
1837  * n-tuple constructors (n<MAXTUPCON) are held in a cache to avoid
1838  * repeated generation of the constructor types.
1839  * ------------------------------------------------------------------------*/
1840
1841 #define MAXTUPCON 10
1842 static Type tupleConTypes[MAXTUPCON];
1843
1844 Void typeTuple(e)                      /* find type for tuple constr, using*/
1845 Cell e; {                              /* tupleConTypes to cache previously*/
1846     Int n   = tupleOf(e);              /* calculated tuple constr. types.  */
1847     typeOff = newTyvars(n);
1848     if (n>=MAXTUPCON)
1849          typeIs = makeTupleType(n);
1850     else if (tupleConTypes[n])
1851          typeIs = tupleConTypes[n];
1852     else
1853          typeIs = tupleConTypes[n] = makeTupleType(n);
1854 }
1855
1856 static Type local makeTupleType(n)     /* construct type for tuple constr. */
1857 Int n; {                               /* t1 -> ... -> tn -> (t1,...,tn)   */
1858     Type h = mkTuple(n);
1859     Int  i;
1860
1861     for (i=0; i<n; ++i)
1862         h = ap(h,mkOffset(i));
1863     while (0<n--)
1864         h = fn(mkOffset(n),h);
1865     return h;
1866 }
1867
1868 /* --------------------------------------------------------------------------
1869  * Two forms of kind expression are used quite frequently:
1870  *      *  -> *  -> ... -> *  -> *      for kinds of ->, [], ->, (,) etc...
1871  *      v1 -> v2 -> ... -> vn -> vn+1   skeletons for constructor kinds
1872  * Expressions of these forms are produced by the following functions which
1873  * use a cache to avoid repeated construction of commonly used values.
1874  * A similar approach is used to store the types of tuple constructors in the
1875  * main type checker.
1876  * ------------------------------------------------------------------------*/
1877
1878 #define MAXKINDFUN 10
1879 static  Kind simpleKindCache[MAXKINDFUN];
1880 static  Kind varKindCache[MAXKINDFUN];
1881
1882 static Kind local makeSimpleKind(n)     /* construct * -> ... -> * (n args)*/
1883 Int n; {
1884     Kind k = STAR;
1885     while (n-- > 0)
1886         k = ap(STAR,k);
1887     return k;
1888 }
1889
1890 Kind simpleKind(n)                      /* return (possibly cached) simple */
1891 Int n; {                                /* function kind                   */
1892     if (n>=MAXKINDFUN)
1893         return makeSimpleKind(n);
1894     else if (nonNull(simpleKindCache[n]))
1895         return simpleKindCache[n];
1896     else if (n==0)
1897         return simpleKindCache[0] = STAR;
1898     else
1899         return simpleKindCache[n] = ap(STAR,simpleKind(n-1));
1900 }
1901
1902 static Kind local makeVarKind(n)        /* construct v0 -> .. -> vn        */
1903 Int n; {
1904     Kind k = mkOffset(n);
1905     while (n-- > 0)
1906         k = ap(mkOffset(n),k);
1907     return k;
1908 }
1909
1910 Void varKind(n)                         /* return (possibly cached) var    */
1911 Int n; {                                /* function kind                   */
1912     typeOff = newKindvars(n+1);
1913     if (n>=MAXKINDFUN)
1914         typeIs = makeVarKind(n);
1915     else if (nonNull(varKindCache[n]))
1916         typeIs = varKindCache[n];
1917     else
1918         typeIs = varKindCache[n] = makeVarKind(n);
1919 }
1920
1921 /* --------------------------------------------------------------------------
1922  * Substitutution control:
1923  * ------------------------------------------------------------------------*/
1924
1925 Void substitution(what)
1926 Int what; {
1927     Int  i;
1928
1929     switch (what) {
1930         case RESET   : emptySubstitution();
1931                        unrestrictBind();
1932                        btyvars = NIL;
1933                        break;
1934
1935         case MARK    : for (i=0; i<MAXTUPCON; ++i)
1936                            mark(tupleConTypes[i]);
1937                        for (i=0; i<MAXKINDFUN; ++i) {
1938                            mark(simpleKindCache[i]);
1939                            mark(varKindCache[i]);
1940                        }
1941                        for (i=0; i<numTyvars; ++i)
1942                            mark(tyvars[i].bound);
1943                        mark(btyvars);
1944                        mark(typeIs);
1945                        mark(predsAre);
1946                        mark(genericVars);
1947 #if TREX
1948                        mark(trexShow);
1949                        mark(trexEq);
1950 #endif
1951                        break;
1952
1953         case POSTPREL: break;
1954
1955         case PREPREL : substitution(RESET);
1956                        for (i=0; i<MAXTUPCON; ++i)
1957                            tupleConTypes[i] = NIL;
1958                        for (i=0; i<MAXKINDFUN; ++i) {
1959                            simpleKindCache[i] = NIL;
1960                            varKindCache[i]    = NIL;
1961                        }
1962 #if TREX
1963                        trexShow = mkQCon(findText("Trex"),
1964                                          findText("ShowRecRow"));
1965                        trexEq   = mkQCon(findText("Trex"),
1966                                          findText("EqRecRow"));
1967 #endif
1968                        break;
1969     }
1970 }
1971
1972 /*-------------------------------------------------------------------------*/