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.4 $
  13  * $Date: 1999/03/01 14:46:56 $
  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     }
 919     else
 920         if (tyv2) {
 921             Cell h1 = getDerefHead(t1,o1);          /* t2 variable, t1 not */
 922             if (isSynonym(h1) && argCount>=tycon(h1).arity) {
 923                 expandSyn(h1,argCount,&t1,&o1);
 924                 deRef(tyv1,t1,o1);
 925                 goto un;
 926             }
 927             return varToTypeBind(tyv2,t1,o1);
 928         }
 929         else {                                      /* t1, t2 not vars     */
 930             Type h1 = getDerefHead(t1,o1);
 931             Int  a1 = argCount;
 932             Type h2 = getDerefHead(t2,o2);
 933             Int  a2 = argCount;
 934
 935 #ifdef DEBUG_TYPES
 936             Printf("tt unifying types: ");
 937             printType(stdout,debugType(t1,o1));
 938             Printf(" with ");
 939             printType(stdout,debugType(t2,o2));
 940             Putchar('\n');
 941 #endif
 942             if (isOffset(h1) || isInt(h1)) h1=NIL;  /* represent var by NIL*/
 943             if (isOffset(h2) || isInt(h2)) h2=NIL;
 944
 945 #if TREX
 946             if (isExt(h1) || isExt(h2)) {
 947                 if (a1==2 && isExt(h1) && a2==2 && isExt(h2)) {
 948                     if (extText(h1)==extText(h2)) {
 949                         return unify(arg(fun(t1)),o1,arg(fun(t2)),o2) &&
 950                                 unify(arg(t1),o1,arg(t2),o2);
 951                     } else {
 952                         return inserter(t1,o1,t2,o2) &&
 953                                   unify(arg(t1),o1,aVar,
 954                                      remover(extText(h1),t2,o2));
 955                     }
 956                 } else {
 957                     unifyFails = "rows are not compatible";
 958                     return FALSE;
 959                 }
 960             }
 961 #endif
 962             if (nonNull(h1) && h1==h2) {/* Assuming well-formed types, both*/
 963                 if (a1!=a2) {           /* t1, t2 must have same no of args*/
 964                     unifyFails = "incompatible constructors";
 965                     return FALSE;
 966                 }
 967                 while (isAp(t1)) {
 968                     if (!unify(arg(t1),o1,arg(t2),o2))
 969                         return FALSE;
 970                     t1 = fun(t1);
 971                     deRef(tyv1,t1,o1);
 972                     t2 = fun(t2);
 973                     deRef(tyv2,t2,o2);
 974                 }
 975                 unifyFails = 0;
 976                 return TRUE;
 977             }
 978
 979             /* Types do not match -- look for type synonyms to expand */
 980
 981             if (isSynonym(h1) && a1>=tycon(h1).arity) {
 982                 expandSyn(h1,a1,&t1,&o1);
 983                 deRef(tyv1,t1,o1);
 984                 goto un;
 985             }
 986             if (isSynonym(h2) && a2>=tycon(h2).arity) {
 987                 expandSyn(h2,a2,&t2,&o2);
 988                 deRef(tyv2,t2,o2);
 989                 goto un;
 990             }
 991
 992             if ((isNull(h1) && a1<=a2) ||       /* last attempt -- maybe   */
 993                 (isNull(h2) && a2<=a1)) {       /* one head is a variable? */
 994                 for (;;) {
 995                     deRef(tyv1,t1,o1);
 996                     deRef(tyv2,t2,o2);
 997
 998                     if (tyv1) {                         /* unify heads!    */
 999                         if (tyv2)
1000                             return varToVarBind(tyv1,tyv2);
1001                         else
1002                             return varToTypeBind(tyv1,t2,o2);
1003                     }
1004                     else if (tyv2)
1005                         return varToTypeBind(tyv2,t1,o1);
1006
1007                     /* at this point, neither t1 nor t2 is a variable. In  */
1008                     /* addition, they must both be APs unless one of the   */
1009                     /* head variables has been bound during unification of */
1010                     /* the arguments.                                      */
1011
1012                     if (!isAp(t1) || !isAp(t2)) {       /* might not be APs*/
1013                         unifyFails = 0;
1014                         return t1==t2;
1015                     }
1016                     if (!unify(arg(t1),o1,arg(t2),o2))  /* o/w must be APs */
1017                         return FALSE;
1018                     t1 = fun(t1);
1019                     t2 = fun(t2);
1020                 }
1021             }
1022         }
1023     unifyFails = 0;
1024     return FALSE;
1025 }
1026
1027 #if TREX
1028 static Bool local inserter(r1,o1,r,o)   /* Insert first field in (r1,o1)   */
1029 Type r1;                                /* into row (r,o), both of which   */
1030 Int  o1;                                /* are known to begin with an EXT  */
1031 Type r;
1032 Int  o; {
1033     Text labt = extText(fun(fun(r1)));  /* Find the text of the label      */
1034 #ifdef DEBUG_TYPES
1035     Printf("inserting ");
1036     printType(stdout,debugType(r1,o1));
1037     Printf(" into ");
1038     printType(stdout,debugType(r,o));
1039     Putchar('\n');
1040 #endif
1041     for (;;) {
1042         Tyvar *tyv;
1043         deRef(tyv,r,o);
1044         if (tyv) {
1045             Int beta;                   /* Test for common tail            */
1046             if (tailVar(arg(r1),o1)==tyvNum(tyv)) {
1047                 unifyFails = "distinct rows have common tail";
1048                 return FALSE;
1049             }
1050             beta = newTyvars(1);        /* Extend row with new field       */
1051             tyvar(beta)->kind = ROW;
1052             return varToTypeBind(tyv,ap(fun(r1),mkInt(beta)),o1);
1053         }
1054         else if (isAp(r) && isAp(fun(r)) && isExt(fun(fun(r)))) {
1055             if (labt==extText(fun(fun(r))))/* Compare existing fields      */
1056                 return unify(arg(fun(r1)),o1,extField(r),o);
1057             r = extRow(r);              /* Or skip to next field           */
1058         }
1059         else {                          /* Nothing else will match         */
1060             unifyFails = "field mismatch";
1061             return FALSE;
1062         }
1063     }
1064 }
1065
1066 static Int local remover(l,r,o)         /* Make a new row by copying (r,o) */
1067 Text l;                                 /* but removing the l field (which */
1068 Type r;                                 /* MUST exist)                     */
1069 Int  o; {
1070     Tyvar *tyv;
1071     Int    beta       = newTyvars(1);
1072     tyvar(beta)->kind = ROW;
1073 #ifdef DEBUG_TYPES
1074     Printf("removing %s from",textToStr(l));
1075     printType(stdout,debugType(r,o));
1076     Putchar('\n');
1077 #endif
1078     deRef(tyv,r,o);
1079     if (tyv || !isAp(r) || !isAp(fun(r)) || !isExt(fun(fun(r))))
1080         internal("remover");
1081     if (l==extText(fun(fun(r))))
1082         r = extRow(r);
1083     else
1084         r = ap(fun(r),mkInt(remover(l,extRow(r),o)));
1085     bindTv(beta,r,o);
1086     return beta;
1087 }
1088
1089
1090 static Int local tailVar(r,o)           /* Find var at tail end of a row   */
1091 Type r;
1092 Int  o; {
1093     for (;;) {
1094         Tyvar *tyv;
1095         deRef(tyv,r,o);
1096         if (tyv) {
1097             return tyvNum(tyv);
1098         }
1099         else if (isAp(r) && isAp(fun(r)) && isExt(fun(fun(r)))) {
1100             r = extRow(r);
1101         }
1102         else {
1103             return (-1);
1104         }
1105     }
1106 }
1107 #endif
1108
1109
1110 Bool typeMatches(type,mt)               /* test if type matches monotype mt*/
1111     Type type, mt; {                    /* imported from STG Hugs          */
1112     Bool result;
1113     if (isPolyType(type) || whatIs(type)==QUAL)
1114         return FALSE;
1115     emptySubstitution();
1116     noBind();
1117     result = unify(mt,0,type,0);
1118     unrestrictBind();
1119     emptySubstitution();
1120     return result;
1121 }
1122
1123
1124 #if IO_MONAD
1125 Bool isProgType(ks,type)                /* Test if type is of the form     */
1126 List ks;                                /* IO t for some t.                */
1127 Type type; {
1128     Bool result;
1129     Int  alpha;
1130     Int  beta;
1131     if (isPolyType(type) || whatIs(type)==QUAL)
1132         return FALSE;
1133     emptySubstitution();
1134     alpha  = newKindedVars(ks);
1135     beta   = newTyvars(1);
1136     bindOnlyAbove(beta);
1137     result = unify(type,alpha,typeProgIO,beta);
1138     unrestrictBind();
1139     emptySubstitution();
1140     return result;
1141 }
1142 #endif
1143
1144 /* --------------------------------------------------------------------------
1145  * Matching predicates:
1146  *
1147  * There are (at least) four situations where we need to match up pairs
1148  * of predicates:
1149  *
1150  *   1) Testing to see if two predicates are the same (ignoring differences
1151  *      caused by the use of type synonyms, for example).
1152  *
1153  *   2) Matching a predicate with the head of its class so that we can
1154  *      find the corresponding superclass predicates.  If the predicates
1155  *      have already been kind-checked, and the classes are known to be
1156  *      the same, then this should never fail.
1157  *
1158  *   3) Matching a predicate against the head of an instance to see if
1159  *      that instance is applicable.
1160  *
1161  *   4) Matching two instance heads to see if there is an overlap.
1162  *
1163  * For (1), we need a matching process that does not bind any variables.
1164  * For (2) and (3), we need to use one-way matching, only allowing
1165  * variables in the class or instance head to be instantiated.  For
1166  * (4), we need two-way unification.
1167  *
1168  * Another situation in which both one-way and two-way unification might
1169  * be used is in an implementation of improvement.  Here, a one-way match
1170  * would be used to determine applicability of a rule for improvement
1171  * that would then be followed by unification with another predicate.
1172  * One possible syntax for this might be:
1173  *
1174  *     instance P => pi [improves pi'] where ...
1175  *
1176  * The intention here is that any predicate matching pi' can be unified
1177  * with pi to get more accurate types.  A simple example of this is:
1178  *
1179  *   instance Collection [a] a improves Collection [a] b where ...
1180  *
1181  * As soon as we know what the collection type is (in this case, a list),
1182  * we will also know what the element type is.  To ensure that the rule
1183  * for improvement is valid, the compilation system will also need to use
1184  * a one-way matching process to ensure that pi is a (substitution) instance
1185  * of pi'.  Another extension would be to allow more than one predicate pi'
1186  * in an improving rule.  Read the paper on simplification and improvement
1187  * for technical background.  Watch this space for implementation news!
1188  * ------------------------------------------------------------------------*/
1189
1190 Bool samePred(pi1,o1,pi,o)              /* Test to see if predicates are   */
1191 Cell pi1;                               /* the same, with no binding of    */
1192 Int  o1;                                /* the variables in either one.    */
1193 Cell pi;                                /* Assumes preds are kind correct  */
1194 Int  o; {                               /* with the same class.            */
1195     Bool result;
1196     noBind();
1197     result = unifyPred(pi1,o1,pi,o);
1198     unrestrictBind();
1199     return result;
1200 }
1201
1202 Bool matchPred(pi1,o1,pi,o)             /* One way match predicate (pi1,o1)*/
1203 Cell pi1;                               /* against (pi,o), allowing only   */
1204 Int  o1;                                /* vars in 2nd pred to be bound.   */
1205 Cell pi;                                /* Assumes preds are kind correct  */
1206 Int  o; {                               /* with the same class and that no */
1207     Bool result;                        /* vars have been alloc'd since o. */
1208     bindOnlyAbove(o);
1209     result = unifyPred(pi1,o1,pi,o);
1210     unrestrictBind();
1211     return result;
1212 }
1213
1214 Bool unifyPred(pi1,o1,pi,o)             /* Unify two predicates            */
1215 Cell pi1;                               /* Assumes preds are kind correct  */
1216 Int  o1;                                /* with the same class.            */
1217 Cell pi;
1218 Int  o; {
1219     for (; isAp(pi1); pi1=fun(pi1), pi=fun(pi))
1220         if (!unify(arg(pi1),o1,arg(pi),o))
1221             return FALSE;
1222     return pi1==pi;
1223 }
1224
1225 #if TREX
1226 static Cell trexShow = NIL;             /* Used to test for show on records*/
1227 static Cell trexEq   = NIL;             /* Used to test for eq on records  */
1228 #endif
1229
1230 Inst findInstFor(pi,o)                  /* Find matching instance for pred */
1231 Cell  pi;                               /* (pi,o), or otherwise NIL.  If a */
1232 Int   o; {                              /* match is found, then tyvars from*/
1233     Class c = getHead(pi);              /* typeOff have been initialized to*/
1234     List  ins;                          /* allow direct use of specifics.  */
1235
1236     if (!isClass(c))
1237         return NIL;
1238
1239     for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins)) {
1240         Inst in   = hd(ins);
1241         Int  beta = newKindedVars(inst(in).kinds);
1242         if (matchPred(pi,o,inst(in).head,beta)) {
1243             typeOff = beta;
1244             return in;
1245         }
1246         else
1247             numTyvars = beta;
1248     }
1249     unrestrictBind();
1250
1251 #if TREX
1252     {   Bool wantShow   = (c==findQualClass(trexShow));
1253         Bool wantEither = wantShow || (c==findQualClass(trexEq));
1254
1255         if (wantEither) {                       /* Generate instances of   */
1256             Type  t = arg(pi);                  /* ShowRecRow and EqRecRow */
1257             Tyvar *tyv;                         /* on the fly              */
1258             Cell  e;
1259             deRef(tyv,t,o);
1260             e = getHead(t);
1261             if (isExt(e)) {
1262                 Inst in = NIL;
1263                 for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins))
1264                     if (getHead(arg(inst(hd(ins)).head))==e) {
1265                         in = hd(ins);
1266                         break;
1267                     }
1268                 if (isNull(in))
1269                     in = (wantShow ? addRecShowInst(c,e) : addRecEqInst(c,e));
1270                 typeOff = newKindedVars(extKind);
1271                 bindTv(typeOff,arg(fun(t)),o);
1272                 bindTv(typeOff+1,arg(t),o);
1273                 return in;
1274             }
1275         }
1276     }
1277 #endif
1278
1279     return NIL;
1280 }
1281
1282 /* --------------------------------------------------------------------------
1283  * Compare type schemes:
1284  * ------------------------------------------------------------------------*/
1285
1286 Bool sameSchemes(s,s1)                  /* Test to see whether two type    */
1287 Type s;                                 /* schemes are the same            */
1288 Type s1; {
1289     Int  o   = 0;
1290     Int  m   = 0;
1291     Int  nr2 = 0;
1292     Bool b   = isPolyType(s);           /* Check quantifiers are the same  */
1293     Bool b1  = isPolyType(s1);
1294     if (b || b1) {
1295         if (b && b1 && eqKind(polySigOf(s),polySigOf(s1))) {
1296             Kind k = polySigOf(s);
1297             s      = monotypeOf(s);
1298             s1     = monotypeOf(s1);
1299             o      = newKindedVars(k);
1300             for (; isAp(k); k=arg(k))
1301                 m++;
1302         }
1303         else
1304             return FALSE;
1305     }
1306
1307     b  = (whatIs(s)==QUAL);             /* Check that contexts are the same*/
1308     b1 = (whatIs(s1)==QUAL);
1309     if (b || b1) {
1310         if (b && b1) {
1311             List ps  = fst(snd(s));
1312             List ps1 = fst(snd(s1));
1313             noBind();
1314             while (nonNull(ps) && nonNull(ps1)) {
1315                 Cell pi  = hd(ps);
1316                 Cell pi1 = hd(ps1);
1317                 if (getHead(pi)!=getHead(pi1)
1318                         || !unifyPred(pi,o,pi1,o))
1319                     break;
1320                 ps  = tl(ps);
1321                 ps1 = tl(ps1);
1322             }
1323             unrestrictBind();
1324             if (nonNull(ps) || nonNull(ps1))
1325                 return FALSE;
1326             s  = snd(snd(s));
1327             s1 = snd(snd(s1));
1328         }
1329         else
1330             return FALSE;
1331     }
1332
1333     b  = (whatIs(s)==RANK2);            /* Check any rank 2 annotations    */
1334     b1 = (whatIs(s1)==RANK2);
1335     if (b || b1) {
1336         if (b && b1 && intOf(fst(snd(s)))==intOf(fst(snd(s1)))) {
1337             nr2 = intOf(fst(snd(s)));
1338             s   = snd(snd(s));
1339             s1  = snd(snd(s1));
1340         }
1341         else
1342             return FALSE;
1343     }
1344
1345     for (; nr2>0; nr2--) {              /* Deal with rank 2 arguments      */
1346         Type t  = arg(fun(s));
1347         Type t1 = arg(fun(s1));
1348         b       = isPolyType(t);
1349         b1      = isPolyType(t1);
1350         if (b || b1) {
1351             if (b && b1) {
1352                 t  = dropRank1(t,o,m);
1353                 t1 = dropRank1(t1,o,m);
1354                 if (!sameSchemes(t,t1))
1355                     return FALSE;
1356             }
1357             else
1358                 return FALSE;
1359         }
1360         else {
1361             noBind();
1362             b = unify(t,o,t1,o);
1363             unrestrictBind();
1364             if (!b)
1365                 return FALSE;
1366         }
1367         s  = arg(s);
1368         s1 = arg(s1);
1369     }
1370
1371     noBind();                           /* Ensure body types are the same  */
1372     b = unify(s,o,s1,o);
1373     unrestrictBind();
1374     return b;
1375 }
1376
1377 /* --------------------------------------------------------------------------
1378  * Unify kind expressions:
1379  * ------------------------------------------------------------------------*/
1380
1381 static Bool local kvarToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2     */
1382 Tyvar *tyv1, *tyv2; {                     /* for kind variable bindings    */
1383     if (tyv1!=tyv2) {
1384         tyv1->bound = aVar;
1385         tyv1->offs  = tyvNum(tyv2);
1386 #ifdef DEBUG_KINDS
1387         Printf("vv binding kvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
1388 #endif
1389     }
1390     return TRUE;
1391 }
1392
1393 static Bool local kvarToTypeBind(tyv,t,o)/* Make binding tyv := (t,o)      */
1394 Tyvar *tyv;                             /* for kind variable bindings      */
1395 Type  t;                                /* guaranteed not to be a v'ble or */
1396 Int   o; {                              /* have synonym as outermost constr*/
1397     if (doesntOccurIn(tyv,t,o)) {
1398         tyv->bound = t;
1399         tyv->offs  = o;
1400 #ifdef DEBUG_KINDS
1401         Printf("vt binding kind variable: _%d to ",tyvNum(tyv));
1402         printType(stdout,debugType(t,o));
1403         Putchar('\n');
1404 #endif
1405         return TRUE;
1406     }
1407     unifyFails = "unification would give infinite kind";
1408     return FALSE;
1409 }
1410
1411 Bool kunify(k1,o1,k2,o2)                /* Unify kind expr (k1,o1) with    */
1412 Kind k1,k2;                             /* (k2,o2)                         */
1413 Int  o1,o2; {
1414     Tyvar *kyv1, *kyv2;
1415
1416     deRef(kyv1,k1,o1);
1417     deRef(kyv2,k2,o2);
1418
1419     if (kyv1) {
1420         if (kyv2)
1421             return kvarToVarBind(kyv1,kyv2);        /* k1, k2 variables    */
1422         else
1423             return kvarToTypeBind(kyv1,k2,o2);      /* k1 variable, k2 not */
1424     }
1425     else
1426         if (kyv2)
1427             return kvarToTypeBind(kyv2,k1,o1);      /* k2 variable, k1 not */
1428         else {
1429 #ifdef DEBUG_KINDS
1430             Printf("unifying kinds: ");
1431             printType(stdout,debugType(k1,o1));
1432             Printf(" with ");
1433             printType(stdout,debugType(k2,o2));
1434             Putchar('\n');
1435 #endif
1436             if (k1==STAR && k2==STAR)               /* k1, k2 not vars     */
1437                 return TRUE;
1438 #if TREX
1439             else if (k1==ROW && k2==ROW)
1440                 return TRUE;
1441 #endif
1442             else if (isAp(k1) && isAp(k2))
1443                 return kunify(fst(k1),o1,fst(k2),o2) &&
1444                        kunify(snd(k1),o1,snd(k2),o2);
1445         }
1446     unifyFails = 0;
1447     return FALSE;
1448 }
1449
1450 /* --------------------------------------------------------------------------
1451  * Tuple type constructors: are generated as necessary.  The most common
1452  * n-tuple constructors (n<MAXTUPCON) are held in a cache to avoid
1453  * repeated generation of the constructor types.
1454  * ------------------------------------------------------------------------*/
1455
1456 #define MAXTUPCON 10
1457 static Type tupleConTypes[MAXTUPCON];
1458
1459 Void typeTuple(e)                      /* find type for tuple constr, using*/
1460 Cell e; {                              /* tupleConTypes to cache previously*/
1461     Int n   = tupleOf(e);              /* calculated tuple constr. types.  */
1462     typeOff = newTyvars(n);
1463     if (n>=MAXTUPCON)
1464          typeIs = makeTupleType(n);
1465     else if (tupleConTypes[n])
1466          typeIs = tupleConTypes[n];
1467     else
1468          typeIs = tupleConTypes[n] = makeTupleType(n);
1469 }
1470
1471 static Type local makeTupleType(n)     /* construct type for tuple constr. */
1472 Int n; {                               /* t1 -> ... -> tn -> (t1,...,tn)   */
1473     Type h = mkTuple(n);
1474     Int  i;
1475
1476     for (i=0; i<n; ++i)
1477         h = ap(h,mkOffset(i));
1478     while (0<n--)
1479         h = fn(mkOffset(n),h);
1480     return h;
1481 }
1482
1483 /* --------------------------------------------------------------------------
1484  * Two forms of kind expression are used quite frequently:
1485  *      *  -> *  -> ... -> *  -> *      for kinds of ->, [], ->, (,) etc...
1486  *      v1 -> v2 -> ... -> vn -> vn+1   skeletons for constructor kinds
1487  * Expressions of these forms are produced by the following functions which
1488  * use a cache to avoid repeated construction of commonly used values.
1489  * A similar approach is used to store the types of tuple constructors in the
1490  * main type checker.
1491  * ------------------------------------------------------------------------*/
1492
1493 #define MAXKINDFUN 10
1494 static  Kind simpleKindCache[MAXKINDFUN];
1495 static  Kind varKindCache[MAXKINDFUN];
1496
1497 static Kind local makeSimpleKind(n)     /* construct * -> ... -> * (n args)*/
1498 Int n; {
1499     Kind k = STAR;
1500     while (n-- > 0)
1501         k = ap(STAR,k);
1502     return k;
1503 }
1504
1505 Kind simpleKind(n)                      /* return (possibly cached) simple */
1506 Int n; {                                /* function kind                   */
1507     if (n>=MAXKINDFUN)
1508         return makeSimpleKind(n);
1509     else if (nonNull(simpleKindCache[n]))
1510         return simpleKindCache[n];
1511     else if (n==0)
1512         return simpleKindCache[0] = STAR;
1513     else
1514         return simpleKindCache[n] = ap(STAR,simpleKind(n-1));
1515 }
1516
1517 static Kind local makeVarKind(n)        /* construct v0 -> .. -> vn        */
1518 Int n; {
1519     Kind k = mkOffset(n);
1520     while (n-- > 0)
1521         k = ap(mkOffset(n),k);
1522     return k;
1523 }
1524
1525 Void varKind(n)                         /* return (possibly cached) var    */
1526 Int n; {                                /* function kind                   */
1527     typeOff = newKindvars(n+1);
1528     if (n>=MAXKINDFUN)
1529         typeIs = makeVarKind(n);
1530     else if (nonNull(varKindCache[n]))
1531         typeIs = varKindCache[n];
1532     else
1533         typeIs = varKindCache[n] = makeVarKind(n);
1534 }
1535
1536 /* --------------------------------------------------------------------------
1537  * Substitutution control:
1538  * ------------------------------------------------------------------------*/
1539
1540 Void substitution(what)
1541 Int what; {
1542     Int  i;
1543
1544     switch (what) {
1545         case RESET   : emptySubstitution();
1546                        unrestrictBind();
1547                        btyvars = NIL;
1548                        break;
1549
1550         case MARK    : for (i=0; i<MAXTUPCON; ++i)
1551                            mark(tupleConTypes[i]);
1552                        for (i=0; i<MAXKINDFUN; ++i) {
1553                            mark(simpleKindCache[i]);
1554                            mark(varKindCache[i]);
1555                        }
1556                        for (i=0; i<numTyvars; ++i)
1557                            mark(tyvars[i].bound);
1558                        mark(btyvars);
1559                        mark(typeIs);
1560                        mark(predsAre);
1561                        mark(genericVars);
1562 #if TREX
1563                        mark(trexShow);
1564                        mark(trexEq);
1565 #endif
1566                        break;
1567
1568         case INSTALL : substitution(RESET);
1569                        for (i=0; i<MAXTUPCON; ++i)
1570                            tupleConTypes[i] = NIL;
1571                        for (i=0; i<MAXKINDFUN; ++i) {
1572                            simpleKindCache[i] = NIL;
1573                            varKindCache[i]    = NIL;
1574                        }
1575 #if TREX
1576                        trexShow = mkQCon(findText("Trex"),
1577                                          findText("ShowRecRow"));
1578                        trexEq   = mkQCon(findText("Trex"),
1579                                          findText("EqRecRow"));
1580 #endif
1581                        break;
1582     }
1583 }
1584
1585 /*-------------------------------------------------------------------------*/