[project @ 2000-12-14 14:19:56 by sewardj]
[ghc-hetmet.git] / ghc / interpreter / subst.c
index 955eabb..812a31c 100644 (file)
@@ -1,19 +1,24 @@
-/* -*- mode: hugs-c; -*- */
+
 /* --------------------------------------------------------------------------
- * subst.c:     Copyright (c) Mark P Jones 1991-1998.   All rights reserved.
- *              See NOTICE for details and conditions of use etc...
- *              Hugs version 1.3c, March 1998
- *
  * Provides an implementation for the `current substitution' used during
  * type and kind inference in both static analysis and type checking.
+ *
+ * The Hugs 98 system is Copyright (c) Mark P Jones, Alastair Reid, the
+ * Yale Haskell Group, and the Oregon Graduate Institute of Science and
+ * Technology, 1994-1999, All rights reserved.  It is distributed as
+ * free software under the license in the file "License", which is
+ * included in the distribution.
+ *
+ * $RCSfile: subst.c,v $
+ * $Revision: 1.17 $
+ * $Date: 2000/03/23 14:54:21 $
  * ------------------------------------------------------------------------*/
 
-#include "prelude.h"
+#include "hugsbasictypes.h"
 #include "storage.h"
 #include "connect.h"
 #include "errors.h"
-#include "link.h"
-#include "subst.h"
+
 
 /*#define DEBUG_TYPES*/
 
@@ -21,11 +26,7 @@ static Int numTyvars;                   /* no. type vars currently in use  */
 static Int maxTyvars = 0;
 static Int nextGeneric;                 /* number of generics found so far */
 
-#if    FIXED_SUBST
-Tyvar  tyvars[NUM_TYVARS];              /* storage for type variables      */
-#else
 Tyvar  *tyvars = 0;                     /* storage for type variables      */
-#endif
 Int    typeOff;                         /* offset of result type           */
 Type   typeIs;                          /* skeleton of result type         */
 Int    typeFree;                        /* freedom in instantiated type    */
@@ -37,23 +38,38 @@ List   btyvars = NIL;                   /* explicitly scoped type vars     */
  * local function prototypes:
  * ------------------------------------------------------------------------*/
 
-static Void local expandSubst           Args((Int));
-static Int  local findBtyvsInt          Args((Text));
-static Type local makeTupleType         Args((Int));
-static Kind local makeSimpleKind        Args((Int));
-static Kind local makeVarKind           Args((Int));
-static Void local expandSyn1            Args((Tycon, Type *, Int *));
-static Type local dropRank1Body         Args((Type,Int,Int));
-static Type local liftRank1Body         Args((Type,Int));
-
-static Bool local varToVarBind          Args((Tyvar *,Tyvar *));
-static Bool local varToTypeBind         Args((Tyvar *,Type,Int));
+static Void local expandSubst           ( Int );
+static Int  local findBtyvsInt          ( Text );
+static Type local makeTupleType         ( Int );
+static Kind local makeSimpleKind        ( Int );
+static Kind local makeVarKind           ( Int );
+static Void local expandSyn1            ( Tycon, Type *, Int * );
+static List local listTyvar            ( Int,List );
+static List local listTyvars           ( Type,Int,List );
+static Cell local dupTyvar             ( Int,List );
+static Cell local dupTyvars            ( Cell,Int,List );
+static Pair local copyNoMark           ( Cell,Int );
+static Type local dropRank1Body         ( Type,Int,Int );
+static Type local liftRank1Body         ( Type,Int );
+static Bool local matchTypeAbove       ( Type,Int,Type,Int,Int );
+
+static Bool local varToVarBind          ( Tyvar *,Tyvar * );
+static Bool local varToTypeBind         ( Tyvar *,Type,Int );
 #if TREX
-static Bool local inserter              Args((Type,Int,Type,Int));
-static Int  local remover               Args((Text,Type,Int));
+static Bool local inserter              ( Type,Int,Type,Int );
+static Int  local remover               ( Text,Type,Int );
+static Int  local tailVar               ( Type,Int );
 #endif
-static Bool local kvarToVarBind         Args((Tyvar *,Tyvar *));
-static Bool local kvarToTypeBind        Args((Tyvar *,Type,Int));
+
+static Bool local improveAgainst       ( Int,List,Cell,Int );
+static Bool local instImprove          ( Int,Class,Cell,Int );
+static Bool local pairImprove          ( Int,Class,Cell,Int,Cell,Int,Int );
+#if IPARAM
+static Bool local ipImprove            ( Int,Cell,Int,Cell,Int );
+#endif
+
+static Bool local kvarToVarBind         ( Tyvar *,Tyvar * );
+static Bool local kvarToTypeBind        ( Tyvar *,Type,Int );
 
 /* --------------------------------------------------------------------------
  * The substitution, types, and kinds:
@@ -96,7 +112,6 @@ static Bool local kvarToTypeBind        Args((Tyvar *,Type,Int));
 
 Void emptySubstitution() {              /* clear current substitution      */
     numTyvars   = 0;
