[project @ 2000-05-15 09:20:11 by simonmar]
[ghc-hetmet.git] / ghc / interpreter / preds.c
index 6a88cb8..7c5a7a8 100644 (file)
@@ -1,43 +1,59 @@
-/* -*- mode: hugs-c; -*- */
+
 /* --------------------------------------------------------------------------
- * preds.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
+ * Part of the type checker dealing with predicates and entailment
+ *
+ * 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.
  *
- * Part of type checker dealing with predicates and entailment.
+ * $RCSfile: preds.c,v $
+ * $Revision: 1.11 $
+ * $Date: 2000/03/13 11:37:16 $
  * ------------------------------------------------------------------------*/
 
 /* --------------------------------------------------------------------------
  * Local function prototypes:
  * ------------------------------------------------------------------------*/
 
-static Cell   local assumeEvid        Args((Cell,Int));
-static List   local makePredAss       Args((List,Int));
-static List   local copyPreds         Args((List));
-static Void   local qualify           Args((List,Cell));
-static Void   local qualifyBinding    Args((List,Cell));
-static Cell   local qualifyExpr       Args((Int,List,Cell));
-static Void   local overEvid          Args((Cell,Cell));
-
-static Cell   local scFind            Args((Cell,Cell,Int,Cell,Int));
-static Cell   local scEntail          Args((List,Cell,Int));
-static Cell   local entail            Args((List,Cell,Int));
-static Cell   local inEntail          Args((List,Cell,Int));
+static Cell   local assumeEvid        ( Cell,Int );
+#if IPARAM
+static Cell   local findIPEvid       ( Text );
+static Void   local removeIPEvid      ( Text );
+#endif
+static List   local makePredAss       ( List,Int );
+static List   local copyPreds         ( List );
+static Void   local qualify           ( List,Cell );
+static Void   local qualifyBinding    ( List,Cell );
+static Cell   local qualifyExpr       ( Int,List,Cell );
+static Void   local overEvid          ( Cell,Cell );
+
+static Void   local cutoffExceeded    ( Cell,Int,List );
+static Cell   local scFind            ( Cell,Cell,Int,Cell,Int,Int );
+static Cell   local scEntail          ( List,Cell,Int,Int );
+static Cell   local entail            ( List,Cell,Int,Int );
+static Cell   local inEntail          ( List,Cell,Int,Int );
+#if MULTI_INST
+static Cell   local inEntails        ( List,Cell,Int,Int );
+static Bool   local instCompare              ( Inst, Inst );
+#endif
 #if TREX
-static Cell   local lacksNorm         Args((Type,Int,Cell));
+static Cell   local lacksNorm         ( Type,Int,Cell );
 #endif
 
-static List   local scSimplify        Args((List));
-static Void   local elimTauts         Args((Void));
-static Bool   local anyGenerics       Args((Type,Int));
-static List   local elimOuterPreds    Args((List));
-static List   local elimPredsUsing    Args((List,List));
-static Void   local reducePreds       Args((Void));
-static Void   local normPreds         Args((Int));
+static List   local scSimplify        ( List );
+static Void   local elimTauts         ( Void );
+static Bool   local anyGenerics       ( Type,Int );
+static List   local elimOuterPreds    ( List );
+static List   local elimPredsUsing    ( List,List );
+static Void   local reducePreds       ( Void );
+static Void   local normPreds         ( Int );
 
