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.13 $
  14  * $Date: 2000/03/10 20:03:37 $
  15  * ------------------------------------------------------------------------*/
  16
  17 #include "prelude.h"
  18 #include "storage.h"
  19 #include "connect.h"
  20 #include "errors.h"
  21 #include "link.h"
  22
  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 Bool isProgType(ks,type)                /* Test if type is of the form     */
1263 List ks;                                /* IO t for some t.                */
1264 Type type; {
1265     Bool result;
1266     Int  alpha;
1267     Int  beta;
1268     emptySubstitution();
1269     alpha  = newKindedVars(ks);
1270     beta   = newTyvars(1);
1271     bindOnlyAbove(beta);
1272     result = unify(type,alpha,typeProgIO,beta);
1273     unrestrictBind();
1274     emptySubstitution();
1275     return result;
1276 }
1277
1278 /* --------------------------------------------------------------------------
1279  * Matching predicates:
1280  *
1281  * There are (at least) four situations where we need to match up pairs
1282  * of predicates:
1283  *
1284  *   1) Testing to see if two predicates are the same (ignoring differences
1285  *      caused by the use of type synonyms, for example).
1286  *
1287  *   2) Matching a predicate with the head of its class so that we can
1288  *      find the corresponding superclass predicates.  If the predicates
1289  *      have already been kind-checked, and the classes are known to be
1290  *      the same, then this should never fail.
1291  *
1292  *   3) Matching a predicate against the head of an instance to see if
1293  *      that instance is applicable.
1294  *
1295  *   4) Matching two instance heads to see if there is an overlap.
1296  *
1297  * For (1), we need a matching process that does not bind any variables.
1298  * For (2) and (3), we need to use one-way matching, only allowing
1299  * variables in the class or instance head to be instantiated.  For
1300  * (4), we need two-way unification.
1301  *
1302  * Another situation in which both one-way and two-way unification might
1303  * be used is in an implementation of improvement.  Here, a one-way match
1304  * would be used to determine applicability of a rule for improvement
1305  * that would then be followed by unification with another predicate.
1306  * One possible syntax for this might be:
1307  *
1308  *     instance P => pi [improves pi'] where ...
1309  *
1310  * The intention here is that any predicate matching pi' can be unified
1311  * with pi to get more accurate types.  A simple example of this is:
1312  *
1313  *   instance Collection [a] a improves Collection [a] b where ...
1314  *
1315  * As soon as we know what the collection type is (in this case, a list),
1316  * we will also know what the element type is.  To ensure that the rule
1317  * for improvement is valid, the compilation system will also need to use
1318  * a one-way matching process to ensure that pi is a (substitution) instance
1319  * of pi'.  Another extension would be to allow more than one predicate pi'
1320  * in an improving rule.  Read the paper on simplification and improvement
1321  * for technical background.  Watch this space for implementation news!
1322  * ------------------------------------------------------------------------*/
1323
1324 Bool samePred(pi1,o1,pi,o)              /* Test to see if predicates are   */
1325 Cell pi1;                               /* the same, with no binding of    */
1326 Int  o1;                                /* the variables in either one.    */
1327 Cell pi;                                /* Assumes preds are kind correct  */
1328 Int  o; {                               /* with the same class.            */
1329     Bool result;
1330     noBind();
1331     result = unifyPred(pi1,o1,pi,o);
1332     unrestrictBind();
1333     return result;
1334 }
1335
1336 Bool matchPred(pi1,o1,pi,o)             /* One way match predicate (pi1,o1)*/
1337 Cell pi1;                               /* against (pi,o), allowing only   */
1338 Int  o1;                                /* vars in 2nd pred to be bound.   */
1339 Cell pi;                                /* Assumes preds are kind correct  */
1340 Int  o; {                               /* with the same class and that no */
1341     Bool result;                        /* vars have been alloc'd since o. */
1342     bindOnlyAbove(o);
1343     result = unifyPred(pi1,o1,pi,o);
1344     unrestrictBind();
1345     return result;
1346 }
1347
1348 Bool unifyPred(pi1,o1,pi,o)             /* Unify two predicates            */
1349 Cell pi1;                               /* Assumes preds are kind correct  */
1350 Int  o1;                                /* with the same class.            */
1351 Cell pi;
1352 Int  o; {
1353   for (; isAp(pi1); pi1=fun(pi1), pi=fun(pi)) {
1354         if (!isAp(pi) || !unify(arg(pi1),o1,arg(pi),o))
1355             return FALSE;
1356   }
1357   /* pi1 has exhausted its argument chain, we also need to check that
1358      pi has no remaining arguments.  However, under this condition,
1359      the pi1 == pi will always return FALSE, giving the desired
1360      result. */
1361
1362 #if IPARAM
1363     if (isIP(pi1) && isIP(pi))
1364         return textOf(pi1)==textOf(pi);
1365     else
1366 #endif
1367     return pi1==pi;
1368 }
1369
1370 #if TREX
1371 static Cell trexShow = NIL;             /* Used to test for show on records*/
1372 static Cell trexEq   = NIL;             /* Used to test for eq on records  */
1373 #endif
1374
1375 Inst findInstFor(pi,o)                  /* Find matching instance for pred */
1376 Cell  pi;                               /* (pi,o), or otherwise NIL.  If a */
1377 Int   o; {                              /* match is found, then tyvars from*/
1378     Class c = getHead(pi);              /* typeOff have been initialized to*/
1379     List  ins;                          /* allow direct use of specifics.  */
1380     Cell  kspi = NIL;
1381
1382     if (!isClass(c))
1383         return NIL;
1384
1385     for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins)) {
1386         Inst in   = hd(ins);
1387         Int  beta = newKindedVars(inst(in).kinds);
1388         if (matchPred(pi,o,inst(in).head,beta)) {
1389             typeOff = beta;
1390             return in;
1391         }
1392         else {
1393             numTyvars = beta;
1394             if (allowOverlap) {
1395                 Int alpha = newKindedVars(inst(in).kinds);
1396                 if (isNull(kspi)) {
1397                     kspi = copyNoMark(pi,o);
1398                 }
1399                 beta = newKindedVars(fst(kspi));
1400                 if (matchPred(inst(in).head,alpha,snd(kspi),beta)) {
1401                     numTyvars = alpha;
1402                     return NIL;
1403                 }
1404                 numTyvars = alpha;
1405             }
1406         }
1407     }
1408     unrestrictBind();
1409
1410 #if TREX
1411     {   Bool wantShow   = (c==findQualClass(trexShow));
1412         Bool wantEither = wantShow || (c==findQualClass(trexEq));
1413
1414         if (wantEither) {                       /* Generate instances of   */
1415             Type  t = arg(pi);                  /* ShowRecRow and EqRecRow */
1416             Tyvar *tyv;                         /* on the fly              */
1417             Cell  e;
1418             deRef(tyv,t,o);
1419             e = getHead(t);
1420             if (isExt(e)) {
1421                 Inst in = NIL;
1422                 for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins))
1423                     if (getHead(arg(inst(hd(ins)).head))==e) {
1424                         in = hd(ins);
1425                         break;
1426                     }
1427                 if (isNull(in))
1428                     in = (wantShow ? addRecShowInst(c,e) : addRecEqInst(c,e));
1429                 typeOff = newKindedVars(extKind);
1430                 bindTv(typeOff,arg(fun(t)),o);
1431                 bindTv(typeOff+1,arg(t),o);
1432                 return in;
1433             }
1434         }
1435     }
1436 #endif
1437
1438     return NIL;
1439 }
1440
1441 #if MULTI_INST
1442 List findInstsFor(pi,o)                 /* Find matching instance for pred */
1443 Cell  pi;                               /* (pi,o), or otherwise NIL.  If a */
1444 Int   o; {                              /* match is found, then tyvars from*/
1445     Class c = getHead(pi);              /* typeOff have been initialized to*/
1446     List  ins;                          /* allow direct use of specifics.  */
1447     List  res = NIL;
1448
1449     if (!isClass(c))
1450         return NIL;
1451
1452     for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins)) {
1453         Inst in   = hd(ins);
1454         Int  beta = newKindedVars(inst(in).kinds);
1455         if (matchPred(pi,o,inst(in).head,beta)) {
1456             res = cons (pair (beta, in), res);
1457             continue;
1458         }
1459         else
1460             numTyvars = beta;
1461     }
1462     if (res == NIL) {
1463         unrestrictBind();
1464     }
1465
1466     return rev(res);
1467 }
1468 #endif
1469
1470 /* --------------------------------------------------------------------------
1471  * Improvement:
1472  * ------------------------------------------------------------------------*/
1473
1474 Void improve(line,sps,ps)               /* Improve a list of predicates    */
1475 Int  line;
1476 List sps;
1477 List ps; {
1478     Bool improved;
1479     List ps1;
1480     do {
1481         improved = FALSE;
1482         for (ps1=ps; nonNull(ps1); ps1=tl(ps1)) {
1483             Cell pi = fst3(hd(ps1));
1484             Int  o  = intOf(snd3(hd(ps1)));
1485             Cell c  = getHead(pi);
1486             if ((isClass(c) && nonNull(cclass(c).xfds)) || isIP(c)) {
1487                 improved |= improveAgainst(line,sps,pi,o);
1488                 if (!isIP(c))
1489                     improved |= instImprove(line,c,pi,o);
1490                 improved |= improveAgainst(line,tl(ps1),pi,o);
1491             }
1492         }
1493     } while (improved);
1494 }
1495
1496 Void improve1(line,sps,pi,o)            /* Improve a single predicate      */
1497 Int  line;
1498 List sps;
1499 Cell pi;
1500 Int o; {
1501     Bool improved;
1502     Cell c  = getHead(pi);
1503     do {
1504         improved = FALSE;
1505         if ((isClass(c) && nonNull(cclass(c).xfds)) || isIP(c)) {
1506             improved |= improveAgainst(line,sps,pi,o);
1507             if (!isIP(c))
1508                 improved |= instImprove(line,c,pi,o);
1509         }
1510     } while (improved);
1511 }
1512
1513 Bool improveAgainst(line,ps,pi,o)
1514 Int line;
1515 List ps;
1516 Cell pi;
1517 Int o; {
1518     Bool improved = FALSE;
1519     Cell h = getHead(pi);
1520     for (; nonNull(ps); ps=tl(ps)) {
1521         Cell pr = hd(ps);
1522         Cell pi1 = fst3(pr);
1523         Int o1 = intOf(snd3(pr));
1524         Cell h1 = getHead(pi1);
1525         /* it would be nice to optimize for the common case
1526            where h == h1 */
1527         if (isClass(h) && isClass(h1)) {
1528             improved |= pairImprove(line,h,pi,o,pi1,o1,numTyvars);
1529             if (h != h1)
1530                 improved |= pairImprove(line,h1,pi1,o1,pi,o,numTyvars);
1531         }
1532 #if IPARAM
1533         else if (isIP(h1) && textOf(h1) == textOf(h))
1534             improved |= ipImprove(line,pi,o,pi1,o1);
1535 #endif
1536     }
1537     return improved;
1538 }
1539 /* should emulate findInsts behavior of shorting out if the
1540    predicate would match a more general signature... */
1541
1542 Bool instImprove(line,c,pi,o)
1543 Int line;
1544 Class c;
1545 Cell pi;
1546 Int o; {
1547     Bool improved = FALSE;
1548     List ins      = cclass(c).instances;
1549     for (; nonNull(ins); ins=tl(ins)) {
1550         Cell in   = hd(ins);
1551         Int alpha = newKindedVars(inst(in).kinds);
1552         improved |= pairImprove(line,c,pi,o,inst(in).head,alpha,alpha);
1553     }
1554     return improved;
1555 }
1556
1557 #if IPARAM
1558 Bool ipImprove(line,pi,o,pi1,o1)
1559 Int line;
1560 Cell pi;
1561 Int o;
1562 Cell pi1;
1563 Int o1; {
1564     Type t  = arg(pi);
1565     Type t1 = arg(pi1);
1566     if (!sameType(t,o,t1,o1)) {
1567         if (!unify(t,o,t1,o1)) {
1568             ERRMSG(line) "Mismatching uses of implicit parameter\n"
1569             ETHEN
1570             ERRTEXT "\n***  "
1571             ETHEN ERRPRED(copyPred(pi1,o1));
1572             ERRTEXT "\n***  "
1573             ETHEN ERRPRED(copyPred(pi,o));
1574             ERRTEXT "\n"
1575             EEND;
1576         }
1577         return TRUE;
1578     }
1579     return FALSE;
1580 }
1581 #endif
1582
1583 Bool pairImprove(line,c,pi1,o1,pi2,o2,above)    /* Look for improvement of (pi1,o1)*/
1584 Int   line;                             /* against (pi2,o2)                */
1585 Class c;
1586 Cell  pi1;
1587 Int   o1;
1588 Cell  pi2;
1589 Int   o2;
1590 Int above; {
1591     Bool improved = FALSE;
1592     List xfds     = cclass(c).xfds;
1593     for (; nonNull(xfds); xfds=tl(xfds)) {
1594         Cell xfd = hd(xfds);
1595         Cell hs  = fst(xfd);
1596         Int alpha;
1597         for (; nonNull(hs); hs=tl(hs)) {
1598             Cell h  = hd(hs);
1599             Class d = getHead(h);
1600             alpha = newKindedVars(cclass(d).kinds);
1601             if (matchPred(pi2,o2,h,alpha))
1602                 break;
1603             numTyvars = alpha;
1604         }
1605         if (nonNull(hs)) {
1606             List fds = snd(xfd);
1607             for (; nonNull(fds); fds=tl(fds)) {
1608                 List as   = fst(hd(fds));
1609                 Bool same = TRUE;
1610                 for (; same && nonNull(as); as=tl(as)) {
1611                     Int n = offsetOf(hd(as));
1612                     same &= matchTypeAbove(nthArg(n,pi1),o1,
1613                                            mkOffset(n),alpha,above);
1614                 }
1615                 if (isNull(as) && same) {
1616                     for (as=snd(hd(fds)); same && nonNull(as); as=tl(as)) {
1617                         Int  n    = offsetOf(hd(as));
1618                         Type t1   = nthArg(n,pi1);
1619                         Type t2   = mkOffset(n);
1620                         if (!matchTypeAbove(t1,o1,t2,alpha,above)) {
1621                             same &= unify(t1,o1,t2,alpha);
1622                             improved = TRUE;
1623                         }
1624                     }
1625                     if (!same) {
1626                         ERRMSG(line)
1627                           "Constraints are not consistent with functional dependency"
1628                         ETHEN
1629                         ERRTEXT "\n*** Constraint       : "
1630                         ETHEN ERRPRED(copyPred(pi1,o1));
1631                         ERRTEXT "\n*** And constraint   : "
1632                         ETHEN ERRPRED(copyPred(pi2,o2));
1633                         ERRTEXT "\n*** For class        : "
1634                         ETHEN ERRPRED(cclass(c).head);
1635                         ERRTEXT "\n*** Break dependency : "
1636                         ETHEN ERRFD(hd(fds));
1637                         ERRTEXT "\n"
1638                         EEND;
1639                     }
1640                 }
1641             }
1642             numTyvars = alpha;
1643         }
1644     }
1645     return improved;
1646 }
1647
1648 /* --------------------------------------------------------------------------
1649  * Compare type schemes:
1650  * ------------------------------------------------------------------------*/
1651
1652 Bool sameSchemes(s,s1)                  /* Test to see whether two type    */
1653 Type s;                                 /* schemes are the same            */
1654 Type s1; {
1655     Int  o   = 0;
1656     Int  m   = 0;
1657     Int  nr2 = 0;
1658     Bool b   = isPolyType(s);           /* Check quantifiers are the same  */
1659     Bool b1  = isPolyType(s1);
1660     if (b || b1) {
1661         if (b && b1 && eqKind(polySigOf(s),polySigOf(s1))) {
1662             Kind k = polySigOf(s);
1663             s      = monotypeOf(s);
1664             s1     = monotypeOf(s1);
1665             o      = newKindedVars(k);
1666             for (; isAp(k); k=arg(k))
1667                 m++;
1668         }
1669         else
1670             return FALSE;
1671     }
1672
1673     b  = (whatIs(s)==QUAL);             /* Check that contexts are the same*/
1674     b1 = (whatIs(s1)==QUAL);
1675     if (b || b1) {
1676         if (b && b1) {
1677             List ps  = fst(snd(s));
1678             List ps1 = fst(snd(s1));
1679             noBind();
1680             while (nonNull(ps) && nonNull(ps1)) {
1681                 Cell pi  = hd(ps);
1682                 Cell pi1 = hd(ps1);
1683                 if (getHead(pi)!=getHead(pi1)
1684                         || !unifyPred(pi,o,pi1,o))
1685                     break;
1686                 ps  = tl(ps);
1687                 ps1 = tl(ps1);
1688             }
1689             unrestrictBind();
1690             if (nonNull(ps) || nonNull(ps1))
1691                 return FALSE;
1692             s  = snd(snd(s));
1693             s1 = snd(snd(s1));
1694         }
1695         else
1696             return FALSE;
1697     }
1698
1699     b  = (whatIs(s)==RANK2);            /* Check any rank 2 annotations    */
1700     b1 = (whatIs(s1)==RANK2);
1701     if (b || b1) {
1702         if (b && b1 && intOf(fst(snd(s)))==intOf(fst(snd(s1)))) {
1703             nr2 = intOf(fst(snd(s)));
1704             s   = snd(snd(s));
1705             s1  = snd(snd(s1));
1706         }
1707         else
1708             return FALSE;
1709     }
1710
1711     for (; nr2>0; nr2--) {              /* Deal with rank 2 arguments      */
1712         Type t  = arg(fun(s));
1713         Type t1 = arg(fun(s1));
1714         b       = isPolyOrQualType(t);
1715         b1      = isPolyOrQualType(t1);
1716         if (b || b1) {
1717             if (b && b1) {
1718                 t  = dropRank1(t,o,m);
1719                 t1 = dropRank1(t1,o,m);
1720                 if (!sameSchemes(t,t1))
1721                     return FALSE;
1722             }
1723             else
1724                 return FALSE;
1725         }
1726         else {
1727             if (!sameType(t,o,t1,o)) {
1728                 return FALSE;
1729             }
1730         }
1731
1732         s  = arg(s);
1733         s1 = arg(s1);
1734     }
1735
1736     return sameType(s,o,s1,o);          /* Ensure body types are the same  */
1737 }
1738
1739 Bool sameType(t1,o1,t,o)                /* Test to see if types are        */
1740 Type t1;                                /* the same, with no binding of    */
1741 Int  o1;                                /* the variables in either one.    */
1742 Cell t;                                 /* Assumes types are kind correct  */
1743 Int  o; {                               /* with the same kind.             */
1744     Bool result;
1745     noBind();
1746     result = unify(t1,o1,t,o);
1747     unrestrictBind();
1748     return result;
1749 }
1750
1751 Bool matchType(t1,o1,t,o)               /* One way match type (t1,o1)      */
1752 Type t1;                                /* against (t,o), allowing only    */
1753 Int  o1;                                /* vars in 2nd type to be bound.   */
1754 Type t;                                 /* Assumes types are kind correct  */
1755 Int  o; {                               /* and that no vars have been      */
1756     Bool result;                        /* alloc'd since o.                */
1757     bindOnlyAbove(o);
1758     result = unify(t1,o1,t,o);
1759     unrestrictBind();
1760     return result;
1761 }
1762
1763 static Bool local matchTypeAbove(t1,o1,t,o,a)   /* match, allowing only vars */
1764 Type t1;                                /* allocated since `a' to be bound   */
1765 Int  o1;                                /* this is deeply hacky, since it    */
1766 Type t;                                 /* relies on careful use of the      */
1767 Int  o;                                 /* substitution stack                */
1768 Int  a; {
1769     Bool result;
1770     bindOnlyAbove(a);
1771     result = unify(t1,o1,t,o);
1772     unrestrictBind();
1773     return result;
1774 }
1775
1776 /* --------------------------------------------------------------------------
1777  * Unify kind expressions:
1778  * ------------------------------------------------------------------------*/
1779
1780 static Bool local kvarToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2     */
1781 Tyvar *tyv1, *tyv2; {                     /* for kind variable bindings    */
1782     if (tyv1!=tyv2) {
1783         tyv1->bound = aVar;
1784         tyv1->offs  = tyvNum(tyv2);
1785 #ifdef DEBUG_KINDS
1786         Printf("vv binding kvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
1787 #endif
1788     }
1789     return TRUE;
1790 }
1791
1792 static Bool local kvarToTypeBind(tyv,t,o)/* Make binding tyv := (t,o)      */
1793 Tyvar *tyv;                             /* for kind variable bindings      */
1794 Type  t;                                /* guaranteed not to be a v'ble or */
1795 Int   o; {                              /* have synonym as outermost constr*/
1796     if (doesntOccurIn(tyv,t,o)) {
1797         tyv->bound = t;
1798         tyv->offs  = o;
1799 #ifdef DEBUG_KINDS
1800         Printf("vt binding kind variable: _%d to ",tyvNum(tyv));
1801         printType(stdout,debugType(t,o));
1802         Putchar('\n');
1803 #endif
1804         return TRUE;
1805     }
1806     unifyFails = "unification would give infinite kind";
1807     return FALSE;
1808 }
1809
1810 Bool kunify(k1,o1,k2,o2)                /* Unify kind expr (k1,o1) with    */
1811 Kind k1,k2;                             /* (k2,o2)                         */
1812 Int  o1,o2; {
1813     Tyvar *kyv1, *kyv2;
1814
1815     deRef(kyv1,k1,o1);
1816     deRef(kyv2,k2,o2);
1817
1818     if (kyv1) {
1819         if (kyv2)
1820             return kvarToVarBind(kyv1,kyv2);        /* k1, k2 variables    */
1821         else
1822             return kvarToTypeBind(kyv1,k2,o2);      /* k1 variable, k2 not */
1823     }
1824     else
1825         if (kyv2)
1826             return kvarToTypeBind(kyv2,k1,o1);      /* k2 variable, k1 not */
1827         else {
1828 #ifdef DEBUG_KINDS
1829             Printf("unifying kinds: ");
1830             printType(stdout,debugType(k1,o1));
1831             Printf(" with ");
1832             printType(stdout,debugType(k2,o2));
1833             Putchar('\n');
1834 #endif
1835             if (k1==STAR && k2==STAR)               /* k1, k2 not vars     */
1836                 return TRUE;
1837 #if TREX
1838             else if (k1==ROW && k2==ROW)
1839                 return TRUE;
1840 #endif
1841             else if (isAp(k1) && isAp(k2))
1842                 return kunify(fst(k1),o1,fst(k2),o2) &&
1843                        kunify(snd(k1),o1,snd(k2),o2);
1844         }
1845     unifyFails = 0;
1846     return FALSE;
1847 }
1848
1849 /* --------------------------------------------------------------------------
1850  * Tuple type constructors: are generated as necessary.  The most common
1851  * n-tuple constructors (n<MAXTUPCON) are held in a cache to avoid
1852  * repeated generation of the constructor types.
1853  * ------------------------------------------------------------------------*/
1854
1855 #define MAXTUPCON 10
1856 static Type tupleConTypes[MAXTUPCON];
1857
1858 Void typeTuple(e)                      /* find type for tuple constr, using*/
1859 Cell e; {                              /* tupleConTypes to cache previously*/
1860     Int n   = tupleOf(e);              /* calculated tuple constr. types.  */
1861     typeOff = newTyvars(n);
1862     if (n>=MAXTUPCON)
1863          typeIs = makeTupleType(n);
1864     else if (tupleConTypes[n])
1865          typeIs = tupleConTypes[n];
1866     else
1867          typeIs = tupleConTypes[n] = makeTupleType(n);
1868 }
1869
1870 static Type local makeTupleType(n)     /* construct type for tuple constr. */
1871 Int n; {                               /* t1 -> ... -> tn -> (t1,...,tn)   */
1872     Type h = mkTuple(n);
1873     Int  i;
1874
1875     for (i=0; i<n; ++i)
1876         h = ap(h,mkOffset(i));
1877     while (0<n--)
1878         h = fn(mkOffset(n),h);
1879     return h;
1880 }
1881
1882 /* --------------------------------------------------------------------------
1883  * Two forms of kind expression are used quite frequently:
1884  *      *  -> *  -> ... -> *  -> *      for kinds of ->, [], ->, (,) etc...
1885  *      v1 -> v2 -> ... -> vn -> vn+1   skeletons for constructor kinds
1886  * Expressions of these forms are produced by the following functions which
1887  * use a cache to avoid repeated construction of commonly used values.
1888  * A similar approach is used to store the types of tuple constructors in the
1889  * main type checker.
1890  * ------------------------------------------------------------------------*/
1891
1892 #define MAXKINDFUN 10
1893 static  Kind simpleKindCache[MAXKINDFUN];
1894 static  Kind varKindCache[MAXKINDFUN];
1895
1896 static Kind local makeSimpleKind(n)     /* construct * -> ... -> * (n args)*/
1897 Int n; {
1898     Kind k = STAR;
1899     while (n-- > 0)
1900         k = ap(STAR,k);
1901     return k;
1902 }
1903
1904 Kind simpleKind(n)                      /* return (possibly cached) simple */
1905 Int n; {                                /* function kind                   */
1906     if (n>=MAXKINDFUN)
1907         return makeSimpleKind(n);
1908     else if (nonNull(simpleKindCache[n]))
1909         return simpleKindCache[n];
1910     else if (n==0)
1911         return simpleKindCache[0] = STAR;
1912     else
1913         return simpleKindCache[n] = ap(STAR,simpleKind(n-1));
1914 }
1915
1916 static Kind local makeVarKind(n)        /* construct v0 -> .. -> vn        */
1917 Int n; {
1918     Kind k = mkOffset(n);
1919     while (n-- > 0)
1920         k = ap(mkOffset(n),k);
1921     return k;
1922 }
1923
1924 Void varKind(n)                         /* return (possibly cached) var    */
1925 Int n; {                                /* function kind                   */
1926     typeOff = newKindvars(n+1);
1927     if (n>=MAXKINDFUN)
1928         typeIs = makeVarKind(n);
1929     else if (nonNull(varKindCache[n]))
1930         typeIs = varKindCache[n];
1931     else
1932         typeIs = varKindCache[n] = makeVarKind(n);
1933 }
1934
1935 /* --------------------------------------------------------------------------
1936  * Substitutution control:
1937  * ------------------------------------------------------------------------*/
1938
1939 Void substitution(what)
1940 Int what; {
1941     Int  i;
1942
1943     switch (what) {
1944         case RESET   : emptySubstitution();
1945                        unrestrictBind();
1946                        btyvars = NIL;
1947                        break;
1948
1949         case MARK    : for (i=0; i<MAXTUPCON; ++i)
1950                            mark(tupleConTypes[i]);
1951                        for (i=0; i<MAXKINDFUN; ++i) {
1952                            mark(simpleKindCache[i]);
1953                            mark(varKindCache[i]);
1954                        }
1955                        for (i=0; i<numTyvars; ++i)
1956                            mark(tyvars[i].bound);
1957                        mark(btyvars);
1958                        mark(typeIs);
1959                        mark(predsAre);
1960                        mark(genericVars);
1961 #if TREX
1962                        mark(trexShow);
1963                        mark(trexEq);
1964 #endif
1965                        break;
1966
1967         case POSTPREL: break;
1968
1969         case PREPREL : substitution(RESET);
1970                        for (i=0; i<MAXTUPCON; ++i)
1971                            tupleConTypes[i] = NIL;
1972                        for (i=0; i<MAXKINDFUN; ++i) {
1973                            simpleKindCache[i] = NIL;
1974                            varKindCache[i]    = NIL;
1975                        }
1976 #if TREX
1977                        trexShow = mkQCon(findText("Trex"),
1978                                          findText("ShowRecRow"));
1979                        trexEq   = mkQCon(findText("Trex"),
1980                                          findText("EqRecRow"));
1981 #endif
1982                        break;
1983     }
1984 }
1985
1986 /*-------------------------------------------------------------------------*/