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