-static Bool   local resolveDefs       Args((List));
-static Bool   local resolveVar        Args((Int));
-static Class  local classConstraining Args((Int,Cell,Int));
+static Bool   local resolveDefs       ( List );
+static Bool   local resolveVar        ( Int );
+static Class  local classConstraining ( Int,Cell,Int );
+static Bool   local instComp_         ( Inst,Inst );
 
 /* --------------------------------------------------------------------------
  * Predicate assignments:
@@ -60,6 +76,33 @@ Int  o; {
     return nd;
 }
 
+#if IPARAM
+static Cell local findIPEvid(t)
+Text t; {
+    List ps = preds;
+    for (; nonNull(ps); ps=tl(ps)) {
+       Cell p = hd(ps);        
+       if (ipMatch(fst3(p), t))
+           return p;
+    }
+    return NIL;
+}
+
+static Void local removeIPEvid(t)
+Text t; {
+    List ps = preds;
+    List *prev = &preds;
+    for (; nonNull(ps); ps = tl(ps))
+       if (ipMatch(fst3(hd(ps)), t)) {
+           *prev = tl(ps);
+           return;
+       } else {
+           prev = &tl(ps);
+       }
+}
+#endif
+
+
 static List local makePredAss(qs,o)     /* Make list of predicate assumps. */
 List qs;                                /* from qs (offset o), w/ new dict */
 Int  o; {                               /* vars for each predicate         */
@@ -167,47 +210,104 @@ Cell ev; {
  *
  * ------------------------------------------------------------------------*/
 
-static Cell local scFind(e,pi1,o1,pi,o) /* Use superclass entailment to    */
+Int cutoff = 64;                        /* Used to limit depth of recursion*/
+
+static Void local cutoffExceeded(pi,o,ps)
+Cell pi;                               /* Display error msg when cutoff   */
+Int  o;
+List ps; {
+    clearMarks();
+    ERRMSG(0)
+        "\n*** The type checker has reached the cutoff limit while trying to\n"
+    ETHEN ERRTEXT
+        "*** determine whether:\n***     "     ETHEN ERRPRED(copyPred(pi,o));
+    ps = copyPreds(ps);
+    ERRTEXT
+        "\n*** can be deduced from:\n***     " ETHEN ERRCONTEXT(ps);
+    ERRTEXT
+        "\n*** This may indicate that the problem is undecidable.  However,\n"
+    ETHEN ERRTEXT
+        "*** you may still try to increase the cutoff limit using the -c\n"
+    ETHEN ERRTEXT
+        "*** option and then try again.  (The current setting is -c%d)\n",
+        cutoff
+    EEND;
+}
+
+static Cell local scFind(e,pi1,o1,pi,o,d)/* Use superclass entailment to   */
 Cell e;                                 /* find evidence for (pi,o) using  */
 Cell pi1;                               /* the evidence e for (pi1,o1).    */
 Int  o1;
 Cell pi;
-Int  o; {
+Int  o;
+Int  d; {
     Class h1 = getHead(pi1);
     Class h  = getHead(pi);
+    Cell ev = NIL;
 
-    if (h==h1 && samePred(pi1,o1,pi,o))
+    /* the h==h1 test is just an optimization, and I'm not
+       sure it will work with IPs, so I'm being conservative
+       and commenting it out */
+    if (/* h==h1 && */ samePred(pi1,o1,pi,o))
         return e;
 
     if (isClass(h1) && (!isClass(h) || cclass(h).level<cclass(h1).level)) {
-        Int  beta  = newKindedVars(cclass(h1).kinds);
-        List scs   = cclass(h1).supers;
-        List dsels = cclass(h1).dsels;
-        if (!matchPred(pi1,o1,cclass(h1).head,beta))
-            internal("scFind");
-        for (; nonNull(scs); scs=tl(scs), dsels=tl(dsels)) {
-            Cell ev = scFind(ap(hd(dsels),e),hd(scs),beta,pi,o);
-            if (nonNull(ev))
-                return ev;
-        }
-    }
+       Int  beta  = newKindedVars(cclass(h1).kinds);
+       List scs   = cclass(h1).supers;
+       List dsels = cclass(h1).dsels;
+       List ps = NIL;
+       if (!matchPred(pi1,o1,cclass(h1).head,beta))
+           internal("scFind");
+
+       for (; nonNull(scs); scs=tl(scs), dsels=tl(dsels))
+           ps = cons(triple(hd(scs),mkInt(beta),ap(hd(dsels),e)),ps);
+       ps = rev(ps);
 
+#if EXPLAIN_INSTANCE_RESOLUTION
+       if (showInstRes) {
+           int i;
+           for (i = 0; i < d; i++)
+             fputc(' ', stdout);
+           fputs("scEntail(scFind): ", stdout);
+           printContext(stdout,copyPreds(ps));
+           fputs(" ||- ", stdout);
+           printPred(stdout, copyPred(pi, o));
+           fputc('\n', stdout);
+       }
+#endif
+       improve1(0,ps,pi,o);
+       ev = scEntail(ps,pi,o,d);
+#if EXPLAIN_INSTANCE_RESOLUTION
+       if (showInstRes && nonNull(ev)) {
+           int i;
+           for (i = 0; i < d; i++)
+             fputc(' ', stdout);
+           fputs("scSat.\n", stdout);
+       }
+#endif
+       return ev;
+    }
     return NIL;
 }
 
-static Cell local scEntail(ps,pi,o)     /* Calc evidence for (pi,o) from ps*/
+static Cell local scEntail(ps,pi,o,d)   /* Calc evidence for (pi,o) from ps*/
 List ps;                                /* Using superclasses and equality.*/
 Cell pi;
-Int  o; {
+Int  o;
+Int  d; {
+    if (d++ >= cutoff)
+       cutoffExceeded(pi,o,ps);
+
     for (; nonNull(ps); ps=tl(ps)) {
         Cell pi1 = hd(ps);
-        Cell ev  = scFind(thd3(pi1),fst3(pi1),intOf(snd3(pi1)),pi,o);
+        Cell ev  = scFind(thd3(pi1),fst3(pi1),intOf(snd3(pi1)),pi,o,d);
         if (nonNull(ev))
             return ev;
     }
     return NIL;
 }
 
+
 /* --------------------------------------------------------------------------
  * Now we reach the main entailment routine:
  *
@@ -256,18 +356,67 @@ Int  o; {
  * to cause any further concern, except in pathological cases.)
  * ------------------------------------------------------------------------*/
 
-static Cell local entail(ps,pi,o)       /* Calc evidence for (pi,o) from ps*/
+static Cell local entail(ps,pi,o,d)     /* Calc evidence for (pi,o) from ps*/
 List ps;                                /* Uses superclasses, equality,    */
 Cell pi;                                /* tautology, and construction     */
-Int  o; {
-    Cell ev = scEntail(ps,pi,o);
-    return nonNull(ev) ? ev : inEntail(ps,pi,o);
+Int  o;
+Int  d; {
+    Cell ev = NIL;
+
+#if EXPLAIN_INSTANCE_RESOLUTION
+    if (showInstRes) {
+       int i;
+       for (i = 0; i < d; i++)
+         fputc(' ', stdout);
+       fputs("entail: ", stdout);
+       printContext(stdout,copyPreds(ps));
+       fputs(" ||- ", stdout);
+       printPred(stdout, copyPred(pi, o));
+       fputc('\n', stdout);
+    }
+#endif
+
+    ev = scEntail(ps,pi,o,d);
+    if (nonNull(ev)) {
+#if EXPLAIN_INSTANCE_RESOLUTION
+       if (showInstRes) {
+           int i;
+           for (i = 0; i < d; i++)
+             fputc(' ', stdout);
+           fputs("scSat.\n", stdout);
+       }
+#endif
+    } else {
+       ev =
+#if MULTI_INST
+             multiInstRes ? inEntails(ps,pi,o,d) :
+                           inEntail(ps,pi,o,d);
+#else
+             inEntail(ps,pi,o,d);
+#endif
+#if EXPLAIN_INSTANCE_RESOLUTION
+       if (nonNull(ev) && showInstRes) {
+           int i;
+           for (i = 0; i < d; i++)
+             fputc(' ', stdout);
+           fputs("inSat.\n", stdout);
+       }
+#endif
+    }
+    return ev;
 }
 
-static Cell local inEntail(ps,pi,o)     /* Calc evidence for (pi,o) from ps*/
+static Cell local inEntail(ps,pi,o,d)   /* Calc evidence for (pi,o) from ps*/
 List ps;                                /* using a top-level instance      */
 Cell pi;                                /* entailment                      */
-Int  o; {
+Int  o;
+Int  d; {
+    int i;
+    Inst in;
+
+    if (d++ >= cutoff)
+       cutoffExceeded(pi,o,ps);
+
 #if TREX
     if (isAp(pi) && isExt(fun(pi))) {   /* Lacks predicates                */
         Cell e  = fun(pi);
@@ -294,26 +443,209 @@ Int  o; {
     }
     else {
 #endif
-    Inst in = findInstFor(pi,o);        /* Class predicates                */
+
+    in = findInstFor(pi,o);    /* Class predicates                */
     if (nonNull(in)) {
         Int  beta = typeOff;
-        Cell d    = inst(in).builder;
-        Cell ds   = inst(in).specifics;
-        for (; nonNull(ds); ds=tl(ds)) {
-            Cell ev = entail(ps,hd(ds),beta);
+        Cell e    = inst(in).builder;
+       List es   = inst(in).specifics;
+       List fs   = NIL;
+       for (; nonNull(es); es=tl(es))
+           fs = cons(triple(hd(es),mkInt(beta),NIL),fs);
+       fs = rev(fs);
+       improve(0,ps,fs);
+#if EXPLAIN_INSTANCE_RESOLUTION
+       if (showInstRes) {
+           for (i = 0; i < d; i++)
+             fputc(' ', stdout);
+           fputs("try ", stdout);
+           printContext(stdout, copyPreds(fs));
+           fputs(" => ", stdout);
+           printPred(stdout, copyPred(inst(in).head,beta));
+           fputc('\n', stdout);
+       }
+#endif
+       for (es=inst(in).specifics; nonNull(es); es=tl(es)) {
+           Cell ev;
+           ev = entail(ps,hd(es),beta,d);
             if (nonNull(ev))
-                d = ap(d,ev);
+                e = ap(e,ev);
             else
                 return NIL;
         }
-        return d;
+        return e;
     }
+#if EXPLAIN_INSTANCE_RESOLUTION
+      else {
+       if (showInstRes) {
+           for (i = 0; i < d; i++)
+             fputc(' ', stdout);
+           fputs("No instance found for ", stdout);
+           printPred(stdout, copyPred(pi, o));
+           fputc('\n', stdout);
+       }
+    }
+#endif
     return NIL;
 #if TREX
     }
 #endif
 }
 
+#if MULTI_INST
+static Cell local inEntails(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
+List ps;                               /* using a top-level instance      */
+Cell pi;                               /* entailment                      */
+Int  o;
+Int  d; {
+    int i;
+    int k = 0;
+    Cell ins;                          /* Class predicates                */
+    Inst in, in_;
+    Cell e_;
+
+    if (d++ >= cutoff)
+       cutoffExceeded(pi,o,ps);
+
+#if TREX
+    if (isAp(pi) && isExt(fun(pi))) {  /* Lacks predicates                */
+       Cell e  = fun(pi);
+       Cell l;
+       l  = lacksNorm(arg(pi),o,e);
+       if (isNull(l) || isInt(l))
+           return l;
+       else {
+           List qs = ps;
+           for (; nonNull(qs); qs=tl(qs)) {
+               Cell qi = fst3(hd(qs));
+               if (isAp(qi) && fun(qi)==e) {
+                   Cell lq = lacksNorm(arg(qi),intOf(snd3(hd(qs))),e);
+                   if (isAp(lq) && intOf(fst(l))==intOf(fst(lq))) {
+                       Int f = intOf(snd(l)) - intOf(snd(lq));
+                       return (f==0) ? thd3(hd(qs)) : ap2(nameAddEv,
+                                                          mkInt(f),
+                                                          thd3(hd(qs)));
+                   }
+               }
+           }
+           return NIL;
+       }
+    }
+    else {
+#endif
+
+#if EXPLAIN_INSTANCE_RESOLUTION
+    if (showInstRes) {
+       for (i = 0; i < d; i++)
+         fputc(' ', stdout);
+       fputs("inEntails: ", stdout);
+       printContext(stdout,copyPreds(ps));
+       fputs(" ||- ", stdout);
+       printPred(stdout, copyPred(pi, o));
+       fputc('\n', stdout);
+    }
+#endif
+
+    ins = findInstsFor(pi,o);
+    for (; nonNull(ins); ins=tl(ins)) {
+        in = snd(hd(ins));
+       if (nonNull(in)) {
+           Int  beta = fst(hd(ins));
+           Cell e    = inst(in).builder;
+           Cell es   = inst(in).specifics;
+
+#if EXPLAIN_INSTANCE_RESOLUTION
+           if (showInstRes) {
+               for (i = 0; i < d; i++)
+                 fputc(' ', stdout);
+               fputs("try ", stdout);
+               printContext(stdout, es);
+               fputs(" => ", stdout);
+               printPred(stdout, inst(in).head);
+               fputc('\n', stdout);
+           }
+#endif
+
+           for (; nonNull(es); es=tl(es)) {
+               Cell ev = entail(ps,hd(es),beta,d);
+               if (nonNull(ev))
+                   e = ap(e,ev);
+               else {
+                   e = NIL;
+                   break;
+               }
+           }
+#if EXPLAIN_INSTANCE_RESOLUTION
+           if (showInstRes)
+               for (i = 0; i < d; i++)
+                 fputc(' ', stdout);
+#endif
+           if (nonNull(e)) {
+#if EXPLAIN_INSTANCE_RESOLUTION
+               if (showInstRes)
+                   fprintf(stdout, "Sat\n");
+#endif
+               if (k > 0) {
+                   if (instCompare (in_, in)) {
+                       ERRMSG(0) "Multiple satisfiable instances for "
+                       ETHEN
+                       ERRPRED(copyPred(pi, o));
+                       ERRTEXT "\nin_ " ETHEN ERRPRED(inst(in_).head);
+                       ERRTEXT "\nin  " ETHEN ERRPRED(inst(in).head);
+                       ERRTEXT "\n"
+                       EEND;
+                   }
+               }
+               if (k++ == 0) {
+                   e_ = e;
+                   in_ = in;
+               }
+               continue;
+           } else {
+#if EXPLAIN_INSTANCE_RESOLUTION
+               if (showInstRes)
+                   fprintf(stdout, "not Sat\n");
+#endif
+               continue;
+           }
+       }
+#if EXPLAIN_INSTANCE_RESOLUTION
+       if (showInstRes) {
+           for (i = 0; i < d; i++)
+             fputc(' ', stdout);
+           fprintf(stdout, "not Sat.\n");
+       }
+#endif
+    }
+    if (k > 0)
+       return e_;
+#if EXPLAIN_INSTANCE_RESOLUTION
+    if (showInstRes) {
+       for (i = 0; i < d; i++)
+         fputc(' ', stdout);
+       fprintf(stdout, "all not Sat.\n");
+    }
+#endif
+    return NIL;
+#if TREX
+    }
+#endif
+}
+
+static Bool local instComp_(ia,ib)     /* See if ia is an instance of ib  */
+Inst ia, ib;{
+    Int alpha = newKindedVars(inst(ia).kinds);
+    Int beta  = newKindedVars(inst(ib).kinds);
+    return matchPred(inst(ia).head,alpha,inst(ib).head,beta);
+}
+
+static Bool local instCompare (ia, ib)
+Inst ia, ib;
+{
+    return instComp_(ia, ib) && instComp_(ib, ia);
+}
+#endif
+
 Cell provePred(ks,ps,pi)                /* Find evidence for predicate pi  */
 Kinds ks;                               /* assuming ps.  If ps is null,    */
 List  ps;                               /* then we get to decide whether   */
@@ -323,7 +655,7 @@ Cell  pi; {                             /* is tautological, and we can use */
     emptySubstitution();
     beta = newKindedVars(ks);           /* (ks provides kinds for any      */
     ps   = makePredAss(ps,beta);        /*  vars that appear in pi.)       */
-    ev   = entail(ps,pi,beta);
+    ev   = entail(ps,pi,beta,0);
     emptySubstitution();
     return ev;
 }
@@ -371,7 +703,17 @@ List qs; {                              /* returning equiv minimal subset  */
 
     while (0<n--) {
         Cell pi = hd(qs);
-        Cell ev = scEntail(tl(qs),fst3(pi),intOf(snd3(pi)));
+       Cell ev = NIL;
+#if EXPLAIN_INSTANCE_RESOLUTION
+       if (showInstRes) {
+           fputs("scSimplify: ", stdout);
+           printContext(stdout,copyPreds(tl(qs)));
+           fputs(" ||- ", stdout);
+           printPred(stdout, copyPred(fst3(pi),intOf(snd3(pi))));
+           fputc('\n', stdout);
+       }
+#endif
+       ev = scEntail(tl(qs),fst3(pi),intOf(snd3(pi)),0);
         if (nonNull(ev)) {
             overEvid(thd3(pi),ev);      /* Overwrite dict var with evidence*/
             qs      = tl(qs);           /* ... and discard predicate       */
@@ -396,20 +738,24 @@ Int  o; {                               /* superclass hierarchy            */
  * ------------------------------------------------------------------------*/
 
 static Void local elimTauts() {         /* Remove tautological constraints */
-    List ps = preds;                    /* from preds                      */
-    preds   = NIL;
-    while (nonNull(ps)) {
-        Cell pi = hd(ps);
-        Cell ev = entail(NIL,fst3(pi),intOf(snd3(pi)));
-        if (nonNull(ev)) {
-            overEvid(thd3(pi),ev);
-            ps = tl(ps);
-        }
-        else {
-            List tmp = tl(ps);
-            tl(ps)   = preds;
-            preds    = ps;
-            ps       = tmp;
+    if (haskell98) {                    /* from preds                      */
+        reducePreds();                  /* (or context reduce for Hask98)  */
+    } else {
+        List ps = preds;
+        preds   = NIL;
+        while (nonNull(ps)) {
+            Cell pi = hd(ps);
+            Cell ev = entail(NIL,fst3(pi),intOf(snd3(pi)),0);
+            if (nonNull(ev)) {
+                overEvid(thd3(pi),ev);
+                ps = tl(ps);
+            }
+            else {
+                List tmp = tl(ps);
+                tl(ps)   = preds;
+                preds    = ps;
+                ps           = tmp;
+            }
         }
     }
 }
@@ -433,13 +779,14 @@ Int  o; {
                 return TRUE;
         }
         deRef(tyv,t,o);
-        if (tyv)
+        if (tyv) {
             if (tyv->offs == FIXED_TYVAR) {
                 numFixedVars++;
                 return FALSE;
             }
             else
                 return TRUE;
+        }
         else
             return FALSE;
     }
@@ -452,9 +799,11 @@ List sps; {                             /* preds that contain no generics. */
     for (preds=scSimplify(preds); nonNull(preds); ) {
         Cell pi = hd(preds);
         Cell nx = tl(preds);
-        if (anyGenerics(fst3(pi),intOf(snd3(pi)))) {    /* Retain predicate*/
-            tl(preds) = qs;
-            qs        = preds;
+       if (anyGenerics(fst3(pi),intOf(snd3(pi)))
+           || !isAp(fst3(pi))
+           || isIP(fun(fst3(pi)))) {
+           tl(preds) = qs;                             /* Retain predicate*/
+           qs        = preds;
         }
         else {                                          /* Defer predicate */
             tl(preds) = sps;
@@ -474,13 +823,16 @@ List sps; {                             /* context ps.  sps = savePreds.   */
         Cell p  = preds;
         Cell pi = fst3(hd(p));
         Int  o  = intOf(snd3(hd(p)));
-        Cell ev = entail(ps,pi,o);
+        Cell ev = entail(ps,pi,o,0);
         preds   = tl(preds);
 
-        if (nonNull(ev))                /* Discharge if ps ||- (pi,o)      */
+       if (nonNull(ev)) {              /* Discharge if ps ||- (pi,o)      */
             overEvid(thd3(hd(p)),ev);
-        else if (!anyGenerics(pi,o)) {  /* Defer if no generics            */
-            tl(p) = sps;
+       } else if (isIP(fun(pi))) {
+           tl(p) = rems;
+           rems  = p;
+       } else if (!isAp(pi) || !anyGenerics(pi,o)) {
+           tl(p) = sps;                /* Defer if no generics            */
             sps   = p;
         }
         else {                          /* Try to split generics and fixed */
@@ -507,7 +859,15 @@ static Void local reducePreds() {       /* Context reduce predicates: uggh!*/
         Cell p  = preds;
         Cell pi = fst3(hd(p));
         Int  o  = intOf(snd3(hd(p)));
-        Inst in = findInstFor(pi,o);
+       Inst in = NIL;
+#if MULTI_INST
+       List ins = NIL;
+       if (multiInstRes) {
+           ins = findInstsFor(pi,o);
+           in = nonNull(ins) && isNull(tl(ins)) ? snd(hd(ins)) : NIL;
+       } else
+#endif
+       in = findInstFor(pi,o);
         preds   = tl(preds);
         if (nonNull(in)) {
             List qs = inst(in).specifics;
@@ -582,11 +942,11 @@ List vs; {                              /* for variables vs subject to  */
     Bool defaulted = FALSE;
 
 #ifdef DEBUG_DEFAULTS
-    printf("Attempt to resolve variables ");
+    Printf("Attempt to resolve variables ");
     printExp(stdout,vs);
-    printf(" with context ");
+    Printf(" with context ");
     printContext(stdout,copyPreds(preds));
-    printf("\n");
+    Printf("\n");
 #endif
 
     resetGenerics();                    /* find type variables in ps    */
@@ -601,16 +961,16 @@ List vs; {                              /* for variables vs subject to  */
         Int vn = intOf(hd(pvs));
 
 #ifdef DEBUG_DEFAULTS
-        printf("is var %d included in ",vn);
+        Printf("is var %d included in ",vn);
         printExp(stdout,vs);
-        printf("?\n");
+        Printf("?\n");
 #endif
 
         if (!intIsMember(vn,vs))
             defaulted |= resolveVar(vn);
 #ifdef DEBUG_DEFAULTS
         else
-            printf("Yes, so no ambiguity!\n");
+            Printf("Yes, so no ambiguity!\n");
 #endif
     }
 
@@ -635,7 +995,7 @@ Int  vn; {                              /* variable vn can be resolved  */
      */
 
 #ifdef DEBUG_DEFAULTS
-    printf("Trying to default variable %d\n",vn);
+    Printf("Trying to default variable %d\n",vn);
 #endif
 
     for (; nonNull(ps); ps=tl(ps)) {
@@ -648,9 +1008,6 @@ Int  vn; {                              /* variable vn can be resolved  */
                 aNumClass = TRUE;
             else if (c!=classEq    && c!=classOrd  && c!=classShow &&
                      c!=classRead  && c!=classIx   && c!=classEnum &&
-#if EVAL_INSTANCES
-                     c!=classEval &&
-#endif
                      c!=classBounded)
                 return FALSE;
 
@@ -676,18 +1033,18 @@ Int  vn; {                              /* variable vn can be resolved  */
     if (aNumClass) {
         List ds = defaultDefns;         /* N.B. guaranteed to be monotypes */
 #ifdef DEBUG_DEFAULTS
-        printf("Default conditions met, looking for type\n");
+        Printf("Default conditions met, looking for type\n");
 #endif
         for (; nonNull(ds); ds=tl(ds)) {
             List cs1 = cs;
-            while (nonNull(cs1) && nonNull(entail(NIL,ap(hd(cs1),hd(ds)),0)))
+            while (nonNull(cs1) && nonNull(entail(NIL,ap(hd(cs1),hd(ds)),0,0)))
                 cs1 = tl(cs1);
             if (isNull(cs1)) {
                 bindTv(vn,hd(ds),0);
 #ifdef DEBUG_DEFAULTS
-                printf("Default type for variable %d is ",vn);
+                Printf("Default type for variable %d is ",vn);
                 printType(stdout,hd(ds));
-                printf("\n");
+                Printf("\n");
 #endif
                 return TRUE;
             }
@@ -695,7 +1052,7 @@ Int  vn; {                              /* variable vn can be resolved  */
     }
 
 #ifdef DEBUG_DEFAULTS
-    printf("No default permitted/found\n");
+    Printf("No default permitted/found\n");
 #endif
     return FALSE;
 }