[project @ 1999-04-27 10:06:47 by sewardj]
[ghc-hetmet.git] / ghc / interpreter / preds.c
1
2 /* --------------------------------------------------------------------------
3  * Part of the type checker dealing with predicates and entailment
4  *
5  * Hugs 98 is Copyright (c) Mark P Jones, Alastair Reid and the Yale
6  * Haskell Group 1994-99, and is distributed as Open Source software
7  * under the Artistic License; see the file "Artistic" that is included
8  * in the distribution for details.
9  *
10  * $RCSfile: preds.c,v $
11  * $Revision: 1.5 $
12  * $Date: 1999/04/27 10:06:59 $
13  * ------------------------------------------------------------------------*/
14
15 /* --------------------------------------------------------------------------
16  * Local function prototypes:
17  * ------------------------------------------------------------------------*/
18
19 static Cell   local assumeEvid        Args((Cell,Int));
20 static List   local makePredAss       Args((List,Int));
21 static List   local copyPreds         Args((List));
22 static Void   local qualify           Args((List,Cell));
23 static Void   local qualifyBinding    Args((List,Cell));
24 static Cell   local qualifyExpr       Args((Int,List,Cell));
25 static Void   local overEvid          Args((Cell,Cell));
26
27 static Void   local cutoffExceeded    Args((Cell,Int,Cell,Int,List));
28 static Cell   local scFind            Args((Cell,Cell,Int,Cell,Int,Int));
29 static Cell   local scEntail          Args((List,Cell,Int,Int));
30 static Cell   local entail            Args((List,Cell,Int,Int));
31 static Cell   local inEntail          Args((List,Cell,Int,Int));
32 #if TREX
33 static Cell   local lacksNorm         Args((Type,Int,Cell));
34 #endif
35
36 static List   local scSimplify        Args((List));
37 static Void   local elimTauts         Args((Void));
38 static Bool   local anyGenerics       Args((Type,Int));
39 static List   local elimOuterPreds    Args((List));
40 static List   local elimPredsUsing    Args((List,List));
41 static Void   local reducePreds       Args((Void));
42 static Void   local normPreds         Args((Int));
43
44 static Bool   local resolveDefs       Args((List));
45 static Bool   local resolveVar        Args((Int));
46 static Class  local classConstraining Args((Int,Cell,Int));
47
48 /* --------------------------------------------------------------------------
49  * Predicate assignments:
50  *
51  * A predicate assignment is represented by a list of triples (pi,o,ev)
52  * where o is the offset for types in pi, with evidence required at the
53  * node pointed to by ev (which is taken as a dictionary parameter if
54  * no other evidence is available).  Note that the ev node will be
55  * overwritten at a later stage if evidence for that predicate is found
56  * subsequently.
57  * ------------------------------------------------------------------------*/
58
59 static List preds;                      /* Current predicate assignment    */
60
61 static Cell local assumeEvid(pi,o)      /* Add predicate pi (offset o) to  */
62 Cell pi;                                /* preds with new dict var nd      */
63 Int  o; {
64     Cell nd = inventDictVar();
65     preds   = cons(triple(pi,mkInt(o),nd),preds);
66     return nd;
67 }
68
69 static List local makePredAss(qs,o)     /* Make list of predicate assumps. */
70 List qs;                                /* from qs (offset o), w/ new dict */
71 Int  o; {                               /* vars for each predicate         */
72     List result = NIL;
73     for (; nonNull(qs); qs=tl(qs))
74         result = cons(triple(hd(qs),mkInt(o),inventDictVar()),result);
75     return rev(result);
76 }
77
78 static List local copyPreds(qs)         /* Copy list of predicates         */
79 List qs; {
80     List result = NIL;
81     for (; nonNull(qs); qs=tl(qs)) {
82         Cell pi = hd(qs);
83         result  = cons(copyPred(fst3(pi),intOf(snd3(pi))),result);
84     }
85     return rev(result);
86 }
87
88 static Void local qualify(qs,alt)       /* Add extra dictionary args to    */
89 List qs;                                /* qualify alt by predicates in qs */
90 Cell alt; {                             /* :: ([Pat],Rhs)                  */
91     List ds;
92     for (ds=NIL; nonNull(qs); qs=tl(qs))
93         ds = cons(thd3(hd(qs)),ds);
94     fst(alt) = revOnto(ds,fst(alt));
95 }
96
97 static Void local qualifyBinding(qs,b)  /* Add extra dict args to each     */
98 List qs;                                /* alternative in function binding */
99 Cell b ; {
100     if (!isVar(fst(b)))                 /* check for function binding      */
101         internal("qualifyBinding");
102     map1Proc(qualify,qs,snd(snd(b)));
103 }
104
105 static Cell local qualifyExpr(l,ps,e)   /* Add dictionary params to expr   */
106 Int  l;
107 List ps;
108 Cell e; {
109     if (nonNull(ps)) {                  /* Qualify input expression with   */
110         if (whatIs(e)!=LAMBDA)          /* additional dictionary params    */
111             e = ap(LAMBDA,pair(NIL,pair(mkInt(l),e)));
112         qualify(ps,snd(e));
113     }
114     return e;
115 }
116
117 static Void local overEvid(dv,ev)       /* Overwrite dict var dv with      */
118 Cell dv;                                /* evidence ev                     */
119 Cell ev; {
120     fst(dv) = nameInd;
121     snd(dv) = ev;
122 }
123
124 /* --------------------------------------------------------------------------
125  * Predicate entailment:
126  *
127  * Entailment plays a prominent role in the theory of qualified types, and
128  * so, unsurprisingly, in the implementation too.  For practical reasons,
129  * we break down entailment into two pieces.  The first, scEntail, uses
130  * only the information provided by class declarations, while the second,
131  * entail, also uses the information in instance declarations.
132  *
133  * scEntail uses the following auxiliary function to do its work:
134  *
135  *   scFind (e : pi') pi : Find evidence for predicate pi using only
136  *                           equality of predicates, superclass entailment,
137  *                           and the evidence e for pi'.
138  *
139  *   scFind (e : pi') pi =
140  *
141  *      if pi = pi' then
142  *          return e
143  *
144  *      if (pi.class.level < pi'.class.level)
145  *          get superclass entailment pi' ||- P
146  *          for each (sc, pi0) in P
147  *              if (ev := scFind (sc e : pi0) pi) /= NIL
148  *                  return ev
149  *
150  *      return NIL
151  *
152  * This code assumes that the class hierarchy is acyclic, and that
153  * each class has been assigned a `level', which is its height in
154  * the hierachy.  The first of the assumptions guarantees that the
155  * algorithm will terminate.  The comparison of levels is an
156  * optimization that cuts down the search space: given that superclass
157  * entailments can only be used to descend the hierarchy, there is no
158  * way we can reach a higher level than the one that we start with,
159  * and hence there is no point in looking if we reach such a position.
160  *
161  * scEntail extends scFind to work on whole predicate assignments:
162  *
163  *   scEntail P pi : Find evidence for predicate pi using the evidence
164  *                   provided by the predicate assignment P, and using
165  *                   only superclass entailments.
166  *
167  *   scEntail P pi =
168  *
169  *       for each (v:pi') in P
170  *           if (ev := scFind (v:pi') pi) /= NIL
171  *               return ev;
172  *       return NIL
173  *
174  * ------------------------------------------------------------------------*/
175
176 Int cutoff = 16;                        /* Used to limit depth of recursion*/
177
178 static Void local cutoffExceeded(pi,o,pi1,o1,ps)
179 Cell pi, pi1;                           /* Display error msg when cutoff   */
180 Int  o,  o1;
181 List ps; {
182     clearMarks();
183     ERRMSG(0)
184         "\n*** The type checker has reached the cutoff limit while trying to\n"
185     ETHEN ERRTEXT
186         "*** determine whether:\n***     "     ETHEN ERRPRED(copyPred(pi,o));
187     ps = (isNull(pi1)) ? copyPreds(ps) : singleton(copyPred(pi1,o1));
188     ERRTEXT
189         "\n*** can be deduced from:\n***     " ETHEN ERRCONTEXT(ps);
190     ERRTEXT
191         "\n*** This may indicate that the problem is undecidable.  However,\n"
192     ETHEN ERRTEXT
193         "*** you may still try to increase the cutoff limit using the -c\n"
194     ETHEN ERRTEXT
195         "*** option and then try again.  (The current setting is -c%d)\n",
196         cutoff
197     EEND;
198 }
199
200 static Cell local scFind(e,pi1,o1,pi,o,d)/* Use superclass entailment to   */
201 Cell e;                                 /* find evidence for (pi,o) using  */
202 Cell pi1;                               /* the evidence e for (pi1,o1).    */
203 Int  o1;
204 Cell pi;
205 Int  o;
206 Int  d; {
207     Class h1 = getHead(pi1);
208     Class h  = getHead(pi);
209
210     if (h==h1 && samePred(pi1,o1,pi,o))
211         return e;
212
213     if (isClass(h1) && (!isClass(h) || cclass(h).level<cclass(h1).level)) {
214         Int  beta  = newKindedVars(cclass(h1).kinds);
215         List scs   = cclass(h1).supers;
216         List dsels = cclass(h1).dsels;
217         if (!matchPred(pi1,o1,cclass(h1).head,beta))
218             internal("scFind");
219
220         if (d++ >= cutoff)
221             cutoffExceeded(pi,o,pi1,o1,NIL);
222
223         for (; nonNull(scs); scs=tl(scs), dsels=tl(dsels)) {
224             Cell ev = scFind(ap(hd(dsels),e),hd(scs),beta,pi,o,d);
225             if (nonNull(ev))
226                 return ev;
227         }
228     }
229
230     return NIL;
231 }
232
233 static Cell local scEntail(ps,pi,o,d)   /* Calc evidence for (pi,o) from ps*/
234 List ps;                                /* Using superclasses and equality.*/
235 Cell pi;
236 Int  o;
237 Int  d; {
238     for (; nonNull(ps); ps=tl(ps)) {
239         Cell pi1 = hd(ps);
240         Cell ev  = scFind(thd3(pi1),fst3(pi1),intOf(snd3(pi1)),pi,o,d);
241         if (nonNull(ev))
242             return ev;
243     }
244     return NIL;
245 }
246
247 /* --------------------------------------------------------------------------
248  * Now we reach the main entailment routine:
249  *
250  *   entail P pi : Find evidence for predicate pi using the evidence
251  *                 provided by the predicate assignment P.
252  *
253  *   entail P pi =
254  *
255  *       if (ev := scEntail P pi) /= NIL
256  *           return ev;
257  *
258  *       if there is an instance entailment i : Q ||- pi
259  *           for each pi' in Q
260  *               if (ev := entail P pi') /= NIL
261  *                   i := ap(i,ev)
262  *               else
263  *                   return NIL
264  *           return i
265  *
266  *       return NIL;
267  *
268  * The form of evidence expressions produced by scEntail can be described
269  * by the grammar:
270  *
271  *    e  =  v  |  sc e            (v = evidence var, sc = superclass sel)
272  *
273  * while entail extends this to include dictionary expressions given by:
274  *
275  *    d  =  e  |  mki d1 ... dn   (mki = dictionary constructor)
276  *
277  * A full grammar for evidence expressions is:
278  *
279  *    d   =   v   |   sc d   |   mki d1 ... dn
280  *
281  * and this includes evidence expressions of the form  sc (mki d1 ... dn)
282  * that can never be produced by either of the entail functions described
283  * above.  This is good, from a practical perspective, because t means
284  * that we won't waste effort building a dictionary (mki d1 ... dn) only
285  * to extract just one superclass component and throw the rest away.
286  * Moreover, conditions on instance decls already guarantee that any
287  * expression of this form can be rewritten in the form  mki' d1' ... dn'.
288  * (Minor point: they don't guarantee that such rewritings will lead to
289  * smaller terms, and hence to termination.  However, we have already
290  * accepted the benefits of an undecidable entailment relation over
291  * guarantees of termination, and this additional quirk is unlikely
292  * to cause any further concern, except in pathological cases.)
293  * ------------------------------------------------------------------------*/
294
295 static Cell local entail(ps,pi,o,d)     /* Calc evidence for (pi,o) from ps*/
296 List ps;                                /* Uses superclasses, equality,    */
297 Cell pi;                                /* tautology, and construction     */
298 Int  o;
299 Int  d; {
300     Cell ev = scEntail(ps,pi,o,d);
301     return nonNull(ev) ? ev : inEntail(ps,pi,o,d);
302 }
303
304 static Cell local inEntail(ps,pi,o,d)   /* Calc evidence for (pi,o) from ps*/
305 List ps;                                /* using a top-level instance      */
306 Cell pi;                                /* entailment                      */
307 Int  o;
308 Int  d; {
309 #if TREX
310     if (isAp(pi) && isExt(fun(pi))) {   /* Lacks predicates                */
311         Cell e  = fun(pi);
312         Cell l;
313         l  = lacksNorm(arg(pi),o,e);
314         if (isNull(l) || isInt(l))
315             return l;
316         else {
317             List qs = ps;
318             for (; nonNull(qs); qs=tl(qs)) {
319                 Cell qi = fst3(hd(qs));
320                 if (isAp(qi) && fun(qi)==e) {
321                     Cell lq = lacksNorm(arg(qi),intOf(snd3(hd(qs))),e);
322                     if (isAp(lq) && intOf(fst(l))==intOf(fst(lq))) {
323                         Int f = intOf(snd(l)) - intOf(snd(lq));
324                         return (f==0) ? thd3(hd(qs)) : ap2(nameAddEv,
325                                                            mkInt(f),
326                                                            thd3(hd(qs)));
327                     }
328                 }
329             }
330             return NIL;
331         }
332     }
333     else {
334 #endif
335     Inst in = findInstFor(pi,o);        /* Class predicates                */
336
337     if (nonNull(in)) {
338         Int  beta = typeOff;
339         Cell e    = inst(in).builder;
340         Cell es   = inst(in).specifics;
341         if (d++ >= cutoff)
342             cutoffExceeded(pi,o,NIL,0,ps);
343         for (; nonNull(es); es=tl(es)) {
344             Cell ev = entail(ps,hd(es),beta,d);
345             if (nonNull(ev))
346                 e = ap(e,ev);
347             else
348                 return NIL;
349         }
350         return e;
351     }
352     return NIL;
353 #if TREX
354     }
355 #endif
356 }
357
358 Cell provePred(ks,ps,pi)                /* Find evidence for predicate pi  */
359 Kinds ks;                               /* assuming ps.  If ps is null,    */
360 List  ps;                               /* then we get to decide whether   */
361 Cell  pi; {                             /* is tautological, and we can use */
362     Int  beta;                          /* the evidence as a dictionary.   */
363     Cell ev;
364     emptySubstitution();
365     beta = newKindedVars(ks);           /* (ks provides kinds for any      */
366     ps   = makePredAss(ps,beta);        /*  vars that appear in pi.)       */
367     ev   = entail(ps,pi,beta,0);
368     emptySubstitution();
369     return ev;
370 }
371
372 #if TREX
373 static Cell local lacksNorm(t,o,e)      /* Normalize lacks pred (t,o)\l    */
374 Type t;                                 /* returning NIL (unsatisfiable),  */
375 Int  o;                                 /* Int (tautological) or pair (v,a)*/
376 Cell e; {                               /* such that, if e is evid for v\l,*/
377     Text l = extText(e);                /* then (e+a) is evid for (t,o)\l. */
378     Int  a = 0;
379     for (;;) {
380         Tyvar *tyv;
381         deRef(tyv,t,o);
382         if (tyv)
383             return pair(mkInt(tyvNum(tyv)),mkInt(a));
384         else {
385             Cell h = getDerefHead(t,o);
386             if (h==typeNoRow && argCount==0)
387                 return mkInt(a);
388             else if (isExt(h) && argCount==2) {
389                 Text l1 = extText(h);
390                 if (l1==l)
391                     return NIL;
392                 else if (strcmp(textToStr(l1),textToStr(l))<0)
393                     a++;
394                 t = arg(t);
395             }
396             else
397                 return NIL;
398         }
399     }
400 }
401 #endif
402
403 /* --------------------------------------------------------------------------
404  * Predicate set Simplification:
405  *
406  * Calculate a minimal equivalent subset of a given set of predicates.
407  * ------------------------------------------------------------------------*/
408
409 static List local scSimplify(qs)        /* Simplify predicates in qs,      */
410 List qs; {                              /* returning equiv minimal subset  */
411     Int n = length(qs);
412
413     while (0<n--) {
414         Cell pi = hd(qs);
415         Cell ev = scEntail(tl(qs),fst3(pi),intOf(snd3(pi)),0);
416         if (nonNull(ev)) {
417             overEvid(thd3(pi),ev);      /* Overwrite dict var with evidence*/
418             qs      = tl(qs);           /* ... and discard predicate       */
419         }
420         else {                          /* Otherwise, retain predicate     */
421             Cell tmp = tl(qs);
422             tl(qs)   = NIL;
423             qs       = appendOnto(tmp,qs);
424         }
425     }
426     return qs;
427 }
428
429 List simpleContext(ps,o)                /* Simplify context of skeletons   */
430 List ps;                                /* skeletons, offset o, using      */
431 Int  o; {                               /* superclass hierarchy            */
432     return copyPreds(scSimplify(makePredAss(ps,o)));
433 }
434
435 /* --------------------------------------------------------------------------
436  * Context splitting --- tautological and locally tautological predicates:
437  * ------------------------------------------------------------------------*/
438
439 static Void local elimTauts() {         /* Remove tautological constraints */
440     if (haskell98) {                    /* from preds                      */
441         reducePreds();                  /* (or context reduce for Hask98)  */
442     } else {
443         List ps = preds;
444         preds   = NIL;
445         while (nonNull(ps)) {
446             Cell pi = hd(ps);
447             Cell ev = entail(NIL,fst3(pi),intOf(snd3(pi)),0);
448             if (nonNull(ev)) {
449                 overEvid(thd3(pi),ev);
450                 ps = tl(ps);
451             }
452             else {
453                 List tmp = tl(ps);
454                 tl(ps)   = preds;
455                 preds    = ps;
456                 ps           = tmp;
457             }
458         }
459     }
460 }
461
462 static Int numFixedVars = 0;            /* Number of fixed vars found      */
463
464 static Bool local anyGenerics(t,o)      /* Test for generic vars, and count*/
465 Type t;                                 /* fixed variables                 */
466 Int  o; {
467     Type h = getDerefHead(t,o);         /* This code is careful to expand  */
468     Int  a = argCount;                  /* synonyms; mark* & copy* do not. */
469     if (isSynonym(h) && a>=tycon(h).arity) {
470         expandSyn(h,a,&t,&o);
471         return anyGenerics(t,o);
472     }
473     else {
474         Tyvar* tyv;
475         for (; 0<a--; t=fun(t)) {       /* cycle through any arguments     */
476             deRef(tyv,t,o);
477             if (anyGenerics(arg(t),o))
478                 return TRUE;
479         }
480         deRef(tyv,t,o);
481         if (tyv) {
482             if (tyv->offs == FIXED_TYVAR) {
483                 numFixedVars++;
484                 return FALSE;
485             }
486             else
487                 return TRUE;
488         }
489         else
490             return FALSE;
491     }
492 }
493
494 static List local elimOuterPreds(sps)   /* Simplify and defer any remaining*/
495 List sps; {                             /* preds that contain no generics. */
496     List qs = NIL;
497     elimTauts();
498     for (preds=scSimplify(preds); nonNull(preds); ) {
499         Cell pi = hd(preds);
500         Cell nx = tl(preds);
501         if (anyGenerics(fst3(pi),intOf(snd3(pi)))) {    /* Retain predicate*/
502             tl(preds) = qs;
503             qs        = preds;
504         }
505         else {                                          /* Defer predicate */
506             tl(preds) = sps;
507             sps       = preds;
508         }
509         preds = nx;
510     }
511     preds = qs;
512     return sps;
513 }
514
515 static List local elimPredsUsing(ps,sps)/* Try to discharge or defer preds,*/
516 List ps;                                /* splitting if necessary to match */
517 List sps; {                             /* context ps.  sps = savePreds.   */
518     List rems = NIL;
519     while (nonNull(preds)) {            /* Pick a predicate from preds     */
520         Cell p  = preds;
521         Cell pi = fst3(hd(p));
522         Int  o  = intOf(snd3(hd(p)));
523         Cell ev = entail(ps,pi,o,0);
524         preds   = tl(preds);
525
526         if (nonNull(ev))                /* Discharge if ps ||- (pi,o)      */
527             overEvid(thd3(hd(p)),ev);
528         else if (!anyGenerics(pi,o)) {  /* Defer if no generics            */
529             tl(p) = sps;
530             sps   = p;
531         }
532         else {                          /* Try to split generics and fixed */
533             Inst in;
534             if (numFixedVars>0 && nonNull(in=findInstFor(pi,o))) {
535                 List qs = inst(in).specifics;
536                 for (ev=inst(in).builder; nonNull(qs); qs=tl(qs))
537                     ev = ap(ev,assumeEvid(hd(qs),typeOff));
538                 overEvid(thd3(hd(p)),ev);
539             }
540             else {                      /* No worthwhile progress possible */
541                 tl(p) = rems;
542                 rems  = p;
543             }
544         }
545     }
546     preds = rems;                       /* Return any remaining predicates */
547     return sps;
548 }
549
550 static Void local reducePreds() {       /* Context reduce predicates: uggh!*/
551     List rems = NIL;                    /* (A last resort for defaulting)  */
552     while (nonNull(preds)) {            /* Pick a predicate from preds     */
553         Cell p  = preds;
554         Cell pi = fst3(hd(p));
555         Int  o  = intOf(snd3(hd(p)));
556         Inst in = findInstFor(pi,o);
557         preds   = tl(preds);
558         if (nonNull(in)) {
559             List qs = inst(in).specifics;
560             Cell ev = inst(in).builder;
561             for (; nonNull(qs); qs=tl(qs))
562                 ev = ap(ev,assumeEvid(hd(qs),typeOff));
563             overEvid(thd3(hd(p)),ev);
564         }
565         else {                          /* No worthwhile progress possible */
566             tl(p) = rems;
567             rems  = p;
568         }
569     }
570     preds = scSimplify(rems);           /* Return any remaining predicates */
571 }
572
573 static Void local normPreds(line)       /* Normalize each element of preds */
574 Int line; {                             /* in some appropriate manner      */
575 #if TREX
576     List ps = preds;
577     List pr = NIL;
578     while (nonNull(ps)) {
579         Cell pi = fst3(hd(ps));
580         Cell ev = thd3(hd(ps));
581         if (isAp(pi) && isExt(fun(pi))) {
582             Cell r = lacksNorm(arg(pi),intOf(snd3(hd(ps))),fun(pi));
583             if (isNull(r)) {
584                 ERRMSG(line) "Cannot satisfy constraint " ETHEN
585                 ERRPRED(copyPred(pi,intOf(snd3(hd(ps)))));
586                 ERRTEXT      "\n"
587                 EEND;
588             }
589             else if (isInt(r)) {
590                 overEvid(ev,r);
591                 ps = tl(ps);
592                 if (isNull(pr))
593                     preds  = ps;
594                 else
595                     tl(pr) = ps;
596             }
597             else if (intOf(snd(r))!=0) {
598                 Cell nd  = inventDictVar();
599                 Cell ev1 = ap2(nameAddEv,snd(r),nd);
600                 pi       = ap(fun(pi),aVar);
601                 hd(ps)   = triple(pi,fst(r),nd);
602                 overEvid(ev,ev1);
603                 pr       = ps;
604                 ps       = tl(ps);
605             }
606             else {
607                 fst3(hd(ps)) = ap(fun(pi),fst(r));
608                 pr = ps;
609                 ps = tl(ps);
610             }
611         }
612         else {
613             pr = ps;
614             ps = tl(ps);
615         }
616     }
617 #endif
618 }
619
620 /* --------------------------------------------------------------------------
621  * Mechanisms for dealing with defaults:
622  * ------------------------------------------------------------------------*/
623
624 static Bool local resolveDefs(vs)       /* Attempt to resolve defaults  */
625 List vs; {                              /* for variables vs subject to  */
626     List pvs       = NIL;               /* constraints in preds         */
627     List qs        = preds;
628     Bool defaulted = FALSE;
629
630 #ifdef DEBUG_DEFAULTS
631     Printf("Attempt to resolve variables ");
632     printExp(stdout,vs);
633     Printf(" with context ");
634     printContext(stdout,copyPreds(preds));
635     Printf("\n");
636 #endif
637
638     resetGenerics();                    /* find type variables in ps    */
639     for (; nonNull(qs); qs=tl(qs)) {
640         Cell pi = fst3(hd(qs));
641         Int  o  = intOf(snd3(hd(qs)));
642         for (; isAp(pi); pi=fun(pi))
643             pvs = genvarType(arg(pi),o,pvs);
644     }
645
646     for (; nonNull(pvs); pvs=tl(pvs)) { /* now try defaults             */
647         Int vn = intOf(hd(pvs));
648
649 #ifdef DEBUG_DEFAULTS
650         Printf("is var %d included in ",vn);
651         printExp(stdout,vs);
652         Printf("?\n");
653 #endif
654
655         if (!intIsMember(vn,vs))
656             defaulted |= resolveVar(vn);
657 #ifdef DEBUG_DEFAULTS
658         else
659             Printf("Yes, so no ambiguity!\n");
660 #endif
661     }
662
663     return defaulted;
664 }
665
666 static Bool local resolveVar(vn)        /* Determine whether an ambig.  */
667 Int  vn; {                              /* variable vn can be resolved  */
668     List ps        = preds;             /* by default in the context of */
669     List cs        = NIL;               /* the predicates in ps         */
670     Bool aNumClass = FALSE;
671
672     if (tyvar(vn)->bound == SKOLEM)
673         return FALSE;
674
675     /* According to the Haskell definition, we can only default an ambiguous
676      * variable if the set of classes that constrain it:
677      *   (a) includes at least one numeric class.
678      *   (b) includes only numeric or standard classes.
679      * In addition, we will not allow a variable to be defaulted unless it
680      * appears only in predicates of the form (Class var).
681      */
682
683 #ifdef DEBUG_DEFAULTS
684     Printf("Trying to default variable %d\n",vn);
685 #endif
686
687     for (; nonNull(ps); ps=tl(ps)) {
688         Cell  pi = hd(ps);
689         Class c  = classConstraining(vn,fst3(pi),intOf(snd3(pi)));
690         if (nonNull(c)) {
691             if (c==classRealFrac   || c==classRealFloat ||
692                 c==classFractional || c==classFloating  ||
693                 c==classReal       || c==classIntegral  || c==classNum)
694                 aNumClass = TRUE;
695             else if (c!=classEq    && c!=classOrd  && c!=classShow &&
696                      c!=classRead  && c!=classIx   && c!=classEnum &&
697                      c!=classBounded)
698                 return FALSE;
699
700             {   Type  t = arg(fst3(pi));/* Check for single var as arg     */
701                 Int   o = intOf(snd3(pi));
702                 Tyvar *tyv;
703                 deRef(tyv,t,o);
704                 if (!tyv || tyvNum(tyv)!=vn)
705                     return FALSE;
706             }
707             if (!cellIsMember(c,cs))
708                 cs = cons(c,cs);
709         }
710     }
711
712     /* Now find the first class (if any) in the list of defaults that
713      * is an instance of all of the required classes.
714      *
715      * If we get this far, then cs only mentions classes from the list
716      * above, all of which have only a single parameter of kind *.
717      */
718
719     if (aNumClass) {
720         List ds = defaultDefns;         /* N.B. guaranteed to be monotypes */
721 #ifdef DEBUG_DEFAULTS
722         Printf("Default conditions met, looking for type\n");
723 #endif
724         for (; nonNull(ds); ds=tl(ds)) {
725             List cs1 = cs;
726             while (nonNull(cs1) && nonNull(entail(NIL,ap(hd(cs1),hd(ds)),0,0)))
727                 cs1 = tl(cs1);
728             if (isNull(cs1)) {
729                 bindTv(vn,hd(ds),0);
730 #ifdef DEBUG_DEFAULTS
731                 Printf("Default type for variable %d is ",vn);
732                 printType(stdout,hd(ds));
733                 Printf("\n");
734 #endif
735                 return TRUE;
736             }
737         }
738     }
739
740 #ifdef DEBUG_DEFAULTS
741     Printf("No default permitted/found\n");
742 #endif
743     return FALSE;
744 }
745
746 static Class local classConstraining(vn,pi,o)
747 Int  vn;                                /* Return class constraining var*/
748 Cell pi;                                /* vn in predicate pi, or NIL if*/
749 Int  o; {                               /* vn is not involved           */
750     for (; isAp(pi); pi=fun(pi))
751         if (!doesntOccurIn(tyvar(vn),arg(pi),o))
752             return getHead(pi);
753     return NIL;
754 }
755
756 /*-------------------------------------------------------------------------*/