ghc/interpreter/subst.c

   1 /* -*- mode: hugs-c; -*- */
   2 /* --------------------------------------------------------------------------
   3  * subst.c:     Copyright (c) Mark P Jones 1991-1998.   All rights reserved.
   4  *              See NOTICE for details and conditions of use etc...
   5  *              Hugs version 1.3c, March 1998
   6  *
   7  * Provides an implementation for the `current substitution' used during
   8  * type and kind inference in both static analysis and type checking.
   9  * ------------------------------------------------------------------------*/
  10
  11 #include "prelude.h"
  12 #include "storage.h"
  13 #include "connect.h"
  14 #include "errors.h"
  15 #include "link.h"
  16 #include "subst.h"
  17
  18 /*#define DEBUG_TYPES*/
  19
  20 static Int numTyvars;                   /* no. type vars currently in use  */
  21 static Int maxTyvars = 0;
  22 static Int nextGeneric;                 /* number of generics found so far */
  23
  24 #if    FIXED_SUBST
  25 Tyvar  tyvars[NUM_TYVARS];              /* storage for type variables      */
  26 #else
  27 Tyvar  *tyvars = 0;                     /* storage for type variables      */
  28 #endif
  29 Int    typeOff;                         /* offset of result type           */
  30 Type   typeIs;                          /* skeleton of result type         */
  31 Int    typeFree;                        /* freedom in instantiated type    */
  32 List   predsAre;                        /* list of predicates in type      */
  33 List   genericVars;                     /* list of generic vars            */
  34 List   btyvars = NIL;                   /* explicitly scoped type vars     */
  35
  36 /* --------------------------------------------------------------------------
  37  * local function prototypes:
  38  * ------------------------------------------------------------------------*/
  39
  40 static Void local expandSubst           Args((Int));
  41 static Int  local findBtyvsInt          Args((Text));
  42 static Type local makeTupleType         Args((Int));
  43 static Kind local makeSimpleKind        Args((Int));
  44 static Kind local makeVarKind           Args((Int));
  45 static Void local expandSyn1            Args((Tycon, Type *, Int *));
  46 static Type local dropRank1Body         Args((Type,Int,Int));
  47 static Type local liftRank1Body         Args((Type,Int));
  48
  49 static Bool local varToVarBind          Args((Tyvar *,Tyvar *));
  50 static Bool local varToTypeBind         Args((Tyvar *,Type,Int));
  51 #if TREX
  52 static Bool local inserter              Args((Type,Int,Type,Int));
  53 static Int  local remover               Args((Text,Type,Int));
  54 #endif
  55 static Bool local kvarToVarBind         Args((Tyvar *,Tyvar *));
  56 static Bool local kvarToTypeBind        Args((Tyvar *,Type,Int));
  57
  58 /* --------------------------------------------------------------------------
  59  * The substitution, types, and kinds:
  60  *
  61  * In early versions of Gofer, the `substitution' data structure was only
  62  * used by the type checker, so it made sense to include support for it in
  63  * type.c.  This changed when kinds and kind inference where introduced,
  64  * which required access to the substitution during static analysis.  The
  65  * links between type.c and static.c that were intially used to accomplish
  66  * this have now been avoided by making the substitution visible as an
  67  * independent data structure in storage.c.
  68  *
  69  * In the same way that values have types, type constructors (and more
  70  * generally, expressions built from such constructors) have kinds.
  71  * The syntax of kinds in the current implementation is very simple:
  72  *
  73  *        kind ::= STAR         -- the kind of types
  74  *              |  kind => kind -- constructors
  75  *              |  variables    -- either INTCELL or OFFSET
  76  *
  77  * For various reasons, this implementation uses structure sharing, instead
  78  * of a copying approach.  In principal, this is fast and avoids the need to
  79  * build new type expressions.  Unfortunately, this implementation will not
  80  * be able to handle *very* large expressions.
  81  *
  82  * The substitution is represented by an array of type variables each of
  83  * which is a triple:
  84  *      bound   a (skeletal) type expression, or NIL if the variable
  85  *              is not bound, or SKOLEM for a Skolem constant (i.e., an
  86  *              uninstantiable variable).
  87  *      offs    offset of skeleton in bound.  If isNull(bound), then offs is
  88  *              used to indicate whether that variable is generic (i.e. free
  89  *              in the current assumption set) or fixed (i.e. bound in the
  90  *              current assumption set).  Generic variables are assigned
  91  *              offset numbers whilst copying type expressions (t,o) to
  92  *              obtain their most general form.
  93  *      kind    kind of value bound to type variable (`type variable' is
  94  *              rather inaccurate -- `constructor variable' would be better).
  95  * ------------------------------------------------------------------------*/
  96
  97 Void emptySubstitution() {              /* clear current substitution      */
  98     numTyvars   = 0;
  99 #if !FIXED_SUBST
 100     if (maxTyvars!=NUM_TYVARS) {
 101         maxTyvars = 0;
 102         if (tyvars) {
 103             free(tyvars);
 104             tyvars = 0;
 105         }
 106     }
 107 #endif
 108     nextGeneric = 0;
 109     genericVars = NIL;
 110     typeIs      = NIL;
 111     predsAre    = NIL;
 112     btyvars     = NIL;
 113 }
 114
 115 static Void local expandSubst(n)        /* add further n type variables to */
 116 Int n; {                                /* current substituion             */
 117 #if FIXED_SUBST
 118     if (numTyvars+n>NUM_TYVARS) {
 119         ERRMSG(0) "Too many type variables in type checker"
 120         EEND;
 121     }
 122 #else
 123     if (numTyvars+n>maxTyvars) {        /* need to expand substitution     */
 124         Int   newMax = maxTyvars+NUM_TYVARS;
 125         Tyvar *newTvs;
 126         Int   i;
 127
 128         if (numTyvars+n>newMax) {       /* safety precaution               */
 129             ERRMSG(0) "Substitution expanding too quickly"
 130             EEND;
 131         }
 132
 133         /* It would be better to realloc() here, but that isn't portable
 134          * enough for calloc()ed arrays.  The following code could cause
 135          * a space leak if an interrupt occurs while we're copying the
 136          * array ... we won't worry about this for the time being because
 137          * we don't expect to have to go through this process much (if at
 138          * all) in normal use of the type checker.
 139          */
 140
 141         newTvs = (Tyvar *)calloc(newMax,sizeof(Tyvar));
 142         if (!newTvs) {
 143             ERRMSG(0) "Too many variables (%d) in type checker", newMax
 144             EEND;
 145         }
 146         for (i=0; i<numTyvars;++i) {            /* copy substitution       */
 147             newTvs[i].offs  = tyvars[i].offs;
 148             newTvs[i].bound = tyvars[i].bound;
 149             newTvs[i].kind  = tyvars[i].kind;
 150         }
 151         maxTyvars = 0;                          /* protection from SIGINT? */
 152         if (tyvars) free(tyvars);
 153         tyvars    = newTvs;
 154         maxTyvars = newMax;
 155     }
 156 #endif
 157 }
 158
 159 Int newTyvars(n)                        /* allocate new type variables     */
 160 Int n; {                                /* all of kind STAR                */
 161     Int beta = numTyvars;
 162
 163     expandSubst(n);
 164     for (numTyvars+=n; n>0; n--) {
 165         tyvars[numTyvars-n].offs  = UNUSED_GENERIC;
 166         tyvars[numTyvars-n].bound = NIL;
 167         tyvars[numTyvars-n].kind  = STAR;
 168 #ifdef DEBUG_TYPES
 169         printf("new type variable: _%d ::: ",numTyvars-n);
 170         printKind(stdout,tyvars[numTyvars-n].kind);
 171         putchar('\n');
 172 #endif
 173     }
 174     return beta;
 175 }
 176
 177 Int newKindedVars(k)                    /* allocate new variables with     */
 178 Kind k; {                               /* specified kinds                 */
 179     Int beta = numTyvars;               /* if k = k0 -> k1 -> ... -> kn    */
 180     for (; isPair(k); k=snd(k)) {       /* then allocate n vars with kinds */
 181         expandSubst(1);                 /* k0, k1, ..., k(n-1)             */
 182         tyvars[numTyvars].offs  = UNUSED_GENERIC;
 183         tyvars[numTyvars].bound = NIL;
 184         tyvars[numTyvars].kind  = fst(k);
 185 #ifdef DEBUG_TYPES
 186         printf("new type variable: _%d ::: ",numTyvars);
 187         printKind(stdout,tyvars[numTyvars].kind);
 188         putchar('\n');
 189 #endif
 190         numTyvars++;
 191     }
 192     return beta;
 193 }
 194
 195 Void instantiate(type)                  /* instantiate type, if nonNull    */
 196 Type type; {
 197     predsAre = NIL;
 198     typeIs   = type;
 199     typeFree = 0;
 200
 201     if (nonNull(typeIs)) {             /* instantiate type expression ?    */
 202
 203         if (isPolyType(typeIs)) {      /* Polymorphic type scheme ?        */
 204             Kinds ks = polySigOf(typeIs);
 205             typeOff  = newKindedVars(ks);
 206             typeIs   = monotypeOf(typeIs);
 207             for (; isAp(ks); ks=arg(ks))
 208                 typeFree++;
 209         }
 210
 211         if (whatIs(typeIs)==QUAL) {    /* Qualified type?                  */
 212             predsAre = fst(snd(typeIs));
 213             typeIs   = snd(snd(typeIs));
 214         }
 215     }
 216 }
 217
 218 /* --------------------------------------------------------------------------
 219  * Bound type variables:
 220  * ------------------------------------------------------------------------*/
 221
 222 Pair findBtyvs(t)                       /* Look for bound tyvar            */
 223 Text t; {
 224     List bts = btyvars;
 225     for (; nonNull(bts); bts=tl(bts)) {
 226         List bts1 = hd(bts);
 227         for (; nonNull(bts1); bts1=tl(bts1))
 228             if (t==textOf(fst(hd(bts1))))
 229                 return hd(bts1);
 230     }
 231     return NIL;
 232 }
 233
 234 static Int local findBtyvsInt(t)        /* Look for bound type variable    */
 235 Text t; {                               /* expecting to find an integer    */
 236     Pair p = findBtyvs(t);
 237     if (isNull(p))
 238         internal("findBtyvsInt");
 239     return intOf(snd(p));
 240 }
 241
 242 Void markBtyvs() {                      /* Mark explicitly scoped vars     */
 243     List bts = btyvars;
 244     for (; nonNull(bts); bts=tl(bts)) {
 245         List bts1 = hd(bts);
 246         for (; nonNull(bts1); bts1=tl(bts1))
 247             markTyvar(intOf(snd(hd(bts1))));
 248     }
 249 }
 250
 251 Type localizeBtyvs(t)                   /* Localize type to eliminate refs */
 252 Type t; {                               /* to explicitly scoped vars       */
 253     switch (whatIs(t)) {
 254         case RANK2    :
 255         case POLYTYPE : snd(snd(t)) = localizeBtyvs(snd(snd(t)));
 256                         break;
 257
 258         case QUAL     : fst(snd(t)) = localizeBtyvs(fst(snd(t)));
 259                         snd(snd(t)) = localizeBtyvs(snd(snd(t)));
 260                         break;
 261
 262         case AP       : fst(t) = localizeBtyvs(fst(t));
 263                         snd(t) = localizeBtyvs(snd(t));
 264                         break;
 265
 266         case VARIDCELL:
 267         case VAROPCELL: return mkInt(findBtyvsInt(textOf(t)));
 268     }
 269     return t;
 270 }
 271
 272 /* --------------------------------------------------------------------------
 273  * Dereference or bind types in subsitution:
 274  * ------------------------------------------------------------------------*/
 275
 276 Tyvar *getTypeVar(t,o)                  /* get number of type variable     */
 277 Type t;                                 /* represented by (t,o) [if any].  */
 278 Int  o; {
 279     switch (whatIs(t)) {
 280         case INTCELL   : return tyvar(intOf(t));
 281         case OFFSET    : return tyvar(o+offsetOf(t));
 282         case VARIDCELL :
 283         case VAROPCELL : return tyvar(findBtyvsInt(textOf(t)));
 284     }
 285     return ((Tyvar *)0);
 286 }
 287
 288 Void tyvarType(vn)                      /* load type held in type variable */
 289 Int vn; {                               /* vn into (typeIs,typeOff)        */
 290     Tyvar *tyv;
 291
 292     while ((tyv=tyvar(vn)), isBound(tyv))
 293         switch(whatIs(tyv->bound)) {
 294             case INTCELL   : vn = intOf(tyv->bound);
 295                              break;
 296
 297             case OFFSET    : vn = offsetOf(tyv->bound)+(tyv->offs);
 298                              break;
 299
 300             case VARIDCELL :
 301             case VAROPCELL : vn = findBtyvsInt(textOf(tyv->bound));
 302                              break;
 303
 304             default        : typeIs  = tyv->bound;
 305                              typeOff = tyv->offs;
 306                              return;
 307         }
 308     typeIs  = aVar;
 309     typeOff = vn;
 310 }
 311
 312 Void bindTv(vn,t,o)                     /* set type variable vn to (t,o)   */
 313 Int  vn;
 314 Type t;
 315 Int  o; {
 316     Tyvar *tyv = tyvar(vn);
 317     tyv->bound = t;
 318     tyv->offs  = o;
 319 #ifdef DEBUG_TYPES
 320     printf("binding type variable: _%d to ",vn);
 321     printType(stdout,debugType(t,o));
 322     putchar('\n');
 323 #endif
 324 }
 325
 326 Cell getDerefHead(t,o)                  /* get value at head of type exp.  */
 327 Type t;
 328 Int  o; {
 329     Tyvar *tyv;
 330     argCount = 0;
 331     for (;;) {
 332         while (isAp(t)) {
 333             argCount++;
 334             t = fun(t);
 335         }
 336         if ((tyv=getTypeVar(t,o)) && isBound(tyv)) {
 337             t = tyv->bound;
 338             o = tyv->offs;
 339         }
 340         else
 341             break;
 342     }
 343     return t;
 344 }
 345
 346 /* --------------------------------------------------------------------------
 347  * Expand type synonyms:
 348  * ------------------------------------------------------------------------*/
 349
 350 Void expandSyn(h,ar,at,ao)              /* Expand type synonym with:       */
 351 Tycon h;                                /* head h                          */
 352 Int   ar;                               /* ar args (NB. ar>=tycon(h).arity)*/
 353 Type  *at;                              /* original expression (*at,*ao)   */
 354 Int   *ao; {                            /* expansion returned in (*at,*ao) */
 355     ar -= tycon(h).arity;               /* calculate surplus arguments     */
 356     if (ar==0)
 357         expandSyn1(h,at,ao);
 358     else {                              /* if there are more args than the */
 359         Type t    = *at;                /* arity, we have to do a little   */
 360         Int  o    = *ao;                /* bit of work to isolate args that*/
 361         Type args = NIL;                /* will not be changed by expansion*/
 362         Int  i;
 363         while (ar-- > 0) {              /* find part to expand, and the    */
 364             Tyvar *tyv;                 /* unused arguments                */
 365             args = cons(arg(t),args);
 366             t    = fun(t);
 367             deRef(tyv,t,o);
 368         }
 369         expandSyn1(h,&t,&o);            /* do the expansion                */
 370         bindTv((i=newTyvars(1)),t,o);   /* and embed the results back in   */
 371         tyvar(i)->kind = getKind(t,o);  /* (*at, *ao) as required          */
 372         *at = applyToArgs(mkInt(i),args);
 373     }
 374 }
 375
 376 static Void local expandSyn1(h,at,ao)   /* Expand type synonym with:       */
 377 Tycon h;                                /* head h, tycon(h).arity args,    */
 378 Type  *at;                              /* original expression (*at,*ao)   */
 379 Int   *ao; {                            /* expansion returned in (*at,*ao) */
 380     Int   n = tycon(h).arity;
 381     Type  t = *at;
 382     Int   o = *ao;
 383     Tyvar *tyv;
 384
 385     *at = tycon(h).defn;
 386     *ao = newKindedVars(tycon(h).kind);
 387     for (; 0<n--; t=fun(t)) {
 388         deRef(tyv,t,o);
 389         if (tyv || !isAp(t))
 390             internal("expandSyn1");
 391         bindTv(*ao+n,arg(t),o);
 392     }
 393 }
 394
 395 /* --------------------------------------------------------------------------
 396  * Marking fixed variables in type expressions:
 397  * ------------------------------------------------------------------------*/
 398
 399 Void clearMarks() {                     /* set all unbound type vars to    */
 400     Int i;                              /* unused generic variables        */
 401     for (i=0; i<numTyvars; ++i)
 402         if (!isBound(tyvar(i)))
 403             tyvar(i)->offs = UNUSED_GENERIC;
 404     genericVars = NIL;
 405     nextGeneric = 0;
 406 }
 407
 408 Void resetGenerics() {                  /* Reset all generic vars to unused*/
 409     Int i;
 410     for (i=0; i<numTyvars; ++i)
 411         if (!isBound(tyvar(i)) && tyvar(i)->offs>=GENERIC)
 412             tyvar(i)->offs = UNUSED_GENERIC;
 413     genericVars = NIL;
 414     nextGeneric = 0;
 415 }
 416
 417 Void markTyvar(vn)                      /* mark fixed vars in type bound to*/
 418 Int vn; {                               /* given type variable             */
 419     Tyvar *tyv = tyvar(vn);
 420
 421     if (isBound(tyv))
 422         markType(tyv->bound, tyv->offs);
 423     else
 424         (tyv->offs) = FIXED_TYVAR;
 425 }
 426
 427 Void markType(t,o)                      /* mark fixed vars in type (t,o)   */
 428 Type t;
 429 Int  o; {
 430     switch (whatIs(t)) {
 431 #if TREX
 432         case EXT       :st
 433 #endif
 434         case TYCON     :
 435         case TUPLE     : return;
 436
 437         case AP        : markType(fst(t),o);
 438                          markType(snd(t),o);
 439                          return;
 440
 441         case OFFSET    : markTyvar(o+offsetOf(t));
 442                          return;
 443
 444         case INTCELL   : markTyvar(intOf(t));
 445                          return;
 446
 447         case VARIDCELL :
 448         case VAROPCELL : markTyvar(findBtyvsInt(textOf(t)));
 449                          return;
 450
 451         case RANK2     : markType(snd(snd(t)),o);
 452                          return;
 453         case POLYTYPE  : /* No need to mark generic types */
 454                          return;
 455
 456         default        : internal("markType");
 457     }
 458 }
 459
 460 Void markPred(pi)                       /* Marked fixed type vars in pi    */
 461 Cell pi; {
 462     Cell cl = fst3(pi);
 463     Int  o  = intOf(snd3(pi));
 464
 465     for (; isAp(cl); cl=fun(cl))
 466         markType(arg(cl),o);
 467 }
 468
 469 /* --------------------------------------------------------------------------
 470  * Copy type expression from substitution to make a single type expression:
 471  * ------------------------------------------------------------------------*/
 472
 473 Type copyTyvar(vn)                      /* calculate most general form of  */
 474 Int vn; {                               /* type bound to given type var    */
 475     Tyvar *tyv = tyvar(vn);
 476
 477     if (isBound(tyv))
 478         return copyType(tyv->bound,tyv->offs);
 479
 480     switch (tyv->offs) {
 481         case FIXED_TYVAR    : return mkInt(vn);
 482
 483         case UNUSED_GENERIC : (tyv->offs) = GENERIC + nextGeneric++;
 484                               if (nextGeneric>=NUM_OFFSETS) {
 485                                   ERRMSG(0)
 486                                       "Too many quantified type variables"
 487                                   EEND;
 488                               }
 489                               genericVars = cons(mkInt(vn),genericVars);
 490
 491         default             : return mkOffset(tyv->offs - GENERIC);
 492     }
 493 }
 494
 495 Type copyType(t,o)                      /* calculate most general form of  */
 496 Type t;                                 /* type expression (t,o)           */
 497 Int  o; {
 498     switch (whatIs(t)) {
 499         case AP        : {   Type l = copyType(fst(t),o);/* ensure correct */
 500                              Type r = copyType(snd(t),o);/* eval. order    */
 501                              return ap(l,r);
 502                          }
 503         case OFFSET    : return copyTyvar(o+offsetOf(t));
 504         case INTCELL   : return copyTyvar(intOf(t));
 505         case VARIDCELL :
 506         case VAROPCELL : return copyTyvar(findBtyvsInt(textOf(t)));
 507     }
 508
 509     return t;
 510 }
 511
 512 Cell copyPred(pi,o)                     /* Copy single predicate (or part  */
 513 Cell pi;                                /* thereof) ...                    */
 514 Int  o; {
 515     if (isAp(pi)) {
 516         Cell temp = copyPred(fun(pi),o);/* to ensure correct order of eval.*/
 517         return ap(temp,copyType(arg(pi),o));
 518     }
 519     else
 520         return pi;
 521 }
 522
 523 #ifdef DEBUG_TYPES
 524 Type debugTyvar(vn)                     /* expand type structure in full   */
 525 Int vn; {                               /* detail                          */
 526     Tyvar *tyv = tyvar(vn);
 527
 528     if (isBound(tyv))
 529         return debugType(tyv->bound,tyv->offs);
 530     return mkInt(vn);
 531 }
 532
 533 Type debugType(t,o)
 534 Type t;
 535 Int  o; {
 536     switch (whatIs(t)) {
 537         case AP        : {   Type l = debugType(fst(t),o);
 538                              Type r = debugType(snd(t),o);
 539                              return ap(l,r);
 540                          }
 541         case OFFSET    : return debugTyvar(o+offsetOf(t));
 542         case INTCELL   : return debugTyvar(intOf(t));
 543         case VARIDCELL :
 544         case VAROPCELL : return debugTyvar(findBtyvsInt(textOf(t)));
 545     }
 546
 547     return t;
 548 }
 549 #endif /*DEBUG_TYPES*/
 550
 551 Kind copyKindvar(vn)                    /* build kind attatched to variable*/
 552 Int vn; {
 553     Tyvar *tyv = tyvar(vn);
 554     if (tyv->bound)
 555         return copyKind(tyv->bound,tyv->offs);
 556     return STAR;                        /* any unbound variable defaults to*/
 557 }                                       /* the kind of all types           */
 558
 559 Kind copyKind(k,o)                      /* build kind expression from      */
 560 Kind k;                                 /* given skeleton                  */
 561 Int  o; {
 562     switch (whatIs(k)) {
 563         case AP      : {   Kind l = copyKind(fst(k),o);  /* ensure correct */
 564                            Kind r = copyKind(snd(k),o);  /* eval. order    */
 565                            return ap(l,r);
 566                        }
 567         case OFFSET  : return copyKindvar(o+offsetOf(k));
 568         case INTCELL : return copyKindvar(intOf(k));
 569     }
 570     return k;
 571 }
 572
 573 /* --------------------------------------------------------------------------
 574  * Droping and lifting of type schemes that appear in rank 2 position:
 575  * ------------------------------------------------------------------------*/
 576
 577 Type dropRank2(t,alpha,n)               /* Drop a (potentially) rank2 type */
 578 Type t;
 579 Int  alpha;
 580 Int  n; {
 581     if (whatIs(t)==RANK2) {
 582         Cell r  = fst(snd(t));
 583         Int  i  = intOf(r);
 584         Type as = NIL;
 585         for (t=snd(snd(t)); i>0; i--) {
 586             Type a = arg(fun(t));
 587             if (isPolyType(a))
 588                 a = dropRank1(a,alpha,n);
 589             as = ap2(typeArrow,a,as);
 590             t  = arg(t);
 591         }
 592         t = ap(RANK2,pair(r,revOnto(as,t)));
 593     }
 594     return t;
 595 }
 596
 597 Type dropRank1(t,alpha,n)               /* Copy rank1 argument type t to   */
 598 Type t;                                 /* make a rank1 type scheme        */
 599 Int  alpha;
 600 Int  n; {
 601     if (n>0 && isPolyType(t))
 602         t = mkPolyType(polySigOf(t),dropRank1Body(monotypeOf(t),alpha,n));
 603     return t;
 604 }
 605
 606 static Type local dropRank1Body(t,alpha,n)
 607 Type t;
 608 Int  alpha;
 609 Int  n; {
 610     switch (whatIs(t)) {
 611         case OFFSET   : {   Int m = offsetOf(t);
 612                             return (m>=n) ? mkOffset(m-n) : mkInt(alpha+m);
 613                         }
 614
 615         case POLYTYPE : return mkPolyType(polySigOf(t),
 616                                           dropRank1Body(monotypeOf(t),alpha,n));
 617
 618         case QUAL     : return ap(QUAL,dropRank1Body(snd(t),alpha,n));
 619
 620         case RANK2    : return ap(RANK2,pair(fst(snd(t)),
 621                                              dropRank1Body(snd(snd(t)),
 622                                                            alpha,
 623                                                            n)));
 624
 625         case AP       : return ap(dropRank1Body(fun(t),alpha,n),
 626                                   dropRank1Body(arg(t),alpha,n));
 627
 628         default       : return t;
 629     }
 630 }
 631
 632 Void liftRank2Args(as,alpha,m)
 633 List as;
 634 Int  alpha;
 635 Int  m; {
 636     Int i = 0;
 637     for (; i<m; i++)
 638         copyTyvar(alpha+i);
 639     for (m=nextGeneric; nonNull(as); as=tl(as)) {
 640         Type ta = arg(fun(as));
 641         ta      = isPolyType(ta) ? liftRank1Body(ta,m) : copyType(ta,alpha);
 642         arg(fun(as))
 643                 = ta;
 644     }
 645 }
 646
 647 Type liftRank2(t,alpha,m)
 648 Type t;
 649 Int  alpha;
 650 Int  m; {
 651     if (whatIs(t)==RANK2) {
 652         Cell r  = fst(snd(t));
 653         Int  i  = 0;
 654         Type as = NIL;
 655         for (; i<m; i++)
 656             copyTyvar(alpha+i);
 657         m = nextGeneric;
 658         t = snd(snd(t));
 659         for (i=intOf(r); i>0; i--) {
 660             Type a = arg(fun(t));
 661             a      = isPolyType(a) ? liftRank1Body(a,m) : copyType(a,alpha);
 662             as     = ap2(typeArrow,a,as);
 663             t      = arg(t);
 664         }
 665         t = ap(RANK2,pair(r,revOnto(as,copyType(t,alpha))));
 666     }
 667     else
 668         t = copyType(t,alpha);
 669     return t;
 670 }
 671
 672 Type liftRank1(t,alpha,m)
 673 Type t;
 674 Int  alpha;
 675 Int  m; {
 676     if (m>0 && isPolyType(t)) {
 677         Int i = 0;
 678         resetGenerics();
 679         for (; i<m; i++)
 680             copyTyvar(alpha+i);
 681         t = liftRank1Body(t,nextGeneric);
 682     }
 683     return t;
 684 }
 685
 686 static Type local liftRank1Body(t,n)
 687 Type t;
 688 Int  n; {
 689     switch (whatIs(t)) {
 690         case OFFSET    : return mkOffset(n+offsetOf(t));
 691
 692         case INTCELL   : return copyTyvar(intOf(t));
 693
 694         case VARIDCELL :
 695         case VAROPCELL : return copyTyvar(findBtyvsInt(textOf(t)));
 696
 697         case POLYTYPE  : return mkPolyType(polySigOf(t),
 698                                            liftRank1Body(monotypeOf(t),n));
 699
 700         case QUAL      : return ap(QUAL,liftRank1Body(snd(t),n));
 701
 702         case RANK2     : return ap(RANK2,pair(fst(snd(t)),
 703                                               liftRank1Body(snd(snd(t)),n)));
 704
 705         case AP        : return ap(liftRank1Body(fun(t),n),
 706                                    liftRank1Body(arg(t),n));
 707
 708         default        : return t;
 709     }
 710 }
 711
 712 /* --------------------------------------------------------------------------
 713  * Support for `kind preserving substitutions' from unification:
 714  * ------------------------------------------------------------------------*/
 715
 716 Bool eqKind(k1,k2)                      /* check that two (mono)kinds are  */
 717 Kind k1, k2; {                          /* equal                           */
 718     return k1==k2
 719            || (isPair(k1) && isPair(k2)
 720               && eqKind(fst(k1),fst(k2))
 721               && eqKind(snd(k1),snd(k2)));
 722 }
 723
 724 Kind getKind(c,o)                       /* Find kind of constr during type */
 725 Cell c;                                 /* checking process                */
 726 Int  o; {
 727     if (isAp(c))                                        /* application     */
 728         return snd(getKind(fst(c),o));
 729     switch (whatIs(c)) {
 730         case TUPLE     : return simpleKind(tupleOf(c)); /*(,)::* -> * -> * */
 731         case OFFSET    : return tyvar(o+offsetOf(c))->kind;
 732         case INTCELL   : return tyvar(intOf(c))->kind;
 733         case VARIDCELL :
 734         case VAROPCELL : return tyvar(findBtyvsInt(textOf(c)))->kind;
 735         case TYCON     : return tycon(c).kind;
 736 #if TREX
 737         case EXT    : return extKind;
 738 #endif
 739     }
 740 #ifdef DEBUG_KINDS
 741     printf("getKind c = %d, whatIs=%d\n",c,whatIs(c));
 742 #endif
 743     internal("getKind");
 744     return STAR;/* not reached */
 745 }
 746
 747 /* --------------------------------------------------------------------------
 748  * Find generic variables in a type:
 749  * ------------------------------------------------------------------------*/
 750
 751 Type genvarTyvar(vn,vs)                 /* calculate list of generic vars  */
 752 Int  vn;                                /* thru variable vn, prepended to  */
 753 List vs; {                              /* list vs                         */
 754     Tyvar *tyv = tyvar(vn);
 755
 756     if (isBound(tyv))
 757         return genvarType(tyv->bound,tyv->offs,vs);
 758     else if (tyv->offs == UNUSED_GENERIC) {
 759         tyv->offs += GENERIC + nextGeneric++;
 760         return cons(mkInt(vn),vs);
 761     }
 762     else if (tyv->offs>=GENERIC && !intIsMember(vn,vs))
 763         return cons(mkInt(vn),vs);
 764     else
 765         return vs;
 766 }
 767
 768 List genvarType(t,o,vs)                 /* calculate list of generic vars  */
 769 Type t;                                 /* in type expression (t,o)        */
 770 Int  o;                                 /* results are prepended to vs     */
 771 List vs; {
 772     switch (whatIs(t)) {
 773         case AP        : return genvarType(snd(t),o,genvarType(fst(t),o,vs));
 774         case OFFSET    : return genvarTyvar(o+offsetOf(t),vs);
 775         case INTCELL   : return genvarTyvar(intOf(t),vs);
 776         case VARIDCELL :
 777         case VAROPCELL : return genvarTyvar(findBtyvsInt(textOf(t)),vs);
 778     }
 779     return vs;
 780 }
 781
 782 /* --------------------------------------------------------------------------
 783  * Occurs check:
 784  * ------------------------------------------------------------------------*/
 785
 786 Bool doesntOccurIn(lookFor,t,o)         /* Return TRUE if var lookFor      */
 787 Tyvar *lookFor;                         /* isn't referenced in (t,o)       */
 788 Type  t;
 789 Int   o; {
 790     Tyvar *tyv;
 791
 792     for (;;) {
 793         deRef(tyv,t,o);
 794         if (tyv)                        /* type variable                   */
 795             return tyv!=lookFor;
 796         else if (isAp(t)) {             /* application                     */
 797             if (doesntOccurIn(lookFor,snd(t),o))
 798                 t = fst(t);
 799             else
 800                 return FALSE;
 801         }
 802         else                            /* no variable found               */
 803             break;
 804     }
 805     return TRUE;
 806 }
 807
 808 /* --------------------------------------------------------------------------
 809  * Unification algorithm:
 810  * ------------------------------------------------------------------------*/
 811
 812 char   *unifyFails   = 0;               /* Unification error message       */
 813 static Int bindAbove = 0;               /* Used to restrict var binding    */
 814
 815 #define bindOnlyAbove(beta)     bindAbove=beta
 816 #define noBind()                bindAbove=MAXPOSINT
 817 #define unrestrictBind()        bindAbove=0
 818
 819 static Bool local varToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2      */
 820 Tyvar *tyv1, *tyv2; {
 821     if (tyv1!=tyv2) {                   /* If vars are same, nothing to do!*/
 822
 823         /* Check that either tyv1 or tyv2 is in allowed range for binding  */
 824         /* and is not a Skolem constant, and swap vars if nec. so we can   */
 825         /* bind to tyv1.                                                   */
 826
 827         if (tyvNum(tyv1)<bindAbove || tyv1->bound==SKOLEM) {
 828             if (tyvNum(tyv2)<bindAbove || tyv2->bound==SKOLEM) {
 829                 unifyFails = "types do not match";
 830                 return FALSE;
 831             }
 832             else {
 833                 Tyvar *tyv = tyv1;
 834                 tyv1       = tyv2;
 835                 tyv2       = tyv;
 836             }
 837         }
 838         if (!eqKind(tyv1->kind,tyv2->kind)) {
 839             unifyFails = "constructor variable kinds do not match";
 840             return FALSE;
 841         }
 842         tyv1->bound = aVar;
 843         tyv1->offs  = tyvNum(tyv2);
 844 #ifdef DEBUG_TYPES
 845         printf("vv binding tyvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
 846 #endif
 847     }
 848     return TRUE;
 849 }
 850
 851 static Bool local varToTypeBind(tyv,t,o)/* Make binding tyv := (t,o)       */
 852 Tyvar *tyv;
 853 Type  t;                                /* guaranteed not to be a v'ble or */
 854 Int   o; {                              /* have synonym as outermost constr*/
 855     if (tyvNum(tyv)<bindAbove) {        /* Check that tyv is in range      */
 856         unifyFails = "types do not match";
 857         return FALSE;
 858     }
 859     else if (tyv->bound == SKOLEM) {    /* Check that it is not Skolemized */
 860         unifyFails = "cannot instantiate Skolem constant";
 861         return FALSE;
 862     }
 863     else if (!doesntOccurIn(tyv,t,o))   /* Carry out occurs check          */
 864         unifyFails = "unification would give infinite type";
 865     else if (!eqKind(tyv->kind,getKind(t,o)))
 866         unifyFails = "kinds do not match";
 867     else {
 868         tyv->bound = t;
 869         tyv->offs  = o;
 870 #ifdef DEBUG_TYPES
 871         printf("vt binding type variable: _%d to ",tyvNum(tyv));
 872         printType(stdout,debugType(t,o));
 873         putchar('\n');
 874 #endif
 875         return TRUE;
 876     }
 877     return FALSE;
 878 }
 879
 880 Bool unify(t1,o1,t2,o2)                 /* Main unification routine        */
 881 Type t1,t2;                             /* unify (t1,o1) with (t2,o2)      */
 882 Int  o1,o2; {
 883     Tyvar *tyv1, *tyv2;
 884
 885     deRef(tyv1,t1,o1);
 886     deRef(tyv2,t2,o2);
 887
 888 un: if (tyv1)
 889         if (tyv2)
 890             return varToVarBind(tyv1,tyv2);         /* t1, t2 variables    */
 891         else {
 892             Cell h2 = getDerefHead(t2,o2);          /* t1 variable, t2 not */
 893             if (isSynonym(h2) && argCount>=tycon(h2).arity) {
 894                 expandSyn(h2,argCount,&t2,&o2);
 895                 deRef(tyv2,t2,o2);
 896                 goto un;
 897             }
 898             return varToTypeBind(tyv1,t2,o2);
 899         }
 900     else
 901         if (tyv2) {
 902             Cell h1 = getDerefHead(t1,o1);          /* t2 variable, t1 not */
 903             if (isSynonym(h1) && argCount>=tycon(h1).arity) {
 904                 expandSyn(h1,argCount,&t1,&o1);
 905                 deRef(tyv1,t1,o1);
 906                 goto un;
 907             }
 908             return varToTypeBind(tyv2,t1,o1);
 909         }
 910         else {                                      /* t1, t2 not vars     */
 911             Type h1 = getDerefHead(t1,o1);
 912             Int  a1 = argCount;
 913             Type h2 = getDerefHead(t2,o2);
 914             Int  a2 = argCount;
 915
 916 #ifdef DEBUG_TYPES
 917             printf("tt unifying types: ");
 918             printType(stdout,debugType(t1,o1));
 919             printf(" with ");
 920             printType(stdout,debugType(t2,o2));
 921             putchar('\n');
 922 #endif
 923
 924             if (isOffset(h1) || isInt(h1)) h1=NIL;  /* represent var by NIL*/
 925             if (isOffset(h2) || isInt(h2)) h2=NIL;
 926
 927 #if TREX
 928             if (isExt(h1) || isExt(h2)) {
 929                 if (a1==2 && isExt(h1) && a2==2 && isExt(h2))
 930                     return inserter(fun(t1),o1,t2,o2) &&
 931                               unify(arg(t1),o1,aVar,
 932                                  remover(extText(h1),t2,o2));
 933                 else {
 934                     unifyFails = "rows are not compatible";
 935                     return FALSE;
 936                 }
 937             }
 938 #endif
 939             if (nonNull(h1) && h1==h2) {/* Assuming well-formed types, both*/
 940                 if (a1!=a2) {           /* t1, t2 must have same no of args*/
 941                     unifyFails = "incompatible constructors";
 942                     return FALSE;
 943                 }
 944                 while (isAp(t1)) {
 945                     if (!unify(arg(t1),o1,arg(t2),o2))
 946                         return FALSE;
 947                     t1 = fun(t1);
 948                     deRef(tyv1,t1,o1);
 949                     t2 = fun(t2);
 950                     deRef(tyv2,t2,o2);
 951                 }
 952                 unifyFails = 0;
 953                 return TRUE;
 954             }
 955
 956             /* Types do not match -- look for type synonyms to expand */
 957
 958             if (isSynonym(h1) && a1>=tycon(h1).arity) {
 959                 expandSyn(h1,a1,&t1,&o1);
 960                 deRef(tyv1,t1,o1);
 961                 goto un;
 962             }
 963             if (isSynonym(h2) && a2>=tycon(h2).arity) {
 964                 expandSyn(h2,a2,&t2,&o2);
 965                 deRef(tyv2,t2,o2);
 966                 goto un;
 967             }
 968
 969             if ((isNull(h1) && a1<=a2) ||       /* last attempt -- maybe   */
 970                 (isNull(h2) && a2<=a1)) {       /* one head is a variable? */
 971                 for (;;) {
 972                     deRef(tyv1,t1,o1);
 973                     deRef(tyv2,t2,o2);
 974
 975                     if (tyv1)                           /* unify heads!    */
 976                         if (tyv2)
 977                             return varToVarBind(tyv1,tyv2);
 978                         else
 979                             return varToTypeBind(tyv1,t2,o2);
 980                     else if (tyv2)
 981                         return varToTypeBind(tyv2,t1,o1);
 982
 983                     /* at this point, neither t1 nor t2 is a variable. In  */
 984                     /* addition, they must both be APs unless one of the   */
 985                     /* head variables has been bound during unification of */
 986                     /* the arguments.                                      */
 987
 988                     if (!isAp(t1) || !isAp(t2)) {       /* might not be APs*/
 989                         unifyFails = 0;
 990                         return t1==t2;
 991                     }
 992                     if (!unify(arg(t1),o1,arg(t2),o2))  /* o/w must be APs */
 993                         return FALSE;
 994                     t1 = fun(t1);
 995                     t2 = fun(t2);
 996                 }
 997             }
 998         }
 999     unifyFails = 0;
1000     return FALSE;
1001 }
1002
1003 #if TREX
1004 static Bool local inserter(ins,o,r,or)  /* Insert field into row (r,or)    */
1005 Type ins;                               /* inserter (ins,o), where ins is  */
1006 Int  o;                                 /* an applic of an EXT to a type.  */
1007 Type r;
1008 Int  or; {
1009     Text labt = extText(fun(ins));      /* Find the text of the label      */
1010     for (;;) {
1011         Tyvar *tyv;
1012         deRef(tyv,r,or);
1013         if (tyv) {
1014             Int beta = newTyvars(1);    /* Extend row with new field       */
1015             tyvar(beta)->kind = ROW;
1016             return varToTypeBind(tyv,ap(ins,mkInt(beta)),o);
1017         }
1018         else if (isAp(r) && isAp(fun(r)) && isExt(fun(fun(r)))) {
1019             if (labt==extText(fun(fun(r))))/* Compare existing fields      */
1020                 return unify(arg(ins),o,extField(r),or);
1021             r = extRow(r);              /* Or skip to next field           */
1022         }
1023         else {                          /* Nothing else will match         */
1024             unifyFails = "field mismatch";
1025             return FALSE;
1026         }
1027     }
1028 }
1029
1030 static Int local remover(l,r,o)         /* Make a new row by copying (r,o) */
1031 Text l;                                 /* but removing the l field (which */
1032 Type r;                                 /* MUST exist)                     */
1033 Int  o; {
1034     Tyvar *tyv;
1035     Int    beta       = newTyvars(1);
1036     tyvar(beta)->kind = ROW;
1037     deRef(tyv,r,o);
1038     if (tyv || !isAp(r) || !isAp(fun(r)) || !isExt(fun(fun(r))))
1039         internal("remover");
1040     if (l==extText(fun(fun(r))))
1041         r = extRow(r);
1042     else
1043         r = ap(fun(r),mkInt(remover(l,extRow(r),o)));
1044     bindTv(beta,r,o);
1045     return beta;
1046 }
1047 #endif
1048
1049 Bool typeMatches(type,mt)               /* test if type matches monotype mt*/
1050 Type type, mt; {
1051     Bool result;
1052     if (isPolyType(type) || whatIs(type)==QUAL)
1053         return FALSE;
1054     emptySubstitution();
1055     noBind();
1056     result = unify(mt,0,type,0);
1057     unrestrictBind();
1058     emptySubstitution();
1059     return result;
1060 }
1061
1062 /* --------------------------------------------------------------------------
1063  * Matching predicates:
1064  *
1065  * There are (at least) four situations where we need to match up pairs
1066  * of predicates:
1067  *
1068  *   1) Testing to see if two predicates are the same (ignoring differences
1069  *      caused by the use of type synonyms, for example).
1070  *
1071  *   2) Matching a predicate with the head of its class so that we can
1072  *      find the corresponding superclass predicates.  If the predicates
1073  *      have already been kind-checked, and the classes are known to be
1074  *      the same, then this should never fail.
1075  *
1076  *   3) Matching a predicate against the head of an instance to see if
1077  *      that instance is applicable.
1078  *
1079  *   4) Matching two instance heads to see if there is an overlap.
1080  *
1081  * For (1), we need a matching process that does not bind any variables.
1082  * For (2) and (3), we need to use one-way matching, only allowing
1083  * variables in the class or instance head to be instantiated.  For
1084  * (4), we need two-way unification.
1085  *
1086  * Another situation in which both one-way and two-way unification might
1087  * be used is in an implementation of improvement.  Here, a one-way match
1088  * would be used to determine applicability of a rule for improvement
1089  * that would then be followed by unification with another predicate.
1090  * One possible syntax for this might be:
1091  *
1092  *     instance P => pi [improves pi'] where ...
1093  *
1094  * The intention here is that any predicate matching pi' can be unified
1095  * with pi to get more accurate types.  A simple example of this is:
1096  *
1097  *   instance Collection [a] a improves Collection [a] b where ...
1098  *
1099  * As soon as we know what the collection type is (in this case, a list),
1100  * we will also know what the element type is.  To ensure that the rule
1101  * for improvement is valid, the compilation system will also need to use
1102  * a one-way matching process to ensure that pi is a (substitution) instance
1103  * of pi'.  Another extension would be to allow more than one predicate pi'
1104  * in an improving rule.  Read the paper on simplification and improvement
1105  * for technical background.  Watch this space for implementation news!
1106  * ------------------------------------------------------------------------*/
1107
1108 Bool samePred(pi1,o1,pi,o)              /* Test to see if predicates are   */
1109 Cell pi1;                               /* the same, with no binding of    */
1110 Int  o1;                                /* the variables in either one.    */
1111 Cell pi;                                /* Assumes preds are kind correct  */
1112 Int  o; {                               /* with the same class.            */
1113     Bool result;
1114     noBind();
1115     result = unifyPred(pi1,o1,pi,o);
1116     unrestrictBind();
1117     return result;
1118 }
1119
1120 Bool matchPred(pi1,o1,pi,o)             /* One way match predicate (pi1,o1)*/
1121 Cell pi1;                               /* against (pi,o), allowing only   */
1122 Int  o1;                                /* vars in 2nd pred to be bound.   */
1123 Cell pi;                                /* Assumes preds are kind correct  */
1124 Int  o; {                               /* with the same class and that no */
1125     Bool result;                        /* vars have been alloc'd since o. */
1126     bindOnlyAbove(o);
1127     result = unifyPred(pi1,o1,pi,o);
1128     unrestrictBind();
1129     return result;
1130 }
1131
1132 Bool unifyPred(pi1,o1,pi,o)             /* Unify two predicates            */
1133 Cell pi1;                               /* Assumes preds are kind correct  */
1134 Int  o1;                                /* with the same class.            */
1135 Cell pi;
1136 Int  o; {
1137     for (; isAp(pi1); pi1=fun(pi1), pi=fun(pi))
1138         if (!unify(arg(pi1),o1,arg(pi),o))
1139             return FALSE;
1140     return pi1==pi;
1141 }
1142
1143 Inst findInstFor(pi,o)                  /* Find matching instance for pred */
1144 Cell  pi;                               /* (pi,o), or otherwise NIL.  If a */
1145 Int   o; {                              /* match is found, then tyvars from*/
1146     Class c = getHead(pi);              /* typeOff have been initialized to*/
1147     List  ins;                          /* allow direct use of specifics.  */
1148
1149     if (!isClass(c))
1150         return NIL;
1151
1152     for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins)) {
1153         Inst in   = hd(ins);
1154         Int  beta = newKindedVars(inst(in).kinds);
1155         if (matchPred(pi,o,inst(in).head,beta)) {
1156             typeOff = beta;
1157             return in;
1158         }
1159         else
1160             numTyvars = beta;
1161     }
1162     unrestrictBind();
1163
1164 #if TREX
1165     {   Int showRow = strcmp(textToStr(cclass(c).text),"ShowRecRow");
1166         Int eqRow   = strcmp(textToStr(cclass(c).text),"EqRecRow");
1167
1168         if (showRow==0 || eqRow==0) {           /* Generate instances of   */
1169             Type  t = arg(pi);                  /* ShowRecRow and EqRecRow */
1170             Tyvar *tyv;                         /* on the fly              */
1171             Cell  e;
1172             deRef(tyv,t,o);
1173             e = getHead(t);
1174             if (isExt(e)) {
1175                 Inst in = NIL;
1176                 for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins))
1177                     if (getHead(arg(inst(hd(ins)).head))==e) {
1178                         in = hd(ins);
1179                         break;
1180                     }
1181                 if (isNull(in))
1182                     in = (showRow==0) ? addRecShowInst(c,e)
1183                                       : addRecEqInst(c,e);
1184                 typeOff = newKindedVars(extKind);
1185                 bindTv(typeOff,arg(fun(t)),o);
1186                 bindTv(typeOff+1,arg(t),o);
1187                 return in;
1188             }
1189         }
1190     }
1191 #endif
1192
1193     return NIL;
1194 }
1195
1196 /* --------------------------------------------------------------------------
1197  * Compare type schemes:
1198  * ------------------------------------------------------------------------*/
1199
1200 Bool sameSchemes(s,s1)                  /* Test to see whether two type    */
1201 Type s;                                 /* schemes are the same            */
1202 Type s1; {
1203     Int  o   = 0;
1204     Int  m   = 0;
1205     Int  nr2 = 0;
1206     Bool b   = isPolyType(s);           /* Check quantifiers are the same  */
1207     Bool b1  = isPolyType(s1);
1208     if (b || b1) {
1209         if (b && b1 && eqKind(polySigOf(s),polySigOf(s1))) {
1210             Kind k = polySigOf(s);
1211             s      = monotypeOf(s);
1212             s1     = monotypeOf(s1);
1213             o      = newKindedVars(k);
1214             for (; isAp(k); k=arg(k))
1215                 m++;
1216         }
1217         else
1218             return FALSE;
1219     }
1220
1221     b  = (whatIs(s)==QUAL);             /* Check that contexts are the same*/
1222     b1 = (whatIs(s1)==QUAL);
1223     if (b || b1) {
1224         if (b && b1) {
1225             List ps  = fst(snd(s));
1226             List ps1 = fst(snd(s1));
1227             noBind();
1228             while (nonNull(ps) && nonNull(ps1)) {
1229                 Cell pi  = hd(ps);
1230                 Cell pi1 = hd(ps1);
1231                 if (getHead(pi)!=getHead(pi1)
1232                         || !unifyPred(pi,o,pi1,o))
1233                     break;
1234                 ps  = tl(ps);
1235                 ps1 = tl(ps1);
1236             }
1237             unrestrictBind();
1238             if (nonNull(ps) || nonNull(ps1))
1239                 return FALSE;
1240             s  = snd(snd(s));
1241             s1 = snd(snd(s1));
1242         }
1243         else
1244             return FALSE;
1245     }
1246
1247     b  = (whatIs(s)==RANK2);            /* Check any rank 2 annotations    */
1248     b1 = (whatIs(s1)==RANK2);
1249     if (b || b1) {
1250         if (b && b1 && intOf(fst(snd(s)))==intOf(fst(snd(s1)))) {
1251             nr2 = intOf(fst(snd(s)));
1252             s   = snd(snd(s));
1253             s1  = snd(snd(s1));
1254         }
1255         else
1256             return FALSE;
1257     }
1258
1259     for (; nr2>0; nr2--) {              /* Deal with rank 2 arguments      */
1260         Type t  = arg(fun(s));
1261         Type t1 = arg(fun(s1));
1262         b       = isPolyType(t);
1263         b1      = isPolyType(t1);
1264         if (b || b1) {
1265             if (b && b1) {
1266                 t  = dropRank1(t,o,m);
1267                 t1 = dropRank1(t1,o,m);
1268                 if (!sameSchemes(t,t1))
1269                     return FALSE;
1270             }
1271             else
1272                 return FALSE;
1273         }
1274         else {
1275             noBind();
1276             b = unify(t,o,t1,o);
1277             unrestrictBind();
1278             if (!b)
1279                 return FALSE;
1280         }
1281         s  = arg(s);
1282         s1 = arg(s1);
1283     }
1284
1285     noBind();                           /* Ensure body types are the same  */
1286     b = unify(s,o,s1,o);
1287     unrestrictBind();
1288     return b;
1289 }
1290
1291 /* --------------------------------------------------------------------------
1292  * Unify kind expressions:
1293  * ------------------------------------------------------------------------*/
1294
1295 static Bool local kvarToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2     */
1296 Tyvar *tyv1, *tyv2; {                     /* for kind variable bindings    */
1297     if (tyv1!=tyv2) {
1298         tyv1->bound = aVar;
1299         tyv1->offs  = tyvNum(tyv2);
1300 #ifdef DEBUG_KINDS
1301         printf("vv binding kvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
1302 #endif
1303     }
1304     return TRUE;
1305 }
1306
1307 static Bool local kvarToTypeBind(tyv,t,o)/* Make binding tyv := (t,o)      */
1308 Tyvar *tyv;                             /* for kind variable bindings      */
1309 Type  t;                                /* guaranteed not to be a v'ble or */
1310 Int   o; {                              /* have synonym as outermost constr*/
1311     if (doesntOccurIn(tyv,t,o)) {
1312         tyv->bound = t;
1313         tyv->offs  = o;
1314 #ifdef DEBUG_KINDS
1315         printf("vt binding kind variable: _%d to ",tyvNum(tyv));
1316         printType(stdout,debugType(t,o));
1317         putchar('\n');
1318 #endif
1319         return TRUE;
1320     }
1321     unifyFails = "unification would give infinite kind";
1322     return FALSE;
1323 }
1324
1325 Bool kunify(k1,o1,k2,o2)                /* Unify kind expr (k1,o1) with    */
1326 Kind k1,k2;                             /* (k2,o2)                         */
1327 Int  o1,o2; {
1328     Tyvar *kyv1, *kyv2;
1329
1330     deRef(kyv1,k1,o1);
1331     deRef(kyv2,k2,o2);
1332
1333     if (kyv1)
1334         if (kyv2)
1335             return kvarToVarBind(kyv1,kyv2);        /* k1, k2 variables    */
1336         else
1337             return kvarToTypeBind(kyv1,k2,o2);      /* k1 variable, k2 not */
1338     else
1339         if (kyv2)
1340             return kvarToTypeBind(kyv2,k1,o1);      /* k2 variable, k1 not */
1341         else {
1342 #ifdef DEBUG_KINDS
1343             printf("unifying kinds: ");
1344             printType(stdout,debugType(k1,o1));
1345             printf(" with ");
1346             printType(stdout,debugType(k2,o2));
1347             putchar('\n');
1348 #endif
1349             if (k1==STAR && k2==STAR)               /* k1, k2 not vars     */
1350                 return TRUE;
1351 #if TREX
1352             else if (k1==ROW && k2==ROW)
1353                 return TRUE;
1354 #endif
1355             else if (isAp(k1) && isAp(k2))
1356                 return kunify(fst(k1),o1,fst(k2),o2) &&
1357                        kunify(snd(k1),o1,snd(k2),o2);
1358         }
1359     unifyFails = 0;
1360     return FALSE;
1361 }
1362
1363 /* --------------------------------------------------------------------------
1364  * Tuple type constructors: are generated as necessary.  The most common
1365  * n-tuple constructors (n<MAXTUPCON) are held in a cache to avoid
1366  * repeated generation of the constructor types.
1367  * ------------------------------------------------------------------------*/
1368
1369 #define MAXTUPCON 10
1370 static Type tupleConTypes[MAXTUPCON];
1371
1372 Void typeTuple(e)                      /* find type for tuple constr, using*/
1373 Cell e; {                              /* tupleConTypes to cache previously*/
1374     Int n   = tupleOf(e);              /* calculated tuple constr. types.  */
1375     typeOff = newTyvars(n);
1376     if (n>=MAXTUPCON)
1377          typeIs = makeTupleType(n);
1378     else if (tupleConTypes[n])
1379          typeIs = tupleConTypes[n];
1380     else
1381          typeIs = tupleConTypes[n] = makeTupleType(n);
1382 }
1383
1384 static Type local makeTupleType(n)     /* construct type for tuple constr. */
1385 Int n; {                               /* t1 -> ... -> tn -> (t1,...,tn)   */
1386     Type h = mkTuple(n);
1387     Int  i;
1388
1389     for (i=0; i<n; ++i)
1390         h = ap(h,mkOffset(i));
1391     while (0<n--)
1392         h = fn(mkOffset(n),h);
1393     return h;
1394 }
1395
1396 /* --------------------------------------------------------------------------
1397  * Two forms of kind expression are used quite frequently:
1398  *      *  -> *  -> ... -> *  -> *      for kinds of ->, [], ->, (,) etc...
1399  *      v1 -> v2 -> ... -> vn -> vn+1   skeletons for constructor kinds
1400  * Expressions of these forms are produced by the following functions which
1401  * use a cache to avoid repeated construction of commonly used values.
1402  * A similar approach is used to store the types of tuple constructors in the
1403  * main type checker.
1404  * ------------------------------------------------------------------------*/
1405
1406 #define MAXKINDFUN 10
1407 static  Kind simpleKindCache[MAXKINDFUN];
1408 static  Kind varKindCache[MAXKINDFUN];
1409
1410 static Kind local makeSimpleKind(n)     /* construct * -> ... -> * (n args)*/
1411 Int n; {
1412     Kind k = STAR;
1413     while (n-- > 0)
1414         k = ap(STAR,k);
1415     return k;
1416 }
1417
1418 Kind simpleKind(n)                      /* return (possibly cached) simple */
1419 Int n; {                                /* function kind                   */
1420     if (n>=MAXKINDFUN)
1421         return makeSimpleKind(n);
1422     else if (nonNull(simpleKindCache[n]))
1423         return simpleKindCache[n];
1424     else if (n==0)
1425         return simpleKindCache[0] = STAR;
1426     else
1427         return simpleKindCache[n] = ap(STAR,simpleKind(n-1));
1428 }
1429
1430 static Kind local makeVarKind(n)        /* construct v0 -> .. -> vn        */
1431 Int n; {
1432     Kind k = mkOffset(n);
1433     while (n-- > 0)
1434         k = ap(mkOffset(n),k);
1435     return k;
1436 }
1437
1438 Void varKind(n)                         /* return (possibly cached) var    */
1439 Int n; {                                /* function kind                   */
1440     typeOff = newKindvars(n+1);
1441     if (n>=MAXKINDFUN)
1442         typeIs = makeVarKind(n);
1443     else if (nonNull(varKindCache[n]))
1444         typeIs = varKindCache[n];
1445     else
1446         typeIs = varKindCache[n] = makeVarKind(n);
1447 }
1448
1449 /* --------------------------------------------------------------------------
1450  * Substitutution control:
1451  * ------------------------------------------------------------------------*/
1452
1453 Void substitution(what)
1454 Int what; {
1455     Int  i;
1456
1457     switch (what) {
1458         case RESET   : emptySubstitution();
1459                        unrestrictBind();
1460                        btyvars = NIL;
1461                        break;
1462
1463         case MARK    : for (i=0; i<MAXTUPCON; ++i)
1464                            mark(tupleConTypes[i]);
1465                        for (i=0; i<MAXKINDFUN; ++i) {
1466                            mark(simpleKindCache[i]);
1467                            mark(varKindCache[i]);
1468                        }
1469                        for (i=0; i<numTyvars; ++i)
1470                            mark(tyvars[i].bound);
1471                        mark(btyvars);
1472                        mark(typeIs);
1473                        mark(predsAre);
1474                        mark(genericVars);
1475                        break;
1476
1477         case INSTALL : substitution(RESET);
1478                        for (i=0; i<MAXTUPCON; ++i)
1479                            tupleConTypes[i] = NIL;
1480                        for (i=0; i<MAXKINDFUN; ++i) {
1481                            simpleKindCache[i] = NIL;
1482                            varKindCache[i]    = NIL;
1483                        }
1484                        break;
1485     }
1486 }
1487
1488 /*-------------------------------------------------------------------------*/