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