[project @ 1999-11-17 16:57:38 by andy]
[ghc-hetmet.git] / ghc / interpreter / type.c
1
2 /* --------------------------------------------------------------------------
3  * This is the Hugs type checker
4  *
5  * The Hugs 98 system is Copyright (c) Mark P Jones, Alastair Reid, the
6  * Yale Haskell Group, and the Oregon Graduate Institute of Science and
7  * Technology, 1994-1999, All rights reserved.  It is distributed as
8  * free software under the license in the file "License", which is
9  * included in the distribution.
10  *
11  * $RCSfile: type.c,v $
12  * $Revision: 1.13 $
13  * $Date: 1999/11/17 16:57:50 $
14  * ------------------------------------------------------------------------*/
15
16 #include "prelude.h"
17 #include "storage.h"
18 #include "backend.h"
19 #include "connect.h"
20 #include "link.h"
21 #include "errors.h"
22 #include "subst.h"
23 #include "Assembler.h" /* for AsmCTypes */
24
25 /*#define DEBUG_TYPES*/
26 /*#define DEBUG_KINDS*/
27 /*#define DEBUG_DEFAULTS*/
28 /*#define DEBUG_SELS*/
29 /*#define DEBUG_DEPENDS*/
30 /*#define DEBUG_DERIVING*/
31 /*#define DEBUG_CODE*/
32
33 Bool catchAmbigs       = FALSE;         /* TRUE => functions with ambig.   */
34                                         /*         types produce error     */
35
36
37 /* --------------------------------------------------------------------------
38  * Local function prototypes:
39  * ------------------------------------------------------------------------*/
40
41 static Void   local emptyAssumption   Args((Void));
42 static Void   local enterBindings     Args((Void));
43 static Void   local leaveBindings     Args((Void));
44 static Int    local defType           Args((Cell));
45 static Type   local useType           Args((Cell));
46 static Void   local markAssumList     Args((List));
47 static Cell   local findAssum         Args((Text));
48 static Pair   local findInAssumList   Args((Text,List));
49 static List   local intsIntersect     Args((List,List));
50 static List   local genvarAllAss      Args((List));
51 static List   local genvarAnyAss      Args((List));
52 static Int    local newVarsBind       Args((Cell));
53 static Void   local newDefnBind       Args((Cell,Type));
54
55 static Void   local enterPendingBtyvs Args((Void));
56 static Void   local leavePendingBtyvs Args((Void));
57 static Cell   local patBtyvs          Args((Cell));
58 static Void   local doneBtyvs         Args((Int));
59 static Void   local enterSkolVars     Args((Void));
60 static Void   local leaveSkolVars     Args((Int,Type,Int,Int));
61
62 static Void   local typeError         Args((Int,Cell,Cell,String,Type,Int));
63 static Void   local reportTypeError   Args((Int,Cell,Cell,String,Type,Type));
64 static Void   local cantEstablish     Args((Int,String,Cell,Type,List));
65 static Void   local tooGeneral        Args((Int,Cell,Type,Type));
66
67 static Cell   local typeExpr          Args((Int,Cell));
68
69 static Cell   local typeAp            Args((Int,Cell));
70 static Type   local typeExpected      Args((Int,String,Cell,Type,Int,Int,Bool));
71 static Void   local typeAlt           Args((String,Cell,Cell,Type,Int,Int));
72 static Int    local funcType          Args((Int));
73 static Void   local typeCase          Args((Int,Int,Cell));
74 static Void   local typeComp          Args((Int,Type,Cell,List));
75 static Cell   local typeMonadComp     Args((Int,Cell));
76 static Void   local typeDo            Args((Int,Cell));
77 static Void   local typeConFlds       Args((Int,Cell));
78 static Void   local typeUpdFlds       Args((Int,Cell));
79 #if IPARAM
80 static Cell   local typeWith          Args((Int,Cell));
81 #endif
82 static Cell   local typeFreshPat      Args((Int,Cell));
83
84 static Void   local typeBindings      Args((List));
85 static Void   local removeTypeSigs    Args((Cell));
86
87 static Void   local monorestrict      Args((List));
88 static Void   local restrictedBindAss Args((Cell));
89 static Void   local restrictedAss     Args((Int,Cell,Type));
90
91 static Void   local unrestricted      Args((List));
92 static List   local itbscc            Args((List));
93 static Void   local addEvidParams     Args((List,Cell));
94
95 static Void   local typeClassDefn     Args((Class));
96 static Void   local typeInstDefn      Args((Inst));
97 static Void   local typeMember        Args((String,Name,Cell,List,Cell,Int));
98
99 static Void   local typeBind          Args((Cell));
100 static Void   local typeDefAlt        Args((Int,Cell,Pair));
101 static Cell   local typeRhs           Args((Cell));
102 static Void   local guardedType       Args((Int,Cell));
103
104 static Void   local genBind           Args((List,Cell));
105 static Void   local genAss            Args((Int,List,Cell,Type));
106 static Type   local genTest           Args((Int,Cell,List,Type,Type,Int));
107 static Type   local generalize        Args((List,Type));
108 static Bool   local equalTypes        Args((Type,Type));
109
110 static Void   local typeDefnGroup     Args((List));
111 static Pair   local typeSel           Args((Name));
112
113
114
115 /* --------------------------------------------------------------------------
116  * Assumptions:
117  *
118  * A basic typing statement is a pair (Var,Type) and an assumption contains
119  * an ordered list of basic typing statements in which the type for a given
120  * variable is given by the most recently added assumption about that var.
121  *
122  * In practice, the assumption set is split between a pair of lists, one
123  * holding assumptions for vars defined in bindings, the other for vars
124  * defined in patterns/binding parameters etc.  The reason for this
125  * separation is that vars defined in bindings may be overloaded (with the
126  * overloading being unknown until the whole binding is typed), whereas the
127  * vars defined in patterns have no overloading.  A form of dependency
128  * analysis (at least as far as calculating dependents within the same group
129  * of value bindings) is required to implement this.  Where it is known that
130  * no overloaded values are defined in a binding (i.e., when the `dreaded
131  * monomorphism restriction' strikes), the list used to record dependents
132  * is flagged with a NODEPENDS tag to avoid gathering dependents at that
133  * level.
134  *
135  * To interleave between vars for bindings and vars for patterns, we use
136  * a list of lists of typing statements for each.  These lists are always
137  * the same length.  The implementation here is very similar to that of the
138  * dependency analysis used in the static analysis component of this system.
139  *
140  * To deal with polymorphic recursion, variables defined in bindings can be
141  * assigned types of the form (POLYREC,(def,use)), where def is a type
142  * variable for the type of the defining occurence, and use is a type
143  * scheme for (recursive) calls/uses of the variable.
144  * ------------------------------------------------------------------------*/
145
146 static List defnBounds;                 /*::[[(Var,Type)]] possibly ovrlded*/
147 static List varsBounds;                 /*::[[(Var,Type)]] not overloaded  */
148 static List depends;                    /*::[?[Var]] dependents/NODEPENDS  */
149 static List skolVars;                   /*::[[Var]] skolem vars            */
150 static List localEvs;                   /*::[[(Pred,offset,ev)]]           */
151 static List savedPs;                    /*::[[(Pred,offset,ev)]]           */
152 static Cell dummyVar;                   /* Used to put extra tvars into ass*/
153
154 #define saveVarsAss()     List saveAssump = hd(varsBounds)
155 #define restoreVarsAss()  hd(varsBounds)  = saveAssump
156 #define addVarAssump(v,t) hd(varsBounds)  = cons(pair(v,t),hd(varsBounds))
157 #define findTopBinding(v) findInAssumList(textOf(v),hd(defnBounds))
158
159 static Void local emptyAssumption() {   /* set empty type assumption       */
160     defnBounds = NIL;
161     varsBounds = NIL;
162     depends    = NIL;
163     skolVars   = NIL;
164     localEvs   = NIL;
165     savedPs    = NIL;
166 }
167
168 static Void local enterBindings() {    /* Add new level to assumption sets */
169     defnBounds = cons(NIL,defnBounds);
170     varsBounds = cons(NIL,varsBounds);
171     depends    = cons(NIL,depends);
172 }
173
174 static Void local leaveBindings() {    /* Drop one level of assumptions    */
175     defnBounds = tl(defnBounds);
176     varsBounds = tl(varsBounds);
177     depends    = tl(depends);
178 }
179
180 static Int local defType(a)             /* Return type for defining occ.   */
181 Cell a; {                               /* of a var from assumption pair  */
182     return (isPair(a) && fst(a)==POLYREC) ? fst(snd(a)) : a;
183 }
184
185 static Type local useType(a)            /* Return type for use of a var    */
186 Cell a; {                               /* defined in an assumption        */
187     return (isPair(a) && fst(a)==POLYREC) ? snd(snd(a)) : a;
188 }
189
190 static Void local markAssumList(as)     /* Mark all types in assumption set*/
191 List as; {                              /* :: [(Var, Type)]                */
192     for (; nonNull(as); as=tl(as)) {    /* No need to mark generic types;  */
193         Type t = defType(snd(hd(as)));  /* the only free variables in those*/
194         if (!isPolyType(t))             /* must have been free earlier too */
195             markType(t,0);
196     }
197 }
198
199 static Cell local findAssum(t)         /* Find most recent assumption about*/
200 Text t; {                              /* variable named t, if any         */
201     List defnBounds1 = defnBounds;     /* return translated variable, with */
202     List varsBounds1 = varsBounds;     /* type in typeIs                   */
203     List depends1    = depends;
204
205     while (nonNull(defnBounds1)) {
206         Pair ass = findInAssumList(t,hd(varsBounds1));/* search varsBounds */
207         if (nonNull(ass)) {
208             typeIs = snd(ass);
209             return fst(ass);
210         }
211
212         ass = findInAssumList(t,hd(defnBounds1));     /* search defnBounds */
213         if (nonNull(ass)) {
214             Cell v = fst(ass);
215             typeIs = snd(ass);
216
217             if (hd(depends1)!=NODEPENDS &&            /* save dependent?   */
218                   isNull(v=varIsMember(t,hd(depends1))))
219                 /* N.B. make new copy of variable and store this on list of*/
220                 /* dependents, and in the assumption so that all uses of   */
221                 /* the variable will be at the same node, if we need to    */
222                 /* overwrite the call of a function with a translation...  */
223                 hd(depends1) = cons(v=mkVar(t),hd(depends1));
224
225             return v;
226         }
227
228         defnBounds1 = tl(defnBounds1);                /* look in next level*/
229         varsBounds1 = tl(varsBounds1);                /* of assumption set */
230         depends1    = tl(depends1);
231     }
232     return NIL;
233 }
234
235 static Pair local findInAssumList(t,as)/* Search for assumption for var    */
236 Text t;                                /* named t in list of assumptions as*/
237 List as; {
238     for (; nonNull(as); as=tl(as))
239         if (textOf(fst(hd(as)))==t)
240             return hd(as);
241     return NIL;
242 }
243
244 static List local intsIntersect(as,bs)  /* calculate intersection of lists */
245 List as, bs; {                          /* of integers (as sets)           */
246     List ts = NIL;                      /* destructively modifies as       */
247     while (nonNull(as))
248         if (intIsMember(intOf(hd(as)),bs)) {
249             List temp = tl(as);
250             tl(as)    = ts;
251             ts        = as;
252             as        = temp;
253         }
254         else
255             as = tl(as);
256     return ts;
257 }
258
259 static List local genvarAllAss(as)      /* calculate generic vars that are */
260 List as; {                              /* in every type in assumptions as */
261     List vs = genvarTyvar(intOf(defType(snd(hd(as)))),NIL);
262     for (as=tl(as); nonNull(as) && nonNull(vs); as=tl(as))
263         vs = intsIntersect(vs,genvarTyvar(intOf(defType(snd(hd(as)))),NIL));
264     return vs;
265 }
266
267 static List local genvarAnyAss(as)      /* calculate generic vars that are */
268 List as; {                              /* in any type in assumptions as   */
269     List vs = genvarTyvar(intOf(defType(snd(hd(as)))),NIL);
270     for (as=tl(as); nonNull(as); as=tl(as))
271         vs = genvarTyvar(intOf(defType(snd(hd(as)))),vs);
272     return vs;
273 }
274
275 static Int local newVarsBind(v)        /* make new assump for pattern var  */
276 Cell v; {
277     Int beta = newTyvars(1);
278     addVarAssump(v,mkInt(beta));
279 #ifdef DEBUG_TYPES
280     Printf("variable, assume ");
281     printExp(stdout,v);
282     Printf(" :: _%d\n",beta);
283 #endif
284     return beta;
285 }
286
287 static Void local newDefnBind(v,type)  /* make new assump for defn var     */
288 Cell v;                                /* and set type if given (nonNull)  */
289 Type type; {
290     Int  beta      = newTyvars(1);
291     Cell ta        = mkInt(beta);
292     instantiate(type);
293     if (nonNull(type) && isPolyType(type))
294         ta = pair(POLYREC,pair(ta,type));
295     hd(defnBounds) = cons(pair(v,ta), hd(defnBounds));
296 #ifdef DEBUG_TYPES
297     Printf("definition, assume ");
298     printExp(stdout,v);
299     Printf(" :: _%d\n",beta);
300 #endif
301     bindTv(beta,typeIs,typeOff);       /* Bind beta to new type skeleton   */
302 }
303
304 /* --------------------------------------------------------------------------
305  * Predicates:
306  * ------------------------------------------------------------------------*/
307
308 #include "preds.c"
309
310 /* --------------------------------------------------------------------------
311  * Bound and skolemized type variables:
312  * ------------------------------------------------------------------------*/
313
314 static List pendingBtyvs = NIL;
315
316 static Void local enterPendingBtyvs() {
317     enterBtyvs();
318     pendingBtyvs = cons(NIL,pendingBtyvs);
319 }
320
321 static Void local leavePendingBtyvs() {
322     List pts     = hd(pendingBtyvs);
323     pendingBtyvs = tl(pendingBtyvs);
324     for (; nonNull(pts); pts=tl(pts)) {
325         Int  line = intOf(fst(hd(pts)));
326         List vs   = snd(hd(pts));
327         Int  i    = 0;
328         clearMarks();
329         for (; nonNull(vs); vs=tl(vs)) {
330             Cell v = fst(hd(vs));
331             Cell t = copyTyvar(intOf(snd(hd(vs))));
332             if (!isOffset(t)) {
333                 ERRMSG(line) "Type annotation uses variable " ETHEN ERREXPR(v);
334                 ERRTEXT      " where a more specific type "   ETHEN ERRTYPE(t);
335                 ERRTEXT      " was inferred"
336                 EEND;
337             }
338             else if (offsetOf(t)!=i) {
339                 List us = snd(hd(pts));
340                 Int  j  = offsetOf(t);
341                 if (j>=i)
342                     internal("leavePendingBtyvs");
343                 for (; j>0; j--)
344                     us = tl(us);
345                 ERRMSG(line) "Type annotation uses distinct variables " ETHEN
346                 ERREXPR(v);  ERRTEXT " and " ETHEN ERREXPR(fst(hd(us)));
347                 ERRTEXT      " where a single variable was inferred"
348                 EEND;
349             }
350             else
351                 i++;
352         }
353     }
354     leaveBtyvs();
355 }
356
357 static Cell local patBtyvs(p)           /* Strip bound type vars from pat  */
358 Cell p; {
359     if (whatIs(p)==BIGLAM) {
360         List bts = hd(btyvars) = fst(snd(p));
361         for (p=snd(snd(p)); nonNull(bts); bts=tl(bts)) {
362             Int beta          = newTyvars(1);
363             tyvar(beta)->kind = snd(hd(bts));
364             snd(hd(bts))      = mkInt(beta);
365         }
366     }
367     return p;
368 }
369
370 static Void local doneBtyvs(l)
371 Int l; {
372     if (nonNull(hd(btyvars))) {         /* Save bound tyvars               */
373         hd(pendingBtyvs) = cons(pair(mkInt(l),hd(btyvars)),hd(pendingBtyvs));
374         hd(btyvars)      = NIL;
375     }
376 }
377
378 static Void local enterSkolVars() {
379     skolVars = cons(NIL,skolVars);
380     localEvs = cons(NIL,localEvs);
381     savedPs  = cons(preds,savedPs);
382     preds    = NIL;
383 }
384
385 static Void local leaveSkolVars(l,t,o,m)
386 Int  l;
387 Type t;
388 Int  o;
389 Int  m; {
390     if (nonNull(hd(localEvs))) {        /* Check for local predicates      */
391         List sks = hd(skolVars);
392         List sps = NIL;
393         if (isNull(sks)) {
394             internal("leaveSkolVars");
395         }
396         markAllVars();                  /* Mark all variables in current   */
397         do {                            /* substitution, then unmark sks.  */
398             tyvar(intOf(fst(hd(sks))))->offs = UNUSED_GENERIC;
399             sks = tl(sks);
400         } while (nonNull(sks));
401         normPreds(l);
402         sps   = elimPredsUsing(hd(localEvs),sps);
403         preds = revOnto(preds,sps);
404     }
405
406     if (nonNull(hd(skolVars))) {        /* Check that Skolem vars do not   */
407         List vs;                        /* escape their scope              */
408         Int  i = 0;
409
410         clearMarks();                   /* Look for occurences in the      */
411         for (; i<m; i++)                /* inferred type                   */
412             markTyvar(o+i);
413         markType(t,o);
414
415         for (vs=hd(skolVars); nonNull(vs); vs=tl(vs)) {
416             Int vn = intOf(fst(hd(vs)));
417             if (tyvar(vn)->offs == FIXED_TYVAR) {
418                 Cell tv = copyTyvar(vn);
419                 Type ty = liftRank2(t,o,m);
420                 ERRMSG(l) "Existentially quantified variable in inferred type"
421                 ETHEN
422                 ERRTEXT   "\n*** Variable     : " ETHEN ERRTYPE(tv);
423                 ERRTEXT   "\n*** From pattern : " ETHEN ERREXPR(snd(hd(vs)));
424                 ERRTEXT   "\n*** Result type  : " ETHEN ERRTYPE(ty);
425                 ERRTEXT   "\n"
426                 EEND;
427             }
428         }
429
430         markBtyvs();                    /* Now check assumptions           */
431         mapProc(markAssumList,defnBounds);
432         mapProc(markAssumList,varsBounds);
433
434         for (vs=hd(skolVars); nonNull(vs); vs=tl(vs)) {
435             Int vn = intOf(fst(hd(vs)));
436             if (tyvar(vn)->offs == FIXED_TYVAR) {
437                 ERRMSG(l)
438                   "Existentially quantified variable escapes from pattern "
439                 ETHEN ERREXPR(snd(hd(vs)));
440                 ERRTEXT "\n"
441                 EEND;
442             }
443         }
444     }
445     localEvs = tl(localEvs);
446     skolVars = tl(skolVars);
447     preds    = revOnto(preds,hd(savedPs));
448     savedPs  = tl(savedPs);
449 }
450
451 /* --------------------------------------------------------------------------
452  * Type errors:
453  * ------------------------------------------------------------------------*/
454
455 static Void local typeError(l,e,in,wh,t,o)
456 Int    l;                             /* line number near type error       */
457 String wh;                            /* place in which error occurs       */
458 Cell   e;                             /* source of error                   */
459 Cell   in;                            /* context if any (NIL if not)       */
460 Type   t;                             /* should be of type (t,o)           */
461 Int    o; {                           /* type inferred is (typeIs,typeOff) */
462
463     clearMarks();                     /* types printed here are monotypes  */
464                                       /* use marking to give sensible names*/
465 #ifdef DEBUG_KINDS
466 { List vs = genericVars;
467   for (; nonNull(vs); vs=tl(vs)) {
468      Int v = intOf(hd(vs));
469      Printf("%c :: ", ('a'+tyvar(v)->offs));
470      printKind(stdout,tyvar(v)->kind);
471      Putchar('\n');
472   }
473 }
474 #endif
475
476     reportTypeError(l,e,in,wh,copyType(typeIs,typeOff),copyType(t,o));
477 }
478
479 static Void local reportTypeError(l,e,in,wh,inft,expt)
480 Int    l;                               /* Error printing part of typeError*/
481 Cell   e, in;
482 String wh;
483 Type   inft, expt; {
484     ERRMSG(l)   "Type error in %s", wh    ETHEN
485     if (nonNull(in)) {
486         ERRTEXT "\n*** Expression     : " ETHEN ERREXPR(in);
487     }
488     ERRTEXT     "\n*** Term           : " ETHEN ERREXPR(e);
489     ERRTEXT     "\n*** Type           : " ETHEN ERRTYPE(inft);
490     ERRTEXT     "\n*** Does not match : " ETHEN ERRTYPE(expt);
491     if (unifyFails) {
492         ERRTEXT "\n*** Because        : %s", unifyFails ETHEN
493     }
494     ERRTEXT "\n"
495     EEND;
496 }
497
498 #define shouldBe(l,e,in,where,t,o) if (!unify(typeIs,typeOff,t,o)) \
499                                        typeError(l,e,in,where,t,o);
500 #define check(l,e,in,where,t,o)    e=typeExpr(l,e); shouldBe(l,e,in,where,t,o)
501 #define inferType(t,o)             typeIs=t; typeOff=o
502 #if IPARAM
503 #define spTypeExpr(l,e)                 svPreds = preds; preds = NIL; e = typeExpr(l,e); preds = revOnto(preds,svPreds);
504 #define spCheck(l,e,in,where,t,o)       svPreds = preds; preds = NIL; check(l,e,in,where,t,o); preds = revOnto(preds,svPreds);
505 #else
506 #define spTypeExpr(l,e)                 e = typeExpr(l,e);
507 #define spCheck(l,e,in,where,t,o)       check(l,e,in,where,t,o);
508 #endif
509
510 static Void local cantEstablish(line,wh,e,t,ps)
511 Int    line;                            /* Complain when declared preds    */
512 String wh;                              /* are not sufficient to discharge */
513 Cell   e;                               /* or defer the inferred context.  */
514 Type   t;
515 List   ps; {
516     ERRMSG(line) "Cannot justify constraints in %s", wh ETHEN
517     ERRTEXT      "\n*** Expression    : " ETHEN ERREXPR(e);
518     ERRTEXT      "\n*** Type          : " ETHEN ERRTYPE(t);
519     ERRTEXT      "\n*** Given context : " ETHEN ERRCONTEXT(ps);
520     ERRTEXT      "\n*** Constraints   : " ETHEN ERRCONTEXT(copyPreds(preds));
521     ERRTEXT "\n"
522     EEND;
523 }
524
525 static Void local tooGeneral(l,e,dt,it) /* explicit type sig. too general  */
526 Int  l;
527 Cell e;
528 Type dt, it; {
529     ERRMSG(l) "Inferred type is not general enough" ETHEN
530     ERRTEXT   "\n*** Expression    : " ETHEN ERREXPR(e);
531     ERRTEXT   "\n*** Expected type : " ETHEN ERRTYPE(dt);
532     ERRTEXT   "\n*** Inferred type : " ETHEN ERRTYPE(it);
533     ERRTEXT   "\n"
534     EEND;
535 }
536
537 /* --------------------------------------------------------------------------
538  * Typing of expressions:
539  * ------------------------------------------------------------------------*/
540
541 #define EXPRESSION  0                   /* type checking expression        */
542 #define NEW_PATTERN 1                   /* pattern, introducing new vars   */
543 #define OLD_PATTERN 2                   /* pattern, involving bound vars   */
544 static int tcMode = EXPRESSION;
545
546 #ifdef DEBUG_TYPES
547 static Cell local mytypeExpr    Args((Int,Cell));
548 static Cell local typeExpr(l,e)
549 Int l;
550 Cell e; {
551     static int number = 0;
552     Cell retv;
553     int  mynumber = number++;
554     List ps;
555     STACK_CHECK
556     Printf("%d) to check: ",mynumber);
557     printExp(stdout,e);
558     Putchar('\n');
559     retv = mytypeExpr(l,e);
560     Printf("%d) result: ",mynumber);
561     printType(stdout,debugType(typeIs,typeOff));
562     Printf("\n%d) preds: ",mynumber);
563     printContext(stdout,debugContext(preds));
564     Putchar('\n');
565     return retv;
566 }
567 static Cell local mytypeExpr(l,e)       /* Determine type of expr/pattern  */
568 #else
569 static Cell local typeExpr(l,e)         /* Determine type of expr/pattern  */
570 #endif
571 Int  l;
572 Cell e; {
573     static String cond    = "conditional";
574     static String list    = "list";
575     static String discr   = "case discriminant";
576     static String aspat   = "as (@) pattern";
577     static String typeSig = "type annotation";
578     static String lambda  = "lambda expression";
579 #if IPARAM
580     List svPreds;
581 #endif
582
583     switch (whatIs(e)) {
584
585         /* The following cases can occur in either pattern or expr. mode   */
586
587         case AP         :
588         case NAME       :
589         case VAROPCELL  :
590         case VARIDCELL  :
591 #if IPARAM
592         case IPVAR      :
593 #endif
594                           return typeAp(l,e);
595
596         case TUPLE      : typeTuple(e);
597                           break;
598
599         case BIGCELL    : {   Int alpha = newTyvars(1);
600                               inferType(aVar,alpha);
601                               return ap(ap(nameFromInteger,
602                                            assumeEvid(predNum,alpha)),
603                                            e);
604                           }
605
606         case INTCELL    : {   Int alpha = newTyvars(1);
607                               inferType(aVar,alpha);
608                               return ap(ap(nameFromInt,
609                                            assumeEvid(predNum,alpha)),
610                                            e);
611                           }
612
613         case FLOATCELL  : {   Int alpha = newTyvars(1);
614                               inferType(aVar,alpha);
615                               return ap(ap(nameFromDouble,
616                                            assumeEvid(predFractional,alpha)),
617                                            e);
618                           }
619
620         case STRCELL    : inferType(typeString,0);
621                           break;
622
623         case CHARCELL   : inferType(typeChar,0);
624                           break;
625
626         case CONFLDS    : typeConFlds(l,e);
627                           break;
628
629         case ESIGN      : snd(snd(e)) = localizeBtyvs(snd(snd(e)));
630                           return typeExpected(l,typeSig,
631                                               fst(snd(e)),snd(snd(e)),
632                                               0,0,FALSE);
633
634 #if TREX
635         case EXT        : {   Int beta = newTyvars(2);
636                               Cell pi  = ap(e,aVar);
637                               Type t   = fn(aVar,
638                                          fn(ap(typeRec,bVar),
639                                             ap(typeRec,ap(ap(e,aVar),bVar))));
640                               tyvar(beta+1)->kind = ROW;
641                               inferType(t,beta);
642                               return ap(e,assumeEvid(pi,beta+1));
643                           }
644 #endif
645
646         /* The following cases can only occur in expr mode                 */
647
648         case UPDFLDS    : typeUpdFlds(l,e);
649                           break;
650
651 #if IPARAM
652         case WITHEXP    : return typeWith(l,e);
653 #endif
654
655         case COND       : {   Int beta = newTyvars(1);
656                               check(l,fst3(snd(e)),e,cond,typeBool,0);
657                               spCheck(l,snd3(snd(e)),e,cond,aVar,beta);
658                               spCheck(l,thd3(snd(e)),e,cond,aVar,beta);
659                               tyvarType(beta);
660                           }
661                           break;
662
663         case LETREC     : enterBindings();
664                           enterSkolVars();
665                           mapProc(typeBindings,fst(snd(e)));
666                           spTypeExpr(l,snd(snd(e)));
667                           leaveBindings();
668                           leaveSkolVars(l,typeIs,typeOff,0);
669                           break;
670
671         case FINLIST    : {   Int  beta = newTyvars(1);
672                               List xs;
673                               for (xs=snd(e); nonNull(xs); xs=tl(xs)) {
674                                  spCheck(l,hd(xs),e,list,aVar,beta);
675                               }
676                               inferType(listof,beta);
677                           }
678                           break;
679
680         case DOCOMP     : typeDo(l,e);
681                           break;
682
683         case COMP       : return typeMonadComp(l,e);
684
685         case CASE       : {    Int beta = newTyvars(2);    /* discr result */
686                                check(l,fst(snd(e)),NIL,discr,aVar,beta);
687                                map2Proc(typeCase,l,beta,snd(snd(e)));
688                                tyvarType(beta+1);
689                           }
690                           break;
691
692         case LAMBDA     : {   Int beta = newTyvars(1);
693                               enterPendingBtyvs();
694                               typeAlt(lambda,e,snd(e),aVar,beta,1);
695                               leavePendingBtyvs();
696                               tyvarType(beta);
697                           }
698                           break;
699
700 #if TREX
701         case RECSEL     : {   Int beta = newTyvars(2);
702                               Cell pi  = ap(snd(e),aVar);
703                               Type t   = fn(ap(typeRec,
704                                                ap(ap(snd(e),aVar),
705                                                             bVar)),aVar);
706                               tyvar(beta+1)->kind = ROW;
707                               inferType(t,beta);
708                               return ap(e,assumeEvid(pi,beta+1));
709                           }
710 #endif
711
712         /* The remaining cases can only occur in pattern mode: */
713
714         case WILDCARD   : inferType(aVar,newTyvars(1));
715                           break;
716
717         case ASPAT      : {   Int beta = newTyvars(1);
718                               snd(snd(e)) = typeExpr(l,snd(snd(e)));
719                               bindTv(beta,typeIs,typeOff);
720                               check(l,fst(snd(e)),e,aspat,aVar,beta);
721                               tyvarType(beta);
722                           }
723                           break;
724
725         case LAZYPAT    : snd(e) = typeExpr(l,snd(e));
726                           break;
727
728 #if NPLUSK
729         case ADDPAT     : {   Int alpha = newTyvars(1);
730                               inferType(typeVarToVar,alpha);
731                               return ap(e,assumeEvid(predIntegral,alpha));
732                           }
733 #endif
734
735         default         : internal("typeExpr");
736    }
737
738    return e;
739 }
740
741 /* --------------------------------------------------------------------------
742  * Typing rules for particular special forms:
743  * ------------------------------------------------------------------------*/
744
745 static Cell local typeAp(l,e)           /* Type check application, which   */
746 Int  l;                                 /* may be headed with a variable   */
747 Cell e; {                               /* requires polymorphism, qualified*/
748     static String app = "application";  /* types, and possible rank2 args. */
749     Cell h = getHead(e);
750     Int  n = argCount;
751     Cell p = NIL;
752     Cell a = e;
753     Int  i;
754 #if IPARAM
755     List svPreds;
756 #endif
757
758     switch (whatIs(h)) {
759         case NAME      : typeIs = name(h).type;
760                          break;
761
762         case VAROPCELL :
763         case VARIDCELL : if (tcMode==NEW_PATTERN) {
764                              inferType(aVar,newVarsBind(e));
765                          }
766                          else {
767                              Cell v = findAssum(textOf(h));
768                              if (nonNull(v)) {
769                                  h      = v;
770                                  typeIs = (tcMode==OLD_PATTERN)
771                                                 ? defType(typeIs)
772                                                 : useType(typeIs);
773                              }
774                              else {
775                                  h = findName(textOf(h));
776                                  if (isNull(h))
777                                      internal("typeAp0");
778                                  typeIs = name(h).type;
779                              }
780                          }
781                          break;
782
783 #if IPARAM
784         case IPVAR    : {   Text t    = textOf(h);
785                             Int alpha = newTyvars(1);
786                             Cell ip   = pair(ap(IPCELL,t),aVar);
787                             Cell ev   = assumeEvid(ip,alpha);
788                             typeIs    = mkInt(alpha);
789                             h         = ap(h,ev);
790                         }
791                         break;
792 #endif
793
794         default        : h = typeExpr(l,h);
795                          break;
796     }
797
798     if (isNull(typeIs)) {
799         internal("typeAp1");
800     }
801
802     instantiate(typeIs);                /* Deal with polymorphism ...      */
803     if (nonNull(predsAre)) {            /* ... and with qualified types.   */
804         List evs = NIL;
805         for (; nonNull(predsAre); predsAre=tl(predsAre)) {
806             evs = cons(assumeEvid(hd(predsAre),typeOff),evs);
807         }
808         if (!isName(h) || !isCfun(h)) {
809             h = applyToArgs(h,rev(evs));
810         }
811     }
812
813     if (whatIs(typeIs)==CDICTS) {       /* Deal with local dictionaries    */
814         List evs = makePredAss(fst(snd(typeIs)),typeOff);
815         List ps  = evs;
816         typeIs   = snd(snd(typeIs));
817         for (; nonNull(ps); ps=tl(ps)) {
818             h = ap(h,thd3(hd(ps)));
819         }
820         if (tcMode==EXPRESSION) {
821             preds = revOnto(evs,preds);
822         } else {
823             hd(localEvs) = revOnto(evs,hd(localEvs));
824         }
825     }
826
827     if (whatIs(typeIs)==EXIST) {        /* Deal with existential arguments */
828         Int n  = intOf(fst(snd(typeIs)));
829         typeIs = snd(snd(typeIs));
830         if (!isCfun(getHead(h)) || n>typeFree) {
831             internal("typeAp2");
832         } else if (tcMode!=EXPRESSION) {
833             Int alpha = typeOff + typeFree;
834             for (; n>0; n--) {
835                 bindTv(alpha-n,SKOLEM,0);
836                 hd(skolVars) = cons(pair(mkInt(alpha-n),e),hd(skolVars));
837             }
838         }
839     }
840
841     if (whatIs(typeIs)==RANK2) {        /* Deal with rank 2 arguments      */
842         Int  alpha = typeOff;
843         Int  m     = typeFree;
844         Int  nr2   = intOf(fst(snd(typeIs)));
845         Type body  = snd(snd(typeIs));
846         List as    = e;
847         Bool added = FALSE;
848
849         if (n<nr2) {                    /* Must have enough arguments      */
850             ERRMSG(l)   "Use of " ETHEN ERREXPR(h);
851             if (n>1) {
852                 ERRTEXT " in "    ETHEN ERREXPR(e);
853             }
854             ERRTEXT     " requires at least %d argument%s\n",
855                         nr2, (nr2==1 ? "" : "s")
856             EEND;
857         }
858
859         for (i=nr2; i<n; ++i)           /* Find rank two arguments         */
860             as = fun(as);
861
862         for (as=getArgs(as); nonNull(as); as=tl(as), body=arg(body)) {
863             Type expect = dropRank1(arg(fun(body)),alpha,m);
864             if (isPolyOrQualType(expect)) {
865                 if (tcMode==EXPRESSION)         /* poly/qual type in expr  */
866                     hd(as) = typeExpected(l,app,hd(as),expect,alpha,m,TRUE);
867                 else if (hd(as)!=WILDCARD) {    /* Pattern binding/match   */
868                     if (!isVar(hd(as))) {
869                         ERRMSG(l) "Argument "    ETHEN ERREXPR(arg(as));
870                         ERRTEXT   " in pattern " ETHEN ERREXPR(e);
871                         ERRTEXT   " where a variable is required\n"
872                         EEND;
873                     }
874                     if (tcMode==NEW_PATTERN) {  /* Pattern match           */
875                         if (m>0 && !added) {
876                             for (i=0; i<m; i++)
877                                 addVarAssump(dummyVar,mkInt(alpha+i));
878                             added = TRUE;
879                         }
880                         addVarAssump(hd(as),expect);
881                     }
882                     else {                      /* Pattern binding         */
883                         Text t = textOf(hd(as));
884                         Cell a = findInAssumList(t,hd(defnBounds));
885                         if (isNull(a))
886                             internal("typeAp3");
887                         instantiate(expect);
888                         if (nonNull(predsAre)) {
889                             ERRMSG(l) "Cannot use pattern binding for " ETHEN
890                             ERREXPR(hd(as));
891                             ERRTEXT   " as a component with a qualified type\n"
892                             EEND;
893                         }
894                         shouldBe(l,hd(as),e,app,aVar,intOf(defType(snd(a))));
895                     }
896                 }
897             }
898             else {                              /* Not a poly/qual type    */
899                 spCheck(l,hd(as),e,app,expect,alpha);
900             }
901             h = ap(h,hd(as));                   /* Save checked argument   */
902         }
903         inferType(body,alpha);
904         n -= nr2;
905     }
906
907     if (n>0) {                          /* Deal with remaining args        */
908         Int beta = funcType(n);         /* check h::t1->t2->...->tn->rn+1  */
909         shouldBe(l,h,e,app,aVar,beta);
910         for (i=n; i>0; --i) {           /* check e_i::t_i for each i       */
911             spCheck(l,arg(a),e,app,aVar,beta+2*i-1);
912             p = a;
913             a = fun(a);
914         }
915         tyvarType(beta+2*n);            /* Inferred type is r_n+1          */
916     }
917
918     if (isNull(p))                      /* Replace head with translation   */
919         e = h;
920     else
921         fun(p) = h;
922
923     return e;
924 }
925
926 static Cell local typeExpected(l,wh,e,reqd,alpha,n,addEvid)
927 Int    l;                               /* Type check expression e in wh   */
928 String wh;                              /* at line l, expecting type reqd, */
929 Cell   e;                               /* and treating vars alpha through */
930 Type   reqd;                            /* (alpha+n-1) as fixed.           */
931 Int    alpha;
932 Int    n;
933 Bool   addEvid; {                       /* TRUE => add \ev -> ...          */
934     List savePreds = preds;
935     Type t;
936     Int  o;
937     Int  m;
938     List ps;
939     Int  i;
940
941     instantiate(reqd);
942     t     = typeIs;
943     o     = typeOff;
944     m     = typeFree;
945     ps    = makePredAss(predsAre,o);
946
947     preds = NIL;
948     check(l,e,NIL,wh,t,o);
949     improve(l,ps,preds);
950
951     clearMarks();
952     mapProc(markAssumList,defnBounds);
953     mapProc(markAssumList,varsBounds);
954     mapProc(markPred,savePreds);
955     markBtyvs();
956
957     if (n > 0) {                  /* mark alpha thru alpha+n-1, plus any   */
958                                   /* type vars that are functionally       */
959         List us = NIL, vs = NIL;  /* dependent on them                     */
960         List fds = calcFunDepsPreds(preds);
961         for (i=0; i<n; i++) {
962             Type t1 = zonkTyvar(alpha+i);
963             us = zonkTyvarsIn(t1,us);
964         }
965         vs = oclose(fds,us);
966         for (; nonNull(vs); vs=tl(vs))
967             markTyvar(intOf(hd(vs)));
968     }
969
970     normPreds(l);
971     savePreds = elimPredsUsing(ps,savePreds);
972     if (nonNull(preds) && resolveDefs(genvarType(t,o,NIL)))
973         savePreds = elimPredsUsing(ps,savePreds);
974     if (nonNull(preds)) {
975         Type ty = copyType(t,o);
976         List qs = copyPreds(ps);
977         cantEstablish(l,wh,e,ty,qs);
978     }
979
980     resetGenerics();
981     for (i=0; i<m; i++)
982         if (copyTyvar(o+i)!=mkOffset(i)) {
983             List qs = copyPreds(ps);
984             Type it = copyType(t,o);
985             tooGeneral(l,e,reqd,generalize(qs,it));
986         }
987
988     if (addEvid) {
989         e     = qualifyExpr(l,ps,e);
990         preds = savePreds;
991     }
992     else
993         preds = revOnto(ps,savePreds);
994
995     inferType(t,o);
996     return e;
997 }
998
999 static Void local typeAlt(wh,e,a,t,o,m) /* Type check abstraction (Alt)    */
1000 String wh;                              /* a = ( [p1, ..., pn], rhs )      */
1001 Cell   e;
1002 Cell   a;
1003 Type   t;
1004 Int    o;
1005 Int    m; {
1006     Type origt = t;
1007     List ps    = fst(a) = patBtyvs(fst(a));
1008     Int  n     = length(ps);
1009     Int  l     = rhsLine(snd(a));
1010     Int  nr2   = 0;
1011     List as    = NIL;
1012     Bool added = FALSE;
1013
1014     saveVarsAss();
1015     enterSkolVars();
1016     if (whatIs(t)==RANK2) {
1017         if (n<(nr2=intOf(fst(snd(t))))) {
1018             ERRMSG(l) "Definition requires at least %d parameters on lhs",
1019                       intOf(fst(snd(t)))
1020             EEND;
1021         }
1022         t = snd(snd(t));
1023     }
1024
1025     while (getHead(t)==typeArrow && argCount==2 && nonNull(ps)) {
1026         Type ta = arg(fun(t));
1027         if (isPolyOrQualType(ta)) {
1028             if (hd(ps)!=WILDCARD) {
1029                 if (!isVar(hd(ps))) {
1030                    ERRMSG(l) "Argument " ETHEN ERREXPR(hd(ps));
1031                    ERRTEXT   " used where a variable or wildcard is required\n"
1032                    EEND;
1033                 }
1034                 if (m>0 && !added) {
1035                     Int i = 0;
1036                     for (; i<m; i++)
1037                         addVarAssump(dummyVar,mkInt(o+i));
1038                     added = TRUE;
1039                 }
1040                 addVarAssump(hd(ps),ta);
1041             }
1042         }
1043         else {
1044             hd(ps) = typeFreshPat(l,hd(ps));
1045             shouldBe(l,hd(ps),NIL,wh,ta,o);
1046         }
1047         t  = arg(t);
1048         ps = tl(ps);
1049         as = fn(ta,as);
1050         n--;
1051     }
1052
1053     if (n==0)
1054         snd(a) = typeRhs(snd(a));
1055     else {
1056         Int beta = funcType(n);
1057         Int i    = 0;
1058         for (; i<n; ++i) {
1059             hd(ps) = typeFreshPat(l,hd(ps));
1060             bindTv(beta+2*i+1,typeIs,typeOff);
1061             ps = tl(ps);
1062         }
1063         snd(a) = typeRhs(snd(a));
1064         bindTv(beta+2*n,typeIs,typeOff);
1065         tyvarType(beta);
1066     }
1067
1068     if (!unify(typeIs,typeOff,t,o)) {
1069         Type req, got;
1070         clearMarks();
1071         req = liftRank2(origt,o,m);
1072         liftRank2Args(as,o,m);
1073         got = ap(RANK2,pair(mkInt(nr2),revOnto(as,copyType(typeIs,typeOff))));
1074         reportTypeError(l,e,NIL,wh,got,req);
1075     }
1076
1077     restoreVarsAss();
1078     doneBtyvs(l);
1079     leaveSkolVars(l,origt,o,m);
1080 }
1081
1082 static Int local funcType(n)            /*return skeleton for function type*/
1083 Int n; {                                /*with n arguments, taking the form*/
1084     Int beta = newTyvars(2*n+1);        /*    r1 t1 r2 t2 ... rn tn rn+1   */
1085     Int i;                              /* with r_i := t_i -> r_i+1        */
1086     for (i=0; i<n; ++i)
1087         bindTv(beta+2*i,arrow,beta+2*i+1);
1088     return beta;
1089 }
1090
1091 static Void local typeCase(l,beta,c)   /* type check case: pat -> rhs      */
1092 Int  l;                                /* (case given by c == (pat,rhs))   */
1093 Int  beta;                             /* need:  pat :: (var,beta)         */
1094 Cell c; {                              /*        rhs :: (var,beta+1)       */
1095     static String casePat  = "case pattern";
1096     static String caseExpr = "case expression";
1097
1098     saveVarsAss();
1099     enterSkolVars();
1100     fst(c) = typeFreshPat(l,patBtyvs(fst(c)));
1101     shouldBe(l,fst(c),NIL,casePat,aVar,beta);
1102     snd(c) = typeRhs(snd(c));
1103     shouldBe(l,rhsExpr(snd(c)),NIL,caseExpr,aVar,beta+1);
1104
1105     restoreVarsAss();
1106     doneBtyvs(l);
1107     leaveSkolVars(l,typeIs,typeOff,0);
1108 }
1109
1110 static Void local typeComp(l,m,e,qs)    /* type check comprehension        */
1111 Int  l;
1112 Type m;                                 /* monad (mkOffset(0))             */
1113 Cell e;
1114 List qs; {
1115     static String boolQual = "boolean qualifier";
1116     static String genQual  = "generator";
1117
1118     STACK_CHECK
1119     if (isNull(qs))                     /* no qualifiers left              */
1120         fst(e) = typeExpr(l,fst(e));
1121     else {
1122         Cell q   = hd(qs);
1123         List qs1 = tl(qs);
1124         switch (whatIs(q)) {
1125             case BOOLQUAL : check(l,snd(q),NIL,boolQual,typeBool,0);
1126                             typeComp(l,m,e,qs1);
1127                             break;
1128
1129             case QWHERE   : enterBindings();
1130                             enterSkolVars();
1131                             mapProc(typeBindings,snd(q));
1132                             typeComp(l,m,e,qs1);
1133                             leaveBindings();
1134                             leaveSkolVars(l,typeIs,typeOff,0);
1135                             break;
1136
1137             case FROMQUAL : {   Int beta = newTyvars(1);
1138                                 saveVarsAss();
1139                                 check(l,snd(snd(q)),NIL,genQual,m,beta);
1140                                 enterSkolVars();
1141                                 fst(snd(q))
1142                                     = typeFreshPat(l,patBtyvs(fst(snd(q))));
1143                                 shouldBe(l,fst(snd(q)),NIL,genQual,aVar,beta);
1144                                 typeComp(l,m,e,qs1);
1145                                 restoreVarsAss();
1146                                 doneBtyvs(l);
1147                                 leaveSkolVars(l,typeIs,typeOff,0);
1148                             }
1149                             break;
1150
1151             case DOQUAL   : check(l,snd(q),NIL,genQual,m,newTyvars(1));
1152                             typeComp(l,m,e,qs1);
1153                             break;
1154         }
1155     }
1156 }
1157
1158 static Cell local typeMonadComp(l,e)    /* type check monad comprehension  */
1159 Int  l;
1160 Cell e; {
1161     Int  alpha        = newTyvars(1);
1162     Int  beta         = newTyvars(1);
1163     Cell mon          = ap(mkInt(beta),aVar);
1164     Cell m            = assumeEvid(predMonad,beta);
1165     tyvar(beta)->kind = starToStar;
1166 #if !MONAD_COMPS
1167     bindTv(beta,typeList,0);
1168      m = nameListMonad;
1169 #endif
1170
1171     typeComp(l,mon,snd(e),snd(snd(e)));
1172     bindTv(alpha,typeIs,typeOff);
1173     inferType(mon,alpha);
1174     return ap(MONADCOMP,pair(m,snd(e)));
1175 }
1176
1177 static Void local typeDo(l,e)           /* type check do-notation          */
1178 Int  l;
1179 Cell e; {
1180     static String finGen = "final generator";
1181     Int  alpha           = newTyvars(1);
1182     Int  beta            = newTyvars(1);
1183     Cell mon             = ap(mkInt(beta),aVar);
1184     Cell m               = assumeEvid(predMonad,beta);
1185     tyvar(beta)->kind    = starToStar;
1186
1187     typeComp(l,mon,snd(e),snd(snd(e)));
1188     shouldBe(l,fst(snd(e)),NIL,finGen,mon,alpha);
1189     snd(e) = pair(m,snd(e));
1190 }
1191
1192 static Void local typeConFlds(l,e)      /* Type check a construction       */
1193 Int  l;
1194 Cell e; {
1195     static String conExpr = "value construction";
1196     Name c  = fst(snd(e));
1197     List fs = snd(snd(e));
1198     Type tc;
1199     Int  to;
1200     Int  tf;
1201     Int  i;
1202
1203     instantiate(name(c).type);
1204     for (; nonNull(predsAre); predsAre=tl(predsAre))
1205         assumeEvid(hd(predsAre),typeOff);
1206     if (whatIs(typeIs)==RANK2)
1207         typeIs = snd(snd(typeIs));
1208     tc = typeIs;
1209     to = typeOff;
1210     tf = typeFree;
1211
1212     for (; nonNull(fs); fs=tl(fs)) {
1213         Type t = tc;
1214         for (i=sfunPos(fst(hd(fs)),c); --i>0; t=arg(t))
1215             ;
1216         t = dropRank1(arg(fun(t)),to,tf);
1217         if (isPolyOrQualType(t))
1218             snd(hd(fs)) = typeExpected(l,conExpr,snd(hd(fs)),t,to,tf,TRUE);
1219         else {
1220             check(l,snd(hd(fs)),e,conExpr,t,to);
1221         }
1222     }
1223     for (i=name(c).arity; i>0; i--)
1224         tc = arg(tc);
1225     inferType(tc,to);
1226 }
1227
1228 static Void local typeUpdFlds(line,e)   /* Type check an update            */
1229 Int  line;                              /* (Written in what might seem a   */
1230 Cell e; {                               /* bizarre manner for the benefit  */
1231     static String update = "update";    /* of as yet unreleased extensions)*/
1232     List cs    = snd3(snd(e));          /* List of constructors            */
1233     List fs    = thd3(snd(e));          /* List of field specifications    */
1234     List ts    = NIL;                   /* List of types for fields        */
1235     Int  n     = length(fs);
1236     Int  alpha = newTyvars(2+n);
1237     Int  i;
1238     List fs1;
1239
1240     /* Calculate type and translation for each expr in the field list      */
1241     for (fs1=fs, i=alpha+2; nonNull(fs1); fs1=tl(fs1), i++) {
1242         snd(hd(fs1)) = typeExpr(line,snd(hd(fs1)));
1243         bindTv(i,typeIs,typeOff);
1244     }
1245
1246     clearMarks();
1247     mapProc(markAssumList,defnBounds);
1248     mapProc(markAssumList,varsBounds);
1249     mapProc(markPred,preds);
1250     markBtyvs();
1251
1252     for (fs1=fs, i=alpha+2; nonNull(fs1); fs1=tl(fs1), i++) {
1253         resetGenerics();
1254         ts = cons(generalize(NIL,copyTyvar(i)),ts);
1255     }
1256     ts = rev(ts);
1257
1258     /* Type check expression to be updated                                 */
1259     fst3(snd(e)) = typeExpr(line,fst3(snd(e)));
1260     bindTv(alpha,typeIs,typeOff);
1261
1262     for (; nonNull(cs); cs=tl(cs)) {    /* Loop through constrs            */
1263         Name c  = hd(cs);
1264         List ta = replicate(name(c).arity,NIL);
1265         Type td, tr;
1266         Int  od, or;
1267
1268         tcMode = NEW_PATTERN;           /* Domain type                     */
1269         instantiate(name(c).type);
1270         tcMode = EXPRESSION;
1271         td     = typeIs;
1272         od     = typeOff;
1273         for (; nonNull(predsAre); predsAre=tl(predsAre))
1274             assumeEvid(hd(predsAre),typeOff);
1275
1276         if (whatIs(typeIs)==RANK2) {
1277             ERRMSG(line) "Sorry, record update syntax cannot currently be "
1278                          "used for datatypes with polymorphic components"
1279             EEND;
1280         }
1281
1282         instantiate(name(c).type);      /* Range type                      */
1283         tr = typeIs;
1284         or = typeOff;
1285         for (; nonNull(predsAre); predsAre=tl(predsAre))
1286             assumeEvid(hd(predsAre),typeOff);
1287
1288         for (fs1=fs, i=1; nonNull(fs1); fs1=tl(fs1), i++) {
1289             Int n    = sfunPos(fst(hd(fs1)),c);
1290             Cell ta1 = ta;
1291             for (; n>1; n--)
1292                 ta1 = tl(ta1);
1293             hd(ta1) = mkInt(i);
1294         }
1295
1296         for (; nonNull(ta); ta=tl(ta)) {        /* For each cfun arg       */
1297             if (nonNull(hd(ta))) {              /* Field to updated?       */
1298                 Int  n = intOf(hd(ta));
1299                 Cell f = fs;
1300                 Cell t = ts;
1301                 for (; n-- > 1; f=tl(f), t=tl(t))
1302                     ;
1303                 f = hd(f);
1304                 t = hd(t);
1305                 instantiate(t);
1306                 shouldBe(line,snd(f),e,update,arg(fun(tr)),or);
1307             }                                   /* Unmentioned component   */
1308             else if (!unify(arg(fun(td)),od,arg(fun(tr)),or))
1309                 internal("typeUpdFlds");
1310
1311             tr = arg(tr);
1312             td = arg(td);
1313         }
1314
1315         inferType(td,od);                       /* Check domain type       */
1316         shouldBe(line,fst3(snd(e)),e,update,aVar,alpha);
1317         inferType(tr,or);                       /* Check range type        */
1318         shouldBe(line,e,NIL,update,aVar,alpha+1);
1319     }
1320     /* (typeIs,typeOff) still carry the result type when we exit the loop  */
1321 }
1322
1323 #if IPARAM
1324 static Cell local typeWith(line,e)      /* Type check a with               */
1325 Int  line;
1326 Cell e; {
1327     List fs    = snd(snd(e));           /* List of field specifications    */
1328     Int  n     = length(fs);
1329     Int  alpha = newTyvars(2+n);
1330     Int  i;
1331     List fs1;
1332     Cell tIs;
1333     Cell tOff;
1334     List dpreds = NIL, dp;
1335     Cell bs = NIL;
1336
1337     /* Type check expression to be updated                                 */
1338     fst(snd(e)) = typeExpr(line,fst(snd(e)));
1339     bindTv(alpha,typeIs,typeOff);
1340     tIs = typeIs;
1341     tOff = typeOff;
1342     /* elim duplicate uses of imp params */
1343     preds = scSimplify(preds);
1344     /* extract preds that we're going to bind */
1345     for (fs1=fs; nonNull(fs1); fs1=tl(fs1)) {
1346         Text t = textOf(fst(hd(fs1)));
1347         Cell p = findIPEvid(t);
1348         dpreds = cons(p, dpreds);
1349         if (nonNull(p)) {
1350             removeIPEvid(t);
1351         } else {
1352             /* maybe give a warning message here... */
1353         }
1354     }
1355     dpreds = rev(dpreds);
1356
1357     /* Calculate type and translation for each expr in the field list      */
1358     for (fs1=fs, dp=dpreds, i=alpha+2; nonNull(fs1); fs1=tl(fs1), dp=tl(dp), i++) {
1359         static String with = "with";
1360         Cell ev = hd(dp);
1361         snd(hd(fs1)) = typeExpr(line,snd(hd(fs1)));
1362         bindTv(i,typeIs,typeOff);
1363         if (nonNull(ev)) {
1364             shouldBe(line,fst(hd(fs1)),e,with,snd(fst3(ev)),intOf(snd3(ev)));
1365             bs = cons(cons(pair(thd3(ev), cons(triple(NIL, mkInt(line), snd(hd(fs1))), NIL)), NIL), bs);
1366         }
1367     }
1368     typeIs = tIs;
1369     typeOff = tOff;
1370     return (ap(LETREC,pair(bs,fst(snd(e)))));
1371 }
1372 #endif
1373
1374 static Cell local typeFreshPat(l,p)    /* find type of pattern, assigning  */
1375 Int  l;                                /* fresh type variables to each var */
1376 Cell p; {                              /* bound in the pattern             */
1377     tcMode = NEW_PATTERN;
1378     p      = typeExpr(l,p);
1379     tcMode = EXPRESSION;
1380     return p;
1381 }
1382
1383 /* --------------------------------------------------------------------------
1384  * Type check group of bindings:
1385  * ------------------------------------------------------------------------*/
1386
1387 static Void local typeBindings(bs)      /* type check a binding group      */
1388 List bs; {
1389     Bool usesPatBindings = FALSE;       /* TRUE => pattern binding in bs   */
1390     Bool usesUntypedVar  = FALSE;       /* TRUE => var bind w/o type decl  */
1391     List bs1;
1392
1393     /* The following loop is used to determine whether the monomorphism    */
1394     /* restriction should be applied.  It could be written marginally more */
1395     /* efficiently by using breaks, but clarity is more important here ... */
1396
1397     for (bs1=bs; nonNull(bs1); bs1=tl(bs1)) {  /* Analyse binding group    */
1398         Cell b = hd(bs1);
1399         if (!isVar(fst(b)))
1400             usesPatBindings = TRUE;
1401         else if (isNull(fst(hd(snd(snd(b)))))           /* no arguments    */
1402                  && whatIs(fst(snd(b)))==IMPDEPS)       /* implicitly typed*/
1403             usesUntypedVar  = TRUE;
1404     }
1405
1406     if (usesPatBindings || usesUntypedVar)
1407         monorestrict(bs);
1408     else
1409         unrestricted(bs);
1410
1411     mapProc(removeTypeSigs,bs);                /* Remove binding type info */
1412     hd(varsBounds) = revOnto(hd(defnBounds),   /* transfer completed assmps*/
1413                              hd(varsBounds));  /* out of defnBounds        */
1414     hd(defnBounds) = NIL;
1415     hd(depends)    = NIL;
1416 }
1417
1418 static Void local removeTypeSigs(b)    /* Remove type info from a binding  */
1419 Cell b; {
1420     snd(b) = snd(snd(b));
1421 }
1422
1423 /* --------------------------------------------------------------------------
1424  * Type check a restricted binding group:
1425  * ------------------------------------------------------------------------*/
1426
1427 static Void local monorestrict(bs)      /* Type restricted binding group   */
1428 List bs; {
1429     List savePreds = preds;
1430     Int  line      = isVar(fst(hd(bs))) ? rhsLine(snd(hd(snd(snd(hd(bs))))))
1431                                         : rhsLine(snd(snd(snd(hd(bs)))));
1432     hd(defnBounds) = NIL;
1433     hd(depends)    = NODEPENDS;         /* No need for dependents here     */
1434
1435     preds = NIL;                        /* Type check the bindings         */
1436     mapProc(restrictedBindAss,bs);
1437     mapProc(typeBind,bs);
1438     improve(line,NIL,preds);
1439     normPreds(line);
1440     elimTauts();
1441     preds = revOnto(preds,savePreds);
1442
1443     clearMarks();                       /* Mark fixed variables            */
1444     mapProc(markAssumList,tl(defnBounds));
1445     mapProc(markAssumList,tl(varsBounds));
1446     mapProc(markPred,preds);
1447     markBtyvs();
1448
1449     if (isNull(tl(defnBounds))) {       /* Top-level may need defaulting   */
1450         normPreds(line);
1451         if (nonNull(preds) && resolveDefs(genvarAnyAss(hd(defnBounds))))
1452             elimTauts();
1453
1454         clearMarks();
1455         reducePreds();
1456         if (nonNull(preds) && resolveDefs(NIL)) /* Nearly Haskell 1.4?     */
1457             elimTauts();
1458
1459         if (nonNull(preds)) {           /* Look for unresolved overloading */
1460             Cell v   = isVar(fst(hd(bs))) ? fst(hd(bs)) : hd(fst(hd(bs)));
1461             Cell ass = findInAssumList(textOf(v),hd(varsBounds));
1462             preds    = scSimplify(preds);
1463
1464             ERRMSG(line) "Unresolved top-level overloading" ETHEN
1465             ERRTEXT     "\n*** Binding             : %s", textToStr(textOf(v))
1466             ETHEN
1467             if (nonNull(ass)) {
1468                 ERRTEXT "\n*** Inferred type       : " ETHEN ERRTYPE(snd(ass));
1469             }
1470             ERRTEXT     "\n*** Outstanding context : " ETHEN
1471                                                 ERRCONTEXT(copyPreds(preds));
1472             ERRTEXT     "\n"
1473             EEND;
1474         }
1475     }
1476
1477     map1Proc(genBind,NIL,bs);           /* Generalize types of def'd vars  */
1478 }
1479
1480 static Void local restrictedBindAss(b)  /* Make assums for vars in binding */
1481 Cell b; {                               /* gp with restricted overloading  */
1482
1483     if (isVar(fst(b))) {                /* function-binding?               */
1484         Cell t = fst(snd(b));
1485         if (whatIs(t)==IMPDEPS)  {      /* Discard implicitly typed deps   */
1486             fst(snd(b)) = t = NIL;      /* in a restricted binding group.  */
1487         }
1488         fst(snd(b)) = localizeBtyvs(t);
1489         restrictedAss(rhsLine(snd(hd(snd(snd(b))))), fst(b), t);
1490     } else {                            /* pattern-binding?                */
1491         List vs   = fst(b);
1492         List ts   = fst(snd(b));
1493         Int  line = rhsLine(snd(snd(snd(b))));
1494
1495         for (; nonNull(vs); vs=tl(vs)) {
1496             if (nonNull(ts)) {
1497                 restrictedAss(line,hd(vs),hd(ts)=localizeBtyvs(hd(ts)));
1498                 ts = tl(ts);
1499             } else {
1500                 restrictedAss(line,hd(vs),NIL);
1501             }
1502         }
1503     }
1504 }
1505
1506 static Void local restrictedAss(l,v,t) /* Assume that type of binding var v*/
1507 Int  l;                                /* is t (if nonNull) in restricted  */
1508 Cell v;                                /* binding group                    */
1509 Type t; {
1510     newDefnBind(v,t);
1511     if (nonNull(predsAre)) {
1512         ERRMSG(l) "Explicit overloaded type for \"%s\"",textToStr(textOf(v))
1513         ETHEN
1514         ERRTEXT   " not permitted in restricted binding"
1515         EEND;
1516     }
1517 }
1518
1519 /* --------------------------------------------------------------------------
1520  * Unrestricted binding group:
1521  * ------------------------------------------------------------------------*/
1522
1523 static Void local unrestricted(bs)      /* Type unrestricted binding group */
1524 List bs; {
1525     List savePreds = preds;
1526     List imps      = NIL;               /* Implicitly typed bindings       */
1527     List exps      = NIL;               /* Explicitly typed bindings       */
1528     List bs1;
1529
1530     /* ----------------------------------------------------------------------
1531      * STEP 1: Separate implicitly typed bindings from explicitly typed 
1532      * bindings and do a dependency analyis, where f depends on g iff f
1533      * is implicitly typed and involves a call to g.
1534      * --------------------------------------------------------------------*/
1535
1536     for (; nonNull(bs); bs=tl(bs)) {
1537         Cell b = hd(bs);
1538         if (whatIs(fst(snd(b)))==IMPDEPS)
1539             imps = cons(b,imps);        /* N.B. New lists are built to     */
1540         else                            /* avoid breaking the original     */
1541             exps = cons(b,exps);        /* list structure for bs.          */
1542     }
1543
1544     for (bs=imps; nonNull(bs); bs=tl(bs)) {
1545         Cell b  = hd(bs);               /* Restrict implicitly typed dep   */
1546         List ds = snd(fst(snd(b)));     /* lists to bindings in imps       */
1547         List cs = NIL;
1548         while (nonNull(ds)) {
1549             bs1 = tl(ds);
1550             if (cellIsMember(hd(ds),imps)) {
1551                 tl(ds) = cs;
1552                 cs     = ds;
1553             }
1554             ds = bs1;
1555         }
1556         fst(snd(b)) = cs;
1557     }
1558     imps = itbscc(imps);                /* Dependency analysis on imps     */
1559     for (bs=imps; nonNull(bs); bs=tl(bs))
1560         for (bs1=hd(bs); nonNull(bs1); bs1=tl(bs1))
1561             fst(snd(hd(bs1))) = NIL;    /* reset imps type fields          */
1562
1563 #ifdef DEBUG_DEPENDS
1564     Printf("Binding group:");
1565     for (bs1=imps; nonNull(bs1); bs1=tl(bs1)) {
1566         Printf(" [imp:");
1567         for (bs=hd(bs1); nonNull(bs); bs=tl(bs))
1568             Printf(" %s",textToStr(textOf(fst(hd(bs)))));
1569         Printf("]");
1570     }
1571     if (nonNull(exps)) {
1572         Printf(" [exp:");
1573         for (bs=exps; nonNull(bs); bs=tl(bs))
1574             Printf(" %s",textToStr(textOf(fst(hd(bs)))));
1575         Printf("]");
1576     }
1577     Printf("\n");
1578 #endif
1579
1580     /* ----------------------------------------------------------------------
1581      * STEP 2: Add type assumptions about any explicitly typed variable.
1582      * --------------------------------------------------------------------*/
1583
1584     for (bs=exps; nonNull(bs); bs=tl(bs)) {
1585         fst(snd(hd(bs))) = localizeBtyvs(fst(snd(hd(bs))));
1586         hd(varsBounds)   = cons(pair(fst(hd(bs)),fst(snd(hd(bs)))),
1587                                 hd(varsBounds));
1588     }
1589
1590     /* ----------------------------------------------------------------------
1591      * STEP 3: Calculate types for each group of implicitly typed bindings.
1592      * --------------------------------------------------------------------*/
1593
1594     for (; nonNull(imps); imps=tl(imps)) {
1595         Cell b   = hd(hd(imps));
1596         Int line = isVar(fst(b)) ? rhsLine(snd(hd(snd(snd(b)))))
1597                                  : rhsLine(snd(snd(snd(b))));
1598         hd(defnBounds) = NIL;
1599         hd(depends)    = NIL;
1600         for (bs1=hd(imps); nonNull(bs1); bs1=tl(bs1))
1601             newDefnBind(fst(hd(bs1)),NIL);
1602
1603         preds = NIL;
1604         mapProc(typeBind,hd(imps));
1605         improve(line,NIL,preds);
1606
1607         clearMarks();
1608         mapProc(markAssumList,tl(defnBounds));
1609         mapProc(markAssumList,tl(varsBounds));
1610         mapProc(markPred,savePreds);
1611         markBtyvs();
1612
1613         normPreds(line);
1614         savePreds = elimOuterPreds(savePreds);
1615         if (nonNull(preds) && resolveDefs(genvarAllAss(hd(defnBounds)))) {
1616             savePreds = elimOuterPreds(savePreds);
1617         }
1618
1619         map1Proc(genBind,preds,hd(imps));
1620         if (nonNull(preds)) {
1621             map1Proc(addEvidParams,preds,hd(depends));
1622             map1Proc(qualifyBinding,preds,hd(imps));
1623         }
1624
1625         h98CheckType(line,"inferred type",
1626                         fst(hd(hd(defnBounds))),snd(hd(hd(defnBounds))));
1627         hd(varsBounds) = revOnto(hd(defnBounds),hd(varsBounds));
1628     }
1629
1630     /* ----------------------------------------------------------------------
1631      * STEP 4: Now infer a type for each explicitly typed variable and
1632      * check for compatibility with the declared type.
1633      * --------------------------------------------------------------------*/
1634
1635     for (; nonNull(exps); exps=tl(exps)) {
1636         static String extbind = "explicitly typed binding";
1637         Cell b    = hd(exps);
1638         List alts = snd(snd(b));
1639         Int  line = rhsLine(snd(hd(alts)));
1640         Type t;
1641         Int  o;
1642         Int  m;
1643         List ps;
1644
1645         hd(defnBounds) = NIL;
1646         hd(depends)    = NODEPENDS;
1647         preds          = NIL;
1648
1649         instantiate(fst(snd(b)));
1650         o              = typeOff;
1651         m              = typeFree;
1652         t              = dropRank2(typeIs,o,m);
1653         ps             = makePredAss(predsAre,o);
1654
1655         enterPendingBtyvs();
1656         for (; nonNull(alts); alts=tl(alts))
1657             typeAlt(extbind,fst(b),hd(alts),t,o,m);
1658         improve(line,ps,preds);
1659         leavePendingBtyvs();
1660
1661         if (nonNull(ps))                /* Add dict params, if necessary   */
1662             qualifyBinding(ps,b);
1663
1664         clearMarks();
1665         mapProc(markAssumList,tl(defnBounds));
1666         mapProc(markAssumList,tl(varsBounds));
1667         mapProc(markPred,savePreds);
1668         markBtyvs();
1669
1670         normPreds(line);
1671         savePreds = elimPredsUsing(ps,savePreds);
1672         if (nonNull(preds)) {
1673             List vs = NIL;
1674             Int  i  = 0;
1675             for (; i<m; ++i)
1676                 vs = cons(mkInt(o+i),vs);
1677             if (resolveDefs(vs)) {
1678                 savePreds = elimPredsUsing(ps,savePreds);
1679             }
1680             if (nonNull(preds)) {
1681                 clearMarks();
1682                 reducePreds();
1683                 if (nonNull(preds) && resolveDefs(vs))
1684                     savePreds = elimPredsUsing(ps,savePreds);
1685             }
1686         }
1687
1688         resetGenerics();                /* Make sure we're general enough  */
1689         ps = copyPreds(ps);
1690         t  = generalize(ps,liftRank2(t,o,m));
1691
1692         if (!sameSchemes(t,fst(snd(b))))
1693             tooGeneral(line,fst(b),fst(snd(b)),t);
1694         h98CheckType(line,"inferred type",fst(b),t);
1695
1696         if (nonNull(preds))             /* Check context was strong enough */
1697             cantEstablish(line,extbind,fst(b),t,ps);
1698     }
1699
1700     preds          = savePreds;                 /* Restore predicates      */
1701     hd(defnBounds) = NIL;
1702 }
1703
1704 #define  SCC             itbscc         /* scc for implicitly typed binds  */
1705 #define  LOWLINK         itblowlink
1706 #define  DEPENDS(t)      fst(snd(t))
1707 #define  SETDEPENDS(c,v) fst(snd(c))=v
1708 #include "scc.c"
1709 #undef   SETDEPENDS
1710 #undef   DEPENDS
1711 #undef   LOWLINK
1712 #undef   SCC
1713
1714 static Void local addEvidParams(qs,v)  /* overwrite VARID/OPCELL v with    */
1715 List qs;                               /* application of variable to evid. */
1716 Cell v; {                              /* parameters given by qs           */
1717     if (nonNull(qs)) {
1718         Cell nv;
1719
1720         if (!isVar(v))
1721             internal("addEvidParams");
1722
1723         for (nv=mkVar(textOf(v)); nonNull(tl(qs)); qs=tl(qs))
1724             nv = ap(nv,thd3(hd(qs)));
1725         fst(v) = nv;
1726         snd(v) = thd3(hd(qs));
1727     }
1728 }
1729
1730 /* --------------------------------------------------------------------------
1731  * Type check bodies of class and instance declarations:
1732  * ------------------------------------------------------------------------*/
1733
1734 static Void local typeClassDefn(c)      /* Type check implementations of   */
1735 Class c; {                              /* defaults for class c            */
1736
1737     /* ----------------------------------------------------------------------
1738      * Generate code for default dictionary builder functions:
1739      * --------------------------------------------------------------------*/
1740
1741     Int  beta   = newKindedVars(cclass(c).kinds);
1742     Cell d      = inventDictVar();
1743     List dparam = singleton(triple(cclass(c).head,mkInt(beta),d));
1744     List mems   = cclass(c).members;
1745     List defs   = cclass(c).defaults;
1746     List dsels  = cclass(c).dsels;
1747     Cell pat    = cclass(c).dcon;
1748     Int  width  = cclass(c).numSupers + cclass(c).numMembers;
1749     char buf[FILENAME_MAX+1];
1750     Int  i      = 0;
1751     Int  j      = 0;
1752
1753     if (isNull(defs) && nonNull(mems)) {
1754         defs = cclass(c).defaults = cons(NIL,NIL);
1755     }
1756
1757     for (; nonNull(mems); mems=tl(mems)) {
1758         static String deftext = "default_";
1759         String s              = textToStr(name(hd(mems)).text);
1760         Name   n;
1761         for (; i<FILENAME_MAX && deftext[i]!='\0'; i++) {
1762             buf[i] = deftext[i];
1763         }
1764         for(; (i+j)<FILENAME_MAX && s[j]!='\0'; j++) {
1765             buf[i+j] = s[j];
1766         }
1767         buf[i+j] = '\0';
1768         n = newName(findText(buf),c);
1769
1770         if (isNull(hd(defs))) {         /* No default definition           */
1771             static String header = "Undefined member: ";
1772             for (i=0; i<FILENAME_MAX && header[i]!='\0'; i++)
1773                 buf[i] = header[i];
1774             for (j=0; (i+j)<FILENAME_MAX && s[j]!='\0'; j++)
1775                 buf[i+j] = s[j];
1776             buf[i+j] = '\0';
1777             name(n).line  = cclass(c).line;
1778             name(n).arity = 1;
1779             name(n).defn  = singleton(pair(singleton(d),
1780                                            ap(mkInt(cclass(c).line),
1781                                               ap(nameError,
1782                                                  mkStr(fixLitText(
1783                                                         findText(buf)))))));
1784         } else {                        /* User supplied default defn      */
1785             List alts = snd(hd(defs));
1786             Int  line = rhsLine(snd(hd(alts)));
1787
1788             typeMember("default member binding",
1789                        hd(mems),
1790                        alts,
1791                        dparam,
1792                        cclass(c).head,
1793                        beta);
1794
1795             name(n).line  = line;
1796             name(n).arity = 1+length(fst(hd(alts)));
1797             name(n).defn  = alts;
1798
1799             for (; nonNull(alts); alts=tl(alts)) {
1800                 fst(hd(alts)) = cons(d,fst(hd(alts)));
1801             }
1802         }
1803
1804         hd(defs) = n;
1805         genDefns = cons(n,genDefns);
1806         if (isNull(tl(defs)) && nonNull(tl(mems))) {
1807             tl(defs) = cons(NIL,NIL);
1808         }
1809         defs     = tl(defs);
1810     }
1811
1812     /* ----------------------------------------------------------------------
1813      * Generate code for superclass and member function selectors:
1814      * --------------------------------------------------------------------*/
1815
1816     for (i=0; i<width; i++) {
1817         pat = ap(pat,inventVar());
1818     }
1819     pat = singleton(pat);
1820     for (i=0; nonNull(dsels); dsels=tl(dsels)) {
1821         name(hd(dsels)).defn = singleton(pair(pat,
1822                                               ap(mkInt(cclass(c).line),
1823                                                  nthArg(i++,hd(pat)))));
1824         genDefns             = cons(hd(dsels),genDefns);
1825     }
1826     for (mems=cclass(c).members; nonNull(mems); mems=tl(mems)) {
1827         name(hd(mems)).defn  = singleton(pair(pat,
1828                                               ap(mkInt(name(hd(mems)).line),
1829                                                  nthArg(i++,hd(pat)))));
1830         genDefns             = cons(hd(mems),genDefns);
1831     }
1832 }
1833
1834 static Void local typeInstDefn(in)      /* Type check implementations of   */
1835 Inst in; {                              /* member functions for instance in*/
1836
1837     /* ----------------------------------------------------------------------
1838      * Generate code for instance specific dictionary builder function:
1839      *
1840      *   inst.maker d1 ... dn = let sc1 = ...
1841      *                                  .
1842      *                                  .
1843      *                                  .
1844      *                              scm = ...
1845      *                              vj ... = ...
1846      *                              d      = Make.C sc1 ... scm v1 ... vk
1847      *                          in d
1848      *
1849      * where sci are superclass dictionaries, d is a new name, vj
1850      * is a newly generated name corresponding to the implementation of a
1851      * member function.  (Additional line number values must be added at
1852      * appropriate places but, for clarity, these are not shown above.)
1853      * If no implementation of a particular vj is available, then we use
1854      * the default implementation, partially applied to d.
1855      * --------------------------------------------------------------------*/
1856
1857     Int  alpha   = newKindedVars(cclass(inst(in).c).kinds);
1858     List supers  = makePredAss(cclass(inst(in).c).supers,alpha);
1859     Int  beta    = newKindedVars(inst(in).kinds);
1860     List params  = makePredAss(inst(in).specifics,beta);
1861     Cell d       = inventDictVar();
1862     List evids   = cons(triple(inst(in).head,mkInt(beta),d),
1863                         appendOnto(dupList(params),supers));
1864
1865     List imps    = inst(in).implements;
1866     Cell l       = mkInt(inst(in).line);
1867     Cell dictDef = cclass(inst(in).c).dcon;
1868     List mems    = cclass(inst(in).c).members;
1869     List defs    = cclass(inst(in).c).defaults;
1870     List args    = NIL;
1871     List locs    = NIL;
1872     List ps;
1873
1874     if (!unifyPred(cclass(inst(in).c).head,alpha,inst(in).head,beta))
1875         internal("typeInstDefn");
1876
1877     for (ps=params; nonNull(ps); ps=tl(ps))     /* Build arglist           */
1878         args = cons(thd3(hd(ps)),args);
1879     args = rev(args);
1880
1881     for (ps=supers; nonNull(ps); ps=tl(ps)) {   /* Superclass dictionaries */
1882         Cell pi = hd(ps);
1883         Cell ev = NIL;
1884 #if EXPLAIN_INSTANCE_RESOLUTION
1885         if (showInstRes) {
1886             fputs("scEntail: ", stdout);
1887             printContext(stdout,copyPreds(params));
1888             fputs(" ||- ", stdout);
1889             printPred(stdout, copyPred(fst3(pi),intOf(snd3(pi))));
1890             fputc('\n', stdout);
1891         }
1892 #endif
1893         ev = scEntail(params,fst3(pi),intOf(snd3(pi)),0);
1894         if (isNull(ev)) {
1895 #if EXPLAIN_INSTANCE_RESOLUTION
1896             if (showInstRes) {
1897                 fputs("inEntail: ", stdout);
1898                 printContext(stdout,copyPreds(evids));
1899                 fputs(" ||- ", stdout);
1900                 printPred(stdout, copyPred(fst3(pi),intOf(snd3(pi))));
1901                 fputc('\n', stdout);
1902             }
1903 #endif
1904             ev = inEntail(evids,fst3(pi),intOf(snd3(pi)),0);
1905         } 
1906         if (isNull(ev)) {
1907             clearMarks();
1908             ERRMSG(inst(in).line) "Cannot build superclass instance" ETHEN
1909             ERRTEXT "\n*** Instance            : " ETHEN
1910                 ERRPRED(copyPred(inst(in).head,beta));
1911             ERRTEXT "\n*** Context supplied    : " ETHEN
1912                 ERRCONTEXT(copyPreds(params));
1913             ERRTEXT "\n*** Required superclass : " ETHEN
1914                 ERRPRED(copyPred(fst3(pi),intOf(snd3(pi))));
1915             ERRTEXT "\n"
1916             EEND;
1917         }
1918         locs    = cons(pair(thd3(pi),singleton(pair(NIL,ap(l,ev)))),locs);
1919         dictDef = ap(dictDef,thd3(pi));
1920     }
1921
1922     for (; nonNull(defs); defs=tl(defs)) {
1923         Cell imp = NIL;
1924         if (nonNull(imps)) {
1925             imp  = hd(imps);
1926             imps = tl(imps);
1927         }
1928         if (isNull(imp)) {
1929             dictDef = ap(dictDef,ap(hd(defs),d));
1930         } else {
1931             Cell v  = inventVar();
1932             dictDef = ap(dictDef,v);
1933             typeMember("instance member binding",
1934                        hd(mems),
1935                        snd(imp),
1936                        evids,
1937                        inst(in).head,
1938                        beta);
1939             locs     = cons(pair(v,snd(imp)),locs);
1940         }
1941         mems = tl(mems);
1942     }
1943     locs = cons(pair(d,singleton(pair(NIL,ap(l,dictDef)))),locs);
1944
1945     name(inst(in).builder).defn                 /* Register builder imp    */
1946              = singleton(pair(args,ap(LETREC,pair(singleton(locs),
1947                                                   ap(l,d)))));
1948     genDefns = cons(inst(in).builder,genDefns);
1949 }
1950
1951 static Void local typeMember(wh,mem,alts,evids,head,beta)
1952 String wh;                              /* Type check alternatives alts of */
1953 Name   mem;                             /* member mem for inst type head   */
1954 Cell   alts;                            /* at offset beta using predicate  */
1955 List   evids;                           /* assignment evids                */
1956 Cell   head;
1957 Int    beta; {
1958     Int  line = rhsLine(snd(hd(alts)));
1959     Type t;
1960     Int  o;
1961     Int  m;
1962     List ps;
1963     List qs;
1964     Type rt;
1965
1966 #ifdef DEBUG_TYPES
1967     Printf("\nType check member: ");
1968     printExp(stdout,mem);
1969     Printf(" :: ");
1970     printType(stdout,name(mem).type);
1971     Printf("\n   for the instance: ");
1972     printPred(stdout,head);
1973     Printf("\n");
1974 #endif
1975
1976     instantiate(name(mem).type);        /* Find required type              */
1977     o  = typeOff;
1978     m  = typeFree;
1979     t  = dropRank2(typeIs,o,m);
1980     ps = makePredAss(predsAre,o);
1981     if (!unifyPred(hd(predsAre),typeOff,head,beta))
1982         internal("typeMember1");
1983     clearMarks();
1984     qs = copyPreds(ps);
1985     rt = generalize(qs,liftRank2(t,o,m));
1986
1987 #ifdef DEBUG_TYPES
1988     Printf("Required type is: ");
1989     printType(stdout,rt);
1990     Printf("\n");
1991 #endif
1992
1993     hd(defnBounds) = NIL;               /* Type check each alternative     */
1994     hd(depends)    = NODEPENDS;
1995     enterPendingBtyvs();
1996     for (preds=NIL; nonNull(alts); alts=tl(alts)) {
1997         typeAlt(wh,mem,hd(alts),t,o,m);
1998         qualify(tl(ps),hd(alts));       /* Add any extra dict params       */
1999     }
2000     improve(line,evids,preds);
2001     leavePendingBtyvs();
2002
2003     evids = appendOnto(dupList(tl(ps)), /* Build full complement of dicts  */
2004                        evids);
2005     clearMarks();
2006     normPreds(line);
2007     qs = elimPredsUsing(evids,NIL);
2008     if (nonNull(preds) && resolveDefs(genvarType(t,o,NIL)))
2009         qs = elimPredsUsing(evids,qs);
2010     if (nonNull(qs)) {
2011         ERRMSG(line)
2012                 "Implementation of %s requires extra context",
2013                  textToStr(name(mem).text) ETHEN
2014         ERRTEXT "\n*** Expected type   : " ETHEN ERRTYPE(rt);
2015         ERRTEXT "\n*** Missing context : " ETHEN ERRCONTEXT(copyPreds(qs));
2016         ERRTEXT "\n"
2017         EEND;
2018     }
2019
2020     resetGenerics();                    /* Make sure we're general enough  */
2021     ps = copyPreds(ps);
2022     t  = generalize(ps,liftRank2(t,o,m));
2023 #ifdef DEBUG_TYPES
2024     Printf("   Inferred type is: ");
2025     printType(stdout,t);
2026     Printf("\n");
2027 #endif
2028     if (!sameSchemes(t,rt))
2029         tooGeneral(line,mem,rt,t);
2030     if (nonNull(preds)) {
2031         preds = scSimplify(preds);
2032         cantEstablish(line,wh,mem,t,ps);
2033     }
2034 }
2035
2036 /* --------------------------------------------------------------------------
2037  * Type check bodies of bindings:
2038  * ------------------------------------------------------------------------*/
2039
2040 static Void local typeBind(b)          /* Type check binding               */
2041 Cell b; {
2042     if (isVar(fst(b))) {                               /* function binding */
2043         Cell ass = findTopBinding(fst(b));
2044         Int  beta;
2045
2046         if (isNull(ass))
2047             internal("typeBind");
2048
2049         beta = intOf(defType(snd(ass)));
2050         enterPendingBtyvs();
2051         map2Proc(typeDefAlt,beta,fst(b),snd(snd(b)));
2052         leavePendingBtyvs();
2053     }
2054     else {                                             /* pattern binding  */
2055         static String lhsPat = "lhs pattern";
2056         static String rhs    = "right hand side";
2057         Int  beta            = newTyvars(1);
2058         Pair pb              = snd(snd(b));
2059         Int  l               = rhsLine(snd(pb));
2060
2061         tcMode  = OLD_PATTERN;
2062         enterPendingBtyvs();
2063         fst(pb) = patBtyvs(fst(pb));
2064         check(l,fst(pb),NIL,lhsPat,aVar,beta);
2065         tcMode  = EXPRESSION;
2066         snd(pb) = typeRhs(snd(pb));
2067         shouldBe(l,rhsExpr(snd(pb)),NIL,rhs,aVar,beta);
2068         doneBtyvs(l);
2069         leavePendingBtyvs();
2070     }
2071 }
2072
2073 static Void local typeDefAlt(beta,v,a) /* type check alt in func. binding  */
2074 Int  beta;
2075 Cell v;
2076 Pair a; {
2077     static String valDef = "function binding";
2078     typeAlt(valDef,v,a,aVar,beta,0);
2079 }
2080
2081 static Cell local typeRhs(e)           /* check type of rhs of definition  */
2082 Cell e; {
2083     switch (whatIs(e)) {
2084         case GUARDED : {   Int beta = newTyvars(1);
2085                            map1Proc(guardedType,beta,snd(e));
2086                            tyvarType(beta);
2087                        }
2088                        break;
2089
2090         case LETREC  : enterBindings();
2091                        enterSkolVars();
2092                        mapProc(typeBindings,fst(snd(e)));
2093                        snd(snd(e)) = typeRhs(snd(snd(e)));
2094                        leaveBindings();
2095                        leaveSkolVars(rhsLine(snd(snd(e))),typeIs,typeOff,0);
2096                        break;
2097
2098         case RSIGN   : fst(snd(e)) = typeRhs(fst(snd(e)));
2099                        shouldBe(rhsLine(fst(snd(e))),
2100                                 rhsExpr(fst(snd(e))),NIL,
2101                                 "result type",
2102                                 snd(snd(e)),0);
2103                        return fst(snd(e));
2104
2105         default      : snd(e) = typeExpr(intOf(fst(e)),snd(e));
2106                        break;
2107     }
2108     return e;
2109 }
2110
2111 static Void local guardedType(beta,gded)/* check type of guard (li,(gd,ex))*/
2112 Int  beta;                             /* should have gd :: Bool,          */
2113 Cell gded; {                           /*             ex :: (var,beta)     */
2114     static String guarded = "guarded expression";
2115     static String guard   = "guard";
2116     Int line = intOf(fst(gded));
2117
2118     gded     = snd(gded);
2119     check(line,fst(gded),NIL,guard,typeBool,0);
2120     check(line,snd(gded),NIL,guarded,aVar,beta);
2121 }
2122
2123 Cell rhsExpr(rhs)                      /* find first expression on a rhs   */
2124 Cell rhs; {
2125     STACK_CHECK
2126     switch (whatIs(rhs)) {
2127         case GUARDED : return snd(snd(hd(snd(rhs))));
2128         case LETREC  : return rhsExpr(snd(snd(rhs)));
2129         case RSIGN   : return rhsExpr(fst(snd(rhs)));
2130         default      : return snd(rhs);
2131     }
2132 }
2133
2134 Int rhsLine(rhs)                       /* find line number associated with */
2135 Cell rhs; {                            /* a right hand side                */
2136     STACK_CHECK
2137     switch (whatIs(rhs)) {
2138         case GUARDED : return intOf(fst(hd(snd(rhs))));
2139         case LETREC  : return rhsLine(snd(snd(rhs)));
2140         case RSIGN   : return rhsLine(fst(snd(rhs)));
2141         default      : return intOf(fst(rhs));
2142     }
2143 }
2144
2145 /* --------------------------------------------------------------------------
2146  * Calculate generalization of types and compare with declared type schemes:
2147  * ------------------------------------------------------------------------*/
2148
2149 static Void local genBind(ps,b)         /* Generalize the type of each var */
2150 List ps;                                /* defined in binding b, qualifying*/
2151 Cell b; {                               /* each with the predicates in ps. */
2152     Cell v = fst(b);
2153     Cell t = fst(snd(b));
2154
2155     if (isVar(fst(b)))
2156         genAss(rhsLine(snd(hd(snd(snd(b))))),ps,v,t);
2157     else {
2158         Int line = rhsLine(snd(snd(snd(b))));
2159         for (; nonNull(v); v=tl(v)) {
2160             Type ty = NIL;
2161             if (nonNull(t)) {
2162                 ty = hd(t);
2163                 t  = tl(t);
2164             }
2165             genAss(line,ps,hd(v),ty);
2166         }
2167     }
2168 }
2169
2170 static Void local genAss(l,ps,v,dt)     /* Calculate inferred type of v and*/
2171 Int  l;                                 /* compare with declared type, dt, */
2172 List ps;                                /* if given & check for ambiguity. */
2173 Cell v;
2174 Type dt; {
2175     Cell ass = findTopBinding(v);
2176
2177     if (isNull(ass))
2178         internal("genAss");
2179
2180     snd(ass) = genTest(l,v,ps,dt,aVar,intOf(defType(snd(ass))));
2181
2182 #ifdef DEBUG_TYPES
2183     printExp(stdout,v);
2184     Printf(" :: ");
2185     printType(stdout,snd(ass));
2186     Printf("\n");
2187 #endif
2188 }
2189
2190 static Type local genTest(l,v,ps,dt,t,o)/* Generalize and test inferred    */
2191 Int  l;                                 /* type (t,o) with context ps      */
2192 Cell v;                                 /* against declared type dt for v. */
2193 List ps;
2194 Type dt;
2195 Type t;
2196 Int  o; {
2197     Type bt = NIL;                      /* Body of inferred type           */
2198     Type it = NIL;                      /* Full inferred type              */
2199
2200     resetGenerics();                    /* Calculate Haskell typing        */
2201     ps = copyPreds(ps);
2202     bt = copyType(t,o);
2203     it = generalize(ps,bt);
2204
2205     if (nonNull(dt)) {                  /* If a declared type was given,   */
2206         instantiate(dt);                /* check body for match.           */
2207         if (!equalTypes(typeIs,bt))
2208             tooGeneral(l,v,dt,it);
2209     }
2210     else if (nonNull(ps))               /* Otherwise test for ambiguity in */
2211         if (isAmbiguous(it))            /* inferred type.                  */
2212             ambigError(l,"inferred type",v,it);
2213
2214     return it;
2215 }
2216
2217 static Type local generalize(qs,t)      /* calculate generalization of t   */
2218 List qs;                                /* having already marked fixed vars*/
2219 Type t; {                               /* with qualifying preds qs        */
2220     if (nonNull(qs))
2221         t = ap(QUAL,pair(qs,t));
2222     if (nonNull(genericVars)) {
2223         Kind k  = STAR;
2224         List vs = genericVars;
2225         for (; nonNull(vs); vs=tl(vs)) {
2226             Tyvar *tyv = tyvar(intOf(hd(vs)));
2227             Kind   ka  = tyv->kind;
2228             k = ap(ka,k);
2229         }
2230         t = mkPolyType(k,t);
2231 #ifdef DEBUG_KINDS
2232     Printf("Generalized type: ");
2233     printType(stdout,t);
2234     Printf(" ::: ");
2235     printKind(stdout,k);
2236     Printf("\n");
2237 #endif
2238     }
2239     return t;
2240 }
2241
2242 static Bool local equalTypes(t1,t2)    /* Compare simple types for equality*/
2243 Type t1, t2; {
2244     STACK_CHECK
2245 et: if (whatIs(t1)!=whatIs(t2))
2246         return FALSE;
2247
2248     switch (whatIs(t1)) {
2249 #if TREX
2250         case EXT     :
2251 #endif
2252         case TYCON   :
2253         case OFFSET  :
2254         case TUPLE   : return t1==t2;
2255
2256         case INTCELL : return intOf(t1)!=intOf(t2);
2257
2258         case AP      : if (equalTypes(fun(t1),fun(t2))) {
2259                            t1 = arg(t1);
2260                            t2 = arg(t2);
2261                            goto et;
2262                        }
2263                        return FALSE;
2264
2265         default      : internal("equalTypes");
2266     }
2267
2268     return TRUE;/*NOTREACHED*/
2269 }
2270
2271 /* --------------------------------------------------------------------------
2272  * Entry points to type checker:
2273  * ------------------------------------------------------------------------*/
2274
2275 Type typeCheckExp(useDefs)              /* Type check top level expression */
2276 Bool useDefs; {                         /* using defaults if reqd          */
2277     Type type;
2278     List ctxt;
2279     Int  beta;
2280
2281     typeChecker(RESET);
2282     emptySubstitution();
2283     enterBindings();
2284     inputExpr = typeExpr(0,inputExpr);
2285     type      = typeIs;
2286     beta      = typeOff;
2287     clearMarks();
2288     improve(0,NIL,preds);
2289     normPreds(0);
2290     elimTauts();
2291     preds     = scSimplify(preds);
2292     if (useDefs && nonNull(preds)) {
2293         clearMarks();
2294         reducePreds();
2295         if (nonNull(preds) && resolveDefs(NIL)) /* Nearly Haskell 1.4?     */
2296             elimTauts();
2297     }
2298     resetGenerics();
2299     ctxt      = copyPreds(preds);
2300     type      = generalize(ctxt,copyType(type,beta));
2301     inputExpr = qualifyExpr(0,preds,inputExpr);
2302     h98CheckType(0,"inferred type",inputExpr,type);
2303     typeChecker(RESET);
2304     emptySubstitution();
2305     return type;
2306 }
2307
2308 Void typeCheckDefns() {                /* Type check top level bindings    */
2309     Target t  = length(selDefns)  + length(valDefns) +
2310                 length(instDefns) + length(classDefns);
2311     Target i  = 0;
2312     List   gs;
2313
2314     typeChecker(RESET);
2315     emptySubstitution();
2316     enterSkolVars();
2317     enterBindings();
2318     setGoal("Type checking",t);
2319
2320     for (gs=selDefns; nonNull(gs); gs=tl(gs)) {
2321         mapOver(typeSel,hd(gs));
2322         soFar(i++);
2323     }
2324     for (gs=valDefns; nonNull(gs); gs=tl(gs)) {
2325         typeDefnGroup(hd(gs));
2326         soFar(i++);
2327     }
2328     clearTypeIns();
2329     for (gs=classDefns; nonNull(gs); gs=tl(gs)) {
2330         emptySubstitution();
2331         typeClassDefn(hd(gs));
2332         soFar(i++);
2333     }
2334     for (gs=instDefns; nonNull(gs); gs=tl(gs)) {
2335         emptySubstitution();
2336         typeInstDefn(hd(gs));
2337         soFar(i++);
2338     }
2339
2340     typeChecker(RESET);
2341     emptySubstitution();
2342     done();
2343 }
2344
2345 static Void local typeDefnGroup(bs)     /* type check group of value defns */
2346 List bs; {                              /* (one top level scc)             */
2347     List as;
2348
2349     emptySubstitution();
2350     hd(defnBounds) = NIL;
2351     preds          = NIL;
2352     setTypeIns(bs);
2353     typeBindings(bs);                   /* find types for vars in bindings */
2354
2355     if (nonNull(preds)) {
2356         Cell v = fst(hd(hd(varsBounds)));
2357         Name n = findName(textOf(v));
2358         Int  l = nonNull(n) ? name(n).line : 0;
2359         preds  = scSimplify(preds);
2360         ERRMSG(l) "Instance%s of ", (length(preds)==1 ? "" : "s") ETHEN
2361         ERRCONTEXT(copyPreds(preds));
2362         ERRTEXT   " required for definition of " ETHEN
2363         ERREXPR(nonNull(n)?n:v);
2364         ERRTEXT   "\n"
2365         EEND;
2366     }
2367
2368     if (nonNull(hd(skolVars))) {
2369         Cell b = hd(bs);
2370         Name n = findName(isVar(fst(b)) ? textOf(fst(b)) : textOf(hd(fst(b))));
2371         Int  l = nonNull(n) ? name(n).line : 0;
2372         leaveSkolVars(l,typeUnit,0,0);
2373         enterSkolVars();
2374     }
2375
2376     for (as=hd(varsBounds); nonNull(as); as=tl(as)) {
2377         Cell a = hd(as);                /* add infered types to environment*/
2378         Name n = findName(textOf(fst(a)));
2379         if (isNull(n))
2380             internal("typeDefnGroup");
2381         name(n).type = snd(a);
2382     }
2383     hd(varsBounds) = NIL;
2384 }
2385
2386 static Pair local typeSel(s)            /* Calculate a suitable type for a */
2387 Name s; {                               /* particular selector, s.         */
2388     List cns  = name(s).defn;
2389     Int  line = name(s).line;
2390     Type dom  = NIL;                    /* Inferred domain                 */
2391     Type rng  = NIL;                    /* Inferred range                  */
2392     Cell nv   = inventVar();
2393     List alts = NIL;
2394     Int  o    = 0;                      /* bogus init to keep gcc -O happy */
2395     Int  m    = 0;                      /* bogus init to keep gcc -O happy */
2396
2397 #ifdef DEBUG_SELS
2398     Printf("Selector %s, cns=",textToStr(name(s).text));
2399     printExp(stdout,cns);
2400     Putchar('\n');
2401 #endif
2402
2403     emptySubstitution();
2404     preds = NIL;
2405
2406     for (; nonNull(cns); cns=tl(cns)) {
2407         Name c   = fst(hd(cns));
2408         Int  n   = intOf(snd(hd(cns)));
2409         Int  a   = name(c).arity;
2410         Cell pat = c;
2411         Type dom1;
2412         Type rng1;
2413         Int  o1;
2414         Int  m1;
2415
2416         instantiate(name(c).type);      /* Instantiate constructor type    */
2417         o1 = typeOff;
2418         m1 = typeFree;
2419         for (; nonNull(predsAre); predsAre=tl(predsAre))
2420             assumeEvid(hd(predsAre),o1);
2421
2422         if (whatIs(typeIs)==RANK2)      /* Skip rank2 annotation, if any   */
2423             typeIs = snd(snd(typeIs));
2424         for (; --n>0; a--) {            /* Get range                       */
2425             pat    = ap(pat,WILDCARD);
2426             typeIs = arg(typeIs);
2427         }
2428         rng1   = dropRank1(arg(fun(typeIs)),o1,m1);
2429         pat    = ap(pat,nv);
2430         typeIs = arg(typeIs);
2431         while (--a>0) {                 /* And then look for domain        */
2432             pat    = ap(pat,WILDCARD);
2433             typeIs = arg(typeIs);
2434         }
2435         dom1   = typeIs;
2436
2437         if (isNull(dom)) {              /* Save first domain type and then */
2438             dom = dom1;                 /* unify with subsequent domains to*/
2439             o   = o1;                   /* match up preds and range types  */
2440             m   = m1;
2441         }
2442         else if (!unify(dom1,o1,dom,o))
2443             internal("typeSel1");
2444
2445         if (isNull(rng))                /* Compare component types         */
2446             rng = rng1;
2447         else if (!sameSchemes(rng1,rng)) {
2448             clearMarks();
2449             rng  = liftRank1(rng,o,m);
2450             rng1 = liftRank1(rng1,o1,m1);
2451             ERRMSG(name(s).line) "Mismatch in field types for selector \"%s\"",
2452                                  textToStr(name(s).text) ETHEN
2453             ERRTEXT "\n*** Field type     : "            ETHEN ERRTYPE(rng1);
2454             ERRTEXT "\n*** Does not match : "            ETHEN ERRTYPE(rng);
2455             ERRTEXT "\n"
2456             EEND;
2457         }
2458         alts = cons(pair(singleton(pat),pair(mkInt(line),nv)),alts);
2459     }
2460     alts = rev(alts);
2461
2462     if (isNull(dom) || isNull(rng))     /* Should have been initialized by */
2463         internal("typeSel2");           /* now, assuming length cns >= 1.  */
2464
2465     clearMarks();                       /* No fixed variables here         */
2466     preds = scSimplify(preds);          /* Simplify context                */
2467     dom   = copyType(dom,o);            /* Calculate domain type           */
2468     instantiate(rng);
2469     rng   = copyType(typeIs,typeOff);
2470     if (nonNull(predsAre)) {
2471         List ps    = makePredAss(predsAre,typeOff);
2472         List alts1 = alts;
2473         for (; nonNull(alts1); alts1=tl(alts1)) {
2474             Cell body = nv;
2475             List qs   = ps;
2476             for (; nonNull(qs); qs=tl(qs))
2477                 body = ap(body,thd3(hd(qs)));
2478             snd(snd(hd(alts1))) = body;
2479         }
2480         preds = appendOnto(preds,ps);
2481     }
2482     name(s).type  = generalize(copyPreds(preds),fn(dom,rng));
2483     name(s).arity = 1 + length(preds);
2484     map1Proc(qualify,preds,alts);
2485
2486 #ifdef DEBUG_SELS
2487     Printf("Inferred arity = %d, type = ",name(s).arity);
2488     printType(stdout,name(s).type);
2489     Putchar('\n');
2490 #endif
2491
2492     return pair(s,alts);
2493 }
2494
2495
2496 /* --------------------------------------------------------------------------
2497  * Local function prototypes:
2498  * ------------------------------------------------------------------------*/
2499
2500 static Type local basicType Args((Char));
2501
2502
2503 static Type stateVar = NIL;
2504 static Type alphaVar = NIL;
2505 static Type betaVar  = NIL;
2506 static Type gammaVar = NIL;
2507 static Type deltaVar = NIL;
2508 static Int  nextVar  = 0;
2509
2510 static Void clearTyVars( void )
2511 {
2512     stateVar = NIL;
2513     alphaVar = NIL;
2514     betaVar  = NIL;
2515     gammaVar = NIL;
2516     deltaVar = NIL;
2517     nextVar  = 0;
2518 }
2519
2520 static Type mkStateVar( void )
2521 {
2522     if (isNull(stateVar)) {
2523         stateVar = mkOffset(nextVar++);
2524     }
2525     return stateVar;
2526 }
2527
2528 static Type mkAlphaVar( void )
2529 {
2530     if (isNull(alphaVar)) {
2531         alphaVar = mkOffset(nextVar++);
2532     }
2533     return alphaVar;
2534 }
2535
2536 static Type mkBetaVar( void )
2537 {
2538     if (isNull(betaVar)) {
2539         betaVar = mkOffset(nextVar++);
2540     }
2541     return betaVar;
2542 }
2543
2544 static Type mkGammaVar( void )
2545 {
2546     if (isNull(gammaVar)) {
2547         gammaVar = mkOffset(nextVar++);
2548     }
2549     return gammaVar;
2550 }
2551
2552 static Type mkDeltaVar( void )
2553 {
2554     if (isNull(deltaVar)) {
2555         deltaVar = mkOffset(nextVar++);
2556     }
2557     return deltaVar;
2558 }
2559
2560 static Type local basicType(k)
2561 Char k; {
2562     switch (k) {
2563     case CHAR_REP:
2564             return typeChar;
2565     case INT_REP:
2566             return typeInt;
2567     case INTEGER_REP:
2568             return typeInteger;
2569     case ADDR_REP:
2570             return typeAddr;
2571     case WORD_REP:
2572             return typeWord;
2573     case FLOAT_REP:
2574             return typeFloat;
2575     case DOUBLE_REP:
2576             return typeDouble;
2577     case ARR_REP:
2578             return ap(typePrimArray,mkAlphaVar());            
2579     case BARR_REP:
2580             return typePrimByteArray;
2581     case REF_REP:
2582             return ap2(typeRef,mkStateVar(),mkAlphaVar());                  
2583     case MUTARR_REP:
2584             return ap2(typePrimMutableArray,mkStateVar(),mkAlphaVar());     
2585     case MUTBARR_REP:
2586             return ap(typePrimMutableByteArray,mkStateVar()); 
2587     case STABLE_REP:
2588             return ap(typeStable,mkAlphaVar());
2589 #ifdef PROVIDE_WEAK
2590     case WEAK_REP:
2591             return ap(typeWeak,mkAlphaVar());
2592     case IO_REP:
2593             return ap(typeIO,typeUnit);
2594 #endif
2595 #ifdef PROVIDE_FOREIGN
2596     case FOREIGN_REP:
2597             return typeForeign;
2598 #endif
2599     case THREADID_REP:
2600             return typeThreadId;
2601     case MVAR_REP:
2602             return ap(typeMVar,mkAlphaVar());
2603     case BOOL_REP:
2604             return typeBool;
2605     case HANDLER_REP:
2606             return fn(typeException,mkAlphaVar());
2607     case ERROR_REP:
2608             return typeException;
2609     case ALPHA_REP:
2610             return mkAlphaVar();  /* polymorphic */
2611     case BETA_REP:
2612             return mkBetaVar();   /* polymorphic */
2613     case GAMMA_REP:
2614             return mkGammaVar();  /* polymorphic */
2615     case DELTA_REP:
2616             return mkDeltaVar();  /* polymorphic */
2617     default:
2618             printf("Kind: '%c'\n",k);
2619             internal("basicType");
2620     }
2621     assert(0); return 0; /* NOTREACHED */
2622 }
2623
2624 /* Generate type of primop based on list of arg types and result types:
2625  *
2626  * eg primType "II" "II" = Int -> Int -> (Int,Int)
2627  *
2628  */
2629 Type primType( Int /*AsmMonad*/ monad, String a_kinds, String r_kinds )
2630 {
2631     List rs    = NIL;
2632     List as    = NIL;
2633     List tvars = NIL; /* for polymorphic types */
2634     Type r;
2635
2636     clearTyVars();
2637
2638     /* build result types */
2639     for(; *r_kinds; ++r_kinds) {
2640         rs = cons(basicType(*r_kinds),rs);
2641     }
2642     /* Construct tuple of results */
2643     if (length(rs) == 0) {
2644         r = typeUnit;
2645     } else if (length(rs) == 1) {
2646         r = hd(rs);
2647     } else {
2648         r = mkTuple(length(rs));
2649         for(rs = rev(rs); nonNull(rs); rs=tl(rs)) {
2650             r = ap(r,hd(rs));
2651         }
2652     }
2653     /* Construct list of arguments */
2654     for(; *a_kinds; ++a_kinds) {
2655         as = cons(basicType(*a_kinds),as);
2656     }
2657     /* Apply any monad magic */
2658     if (monad == MONAD_IO) {
2659         r = ap(typeIO,r);
2660     } else if (monad == MONAD_ST) {
2661         r = ap2(typeST,mkStateVar(),r);
2662     }
2663     /* glue it all together */
2664     for(; nonNull(as); as=tl(as)) {
2665         r = fn(hd(as),r);
2666     }
2667     tvars = offsetTyvarsIn(r,NIL);
2668     if (nonNull(tvars)) {
2669         assert(length(tvars) == nextVar);
2670         r = mkPolyType(simpleKind(length(tvars)),r);
2671     }
2672 #if DEBUG_CODE
2673     if (debugCode) {
2674         printType(stdout,r); printf("\n");
2675     }
2676 #endif
2677     return r;
2678 }    
2679
2680 /* forall a1 .. am. TC a1 ... am -> Int */
2681 Type conToTagType(t)
2682 Tycon t; {
2683     Type   ty  = t;
2684     List   tvars = NIL;
2685     Int    i   = 0;
2686     for (i=0; i<tycon(t).arity; ++i) {
2687         Offset tv = mkOffset(i);
2688         ty = ap(ty,tv);
2689         tvars = cons(tv,tvars);
2690     }
2691     ty = fn(ty,typeInt);
2692     if (nonNull(tvars)) {
2693         ty = mkPolyType(simpleKind(tycon(t).arity),ty);
2694     }
2695     return ty;
2696 }
2697
2698 /* forall a1 .. am. Int -> TC a1 ... am */
2699 Type tagToConType(t)
2700 Tycon t; {
2701     Type   ty  = t;
2702     List   tvars = NIL;
2703     Int    i   = 0;
2704     for (i=0; i<tycon(t).arity; ++i) {
2705         Offset tv = mkOffset(i);
2706         ty = ap(ty,tv);
2707         tvars = cons(tv,tvars);
2708     }
2709     ty = fn(typeInt,ty);
2710     if (nonNull(tvars)) {
2711         ty = mkPolyType(simpleKind(tycon(t).arity),ty);
2712     }
2713     return ty;
2714 }
2715
2716 /* --------------------------------------------------------------------------
2717  * Type checker control:
2718  * ------------------------------------------------------------------------*/
2719
2720 Void typeChecker(what)
2721 Int what; {
2722     switch (what) {
2723         case RESET   : tcMode       = EXPRESSION;
2724 +                      daSccs       = NIL;
2725                        preds        = NIL;
2726                        pendingBtyvs = NIL;
2727                        daSccs       = NIL;
2728                        emptyAssumption();
2729                        break;
2730
2731         case MARK    : mark(defnBounds);
2732                        mark(varsBounds);
2733                        mark(depends);
2734                        mark(pendingBtyvs);
2735                        mark(skolVars);
2736                        mark(localEvs);
2737                        mark(savedPs);
2738                        mark(dummyVar);
2739                        mark(daSccs);
2740                        mark(preds);
2741                        mark(stdDefaults);
2742                        mark(arrow);
2743                        mark(boundPair);
2744                        mark(listof);
2745                        mark(typeVarToVar);
2746                        mark(predNum);
2747                        mark(predFractional);
2748                        mark(predIntegral);
2749                        mark(starToStar);
2750                        mark(predMonad);
2751                        break;
2752
2753         case INSTALL : typeChecker(RESET);
2754                        dummyVar     = inventVar();
2755
2756                        setCurrModule(modulePrelude);
2757
2758                        starToStar   = simpleKind(1);
2759
2760                        typeUnit     = addPrimTycon(findText("()"),
2761                                                    STAR,0,DATATYPE,NIL);
2762                        typeArrow    = addPrimTycon(findText("(->)"),
2763                                                    simpleKind(2),2,
2764                                                    DATATYPE,NIL);
2765                        typeList     = addPrimTycon(findText("[]"),
2766                                                    starToStar,1,
2767                                                    DATATYPE,NIL);
2768
2769                        arrow        = fn(aVar,bVar);
2770                        listof       = ap(typeList,aVar);
2771                        boundPair    = ap(ap(mkTuple(2),aVar),aVar);
2772
2773                        nameUnit     = addPrimCfun(findText("()"),0,0,typeUnit);
2774                        tycon(typeUnit).defn
2775                                     = singleton(nameUnit);
2776
2777                        nameNil      = addPrimCfun(findText("[]"),0,1,
2778                                                    mkPolyType(starToStar,
2779                                                               listof));
2780                        nameCons     = addPrimCfun(findText(":"),2,2,
2781                                                    mkPolyType(starToStar,
2782                                                               fn(aVar,
2783                                                               fn(listof,
2784                                                                  listof))));
2785                        name(nameNil).parent =
2786                        name(nameCons).parent = typeList;
2787
2788                        name(nameCons).syntax
2789                                     = mkSyntax(RIGHT_ASS,5);
2790
2791                        tycon(typeList).defn
2792                                     = cons(nameNil,cons(nameCons,NIL));
2793
2794                        typeVarToVar = fn(aVar,aVar);
2795 #if TREX
2796                        typeNoRow    = addPrimTycon(findText("EmptyRow"),
2797                                                    ROW,0,DATATYPE,NIL);
2798                        typeRec      = addPrimTycon(findText("Rec"),
2799                                                    pair(ROW,STAR),1,
2800                                                    DATATYPE,NIL);
2801                        nameNoRec    = addPrimCfun(findText("EmptyRec"),0,0,
2802                                                         ap(typeRec,typeNoRow));
2803 #else
2804                        /* bogus definitions to avoid changing the prelude */
2805                        addPrimCfun(findText("Rec"),      0,0,typeUnit);
2806                        addPrimCfun(findText("EmptyRow"), 0,0,typeUnit);
2807                        addPrimCfun(findText("EmptyRec"), 0,0,typeUnit);
2808 #endif
2809                        break;
2810     }
2811 }
2812
2813 /*-------------------------------------------------------------------------*/