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