-#if !FIXED_SUBST
     if (maxTyvars!=NUM_TYVARS) {
         maxTyvars = 0;
         if (tyvars) {
@@ -104,7 +119,6 @@ Void emptySubstitution() {              /* clear current substitution      */
             tyvars = 0;
         }
     }
-#endif
     nextGeneric = 0;
     genericVars = NIL;
     typeIs      = NIL;
@@ -114,12 +128,6 @@ Void emptySubstitution() {              /* clear current substitution      */
 
 static Void local expandSubst(n)        /* add further n type variables to */
 Int n; {                                /* current substituion             */
-#if FIXED_SUBST
-    if (numTyvars+n>NUM_TYVARS) {
-        ERRMSG(0) "Too many type variables in type checker"
-        EEND;
-    }
-#else
     if (numTyvars+n>maxTyvars) {        /* need to expand substitution     */
         Int   newMax = maxTyvars+NUM_TYVARS;
         Tyvar *newTvs;
@@ -153,7 +161,6 @@ Int n; {                                /* current substituion             */
         tyvars    = newTvs;
         maxTyvars = newMax;
     }
-#endif
 }
 
 Int newTyvars(n)                        /* allocate new type variables     */
@@ -166,9 +173,9 @@ Int n; {                                /* all of kind STAR                */
         tyvars[numTyvars-n].bound = NIL;
         tyvars[numTyvars-n].kind  = STAR;
 #ifdef DEBUG_TYPES
-        printf("new type variable: _%d ::: ",numTyvars-n);
+        Printf("new type variable: _%d ::: ",numTyvars-n);
         printKind(stdout,tyvars[numTyvars-n].kind);
-        putchar('\n');
+        Putchar('\n');
 #endif
     }
     return beta;
@@ -183,9 +190,9 @@ Kind k; {                               /* specified kinds                 */
         tyvars[numTyvars].bound = NIL;
         tyvars[numTyvars].kind  = fst(k);
 #ifdef DEBUG_TYPES
-        printf("new type variable: _%d ::: ",numTyvars);
+        Printf("new type variable: _%d ::: ",numTyvars);
         printKind(stdout,tyvars[numTyvars].kind);
-        putchar('\n');
+        Putchar('\n');
 #endif
         numTyvars++;
     }
@@ -208,7 +215,7 @@ Type type; {
                 typeFree++;
         }
 
-        if (whatIs(typeIs)==QUAL) {    /* Qualified type?                  */
+       if (isQualType(typeIs)) {    /* Qualified type?                    */
             predsAre = fst(snd(typeIs));
             typeIs   = snd(snd(typeIs));
         }
@@ -317,9 +324,9 @@ Int  o; {
     tyv->bound = t;
     tyv->offs  = o;
 #ifdef DEBUG_TYPES
-    printf("binding type variable: _%d to ",vn);
+    Printf("binding type variable: _%d to ",vn);
     printType(stdout,debugType(t,o));
-    putchar('\n');
+    Putchar('\n');
 #endif
 }
 
@@ -396,7 +403,7 @@ Int   *ao; {                            /* expansion returned in (*at,*ao) */
  * Marking fixed variables in type expressions:
  * ------------------------------------------------------------------------*/
 
-Void clearMarks() {                     /* set all unbound type vars to    */
+Void clearMarks() {                     /* Set all unbound type vars to    */
     Int i;                              /* unused generic variables        */
     for (i=0; i<numTyvars; ++i)
         if (!isBound(tyvar(i)))
@@ -405,6 +412,15 @@ Void clearMarks() {                     /* set all unbound type vars to    */
     nextGeneric = 0;
 }
 
+Void markAllVars() {                    /* Set all unbound type vars to    */
+    Int i;                              /* be fixed vars                   */
+    for (i=0; i<numTyvars; ++i)
+        if (!isBound(tyvar(i)))
+            tyvar(i)->offs = FIXED_TYVAR;
+    genericVars = NIL;
+    nextGeneric = 0;
+}
+
 Void resetGenerics() {                  /* Reset all generic vars to unused*/
     Int i;
     for (i=0; i<numTyvars; ++i)
@@ -427,9 +443,12 @@ Int vn; {                               /* given type variable             */
 Void markType(t,o)                      /* mark fixed vars in type (t,o)   */
 Type t;
 Int  o; {
+    STACK_CHECK
     switch (whatIs(t)) {
+        case POLYTYPE  :
+        case QUAL      :
 #if TREX
-        case EXT       :st
+        case EXT       :
 #endif
         case TYCON     :
         case TUPLE     : return;
@@ -450,8 +469,6 @@ Int  o; {
 
         case RANK2     : markType(snd(snd(t)),o);
                          return;
-        case POLYTYPE  : /* No need to mark generic types */
-                         return;
 
         default        : internal("markType");
     }
@@ -474,14 +491,17 @@ Type copyTyvar(vn)                      /* calculate most general form of  */
 Int vn; {                               /* type bound to given type var    */
     Tyvar *tyv = tyvar(vn);
 
-    if (isBound(tyv))
+    if ((tyv->bound)==SKOLEM) {
+        return mkInt(vn);
+    } else if (tyv->bound) {
         return copyType(tyv->bound,tyv->offs);
+    }
 
     switch (tyv->offs) {
         case FIXED_TYVAR    : return mkInt(vn);
 
         case UNUSED_GENERIC : (tyv->offs) = GENERIC + nextGeneric++;
-                              if (nextGeneric>=NUM_OFFSETS) {
+                              if (nextGeneric>=(OFF_MAX-OFF_MIN+1)) {
                                   ERRMSG(0)
                                       "Too many quantified type variables"
                                   EEND;
@@ -495,6 +515,7 @@ Int vn; {                               /* type bound to given type var    */
 Type copyType(t,o)                      /* calculate most general form of  */
 Type t;                                 /* type expression (t,o)           */
 Int  o; {
+    STACK_CHECK
     switch (whatIs(t)) {
         case AP        : {   Type l = copyType(fst(t),o);/* ensure correct */
                              Type r = copyType(snd(t),o);/* eval. order    */
@@ -520,6 +541,32 @@ Int  o; {
         return pi;
 }
 
+Type zonkTyvar(vn)     /* flatten type by chasing all references          */
+Int vn; {              /* and collapsing OFFSETS to absolute indexes      */
+    Tyvar *tyv = tyvar(vn);
+
+    if (tyv->bound)
+       return zonkType(tyv->bound,tyv->offs);
+    else
+       return mkInt(vn);
+}
+
+Type zonkType(t,o)     /* flatten type by chasing all references          */
+Type t;                        /* and collapsing OFFSETS to absolute indexes      */
+Int  o; {
+    STACK_CHECK
+    switch (whatIs(t)) {
+       case AP        : {   Type l = zonkType(fst(t),o);/* ensure correct */
+                            Type r = zonkType(snd(t),o);/* eval. order    */
+                            return ap(l,r);
+                        }
+       case OFFSET    : return zonkTyvar(o+offsetOf(t));
+       case INTCELL   : return zonkTyvar(intOf(t));
+    }
+
+    return t;
+}
+
 #ifdef DEBUG_TYPES
 Type debugTyvar(vn)                     /* expand type structure in full   */
 Int vn; {                               /* detail                          */
@@ -533,6 +580,7 @@ Int vn; {                               /* detail                          */
 Type debugType(t,o)
 Type t;
 Int  o; {
+    STACK_CHECK
     switch (whatIs(t)) {
         case AP        : {   Type l = debugType(fst(t),o);
                              Type r = debugType(snd(t),o);
@@ -546,6 +594,25 @@ Int  o; {
 
     return t;
 }
+List debugContext(ps)
+List ps; {
+    Cell p;
+    List qs = NIL;
+    for (; nonNull(ps); ps=tl(ps)) {
+        p = debugPred(fst3(hd(ps)),intOf(snd3(hd(ps))));
+       qs = cons(p,qs);
+    }
+    return rev(qs);
+}
+
+Cell debugPred(pi,o)
+Cell pi;
+Int  o; {
+    if (isAp(pi)) {
+       return pair(debugPred(fun(pi),o),debugType(arg(pi),o));
+    }
+    return pi;
+}
 #endif /*DEBUG_TYPES*/
 
 Kind copyKindvar(vn)                    /* build kind attatched to variable*/
@@ -571,6 +638,80 @@ Int  o; {
 }
 
 /* --------------------------------------------------------------------------
+ * Copy type expression from substitution without marking:
+ * ------------------------------------------------------------------------*/
+
+static List local listTyvar(vn,ns)
+Int  vn;
+List ns; {
+    Tyvar *tyv = tyvar(vn);
+
+    if (isBound(tyv)) {
+       return listTyvars(tyv->bound,tyv->offs,ns);
+    } else if (!intIsMember(vn,ns)) {
+       ns = cons(mkInt(vn),ns);
+    }
+    return ns;
+}
+
+static List local listTyvars(t,o,ns)
+Cell t;
+Int  o;
+List ns; {
+    switch (whatIs(t)) {
+       case AP        : return listTyvars(fst(t),o,
+                                listTyvars(snd(t),o,
+                                 ns));
+       case OFFSET    : return listTyvar(o+offsetOf(t),ns);
+       case INTCELL   : return listTyvar(intOf(t),ns);
+       default        : break;
+    }
+    return ns;
+}
+
+static Cell local dupTyvar(vn,ns)
+Int  vn;
+List ns; {
+    Tyvar *tyv = tyvar(vn);
+
+    if (isBound(tyv)) {
+       return dupTyvars(tyv->bound,tyv->offs,ns);
+    } else {
+       Int i = 0;
+       for (; nonNull(ns) && vn!=intOf(hd(ns)); ns=tl(ns)) {
+           i++;
+       }
+       return mkOffset(i);
+    }
+}
+
+static Cell local dupTyvars(t,o,ns)
+Cell t;
+Int  o;
+List ns; {
+    switch (whatIs(t)) {
+       case AP        : {   Type l = dupTyvars(fst(t),o,ns);
+                            Type r = dupTyvars(snd(t),o,ns);
+                            return ap(l,r);
+                        }
+       case OFFSET    : return dupTyvar(o+offsetOf(t),ns);
+       case INTCELL   : return dupTyvar(intOf(t),ns);
+    }
+    return t;
+}
+
+static Cell local copyNoMark(t,o)      /* Copy a type or predicate without*/
+Cell t;                                        /* changing marks                  */
+Int  o; {
+    List ns     = listTyvars(t,o,NIL);
+    Cell result = pair(ns,dupTyvars(t,o,ns));
+    for (; nonNull(ns); ns=tl(ns)) {
+       hd(ns) = tyvar(intOf(hd(ns)))->kind;
+    }
+    return result;
+}
+
+/* --------------------------------------------------------------------------
  * Droping and lifting of type schemes that appear in rank 2 position:
  * ------------------------------------------------------------------------*/
 
@@ -586,7 +727,7 @@ Int  n; {
             Type a = arg(fun(t));
             if (isPolyType(a))
                 a = dropRank1(a,alpha,n);
-            as = ap2(typeArrow,a,as);
+            as = fn(a,as);
             t  = arg(t);
         }
         t = ap(RANK2,pair(r,revOnto(as,t)));
@@ -659,7 +800,7 @@ Int  m; {
         for (i=intOf(r); i>0; i--) {
             Type a = arg(fun(t));
             a      = isPolyType(a) ? liftRank1Body(a,m) : copyType(a,alpha);
-            as     = ap2(typeArrow,a,as);
+            as     = fn(a,as);
             t      = arg(t);
         }
         t = ap(RANK2,pair(r,revOnto(as,copyType(t,alpha))));
@@ -738,7 +879,7 @@ Int  o; {
 #endif
     }
 #ifdef DEBUG_KINDS
-    printf("getKind c = %d, whatIs=%d\n",c,whatIs(c));
+    Printf("getKind c = %d, whatIs=%d\n",c,whatIs(c));
 #endif
     internal("getKind");
     return STAR;/* not reached */
@@ -789,6 +930,7 @@ Type  t;
 Int   o; {
     Tyvar *tyv;
 
+    STACK_CHECK
     for (;;) {
         deRef(tyv,t,o);
         if (tyv)                        /* type variable                   */
@@ -842,7 +984,7 @@ Tyvar *tyv1, *tyv2; {
         tyv1->bound = aVar;
         tyv1->offs  = tyvNum(tyv2);
 #ifdef DEBUG_TYPES
-        printf("vv binding tyvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
+        Printf("vv binding tyvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
 #endif
     }
     return TRUE;
@@ -868,9 +1010,9 @@ Int   o; {                              /* have synonym as outermost constr*/
         tyv->bound = t;
         tyv->offs  = o;
 #ifdef DEBUG_TYPES
-        printf("vt binding type variable: _%d to ",tyvNum(tyv));
+        Printf("vt binding type variable: _%d to ",tyvNum(tyv));
         printType(stdout,debugType(t,o));
-        putchar('\n');
+        Putchar('\n');
 #endif
         return TRUE;
     }
@@ -882,10 +1024,11 @@ Type t1,t2;                             /* unify (t1,o1) with (t2,o2)      */
 Int  o1,o2; {
     Tyvar *tyv1, *tyv2;
 
+    STACK_CHECK
     deRef(tyv1,t1,o1);
     deRef(tyv2,t2,o2);
 
-un: if (tyv1)
+un: if (tyv1) {
         if (tyv2)
             return varToVarBind(tyv1,tyv2);         /* t1, t2 variables    */
         else {
@@ -897,6 +1040,7 @@ un: if (tyv1)
             }
             return varToTypeBind(tyv1,t2,o2);
         }
+    }
     else
         if (tyv2) {
             Cell h1 = getDerefHead(t1,o1);          /* t2 variable, t1 not */
@@ -914,23 +1058,27 @@ un: if (tyv1)
             Int  a2 = argCount;
 
 #ifdef DEBUG_TYPES
-            printf("tt unifying types: ");
+            Printf("tt unifying types: ");
             printType(stdout,debugType(t1,o1));
-            printf(" with ");
+            Printf(" with ");
             printType(stdout,debugType(t2,o2));
-            putchar('\n');
+            Putchar('\n');
 #endif
-
             if (isOffset(h1) || isInt(h1)) h1=NIL;  /* represent var by NIL*/
             if (isOffset(h2) || isInt(h2)) h2=NIL;
 
 #if TREX
             if (isExt(h1) || isExt(h2)) {
-                if (a1==2 && isExt(h1) && a2==2 && isExt(h2))
-                    return inserter(fun(t1),o1,t2,o2) &&
-                              unify(arg(t1),o1,aVar,
-                                 remover(extText(h1),t2,o2));
-                else {
+                if (a1==2 && isExt(h1) && a2==2 && isExt(h2)) {
+                    if (extText(h1)==extText(h2)) {
+                        return unify(arg(fun(t1)),o1,arg(fun(t2)),o2) &&
+                                unify(arg(t1),o1,arg(t2),o2);
+                    } else {
+                        return inserter(t1,o1,t2,o2) &&
+                                  unify(arg(t1),o1,aVar,
+                                     remover(extText(h1),t2,o2));
+                    }
+                } else {
                     unifyFails = "rows are not compatible";
                     return FALSE;
                 }
@@ -972,11 +1120,12 @@ un: if (tyv1)
                     deRef(tyv1,t1,o1);
                     deRef(tyv2,t2,o2);
 
-                    if (tyv1)                           /* unify heads!    */
+                    if (tyv1) {                         /* unify heads!    */
                         if (tyv2)
                             return varToVarBind(tyv1,tyv2);
                         else
                             return varToTypeBind(tyv1,t2,o2);
+                    }
                     else if (tyv2)
                         return varToTypeBind(tyv2,t1,o1);
 
@@ -1001,23 +1150,35 @@ un: if (tyv1)
 }
 
 #if TREX
-static Bool local inserter(ins,o,r,or)  /* Insert field into row (r,or)    */
-Type ins;                               /* inserter (ins,o), where ins is  */
-Int  o;                                 /* an applic of an EXT to a type.  */
+static Bool local inserter(r1,o1,r,o)   /* Insert first field in (r1,o1)   */
+Type r1;                                /* into row (r,o), both of which   */
+Int  o1;                                /* are known to begin with an EXT  */
 Type r;
-Int  or; {
-    Text labt = extText(fun(ins));      /* Find the text of the label      */
+Int  o; {
+    Text labt = extText(fun(fun(r1)));  /* Find the text of the label      */
+#ifdef DEBUG_TYPES
+    Printf("inserting ");
+    printType(stdout,debugType(r1,o1));
+    Printf(" into ");
+    printType(stdout,debugType(r,o));
+    Putchar('\n');
+#endif
     for (;;) {
         Tyvar *tyv;
-        deRef(tyv,r,or);
+        deRef(tyv,r,o);
         if (tyv) {
-            Int beta = newTyvars(1);    /* Extend row with new field       */
+            Int beta;                   /* Test for common tail            */
+            if (tailVar(arg(r1),o1)==tyvNum(tyv)) {
+                unifyFails = "distinct rows have common tail";
+                return FALSE;
+            }
+            beta = newTyvars(1);        /* Extend row with new field       */
             tyvar(beta)->kind = ROW;
-            return varToTypeBind(tyv,ap(ins,mkInt(beta)),o);
+            return varToTypeBind(tyv,ap(fun(r1),mkInt(beta)),o1);
         }
         else if (isAp(r) && isAp(fun(r)) && isExt(fun(fun(r)))) {
             if (labt==extText(fun(fun(r))))/* Compare existing fields      */
-                return unify(arg(ins),o,extField(r),or);
+                return unify(arg(fun(r1)),o1,extField(r),o);
             r = extRow(r);              /* Or skip to next field           */
         }
         else {                          /* Nothing else will match         */
@@ -1034,6 +1195,11 @@ Int  o; {
     Tyvar *tyv;
     Int    beta       = newTyvars(1);
     tyvar(beta)->kind = ROW;
+#ifdef DEBUG_TYPES
+    Printf("removing %s from",textToStr(l));
+    printType(stdout,debugType(r,o));
+    Putchar('\n');
+#endif
     deRef(tyv,r,o);
     if (tyv || !isAp(r) || !isAp(fun(r)) || !isExt(fun(fun(r))))
         internal("remover");
@@ -1044,12 +1210,32 @@ Int  o; {
     bindTv(beta,r,o);
     return beta;
 }
+
+
+static Int local tailVar(r,o)           /* Find var at tail end of a row   */
+Type r;
+Int  o; {
+    for (;;) {
+        Tyvar *tyv;
+        deRef(tyv,r,o);
+        if (tyv) {
+            return tyvNum(tyv);
+        }
+        else if (isAp(r) && isAp(fun(r)) && isExt(fun(fun(r)))) {
+            r = extRow(r);
+        }
+        else {
+            return (-1);
+        }
+    }
+}
 #endif
 
+
 Bool typeMatches(type,mt)               /* test if type matches monotype mt*/
-Type type, mt; {
+    Type type, mt; {                    /* imported from STG Hugs          */
     Bool result;
-    if (isPolyType(type) || whatIs(type)==QUAL)
+     if (isPolyOrQualType(type))
         return FALSE;
     emptySubstitution();
     noBind();
@@ -1059,6 +1245,22 @@ Type type, mt; {
     return result;
 }
 
+Bool isProgType(ks,type)               /* Test if type is of the form     */
+List ks;                               /* IO t for some t.                */
+Type type; {
+    Bool result;
+    Int  alpha;
+    Int  beta;
+    emptySubstitution();
+    alpha  = newKindedVars(ks);
+    beta   = newTyvars(1);
+    bindOnlyAbove(beta);
+    result = unify(type,alpha,typeProgIO,beta);
+    unrestrictBind();
+    emptySubstitution();
+    return result;
+}
+
 /* --------------------------------------------------------------------------
  * Matching predicates:
  *
@@ -1134,17 +1336,34 @@ Cell pi1;                               /* Assumes preds are kind correct  */
 Int  o1;                                /* with the same class.            */
 Cell pi;
 Int  o; {
-    for (; isAp(pi1); pi1=fun(pi1), pi=fun(pi))
-        if (!unify(arg(pi1),o1,arg(pi),o))
-            return FALSE;
+  for (; isAp(pi1); pi1=fun(pi1), pi=fun(pi)) {
+       if (!isAp(pi) || !unify(arg(pi1),o1,arg(pi),o))
+           return FALSE;
+  }
+  /* pi1 has exhausted its argument chain, we also need to check that
+     pi has no remaining arguments.  However, under this condition,
+     the pi1 == pi will always return FALSE, giving the desired
+     result. */
+
+#if IPARAM
+    if (isIP(pi1) && isIP(pi))
+       return textOf(pi1)==textOf(pi);
+    else
+#endif
     return pi1==pi;
 }
 
+#if TREX
+static Cell trexShow = NIL;             /* Used to test for show on records*/
+static Cell trexEq   = NIL;             /* Used to test for eq on records  */
+#endif
+
 Inst findInstFor(pi,o)                  /* Find matching instance for pred */
 Cell  pi;                               /* (pi,o), or otherwise NIL.  If a */
 Int   o; {                              /* match is found, then tyvars from*/
     Class c = getHead(pi);              /* typeOff have been initialized to*/
     List  ins;                          /* allow direct use of specifics.  */
+    Cell  kspi = NIL;
 
     if (!isClass(c))
         return NIL;
@@ -1156,16 +1375,29 @@ Int   o; {                              /* match is found, then tyvars from*/
             typeOff = beta;
             return in;
         }
-        else
-            numTyvars = beta;
+       else {
+           numTyvars = beta;
+           if (allowOverlap) {
+               Int alpha = newKindedVars(inst(in).kinds);
+               if (isNull(kspi)) {
+                   kspi = copyNoMark(pi,o);
+               }
+               beta = newKindedVars(fst(kspi));
+               if (matchPred(inst(in).head,alpha,snd(kspi),beta)) {
+                   numTyvars = alpha;
+                   return NIL;
+               }
+               numTyvars = alpha;
+           }
+       }
     }
     unrestrictBind();
 
 #if TREX
-    {   Int showRow = strcmp(textToStr(cclass(c).text),"ShowRecRow");
-        Int eqRow   = strcmp(textToStr(cclass(c).text),"EqRecRow");
+    {   Bool wantShow   = (c==findQualClass(trexShow));
+        Bool wantEither = wantShow || (c==findQualClass(trexEq));
 
-        if (showRow==0 || eqRow==0) {           /* Generate instances of   */
+        if (wantEither) {                       /* Generate instances of   */
             Type  t = arg(pi);                  /* ShowRecRow and EqRecRow */
             Tyvar *tyv;                         /* on the fly              */
             Cell  e;
@@ -1179,8 +1411,7 @@ Int   o; {                              /* match is found, then tyvars from*/
                         break;
                     }
                 if (isNull(in))
-                    in = (showRow==0) ? addRecShowInst(c,e)
-                                      : addRecEqInst(c,e);
+                    in = (wantShow ? addRecShowInst(c,e) : addRecEqInst(c,e));
                 typeOff = newKindedVars(extKind);
                 bindTv(typeOff,arg(fun(t)),o);
                 bindTv(typeOff+1,arg(t),o);
@@ -1193,6 +1424,213 @@ Int   o; {                              /* match is found, then tyvars from*/
     return NIL;
 }
 
+#if MULTI_INST
+List findInstsFor(pi,o)                        /* Find matching instance for pred */
+Cell  pi;                              /* (pi,o), or otherwise NIL.  If a */
+Int   o; {                             /* match is found, then tyvars from*/
+    Class c = getHead(pi);             /* typeOff have been initialized to*/
+    List  ins;                         /* allow direct use of specifics.  */
+    List  res = NIL;
+
+    if (!isClass(c))
+       return NIL;
+
+    for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins)) {
+       Inst in   = hd(ins);
+       Int  beta = newKindedVars(inst(in).kinds);
+       if (matchPred(pi,o,inst(in).head,beta)) {
+           res = cons (pair (beta, in), res);
+           continue;
+       }
+       else
+           numTyvars = beta;
+    }
+    if (res == NIL) {
+       unrestrictBind();
+    }
+
+    return rev(res);
+}
+#endif
+
+/* --------------------------------------------------------------------------
+ * Improvement:
+ * ------------------------------------------------------------------------*/
+
+Void improve(line,sps,ps)              /* Improve a list of predicates    */
+Int  line;
+List sps;
+List ps; {
+    Bool improved;
+    List ps1;
+    do {
+       improved = FALSE;
+       for (ps1=ps; nonNull(ps1); ps1=tl(ps1)) {
+           Cell pi = fst3(hd(ps1));
+           Int  o  = intOf(snd3(hd(ps1)));
+           Cell c  = getHead(pi);
+           if ((isClass(c) && nonNull(cclass(c).xfds)) || isIP(c)) {
+               improved |= improveAgainst(line,sps,pi,o);
+               if (!isIP(c))
+                   improved |= instImprove(line,c,pi,o);
+               improved |= improveAgainst(line,tl(ps1),pi,o);
+           }
+       }
+    } while (improved);
+}
+
+Void improve1(line,sps,pi,o)           /* Improve a single predicate      */
+Int  line;
+List sps;
+Cell pi;
+Int o; {
+    Bool improved;
+    Cell c  = getHead(pi);
+    do {
+       improved = FALSE;
+       if ((isClass(c) && nonNull(cclass(c).xfds)) || isIP(c)) {
+           improved |= improveAgainst(line,sps,pi,o);
+           if (!isIP(c))
+               improved |= instImprove(line,c,pi,o);
+       }
+    } while (improved);
+}
+
+Bool improveAgainst(line,ps,pi,o)
+Int line;
+List ps;
+Cell pi;
+Int o; {
+    Bool improved = FALSE;
+    Cell h = getHead(pi);
+    for (; nonNull(ps); ps=tl(ps)) {
+       Cell pr = hd(ps);
+       Cell pi1 = fst3(pr);
+       Int o1 = intOf(snd3(pr));
+       Cell h1 = getHead(pi1);
+       /* it would be nice to optimize for the common case
+          where h == h1 */
+       if (isClass(h) && isClass(h1)) {
+           improved |= pairImprove(line,h,pi,o,pi1,o1,numTyvars);
+           if (h != h1)
+               improved |= pairImprove(line,h1,pi1,o1,pi,o,numTyvars);
+       }
+#if IPARAM
+       else if (isIP(h1) && textOf(h1) == textOf(h))
+           improved |= ipImprove(line,pi,o,pi1,o1);
+#endif
+    }
+    return improved;
+}
+/* should emulate findInsts behavior of shorting out if the
+   predicate would match a more general signature... */
+
+Bool instImprove(line,c,pi,o)
+Int line;
+Class c;
+Cell pi;
+Int o; {
+    Bool improved = FALSE;
+    List ins      = cclass(c).instances;
+    for (; nonNull(ins); ins=tl(ins)) {
+       Cell in   = hd(ins);
+       Int alpha = newKindedVars(inst(in).kinds);
+       improved |= pairImprove(line,c,pi,o,inst(in).head,alpha,alpha);
+    }
+    return improved;
+}
+
+#if IPARAM
+Bool ipImprove(line,pi,o,pi1,o1)
+Int line;
+Cell pi;
+Int o;
+Cell pi1;
+Int o1; {
+    Type t  = arg(pi);
+    Type t1 = arg(pi1);
+    if (!sameType(t,o,t1,o1)) {
+       if (!unify(t,o,t1,o1)) {
+           ERRMSG(line) "Mismatching uses of implicit parameter\n"
+           ETHEN
+           ERRTEXT "\n***  "
+           ETHEN ERRPRED(copyPred(pi1,o1));
+           ERRTEXT "\n***  "
+           ETHEN ERRPRED(copyPred(pi,o));
+           ERRTEXT "\n"
+           EEND;
+       }
+       return TRUE;
+    }
+    return FALSE;
+}
+#endif
+
+Bool pairImprove(line,c,pi1,o1,pi2,o2,above)   /* Look for improvement of (pi1,o1)*/
+Int   line;                            /* against (pi2,o2)                */
+Class c;
+Cell  pi1;
+Int   o1;
+Cell  pi2;
+Int   o2;
+Int above; {
+    Bool improved = FALSE;
+    List xfds     = cclass(c).xfds;
+    for (; nonNull(xfds); xfds=tl(xfds)) {
+       Cell xfd = hd(xfds);
+       Cell hs  = fst(xfd);
+       Int alpha;
+       for (; nonNull(hs); hs=tl(hs)) {
+           Cell h  = hd(hs);
+           Class d = getHead(h);
+           alpha = newKindedVars(cclass(d).kinds);
+           if (matchPred(pi2,o2,h,alpha))
+               break;
+           numTyvars = alpha;
+       }
+       if (nonNull(hs)) {
+           List fds = snd(xfd);
+           for (; nonNull(fds); fds=tl(fds)) {
+               List as   = fst(hd(fds));
+               Bool same = TRUE;
+               for (; same && nonNull(as); as=tl(as)) {
+                   Int n = offsetOf(hd(as));
+                   same &= matchTypeAbove(nthArg(n,pi1),o1,
+                                          mkOffset(n),alpha,above);
+               }
+               if (isNull(as) && same) {
+                   for (as=snd(hd(fds)); same && nonNull(as); as=tl(as)) {
+                       Int  n    = offsetOf(hd(as));
+                       Type t1   = nthArg(n,pi1);
+                       Type t2   = mkOffset(n);
+                       if (!matchTypeAbove(t1,o1,t2,alpha,above)) {
+                           same &= unify(t1,o1,t2,alpha);
+                           improved = TRUE;
+                       }
+                   }
+                   if (!same) {
+                       ERRMSG(line)
+                         "Constraints are not consistent with functional dependency"
+                       ETHEN
+                       ERRTEXT "\n*** Constraint       : "
+                       ETHEN ERRPRED(copyPred(pi1,o1));
+                       ERRTEXT "\n*** And constraint   : "
+                       ETHEN ERRPRED(copyPred(pi2,o2));
+                       ERRTEXT "\n*** For class        : "
+                       ETHEN ERRPRED(cclass(c).head);
+                       ERRTEXT "\n*** Break dependency : "
+                       ETHEN ERRFD(hd(fds));
+                       ERRTEXT "\n"
+                       EEND;
+                   }
+               }
+           }
+           numTyvars = alpha;
+       }
+    }
+    return improved;
+}
+
 /* --------------------------------------------------------------------------
  * Compare type schemes:
  * ------------------------------------------------------------------------*/
@@ -1259,8 +1697,8 @@ Type s1; {
     for (; nr2>0; nr2--) {              /* Deal with rank 2 arguments      */
         Type t  = arg(fun(s));
         Type t1 = arg(fun(s1));
-        b       = isPolyType(t);
-        b1      = isPolyType(t1);
+       b       = isPolyOrQualType(t);
+       b1      = isPolyOrQualType(t1);
         if (b || b1) {
             if (b && b1) {
                 t  = dropRank1(t,o,m);
@@ -1272,20 +1710,53 @@ Type s1; {
                 return FALSE;
         }
         else {
-            noBind();
-            b = unify(t,o,t1,o);
-            unrestrictBind();
-            if (!b)
+           if (!sameType(t,o,t1,o)) {
                 return FALSE;
+           }
         }
+
         s  = arg(s);
         s1 = arg(s1);
     }
 
-    noBind();                           /* Ensure body types are the same  */
-    b = unify(s,o,s1,o);
+    return sameType(s,o,s1,o);         /* Ensure body types are the same  */
+}
+
+Bool sameType(t1,o1,t,o)               /* Test to see if types are        */
+Type t1;                               /* the same, with no binding of    */
+Int  o1;                               /* the variables in either one.    */
+Cell t;                                        /* Assumes types are kind correct  */
+Int  o; {                              /* with the same kind.             */
+    Bool result;
+    noBind();
+    result = unify(t1,o1,t,o);
     unrestrictBind();
-    return b;
+    return result;
+}
+
+Bool matchType(t1,o1,t,o)              /* One way match type (t1,o1)      */
+Type t1;                               /* against (t,o), allowing only    */
+Int  o1;                               /* vars in 2nd type to be bound.   */
+Type t;                                        /* Assumes types are kind correct  */
+Int  o; {                              /* and that no vars have been      */
+    Bool result;                       /* alloc'd since o.                */
+    bindOnlyAbove(o);
+    result = unify(t1,o1,t,o);
+    unrestrictBind();
+    return result;
+}
+
+static Bool local matchTypeAbove(t1,o1,t,o,a)  /* match, allowing only vars */
+Type t1;                               /* allocated since `a' to be bound   */
+Int  o1;                               /* this is deeply hacky, since it    */
+Type t;                                        /* relies on careful use of the      */
+Int  o;                                        /* substitution stack                */
+Int  a; {
+    Bool result;
+    bindOnlyAbove(a);
+    result = unify(t1,o1,t,o);
+    unrestrictBind();
+    return result;
 }
 
 /* --------------------------------------------------------------------------
@@ -1298,7 +1769,7 @@ Tyvar *tyv1, *tyv2; {                     /* for kind variable bindings    */
         tyv1->bound = aVar;
         tyv1->offs  = tyvNum(tyv2);
 #ifdef DEBUG_KINDS
-        printf("vv binding kvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
+        Printf("vv binding kvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
 #endif
     }
     return TRUE;
@@ -1312,9 +1783,9 @@ Int   o; {                              /* have synonym as outermost constr*/
         tyv->bound = t;
         tyv->offs  = o;
 #ifdef DEBUG_KINDS
-        printf("vt binding kind variable: _%d to ",tyvNum(tyv));
+        Printf("vt binding kind variable: _%d to ",tyvNum(tyv));
         printType(stdout,debugType(t,o));
-        putchar('\n');
+        Putchar('\n');
 #endif
         return TRUE;
     }
@@ -1330,21 +1801,22 @@ Int  o1,o2; {
     deRef(kyv1,k1,o1);
     deRef(kyv2,k2,o2);
 
-    if (kyv1)
+    if (kyv1) {
         if (kyv2)
             return kvarToVarBind(kyv1,kyv2);        /* k1, k2 variables    */
         else
             return kvarToTypeBind(kyv1,k2,o2);      /* k1 variable, k2 not */
+    }
     else
         if (kyv2)
             return kvarToTypeBind(kyv2,k1,o1);      /* k2 variable, k1 not */
         else {
 #ifdef DEBUG_KINDS
-            printf("unifying kinds: ");
+            Printf("unifying kinds: ");
             printType(stdout,debugType(k1,o1));
-            printf(" with ");
+            Printf(" with ");
             printType(stdout,debugType(k2,o2));
-            putchar('\n');
+            Putchar('\n');
 #endif
             if (k1==STAR && k2==STAR)               /* k1, k2 not vars     */
                 return TRUE;
@@ -1472,15 +1944,27 @@ Int what; {
                        mark(typeIs);
                        mark(predsAre);
                        mark(genericVars);
+#if TREX
+                       mark(trexShow);
+                       mark(trexEq);
+#endif
                        break;
 
-        case INSTALL : substitution(RESET);
+        case POSTPREL: break;
+
+        case PREPREL : substitution(RESET);
                        for (i=0; i<MAXTUPCON; ++i)
                            tupleConTypes[i] = NIL;
                        for (i=0; i<MAXKINDFUN; ++i) {
                            simpleKindCache[i] = NIL;
                            varKindCache[i]    = NIL;
                        }
+#if TREX
+                       trexShow = mkQCon(findText("Trex"),
+                                         findText("ShowRecRow"));
+                       trexEq   = mkQCon(findText("Trex"),
+                                         findText("EqRecRow"));
+#endif
                        break;
     }
 }