3355 lines · 97.0 KB · C
RawDownload
/* -------------------------------------------------------------------------- * This is the Hugs type checker * * The Hugs 98 system is Copyright (c) Mark P Jones, Alastair Reid, the * Yale Haskell Group, and the OGI School of Science & Engineering at OHSU, * 1994-2003, All rights reserved.  It is distributed as free software under * the license in the file "License", which is included in the distribution. * * $RCSfile: type.c,v $ * $Revision: 1.81 $ * $Date: 2005/12/10 11:25:13 $ * ------------------------------------------------------------------------*/ #include "prelude.h"#include "storage.h"#include "connect.h"#include "errors.h"#include "output.h"#include "subst.h"#include "goal.h"#include "opts.h"	/* needed for EXPLAIN_INSTANCE_RESOLUTION|MULTI_INST */ Bool catchAmbigs       = FALSE;		/* TRUE => functions with ambig.   */					/* 	   types produce error	   */ Type typeArrow,   typeList;		/* Important primitive types	   */Type typeUnit; Module modulePrelude;Module moduleUserPrelude; Type typeInt;                          Type typeInt8;                          Type typeInt16;                          Type typeInt32;                          Type typeInt64;                          Type typeWord;Type typeWord8;Type typeWord16;Type typeWord32;Type typeWord64;Type typeFunPtr;Type typePtr;Type typeAddr;Type typeFloat;Type typeDouble;Type typeChar;Type typeForeignP;Type typeForeign;Type typeStable;Type typeBool;Type typeString;#ifdef DOTNETType typeObject;#endif static Type typeInteger; static Type typeMaybe;static Type typeOrdering; Class classEq,    classOrd;		/* `standard' classes		   */Class classIx,    classEnum;Class classShow,  classRead;Class classBounded; Class classReal,       classIntegral;	/* `numeric' classes		   */Class classRealFrac,   classRealFloat;Class classFractional, classFloating;Class classNum; List stdDefaults;			/* standard default values	   */ Name nameFromInt, nameFromDouble;	/* coercion of numerics		   */Name nameFromInteger;Name nameEq,      nameCompare;		/* derivable names		   */Name nameLe;Name nameShowsPrec;Name nameReadsPrec;Name nameMinBnd,  nameMaxBnd;Name nameIndex,	  nameInRange;Name nameRange;Name nameMult,	  namePlus;Name nameTrue,	  nameFalse;		/* primitive boolean constructors  */Name nameNil,     nameCons;		/* primitive list constructors	   */Name nameJust,	  nameNothing;		/* primitive Maybe constructors	   */Name nameLeft,    nameRight;		/* primitive Either constructors   */Name nameUnit;				/* primitive Unit type constructor */Name nameLT,	  nameEQ;		/* Ordering constructors	   */Name nameGT;Class classMonad;			/* Monads			   */Name nameReturn,  nameBind, nameThen;   /* for translating do/monad comps  */Name nameMFail;Name nameGt;				/* for readsPrec		   */ #if MUDOClass classMonadRec;			/* Recursive monads		   */Name nameMFix;#endif #if    IO_MONADType   typeIO;			        /* For the IO monad, IO 	   */Type   typeProgIO;			/* For the IO monad, IO a	   */ Name   nameIOError, nameUserErr;	/* loosely coupled IOError cfuns   */Name   namePermDenied;Name   nameAlreadyExists, nameAlreadyInUse, nameDoesNotExist, nameIsFull;Name   nameIllegal;#endif#if    IO_HANDLESName   nameEOFErr;Name   nameProtocolError;#endifName   nameArithException;Name   nameArrayException;Name   nameErrorCall;Name   nameIOException;Name   nameNoMethodError;Name   nameNonTermination;Name   namePatternMatchFail;Name   nameRecConError;Name   nameRecSelError;Name   nameRecUpdError; Name   nameOverflow;Name   nameDivideByZero;Name   nameIndexOutOfBounds;Name   nameUndefinedElement; #if TREXType  typeNoRow;			/* Empty row			   */Type  typeRec;				/* Record formation		   */Name  nameNoRec;			/* Empty record			   */#endif #if DOTNETName   nameNetException;#endif  /* -------------------------------------------------------------------------- * Local function prototypes: * ------------------------------------------------------------------------*/ static Void   local emptyAssumption   Args((Void));static Void   local enterBindings     Args((Void));static Void   local leaveBindings     Args((Void));static Int    local defType	      Args((Cell));static Type   local useType	      Args((Cell));static Void   local markAssumList     Args((List));static Cell   local findAssum         Args((Text));static Pair   local findInAssumList   Args((Text,List));static List   local intsIntersect     Args((List,List));static List   local genvarAllAss      Args((List));static List   local genvarAnyAss      Args((List));static Int    local newVarsBind       Args((Cell));static Void   local newDefnBind       Args((Cell,Type)); static Void   local enterPendingBtyvs Args((Void));static Void   local leavePendingBtyvs Args((Void));static Cell   local patBtyvs	      Args((Cell));static Void   local doneBtyvs	      Args((Int));static Void   local enterSkolVars     Args((Void));static Void   local leaveSkolVars     Args((Int,Type,Int,Int)); static Void   local typeError         Args((Int,Cell,Cell,String,Type,Int));static Void   local reportTypeError   Args((Int,Cell,Cell,String,Type,Type));static Void   local cantEstablish     Args((Int,String,Cell,Type,List));static Void   local tooGeneral        Args((Int,Cell,Type,Type)); static Cell   local typeExpr          Args((Int,Cell)); static Cell   local typeAp	      Args((Int,Cell));static Type   local typeExpected      Args((Int,String,Cell,Type,Int,Int,Bool));static Void   local typeAlt	      Args((String,Cell,Cell,Type,Int,Int));static Int    local funcType          Args((Int));static Void   local typeCase          Args((Int,Int,Cell));static Void   local typeComp	      Args((Int,Type,Cell,List));static Cell   local typeMonadComp     Args((Int,Cell));#if ZIP_COMPstatic Cell   local typeZComp	      Args((Int,Type,Cell,List));static Void   local typeCompy	      Args((Int,Type,List));static Cell   local typeMonadZComp    Args((Int,Cell));static List   local getPats           Args((List));static Cell   local tupleUp           Args((List));#endifstatic Void   local typeDo	      Args((Int,Cell));#if MUDOstatic Void   local typeRecComp	      Args((Int,Type,Cell,List));static Void   local typeMDo	      Args((Int,Cell));static Void   local typeRecursiveDo   Args((Int,Cell));#endifstatic Void   local typeConFlds	      Args((Int,Cell));static Void   local typeUpdFlds	      Args((Int,Cell));#if IPARAMstatic Cell   local typeWith	      Args((Int,Cell));#endifstatic Cell   local typeFreshPat      Args((Int,Cell)); static Void   local typeBindings      Args((List));static Void   local removeTypeSigs    Args((Cell)); static Void   local monorestrict      Args((List));static Void   local restrictedBindAss Args((Cell));static Void   local restrictedAss     Args((Int,Cell,Type)); static Void   local unrestricted      Args((List));static List   local itbscc	      Args((List));static Void   local addEvidParams     Args((List,Cell)); static Void   local typeClassDefn     Args((Class));static Void   local typeInstDefn      Args((Inst));static Void   local typeMember	      Args((String,Name,Cell,List,Cell,Int)); static Void   local typeBind          Args((Cell));static Void   local typeDefAlt        Args((Int,Cell,Pair));static Cell   local typeRhs           Args((Cell));static Void   local guardedType       Args((Int,Cell)); static Void   local genBind	      Args((List,Cell));static Void   local genAss	      Args((Int,List,Cell,Type));static Type   local genTest	      Args((Int,Cell,List,Type,Type,Int));static Type   local generalize	      Args((List,Type));static Bool   local equalTypes        Args((Type,Type)); static Void   local typeDefnGroup     Args((List));static Void   local typeForeignExport Args((Name));static Pair   local typeSel	      Args((Name)); static Name   local linkName          Args((String));static Tycon  local linkTycon         Args((String));static Class  local linkClass         Args((String)); /* -------------------------------------------------------------------------- * Frequently used type skeletons: * ------------------------------------------------------------------------*/ static Type  arrow;			/* mkOffset(0) -> mkOffset(1)      */static Type  boundPair;			/* (mkOffset(0),mkOffset(0))	   */static Type  listof;			/* [ mkOffset(0) ] 	    	   */static Type  typeVarToVar;		/* mkOffset(0) -> mkOffset(0)  	   */ static Cell  predNum;			/* Num (mkOffset(0))		   */static Cell  predFractional;		/* Fractional (mkOffset(0))	   */static Cell  predIntegral;		/* Integral (mkOffset(0))	   */static Kind  starToStar;		/* Type -> Type			   */static Cell  predMonad;			/* Monad (mkOffset(0))		   */#if MUDOstatic Cell  predMonadRec;		/* MonadRec/MonadFix (mkOffset(0)) */#endif /* -------------------------------------------------------------------------- * Assumptions: * * A basic typing statement is a pair (Var,Type) and an assumption contains * an ordered list of basic typing statements in which the type for a given * variable is given by the most recently added assumption about that var. * * In practice, the assumption set is split between a pair of lists, one * holding assumptions for vars defined in bindings, the other for vars * defined in patterns/binding parameters etc.	The reason for this * separation is that vars defined in bindings may be overloaded (with the * overloading being unknown until the whole binding is typed), whereas the * vars defined in patterns have no overloading.  A form of dependency * analysis (at least as far as calculating dependents within the same group * of value bindings) is required to implement this.  Where it is known that * no overloaded values are defined in a binding (i.e., when the `dreaded * monomorphism restriction' strikes), the list used to record dependents * is flagged with a NODEPENDS tag to avoid gathering dependents at that * level. * * To interleave between vars for bindings and vars for patterns, we use * a list of lists of typing statements for each.  These lists are always * the same length.  The implementation here is very similar to that of the * dependency analysis used in the static analysis component of this system. * * To deal with polymorphic recursion, variables defined in bindings can be * assigned types of the form (POLYREC,(def,use)), where def is a type * variable for the type of the defining occurence, and use is a type * scheme for (recursive) calls/uses of the variable. * ------------------------------------------------------------------------*/ static List defnBounds;			/*::[[(Var,Type)]] possibly ovrlded*/static List varsBounds;			/*::[[(Var,Type)]] not overloaded  */static List depends;			/*::[?[Var]] dependents/NODEPENDS  */static List skolVars;			/*::[[Var]] skolem vars		   */static List localEvs;			/*::[[(Pred,offset,ev)]]	   */static List savedPs;			/*::[[(Pred,offset,ev)]]	   */static Cell dummyVar;			/* Used to put extra tvars into	ass*/ #define saveVarsAss()     List saveAssump = hd(varsBounds)#define restoreVarsAss()  hd(varsBounds)  = saveAssump#define addVarAssump(v,t) hd(varsBounds)  = cons(pair(v,t),hd(varsBounds))#define findTopBinding(v) findInAssumList(textOf(v),hd(defnBounds)) static Void local emptyAssumption() {  	/* set empty type assumption	   */    defnBounds = NIL;    varsBounds = NIL;    depends    = NIL;    skolVars   = NIL;    localEvs   = NIL;    savedPs    = NIL;} static Void local enterBindings() {    /* Add new level to assumption sets */    defnBounds = cons(NIL,defnBounds);    varsBounds = cons(NIL,varsBounds);    depends    = cons(NIL,depends);} static Void local leaveBindings() {    /* Drop one level of assumptions    */    defnBounds = tl(defnBounds);    varsBounds = tl(varsBounds);    depends    = tl(depends);} static Int local defType(a)		/* Return type for defining occ.   */Cell a; {				/* of a var from assumption pair  */    return (isPair(a) && fst(a)==POLYREC) ? fst(snd(a)) : a;} static Type local useType(a)		/* Return type for use of a var	   */Cell a; {				/* defined in an assumption	   */    return (isPair(a) && fst(a)==POLYREC) ? snd(snd(a)) : a;} static Void local markAssumList(as)	/* Mark all types in assumption set*/List as; {				/* :: [(Var, Type)]		   */    for (; nonNull(as); as=tl(as)) {	/* No need to mark generic types;  */	Type t = defType(snd(hd(as)));	/* the only free variables in those*/	if (!isPolyType(t))		/* must have been free earlier too */	    markType(t,0);    }} static Cell local findAssum(t)	       /* Find most recent assumption about*/Text t; {			       /* variable named t, if any	   */    List defnBounds1 = defnBounds;     /* return translated variable, with */    List varsBounds1 = varsBounds;     /* type in typeIs		   */    List depends1    = depends;     while (nonNull(defnBounds1)) {	Pair ass = findInAssumList(t,hd(varsBounds1));/* search varsBounds */	if (nonNull(ass)) {	    typeIs = snd(ass);	    return fst(ass);	} 	ass = findInAssumList(t,hd(defnBounds1));     /* search defnBounds */	if (nonNull(ass)) {	    Cell v = fst(ass);	    typeIs = snd(ass); 	    if (hd(depends1)!=NODEPENDS &&	      /* save dependent?   */		  isNull(v=varIsMember(t,hd(depends1))))		/* N.B. make new copy of variable and store this on list of*/		/* dependents, and in the assumption so that all uses of   */		/* the variable will be at the same node, if we need to    */		/* overwrite the call of a function with a translation...  */		hd(depends1) = cons(v=mkVar(t),hd(depends1)); 	    return v;	} 	defnBounds1 = tl(defnBounds1);		      /* look in next level*/	varsBounds1 = tl(varsBounds1);		      /* of assumption set */	depends1    = tl(depends1);    }    return NIL;} static Pair local findInAssumList(t,as)/* Search for assumption for var    */Text t;				       /* named t in list of assumptions as*/List as; {    for (; nonNull(as); as=tl(as))	if (textOf(fst(hd(as)))==t)	    return hd(as);    return NIL;} static List local intsIntersect(as,bs)	/* calculate intersection of lists */List as, bs; {				/* of integers (as sets)	   */    List ts = NIL;			/* destructively modifies as	   */    while (nonNull(as))	if (intIsMember(intOf(hd(as)),bs)) {	    List temp = tl(as);	    tl(as)    = ts;	    ts	      = as;	    as	      = temp;	}	else	    as = tl(as);    return ts;} static List local genvarAllAss(as)	/* calculate generic vars that are */List as; {				/* in every type in assumptions as */    List vs = genvarTyvar(intOf(defType(snd(hd(as)))),NIL);    for (as=tl(as); nonNull(as) && nonNull(vs); as=tl(as))	vs = intsIntersect(vs,genvarTyvar(intOf(defType(snd(hd(as)))),NIL));    return vs;} static List local genvarAnyAss(as)	/* calculate generic vars that are */List as; {				/* in any type in assumptions as   */    List vs = genvarTyvar(intOf(defType(snd(hd(as)))),NIL);    for (as=tl(as); nonNull(as); as=tl(as))	vs = genvarTyvar(intOf(defType(snd(hd(as)))),vs);    return vs;} static Int local newVarsBind(v)        /* make new assump for pattern var  */Cell v; {    Int beta = newTyvars(1);    addVarAssump(v,mkInt(beta));#if DEBUG_TYPES    Printf("variable, assume ");    printExp(stdout,v);    Printf(" :: _%d\n",beta);#endif    return beta;} static Void local newDefnBind(v,type)  /* make new assump for defn var	   */Cell v; 			       /* and set type if given (nonNull)  */Type type; {    Int  beta	   = newTyvars(1);    Cell ta        = mkInt(beta);    instantiate(type);    if (nonNull(type) && isPolyType(type))	ta = pair(POLYREC,pair(ta,type));    hd(defnBounds) = cons(pair(v,ta), hd(defnBounds));#if DEBUG_TYPES    Printf("definition, assume ");    printExp(stdout,v);    Printf(" :: _%d\n",beta);#endif    bindTv(beta,typeIs,typeOff);       /* Bind beta to new type skeleton   */} /* -------------------------------------------------------------------------- * Predicates: * ------------------------------------------------------------------------*/ #include "preds.c" /* -------------------------------------------------------------------------- * Bound and skolemized type variables: * ------------------------------------------------------------------------*/ static List pendingBtyvs = NIL; static Void local enterPendingBtyvs() {    enterBtyvs();    pendingBtyvs = cons(NIL,pendingBtyvs);} static Void local leavePendingBtyvsQuietly() {    pendingBtyvs = tl(pendingBtyvs);    leaveBtyvs();} static Void local leavePendingBtyvs() {    List pts     = hd(pendingBtyvs);    pendingBtyvs = tl(pendingBtyvs);    for (; nonNull(pts); pts=tl(pts)) {	Int  line = intOf(fst(hd(pts)));	List vs   = snd(hd(pts));	Int  i    = 0;	clearMarks();	for (; nonNull(vs); vs=tl(vs)) {	    Cell v = fst(hd(vs));	    Cell t = copyTyvar(intOf(snd(hd(vs))));	    if (!isOffset(t)) {		ERRMSG(line) "Type annotation uses variable " ETHEN ERREXPR(v);		ERRTEXT      " where a more specific type "   ETHEN ERRTYPE(t);		ERRTEXT      " was inferred"		EEND;	    }	    else if (offsetOf(t)!=i) {		List us = snd(hd(pts));		Int  j  = offsetOf(t);		if (j>=i)		    internal("leavePendingBtyvs");		for (; j>0; j--)		    us = tl(us);		ERRMSG(line) "Type annotation uses distinct variables " ETHEN		ERREXPR(v);  ERRTEXT " and " ETHEN ERREXPR(fst(hd(us)));		ERRTEXT      " where a single variable was inferred"		EEND;	    }	    else		i++;	}    }    leaveBtyvs();} static Cell local patBtyvs(p)		/* Strip bound type vars from pat  */Cell p; {    if (whatIs(p)==BIGLAM) {

Lines 1–500 of 3355.