{-
    Kaya - My favourite toy language.
    Copyright (C) 2004, 2005 Edwin Brady

    This file is distributed under the terms of the GNU General
    Public Licence. See COPYING for licence.
-}

module Inference where

-- Type inference algorithm

import Options
import Language
import InfGadgets
import VarUsage
import PMComp
import Module

import Debug.Trace
import List
import Control.Monad

-- Step one : insert type declarations (with UnknownType) so that at least
-- we know what all the variables are.

mkpub (x,y) = (x,(y,[Public]))
mkCtxtEntry opts (x,y) = (x,(y,opts))

insertdecl :: Name -> -- Module
              EContext ->
              GContext -> Context -> Raw -> Raw
-- Make sure we insert *below* the top level lambda, or we'll have problems.
insertdecl mod excs globs ctxt (RLambda str l tvs ns exp) =
      (RLambda str l tvs ns (insertdecl mod excs globs 
			     (addNames ctxt (map mkpub ns)) exp))
insertdecl mod excs globs ctxt t = 
    declare (nubBy cmpnames (gu False ((getNames ctxt)++(map fst globs)) t)) t
 -- Pass through list of vars declared
 where
   cmpnames (_,_,x) (_,_,y) = x==y
   gu mtch ds (RVar str l n) = checkdecl mtch (str,l,n) ds []
   gu mtch ds (RQVar str l n) = checkdecl mtch (str,l,n) ds []
   gu mtch ds (RLambda str l tvs ns exp) = 
         gu mtch (ds++(map fst ns)) exp
   gu mtch ds (RClosure str l ns exp) = 
         gu mtch (ds++(map fst ns)) exp
   gu mtch ds (RDeclare str l (n,loc) ty exp) =
         gu mtch (n:ds) exp
   gu mtch ds (RBind str l n ty val exp) =
         {- gu mtch ds val ++ -} gu mtch (n:ds) exp
   -- We want to check the rhs of an assignment, but not if it's a name.
   -- We look because we might find a case statement or some kind of embedded
   -- sequence with an assignment. We eliminate names at first because we don't
   -- want a declaration inserted if this is the only place they are referred 
   -- to!
   gu mtch ds (RAssign str l lval (RVar _ _ _)) 
       = checkdecl mtch (getlv lval) ds [] --(gu mtch ds exp)
   gu mtch ds (RAssign str l lval (RQVar _ _ _)) 
       = checkdecl mtch (getlv lval) ds [] --(gu mtch ds exp)
   gu mtch ds (RAssign str l lval exp) = checkdecl mtch (getlv lval) ds (gu mtch ds exp)
   gu mtch ds (RAssignOp str l op lval exp) = 
       checkdecl mtch (getlv lval) ds [] --(gu mtch ds exp)
   gu mtch ds (RSeq str l lseq rseq) =
       gu mtch ds lseq ++ gu mtch ds rseq
   gu mtch ds (RReturn _ _ (RCase str l v exps)) 
       = {-gu mtch ds v ++ -} (concat (map (gua mtch ds) exps))
   -- if we're returning something complicated (like a for loop generated
   -- from a list comprehension, we'd better look for variables assigned
   -- inside it.
   gu mtch ds (RReturn _ _ a@(RSeq _ _ _ _)) = gu mtch ds a
   gu mtch ds (RReturn str l a) = []
   gu mtch ds (RApply str l fn args) =
       -- Names in applications must be declared or used already, except
       -- in match patterns, and except if the arguments are closures.
       -- (i.e. it's an argument which may cause assignment to happen)
       if mtch then (concat (map (gu True ds) args))
          else (concat (map (gcu ds) args))
      where gcu ds rc@(RClosure _ _ _ _) = gu mtch ds rc
            gcu _ _ = []
   gu mtch ds (RPartial str l fn args) = []
       -- Names in applications must be declared or used already.
       --checkdecl mtch fn ds (concat (map (gu mtch ds) args))
   gu mtch ds (RForeign str l ty fn args) = []
       -- Names in applications must be declared or used already.
       --checkdecl mtch fn ds (concat (map (gu mtch ds) args))
       --concat (map (gu mtch ds) args)
   gu mtch ds (RWhile str l c body) =
       {-gu mtch ds c ++ -} gu mtch ds body
   gu mtch ds (RDoWhile str l body c) =
       {-gu mtch ds c ++ -} gu mtch ds body
   gu mtch ds (RFor str l lval nm (RVar _ _ _) body) =
       checkdecl mtch (getlv lval) ds (gu mtch ds body)
   gu mtch ds (RFor str l lval nm t body) =
       checkdecl mtch (getlv lval) ds (gu mtch ds body ++ gu mtch ds t)
--   gu mtch ds (RFor str l lval (Just nm) t body) =
--       checkdecl mtch (str,l,nm) ds $ checkdecl mtch (getlv lval) ds (gu mtch ds body)
   gu mtch ds (RTryCatch str l tr ca x fin) =
       checkdecl mtch (str,l,x) ds ((gu mtch ds tr) ++ (gu mtch ds ca) ++ (gu mtch ds fin))
   gu mtch ds (RNewTryCatch str l tblock cs) =
       gu mtch ds tblock ++ (concat (map (gue mtch ds) cs))
   gu mtch ds (RThrow str l a) = []
   gu mtch ds (RExcept str l a b) = []
   gu mtch ds (RPrint str l v) = [] --gu mtch ds v
   gu mtch ds (RInfix str l op x y) = [] -- gu mtch ds x ++ gu mtch ds y
   gu mtch ds (RUnary str l op v) = [] -- gu mtch ds v
   gu mtch ds (RCoerce str l t v) = [] --gu mtch ds v
   gu mtch ds (RCase str l v exps) = {-gu mtch ds v ++ -} 
                                     (concat (map (gua mtch ds) exps))
   gu mtch ds (RMatch str l v exps) = {-gu mtch ds v ++ -} 
                                      (concat (map (guma ds) exps))
   gu mtch ds (RIf str l c t f) = {-gu mtch ds c ++ -} 
                                  gu mtch ds t ++ gu mtch ds f
   gu mtch ds (RIndex str l x y) = [] -- gu mtch ds x ++ gu mtch ds y
   gu mtch ds (RArrayInit str l xs) = 
       -- Names in array initialisation must be declared or used already, 
       -- except in match patterns
       if mtch then (concat (map (gu True ds) xs))
          else []
   gu mtch ds x = []

   -- Look for variables used in case branches
   gua mtch ds (RAlt str l f as exp) = (cd mtch str l as ds) ++ (gu mtch ds exp)
   gua mtch ds (RArrayAlt str l as exp) = (cd mtch str l as ds) ++ (gu mtch ds exp)
   gua mtch ds (RConstAlt str l c exp) = gu mtch ds exp
   gua mtch ds (RDefault str l exp) = gu mtch ds exp

   guma ds (MAlt str l ps exp)
       = (concat (map (gu True ds) ps)) ++ (gu False ds exp)

   -- Look for variables used in catch clauses
   gue mtch ds (RCatch str l (Left (ex,as)) exp) = (cd mtch str l as ds) ++ (gu mtch ds exp)
   -- only insert the declaration if 'v' isn't a global name
   gue mtch ds (RCatch str l (Right v) exp) 
       = case lookupname mod v excs of
            [] -> checkdecl mtch (str,l,v) ds (gu mtch ds exp)
            _ -> gue mtch ds (RCatch str l (Left (v,[])) exp)
   -- Check for whether each in a list of vars has been declared
   -- Return those which need declarations inserted
   cd mtch str l [] ds = []
   cd mtch str l (x:xs) ds = checkdecl mtch (str,l,x) ds (cd mtch str l xs ds)

   -- Add a declaration if we come across a variable that hasn't been declared.
   -- If we're in a match pattern, also check whether the name is in global
   -- scope.
   checkdecl mtch (f,l,var) ds rest 
       = case (var `elem` ds, mtch, lookupname mod var ctxt) of
             -- in local scope, do nothing
	    (True, _, _) -> rest
             -- in global scope, and we're in a match
            (_, True, xs) -> if (all nonConstructor xs) then (f,l,var):rest
                                else rest
             -- not in local scope, so add it (don't care about global scope)
	    (False, _, _) -> (f,l,var):rest

   nonConstructor (n,(ty,opts)) = not (Constructor `elem` opts)

   getlv (RAName str l x) = (str,l,x)
   getlv (RAIndex str l lv t) = getlv lv
   getlv (RAField str l lv n) = getlv lv

   declare :: [(String,Int,Name)] -> Raw -> Raw
   declare [] t = t
   declare ((str,l,x):xs) t = RDeclare str l (x,False) UnknownType (declare xs t)

-- Now do type inference/checking. If there's a declaration, work out the
-- type declared.
-- Step two: Create a list of type equations to solve.

{- We record equations as a list of the equations we initially made (so
   they can be dumped for debugging) and build a substitution as we go (for
   the sake of efficiency; we don't want to have to rebuild it) -} 
type Equation = ([(Type, Type, String, Int, String)], Subst)

ideq = ([],id_subst)

infer mod ctxt globs excs tags tys fld t ftyp copts =
  infertype mod ctxt globs excs tags tys fld t ftyp (Prim Void) copts

infertype :: MonadPlus m => 
	     Name -> -- Module name
	     Context -> -- Global definitions
	     GContext -> -- Global variables
             EContext -> -- Exception types
	     Tags -> -- Constructor tags
	     Types -> -- Type information
	     Fields -> -- Field names
	     Raw -> -- Term to check
	     Type -> -- Expected return type (for a function)
             Type -> -- Expected value type
             Options -> -- Compiler options
	     m (Expr Name, Equation) -- Well typed term, substitution
infertype mod ctxt globs excs tags tys flds t ftype vtype copts = do 
      (exp',eqn,_) <- ti [] 0 t ideq vtype mkrexp
      return (exp',eqn)
 where 
   mkrexp = case ftype of 
                (Fn _ _ UnknownType) -> TyVar (MN ("rettype", 0))
                _ -> getrtype (appsyn tys ftype)
   getrtype (Fn _ _ ret) = ret

   tiVar env next (RVar file line n) eqns exp disambig rexp =
   -- reverse the environment to get most recent binding first.
      case (lookup n (reverse env)) of
        Nothing -> findfun n
        (Just t) -> do let (nt, next') = (t,next) -- fudgevars t next -- NO! Only generalise type variables for global functions!
                       let (realt, realn) = isapply nt (Global n "" (argSpace t))
		       neweqn <- addEq file line (realt,exp,"identifier '" ++ showuser n++"'") eqns
		       return (realn, neweqn, next')
     where findfun n
	    = case (ctxtlookup mod n ctxt disambig copts) of
	      -- TMP HACK!
	        (Failure err f l) -> if take 4 err == "Ambi" || take 4 err == "Can'"
				      then fail $ file++":"++show line ++ ":" ++err
				      else findglob n
		(Success (rn,t)) -> do let (nt, next') = fudgevars t next
				       let (realt, realn) = isapply nt (Global rn (mangling t) (argSpace t))
				       neweqn <- addEq file line (realt,exp,"identifier '" ++ showuser n ++ "'") eqns
				       return (realn, neweqn, next')
	   findglob n 
                = case lookup n globs of
		     Nothing -> fail $ tyerror file line ("Unknown name:" ++ showuser n ++ "\n")-- ++ ctxtdump ctxt)
		     (Just (t,i)) -> do
		         neweqn <- addEq file line (t,exp,"identifier '" ++ showuser n ++ "'") eqns
			 return (GVar i, neweqn, next)
	   isapply t@(Fn [] [] ty) f = (ty,Annotation (Line file line) (Apply f []))
	   isapply t f = (t,f)
   tiVar env next (RQVar file line n) eqns exp disambig rexp =
   -- reverse the environment to get most recent binding first.
   -- trace ("*** trying " ++ (show n) ++ " : " ++ (show exp)) $
      case (lookup n (reverse env)) of
        Nothing -> findfun n
        (Just t) -> do let (nt, next') = (t,next) -- fudgevars t next
		       neweqn <- addEq file line (nt,exp,"identifier '" ++ showuser n ++ "'") eqns
		       return (Global n "" (argSpace t), neweqn, next')
      where findfun n = case (ctxtlookup mod n ctxt disambig copts) of
	      -- TMP HACK!
	        (Failure err f l) -> if take 4 err == "Ambi" || take 4 err == "Can'" 
				      then fail $ file++":"++show line++ ":" ++err
				      else findglob n
	        (Success (rn,t)) -> do let (nt, next') = fudgevars t next
				       neweqn <- addEq file line (nt,exp,"identifier '" ++ showuser n ++ "'") eqns
				       return (Global rn (mangling t) (argSpace t), neweqn, next')
	    findglob n 
                = case lookup n globs of
		     Nothing -> fail $ tyerror file line ("Unknown name:" ++ showuser n ++ "\n")-- ++ ctxtdump ctxt)
		     (Just (t,i)) -> do
		         neweqn <- addEq file line (t,exp,"identifier '" ++ showuser n ++ "'") eqns
			 return (GVar i, neweqn, next)
   tiVar env next e eqns exp disambig rexp = ti env next e eqns exp rexp

   ti env next v@(RVar file line n) eqns exp rexp =
       tiVar env next v eqns exp Nothing rexp
   ti env next v@(RQVar file line n) eqns exp rexp =
       tiVar env next v eqns exp Nothing rexp
   ti env next (RConst file line c) eqns exp rexp = do
      let (cv,ct) = tcConst c
      eqn' <- addEq file line (ct,exp,"constant " ++ show c) eqns
      return (cv, eqn', next)
   ti env next (RLambda file line isvars ns body) eqns exp rexp = do
      ns' <- mapM (normalisectx file line mod tys) ns
      (bcheck,beqns,next') <- ti (env++(map (synctx tys) ns')) next body eqns (Prim Void) rexp 
      let vbody = pToV (map mkpub ns') bcheck 
      return (Lambda isvars ns' vbody, beqns, next')
   ti env next (RClosure file line ns body) eqns exp rexp = do
      (tns,next') <- inserttvs ns next
      ns' <- mapM (normalisectx file line mod tys) tns
      let newrexp = TyVar (MN ("CLOSRET",next'))
      let closenv = (env++(map (synctx tys) ns'))
      (bcheck,beqns,next'') <- {-trace (show closenv) $-} ti closenv (next'+1) body eqns (Prim Void) newrexp 
      let vbody = pToV (map mkpub closenv) bcheck 
      let clostype = Fn [] (map snd ns') newrexp
      ceqns <- addEq file line (clostype,exp,"closure") beqns
      -- phi <- mkSubst ceqns
      -- checkReturn file line "lambda" (subst phi clostype) vbody
      -- use annotation for return checking
      return (Annotation (Line file line) (Closure ns' newrexp vbody), 
                         ceqns, next'')
    where inserttvs [] next = return ([],next)
	  inserttvs ((n,UnknownType):xs) next = do
	      (xs',next') <- inserttvs xs next
	      let newtv = TyVar (MN ("CLOS",next'))
	      return ((n,newtv):xs',next'+1)
	  inserttvs (x:xs) next = do
	      (xs',next') <- inserttvs xs next
	      return ((x:xs'),next')
   ti env next (RBind file line n t v sc) eqns exp rexp = do
      let syntin = appsyn tys t
      synt <- normalise False file line mod tys syntin
      let newenv = env ++ [(n,synt)]
      (vinf,veqns,next') <- ti env (next+1) v eqns synt rexp 
      (scinf,sceqns,next'') <- ti newenv next' sc veqns exp rexp
      let vsc = pToV (map mkpub newenv) scinf
      return (Bind n synt vinf vsc, sceqns, next'')
   ti env next (RDeclare file line (n,loc) UnknownType sc) eqns exp rexp = do
      let newtv = TyVar (MN ("TYPE",next))
      let newenv = env ++ [(n,newtv)]
      (scinf,sceqns,next') <- ti newenv (next+1) sc eqns exp rexp
      let vsc = pToV (map mkpub newenv) scinf
      let used = isUsed (length env) vsc
      return (Declare file line (n, not used) newtv vsc, sceqns, next')
   ti env next (RDeclare file line (n,loc) t sc) eqns exp rexp = do
--      let newtv = TyVar (MN ("TYPE",next))
      let synt = appsyn tys t
      let newenv = env ++ [(n,synt)]
      (scinf,sceqns,next') <- ti newenv (next+1) sc eqns exp rexp
      let vsc = pToV (map mkpub newenv) scinf
      let used = isUsed (length env) vsc
      return (Declare file line (n, not used) synt vsc, sceqns, next')
   ti env next (RReturn file line v) eqns exp rexp = do
      (vinf, veqns, next') <- ti env next v eqns rexp rexp
      neweqns <- addEq file line (Prim Void, exp, "return") veqns
      return (Return vinf, neweqns, next')
   ti env next (RAssign file line l v) eqns exp rexp = do
      (lcheck,lt,leqns,next') <- tclval env next l eqns rexp
      (vinf,veqns,next'') <- ti env next' v leqns lt rexp
      neweqns <- addEq file line (Prim Void,exp, "assignment") veqns
      return (Annotation (Line file line) (Assign lcheck vinf), neweqns, next'')
   ti env next (RAssignOp file line op l v) eqns exp rexp = do
      (lcheck,lt,leqns,next') <- tclval env next l eqns rexp
      (vinf,veqns,next'') <- ti env next' v leqns lt rexp
      neweqns <- addEq file line (Prim Void,exp, "assignment") veqns
      return (AssignOp op lcheck vinf, neweqns, next'')
   ti env next (RSeq file line a b) eqns exp  rexp= do
      (ainf, aeqns, next') <- ti env next a eqns (Prim Void) rexp
      (binf, beqns, next'') <- ti env next' b aeqns exp rexp
      return (Seq ainf binf, beqns, next'')
   ti env next (RApply file line f args) eqns exp rexp = do
      let newtv = TyVar (MN ("TYPE",next))
      -- Try checking f with expected type newtv(pre_atypes); if 
      -- checking it with any old expected type doesn't work.
      (finf,feqns,next') <- mplus
         (ti env (next+1) f eqns newtv rexp)
         (do -- need args to help us disambiguate f
             let (pre_atypesin, next') = mkatypes args (next+1)
             (_, pre_aeqns, next'') <- checkargs args pre_atypesin eqns next'
             phi <- mkSubst pre_aeqns
             let calledFnType = Fn [] (map (subst phi) pre_atypesin) newtv
             tiVar env next'' f eqns newtv (Just calledFnType) rexp)
      phi <- mkSubst feqns
      let ftype = subst phi newtv
      let (Fn defs argtypes _) = ftype
      let fcheck = needsCheck ftype
      -- Change the application so that default args are added
      let args' = insertdefaults args ftype
      let (atypes, next'') = mkatypes args' next'
      let reqtype = Fn [] atypes exp
      neweqns <- addEq file line (ftype, reqtype, "application" ++ showraw f) feqns
      --let atypes' = map (subst phi) atypes
      (achecks, aeqns, next'') <- checkargs args' atypes neweqns next''
--      (finf,feqns,next'') <- ti env next' (RQVar file line f) aeqns reqtype
      let app = case fcheck of
                   False -> (Apply finf achecks)
                   True -> Annotation (DynCheck exp) 
                               (Apply finf achecks)
--      neweqns <- addEq file line (reqtype, ftype) aeqns
      return (Annotation (Line file line) app, aeqns, next'')
     where mkatypes :: [Raw] -> Int -> ([Type],Int)
           mkatypes [] next = ([],next)
           mkatypes (x:xs) next = 
               let (xs', next') = mkatypes xs next in
                   ((TyVar (MN ("TYPE", next')):xs'), next'+1)
           checkargs [] [] eqns next = return ([],eqns,next)
	   checkargs (a:as) (at:ats) eqns next = do
              (achecks, aeqns,next') <- checkargs as ats eqns next
              phi <- mkSubst aeqns
	      let phi_at = subst phi at --TyVar (MN ("TYPE",next'))
	      (ainf,aeqns',next'') <- tiVar env (next'+1) a aeqns phi_at (Just phi_at) rexp
	      return (ainf:achecks,aeqns',next'')
-- ECB: This is awful. I only *think* I know how it works...
   ti env next (RPartial file line f args) eqns exp rexp = do
      let (atypes, next') = mkatypes args next
      (achecks, aeqns, next') <- checkargs args atypes eqns next'
      let newtv = TyVar (MN ("TYPE",next'))
      phi_pre <- mkSubst aeqns
      let calledFnType = Fn [] (map (subst phi_pre) atypes) newtv
      (finf,feqns,next'') <- mplus 
          -- Do it in this order to get better error messages. If the program
          -- is type correct, the first one will always work.
          (tiVar env (next'+1) f aeqns newtv (Just calledFnType) rexp)
          (ti env (next'+1) f aeqns newtv rexp)
      phi <- mkSubst feqns
      -- Replace f's real arg types with atype, to get equations right
      let (ftype,numleft) = insertatypes atypes (subst phi newtv)
      -- Work out the type of the whole partial application
      reqtype <- mangleType atypes ftype
      eqns' <- addEq file line (reqtype,exp, "partial application" ++ showraw f) feqns
      eqns'' <- addEq file line (newtv,ftype, "partial application" ++ showraw f) eqns'
--      (finf,feqns,next'') <- ti env next' (RQVar file line f) aeqns reqtype
      return (Partial False finf achecks numleft, eqns'', next'')
     where mkatypes :: [Raw] -> Int -> ([Type],Int)
           mkatypes [] next = ([],next)
           mkatypes (x:xs) next = 
               let (xs', next') = mkatypes xs next in
                   ((TyVar (MN ("TYPE", next')):xs'), next'+1)
           checkargs [] [] eqns next = return ([],eqns,next)
	   checkargs (a:as) (at:ats) eqns next = do
              (achecks,aeqns,next') <- checkargs as ats eqns next
              phi <- mkSubst aeqns
	      let phi_at = subst phi at --TyVar (MN ("TYPE",next'))
	      (ainf,aeqns',next'') <- tiVar env (next'+1) a aeqns phi_at (Just phi_at) rexp
	      return (ainf:achecks,aeqns',next'')
	   mangleType atypes (Fn defs args ret) 
	       = do (newdefs, newargs) <- remove atypes defs args
		    return $ Fn newdefs newargs ret
	   mangleType atypes ret = return $ Fn [] atypes ret

	   remove (a:as) (d:ds) (b:bs) = remove as ds bs
	   remove (a:as) [] (b:bs) = remove as [] bs
	   remove [] ds xs = return (ds,xs)
	   remove xs _ [] = fail $ file ++":" ++show line ++ 
			      ":Too many arguments in partial application"

	   insertatypes xs (Fn defs args ret) = 
	       let (newargs,numleft) = ia xs args in
		   (Fn defs newargs ret, numleft)
	   ia [] as = (as, length as)
	   ia (x:xs) (a:as) = let (newargs,numleft) = (ia xs as) in
				  (x:newargs,numleft)
	   ia xs [] = ([], 0)
   ti env next (RForeign file line ty f args) eqns exp rexp = do
      (achecks,aeqns,next') <- checkargs args eqns next 
      neweqns <- addEq file line (appsyn tys ty, exp, "foreign application") aeqns
      return (Foreign (appsyn tys ty) f achecks, neweqns, next')
     where checkargs [] eqns next = return ([],eqns,next)
	   checkargs (a:as) eqns next = do
              (achecks,aeqns,next') <- checkargs as eqns next
	      let newtv = TyVar (MN ("TYPE",next'))
	      (ainf,aeqns',next'') <- ti env (next'+1) a aeqns newtv rexp
	      return ((ainf,newtv):achecks,aeqns',next'')
   ti env next (RWhile file line cond loop) eqns exp rexp = do
      (cinf, ceqns, next') <- ti env next cond eqns (Prim Boolean) rexp
      (linf, leqns, next'') <- ti env next' loop ceqns (Prim Void) rexp
      neweqns <- addEq file line (Prim Void, exp, "while loop") leqns
      return (While cinf linf, neweqns, next'')
   ti env next (RDoWhile file line loop cond) eqns exp rexp = do
      (cinf, ceqns, next') <- ti env next cond eqns (Prim Boolean) rexp
      (linf, leqns, next'') <- ti env next' loop ceqns (Prim Void) rexp
      neweqns <- addEq file line (Prim Void, exp, "do...while loop") leqns
      return (DoWhile linf cinf, neweqns, next'')
   ti env next (RFor file line l idxname vals loop) eqns exp rexp = do
      let counter1 = case idxname of
                       Nothing -> MN ("counter",(length env))
                       Just x -> x
      let counter2 = MN ("counter",(length env)+1)
      (lcheck,lt,leqns,next') <- tclval env next l eqns rexp
      let arraylt = TyVar (MN ("TYPE",next'))
      let env' = env ++ [(counter1,Prim Number),(counter2,arraylt)]
      (vinf, veqns, next'') <- ti env' (next'+1) vals leqns arraylt rexp
      phi <- mkSubst veqns
      let atype = subst phi arraylt
      case atype of
         Array _ -> do
	   veqns' <- addEq file line (arraylt, Array lt, "for loop") veqns
	   (linf, leqns, next''') <- ti env' next'' loop veqns' (Prim Void) rexp
           let vl = pToV (map mkpub env') linf
	   neweqns <- addEq file line (Prim Void, exp, "for loop") leqns
	   let counteri = length env
	   let counterj = (length env)+1
	   return (For counteri (Just counter1) counterj lcheck vinf vl, neweqns, next''')
-- convert into a call to 
-- try {
--    traverse(\(lt l, Int idxname) { loop; return true; }, vals);
-- } catch(Return(v)) {
--     return v;
-- } (or equivalent VoidReturn if we're in a void function)
-- inside loop, top level break becomes 'return false'
-- VoidReturn becomes throw(VoidReturn), return x becomes throw(Return(x))
-- Check it like it's an ordinary loop, then mangle the contents.
         TyApp _ [argt] -> 
             do let countername = case idxname of
                                    (Just n) -> n
                                    Nothing -> (MN ("counter", next'))
            -- TMP HACK: don't care about the answer, just want to verify it
                -- It's needlessly slow to do this twice. But while we get
                -- it working it's much easier than manipulating typechecked
                -- things where we have to deal with the new exception variable
                -- we're about to introduce...
	        (_,_,_) <- ti env' next'' loop veqns (Prim Void) rexp
                lname <- case l of
                           (RAName f l n) -> return n
                           _ -> fail $ file ++ ":" ++ show line ++ ":for loop must assign to a variable"
                let blocklam = RClosure file line [(lname, argt),
                                                   (countername, Prim Number)]
                                                  (RSeq file line modloop
                                                        (RReturn file line 
                                                           (RConst file line
                                                             (Bo True))))
                let code = RDeclare file line ((MN ("c", next'+1)), True)
                                              UnknownType
                           (RNewTryCatch file line 
                           (RApply file line (RQVar file line (UN "traverse")) 
                                            [blocklam, vals])
                            (catchBlock rexp (next'+1)))
                ti env (next'+2) code veqns exp rexp
         t -> fail $ file ++ ":" ++ show line ++ ":for loop cannot iterate over " ++ show t
      where seq x y = RSeq file line x y
	    bind n t v b = RBind file line n t v b
	    cname = (MN ("lazycount",next))
	    count = RVar file line cname
	    apply x y = RApply file line 
			  (RQVar file line (NS (UN "LazyArray") (UN x))) y
	    while x y = RWhile file line x y
	    not b = RUnary file line Not b
	    assign l v = RAssign file line l v
	    assignname l v = RAssign file line (RAName file line l) v
            modloop = mkTraverse loop
            catchBlock (Prim Void) next
                = [RCatch file line (Left ((UN "Loop_VoidReturn"),[]))
                          (RVoidReturn file line)]
            catchBlock _ next
                = [RCatch file line (Left ((UN "Loop_Return"), 
                                           [(MN ("c", next))]))
                         (RReturn file line 
                            (RApply file line (RVar file line (UN "subvert"))
                              [(RQVar file line (MN ("c", next)))]))]

   ti env next (RTryCatch file line tr ca x fin) eqns exp rexp = do
      (trinf, treqns, next') <- ti env next tr eqns (Prim Void) rexp
      (cainf, caeqns, next'') <- ti env next' ca treqns (Prim Void) rexp
      (xinf, xeqns, next''') <- ti env next'' (RVar file line x) caeqns (Prim Exception) rexp
      (fininf, feqns, next'''') <- ti env next''' fin xeqns (Prim Void) rexp
--      (yinf, yeqns, next'''') <- ti env next''' (RVar file line y) xeqns (Prim Number)
      return (TryCatch trinf cainf xinf fininf, feqns, next'''')
   ti env next (RNewTryCatch file line tr cs) eqns exp rexp = do
      (trinf, treqns, next') <- ti env next tr eqns (Prim Void) rexp
      (csinf, cseqns, next'') <- exinf env next' cs treqns (Prim Void) rexp
      return (NewTryCatch trinf csinf, cseqns, next'')
   ti env next (RThrow file line exc) eqns exp rexp = do
      (einf, eeqns, next') <- ti env next exc eqns (Prim Exception) rexp
      return (Annotation (Line file line) (Throw einf), eeqns, next')
   ti env next (RExcept file line str code) eqns exp rexp = do
      (sinf, seqns, next') <- ti env next str eqns (Prim StringType) rexp
      (cinf, ceqns, next'') <- ti env next' code seqns (Prim Number) rexp
      return (Except sinf cinf, ceqns, next'')
   ti env next (RBreak file line) eqns exp rexp = do
       neweqns <- addEq file line (Prim Void, exp, "break") eqns
       return (Break file line, neweqns, next)
   ti env next (RVoidReturn file line) eqns exp rexp =
       case rexp of
           (Prim Void) -> do
               neweqns <- addEq file line (Prim Void, exp, "return") eqns
               return (VoidReturn, neweqns, next)
           _ -> fail $ file ++ ":" ++ show line ++ ":must return a value from non-void function"
   ti env next (RPrint file line r) eqns exp rexp = do
      let rtv = TyVar (MN ("TYPE",next))
      (rinf, reqns, next') <- ti env (next+1) r eqns rtv rexp
      neweqns <- addEq file line (Prim Void,exp,"trace") reqns
      return (InferPrint rinf rtv file line, neweqns, next')
   ti env next (RInfix file line op x y) eqns exp rexp = do
      let xtv = TyVar (MN ("TYPE",next))
      (xinf, xeqns, next') <- ti env (next+1) x eqns xtv rexp
      let ytv = TyVar (MN ("TYPE",next'))
      (yinf, yeqns, next'') <- ti env (next'+1) y xeqns ytv rexp
      phi <- mkSubst yeqns
      let xtype = subst phi xtv
      let ytype = subst phi ytv
      neweqns <- addEq file line ((getOpType op xtype ytype),exp,"operator "++show op) yeqns
      -- Some infix operators must act on variables
      -- of the same type, others can have coercions inserted
      neweqns' <- addOpEq op file line (xtv,ytv,"operator "++show op) neweqns
      return (InferInfix op xinf yinf (xtype,ytype,(getOpType op xtype ytype)) file line, neweqns', next'')
    where addOpEq Equal f l eq eqns = addEq f l eq eqns
	  addOpEq NEqual f l eq eqns = addEq f l eq eqns
	  addOpEq _ f l eq eqns = return eqns
   ti env next (RUnary file line op x) eqns exp rexp = do
      let xtv = TyVar (MN ("TYPE",next))
      (xinf, xeqns, next') <- ti env (next+1) x eqns xtv rexp
      neweqns <- addEq file line ((getUnaryType op xtv),exp,"operator "++show op) xeqns
      return (InferUnary op xinf (xtv,getUnaryType op xtv) file line, neweqns, next')
   ti env next (RCoerce file line t v) eqns exp rexp = do
      let vtv = TyVar (MN ("TYPE",next))
      (vinf,veqns,next') <- ti env (next+1) v eqns vtv rexp
      neweqns <- addEq file line (t,exp,"coercion") veqns
      return (InferCoerce vtv t vinf file line, neweqns, next')
   ti env next (RCase file line v alts) eqns exp rexp = do
      let vtv = TyVar (MN ("TYPE",next))
      (vinf,veqns,next') <- ti env (next+1) v eqns vtv rexp
      (alts,aeqns,next'') <- altinf env next' alts veqns vtv exp rexp
      return (Annotation (Line file line) (Case vinf (sort alts)), 
                         aeqns, next'')
   ti env next (RMatch file line v alts) eqns exp rexp = do
      -- Check the alternatives before we do anything, because then the
      -- error message will be based on the actual code, not the transformed
      -- code. It's a bit wasteful, because we have to do it again anyway,
      -- but at least it gives meaningful feedback, and helps verify that
      -- the match compiler is correct,
      let vtv = TyVar (MN ("TYPE",next))
      (eqns', next') <- verifyAlts env (next+1) alts eqns vtv exp rexp
      case (mkSubst eqns') of
          Failure e f l -> fail e
          _ -> return ()
      mapM_ (checkLinear mod ctxt) alts
      let (simpleCase, next') = mkCase file line ctxt mod next v alts
      {- trace (show simpleCase) $ -} 
      ti env next simpleCase eqns exp rexp
   ti env next (RIf file line cond ift iff) eqns exp rexp = do
      (cinf, ceqns, next') <- ti env next cond eqns (Prim Boolean) rexp
      (tinf, teqns, next'') <- ti env next' ift ceqns exp rexp
      (finf, eeqns, next''') <- ti env next'' iff teqns exp rexp
      return (If cinf tinf finf, eeqns, next''')
   ti env next (RIndex file line e i) eqns exp rexp = do
       (einf, eeqns, next') <- ti env next e eqns (Array exp) rexp
       (iinf, ieqns, next'') <- ti env next' i eeqns (Prim Number) rexp
       return (Index einf iinf, ieqns, next'')
   ti env next (RField file line v f) eqns exp rexp = do
       let newtv = TyVar (MN ("FV",next))
       (vinf, veqns, next') <- ti env (next+1) v eqns newtv rexp
       -- Need to know what newtv really is before we go on...
       phi <- mkSubst veqns
       let vtype = subst phi newtv
       let (fudgedt, next'') = fudgevars vtype next'
       lookt <- normalise False file line mod tys fudgedt
       (fty, arg, tag) <- getFieldType flds f lookt file line
       eqns' <- addEq file line (fty, exp, "field access '" ++ showuser f ++ "'") veqns
       return (Annotation (Line file line) (Field vinf f arg tag), 
	      eqns', next'')
   ti env next (RArrayInit file line xs) eqns exp rexp = do
       let newtv = TyVar (MN ("TYPE",next))
       eqns' <- addEq file line (Array newtv, exp, "array initialisation") eqns 
       (xsinf, xseqns, next') <- tis env (next+1) xs eqns' newtv
       return (ArrayInit xsinf, xseqns, next')
     where tis env next [] eqns exp = return ([], eqns, next)
	   tis env next (x:xs) eqns exp = do
	       (xinf,xeqns,next') <- ti env next x eqns exp rexp
	       (xsinf,xseqns,next'') <- tis env next' xs xeqns exp
	       return (xinf:xsinf, xseqns, next'')
   ti env next (RNoop file line) eqns exp rexp = do
       neweqns <- addEq file line (Prim Void, exp, "no-op") eqns
       return (Noop, neweqns, next)
   ti env next (RUnderscore file line) eqns exp rexp = 
       -- placeholder - this never gets compiled.
       return (Noop, eqns, next)
   ti env next (RVMPtr file line) eqns exp rexp = do
       neweqns <- addEq file line (Prim Pointer, exp, "VM pointer") eqns
       return (VMPtr, neweqns, next)
   ti env next (RLength file line str) eqns exp rexp = do
       eqns' <- addEq file line (Prim Number, exp, "string length") eqns 
       (strinf, streqns, next') <- ti env (next+1) str eqns' (Prim StringType) rexp
       return (Length strinf, streqns, next')
   ti env next (RMetavar f l i) eqns exp rexp = 
       return (Metavar f l i, eqns, next)
       
--   ti env next x eqns exp = error $ show x

   verifyAlts env next [] eqns vt exp rexp = return (eqns, next)
   -- the parser will only ever give us one pattern, this only becomes a list
   -- during intermediate stages (for the moment). Don't check the return
   -- value, that'll get done later.
   -- All we're doing here is checking that the patterns are all consistent
   -- with each other.
   verifyAlts env next ((MAlt _ _ [p] res):ms) eqns vt exp rexp
      = do (pinf, peqns, next') <- ti env next p eqns vt rexp
           (eqns', next'') <- verifyAlts env next' ms peqns vt exp rexp
           return (eqns', next'')

   altinf env next [] eqns vt exp rexp = return ([],eqns,next)
   altinf env next ((RDefault file line r):xs) eqns vt exp rexp
    = do (xsinf, xseqns, next') <- altinf env next xs eqns vt exp rexp
         (rinf, reqns, next'') <- ti env next' r xseqns exp rexp
         return ((Default rinf):xsinf, reqns, next'')
   altinf env next ((RConstAlt file line c r):xs) eqns vt exp rexp
    = do (xsinf, xseqns, next') <- altinf env next xs eqns vt exp rexp
         let (cv,Prim ct) = tcConst c -- ct and vt should be the same
	 -- ct must be something we can do a case on
	 checkCaseable ct file line
         (rinf, reqns, next'') <- ti env next' r xseqns exp rexp
         neweqns <- addEq file line (vt, Prim ct, "case constant") reqns
         return ((ConstAlt ct c rinf):xsinf, neweqns, next'')   
     where checkCaseable Number _ _ = return ()
	   checkCaseable Character _ _ = return ()
	   checkCaseable Boolean _ _ = return ()
	   checkCaseable StringType _ _ = return ()
	   checkCaseable x f l = fail $ f ++":"++show l++":" ++
		   "Can't do case analysis on " ++ show (Prim x)
   altinf env next ((RArrayAlt file line args r):xs) eqns vt exp rexp 
    = do let arr = RArrayInit file line (map (RVar file line) args)
         (arinf, areqns, next') <- ti env next arr eqns vt rexp
         (xsinf, xseqns, next'') <- altinf env next' xs areqns vt exp rexp
         (rinf, reqns, next''') <- ti env next'' r xseqns exp rexp
         return ((ArrayAlt (map (\x -> Global x file line) args) rinf):xsinf,
                  reqns, next''')
   altinf env next ((RAlt file line con args r):xs) eqns vt exp rexp 
    = do
       conname <- case ctxtlookup mod con ctxt Nothing copts of
                     Success x -> return x
                     Failure err _ _ -> fail $ file ++ ":" ++ show line ++
                                               ":" ++ err
       let app = RApply file line (RQVar file line (fst conname)) (map (RVar file line) args)
--       let app = RApply file line con (map (RVar file line) args)
       (ainf,aeqns,next') <- ti env next app eqns vt rexp
       (xsinf, xseqns, next'') <- altinf env next' xs aeqns vt exp rexp
       (rinf,reqns,next''') <- ti env next'' r xseqns exp rexp
       (tag,tot) <- gettag (fst conname)
       return ((Alt tag tot (map (\x -> Global x file line) args) rinf):xsinf,reqns,next''')

   exinf env next [] eqns exp rexp = return ([], eqns, next)
   exinf env next ((RCatch f l (Left (ex,args)) handler):xs) eqns exp rexp = do
      (rest, eqns', next') <- exinf env next xs eqns exp rexp
      case exceptlookup mod ex excs of
          Got (fulln, tys) -> do
             (args, eqns'', next'') <- checkExArgs f l tys args env eqns' next' rexp
             (hinf, heqns, next''') <- ti env next'' handler eqns'' exp rexp
             return ((Catch (Left (fulln, args)) hinf):rest, heqns, next''')
          am -> fail $ f ++ ":" ++ show l ++ ":" ++ show am
   exinf env next ((RCatch f l (Right x) handler):xs) eqns exp rexp = do
      -- if x is a defined exception, we should match against it rather
      -- than use this as the catch all case.
      case exceptlookup mod x excs of
          Got (fulln, _) ->
              exinf env next ((RCatch f l (Left (x, [])) handler):xs) eqns exp rexp
          _ -> do (rest, eqns', next') <- exinf env next xs eqns exp rexp
                  -- 'rest' will never get caught, so don't compile it.
                  (hinf, heqns, next'') <- ti env next' handler eqns' exp rexp
                  (xinf, xeqns, next''') <- ti env next'' (RVar f l x) heqns (Prim Exception) rexp
                  return ((Catch (Right xinf) hinf):[], xeqns, next''')
   checkExArgs f l [] [] env eqns next rexp = return ([], eqns, next)
   checkExArgs f l (ty:tys) (x:args) env eqns next rexp = do
      (rest, eqns', next') <- checkExArgs f l tys args env eqns next rexp
      (xinf, xeqns, next'') <- ti env next' (RVar f l x) eqns' ty rexp
      return (xinf:rest, xeqns, next'')
   checkExArgs f l [] _ _ _ _ _ = fail $ f ++ ":" ++ show l ++ ":Too many arguments to exception"
   checkExArgs f l _ _ _ _ _ _ = fail $ f ++ ":" ++ show l ++ ":Too few arguments to exception"


   gettag n = case lookup n tags of
	         Nothing -> fail $ "Internal tag error (" ++ showuser n ++ "\n" ++ show tags ++ ")"
		 (Just a) -> return a

   tclval env next (RAName file line n) eqns rexp = do
       let np = getpos n (map mkpub env)
       case (getType n env) of
               Just nt -> return (AName np,(appsyn tys nt),eqns, next)
	       Nothing -> do case getType n globs of
				Just (gt,gid) ->
				    return (AGlob gid,(appsyn tys gt), eqns, next)
				Nothing -> fail $ file++":"++show line++":Need type declaration for name " ++ showuser n
   tclval env next (RAIndex file line r idx) eqns rexp = do
       (iinf,ieqns,next') <- ti env next idx eqns (Prim Number) rexp
       (rcheck,rt,reqns,next'') <- tclval env next' r ieqns rexp
       let newtv = TyVar (MN ("TYPE",next''))
       neweqns <- addEq file line (rt,Array newtv, "array lvalue") reqns 
       return (AIndex rcheck iinf, newtv, neweqns,(next''+1))
   tclval env next (RAField file line r f) eqns rexp = do
       (rcheck,rt,reqns,next') <- tclval env next r eqns rexp
       -- n needs to be a valid field for the type of r
       -- get the real type of r
       phi <- mkSubst reqns
       let realrt = subst phi rt
       let (fudgedt, next'') = fudgevars realrt next'
       lookt <- normalise False file line mod tys fudgedt
       (fty, arg, tag) <- getFieldType flds f lookt file line
       return (AField rcheck f arg tag, (appsyn tys fty), reqns, next'')

-- Need to take possible coercions into account too!
   getOpType Plus x y = (biggert x y)
   getOpType Minus x y = (biggert x y)
   getOpType Times x y = (biggert x y)
   getOpType Divide x y = (biggert x y)
   getOpType Modulo x y = (biggert x y)
   getOpType Power x y = (biggert x y)
   getOpType OpShLeft x y = (biggert x y)
   getOpType OpShRight x y = (biggert x y)
   getOpType OpAnd x y = (biggert x y)
   getOpType OpOr x y = (biggert x y)
   getOpType OpXOR x y = (biggert x y)
   getOpType _ _ _ = Prim Boolean

   getUnaryType Not x = x
   getUnaryType Neg x = x

   tyerror file line x = file ++ ":" ++ show line ++ ":" ++ x

   -- FIXME: Check that the default arguments are valid things
{-
   insertdefaults :: [Raw] -> Raw -> Context -> [Raw]
   insertdefaults args (RQVar _ _ f) ctxt =
       case (ctxtlookup mod f ctxt) of
          Nothing -> args
	  Just (n,(Fn defs _ _)) -> idefs' defs args
   insertdefaults args (RVar _ _ f) ctxt =
       case (ctxtlookup mod f ctxt) of
          Nothing -> args
	  Just (n,(Fn defs _ _)) -> idefs' defs args
   insertdefaults args _ _ = args -}
   insertdefaults :: [Raw] -> Type -> [Raw]
   insertdefaults args (Fn defs _ _) = idefs' defs args
   insertdefaults args _ = args

   idefs' [] [] = []
   idefs' (x:xs) (y:ys) = y:(idefs' xs ys)
   idefs' (Just v:xs) [] = v:(idefs' xs [])
   idefs' _ ys = ys



addEq :: Monad m => String -> Int -> (Type,Type,String) -> 
         Equation -> m Equation
--addEq file line (lt,rt) phi = unify phi ((subst phi lt),(subst phi rt),file,line)
addEq file line (lt,rt,ctxt) (eqn,subst) 
    = case unify subst (lt,rt,file,line,ctxt) of
          Success subst' -> return ((lt,rt,file,line,ctxt):eqn,subst')
	  Failure err f l -> fail $ err

getFieldType :: Monad m => Fields -> 
		Name -> -- Field name
		Type -> -- Type to project field from (needs to be concrete)
		String ->
		Int ->
		m (Type, Int, Int) -- Field type, argument and tag.
getFieldType fs f ty file line = {- trace (show fs) $ -}
		       fieldLookup fs f ty file line

fieldLookup :: Monad m => Fields -> Name -> Type -> String -> Int ->
	       m (Type, Int, Int)
fieldLookup [] n ty f l = fail $ f ++ ":" ++ show l ++ ":" ++ showuser n ++ " is an unknown field of " ++ show ty 
fieldLookup (((n,ty),(fty, arg, tag)): xs) fn exp f l
    | n == fn = case (getVarTypes ty exp ("field access '" ++ showuser fn ++ "'")) of
	          Nothing -> fieldLookup xs fn exp f l
		  (Just phi) -> return ({-trace ("Found " ++ show ty ++ "," ++ show fty ++ "," ++ show (subst phi fty))-} (subst phi fty, arg,tag))
    | otherwise = fieldLookup xs fn exp f l


tcConst :: Const -> (Expr Name, Type)
tcConst (Num x) = (GConst (Num x), Prim Number)
tcConst (Ch c) = (GConst (Ch c), Prim Character)
tcConst (Bo b) = (GConst (Bo b), Prim Boolean)
tcConst (Re r) = (GConst (Re r), Prim RealNum)
tcConst (Str s) = (GConst (Str s), Prim StringType)
tcConst (Exc s i) = (GConst (Exc s i), Prim Exception)
tcConst Empty = (GConst Empty, Prim Void)

appsyn tys t = {- trace ((show t) ++ " to " ++ show (syn t)) $ -} syn t where
    syn (Prim p) = (Prim p)
    syn (Fn ns ts t) = Fn ns (map syn ts) (syn t)
    syn (Array t) = Array (syn t)
    syn (User n) = User (resolve tys n)
    syn (TyApp n ts) = TyApp (syn n) (map syn ts)
    syn UnknownType = UnknownType
{-       where resolve [] n = n
	     resolve ((cn@(NS _ bn),ti):xs) n | bn == n = cn
	     resolve ((x,ti):xs) n | x == n = x
	     resolve (_:xs) n = resolve xs n-}
--    syn (Syn n) = error "Internal error"
{- case lookup n tys of
		     Nothing -> (TyVar n)
		     (Just x) -> x -}
    syn (TyVar n) = TyVar n

synctx tys (n,ty) = (n,appsyn tys ty)
normalisectx f l mod tys (n,ty) = do ty' <- normalise True f l mod tys ty
                                     return (n,ty')

checkTy :: Monad m => Types -> Type -> Type -> String -> m ()
checkTy tys x y err = if convert (appsyn tys x) (appsyn tys y)
			     then return ()
			     else fail err


-- Step 3: Given a list of type equations, work out what types the
-- type variables actually are. Do this by unifying all the equations.
-- Do something hairy to maintain a list of all the errors that come up.

mkSubst :: Monad m => Equation -> m Subst
mkSubst (eqs,s) = return s

{-
mkSubst eqs = do phi <- mkS' [] eqs
		 case phi of
		     (x,[]) -> return x
		     (_,errs) -> fail $ concat $ reverse $ map (++"\n") (nub errs)
mkS' errs [] = return (id_subst,[])
mkS' errs ((t1,t2,f,l):xs) = do
    (phi',errs') <- mkS' errs xs
    case unify phi' (t1,t2,f,l) of
        Success newphi -> return (newphi,errs')
	Failure err f l -> return (phi',err:errs')
-}

-- Step 4: Substitute the type equations into the term with the substitution
-- we got from the last step.

substTerm :: Monad m => Name -> -- Module name
             Context -> Subst -> Expr Name -> m (Expr Name)
substTerm mod ctxt phi t = st t
   where
     st (Lambda iv args exp) = do exp' <- st exp
				  return $ Lambda iv (lamsubst args) exp'
 	where lamsubst [] = []
 	      lamsubst ((n,ty):xs) = (n,subst phi ty):(lamsubst xs)
     st (Annotation (Line f l) (Closure args rt exp)) = 
	 do exp' <- st exp
            -- Check here that closure contains a return statement
            checkReturn f l "lambda" (Fn [] [] (subst phi rt)) exp'
            -- finished with annotation now
	    return $ Closure (lamsubst args) (subst phi rt) exp'
 	where lamsubst [] = []
 	      lamsubst ((n,ty):xs) = (n,subst phi ty):(lamsubst xs)
     st (Bind n ty e1 e2) = do e1' <- st e1
			       e2' <- st e2
			       return $ Bind n (subst phi ty) e1' e2'
     st (Declare f l n ty e) = 
	 do e' <- st e
	    let ty' = subst phi ty
	    case ty' of
	        (Prim Void) ->
		     fail $ f ++":"++ show l ++":"++
			  showuser (fst n) ++ " has type Void"
		_ -> return $ Declare f l n ty' e'
     st (Return r) = do r' <- st r
			return $ Return r'
     st (Assign a e) = do e' <- st e
			  a' <- asubst a
			  return $ Assign a' e'
         where asubst (AName x) = return $ AName x
	       asubst (AGlob i) = return $ AGlob i
 	       asubst (AIndex a e) = do a' <- asubst a
					e' <- st e
					return $ AIndex a' e'
	       asubst (AField a n arg t) = do a' <- asubst a
					      return $ AField a' n arg t
     st (AssignOp op a e) = do e' <- st e
			       a' <- asubst a
			       return $ AssignOp op a' e'
         where asubst (AName x) = return $ AName x
	       asubst (AGlob i) = return $ AGlob i
 	       asubst (AIndex a e) = do a' <- asubst a
					e' <- st e
					return $ AIndex a' e'
	       asubst (AField a n arg t) = do a' <- asubst a
					      return $ AField a' n arg t
     st (Seq e1 e2) = do e1' <- st e1
			 e2' <- st e2
			 return $ Seq e1' e2'
     st (Apply e1 args) = do e1' <- st e1
			     args' <- mapM st args
			     return $ Apply e1' args'
     st (Partial b e1 args i) 
	   = do e1' <- st e1
		args' <- mapM st args
		return $ Partial b e1' args' i
     st (Foreign ty n args) = do args' <- fsubst args
				 return $ Foreign (subst phi ty) n args'
         where fsubst [] = return []
 	       fsubst ((e,ty):xs) = do e' <- st e
				       rest <- fsubst xs
				       return $ (e',subst phi ty):rest
     st (While e1 e2) = do e1' <- st e1
			   e2' <- st e2
			   return $ While e1' e2'
     st (DoWhile e1 e2) = do e1' <- st e1
			     e2' <- st e2
			     return $ DoWhile e1' e2'
     st (For x nm y a e1 e2) = do e1' <- st e1
                                  e2' <- st e2
                                  a' <- asubst a
                                  return $ For x nm y a' e1' e2'
         where asubst (AName x) = return $ AName x
 	       asubst (AIndex a e) = do a' <- asubst a
					e' <- st e
					return $ AIndex a' e'
     st (TryCatch t c x f) = do t' <- st t
				c' <- st c
				f' <- st f
				return $ TryCatch t' c' x f'
     st (NewTryCatch t cs) = do t' <- st t
				cs' <- stc cs
				return $ NewTryCatch t' cs'
          where stc [] = return []
                stc ((Catch (Right e) h):cs) = do
                     cs' <- stc cs
                     e' <- st e
                     h' <- st h
                     return ((Catch (Right e') h'):cs')
                stc ((Catch (Left (n,es)) h):cs) = do
                     cs' <- stc cs
                     es' <- mapM st es
                     h' <- st h
                     return ((Catch (Left (n,es')) h'):cs')
     st (Throw x) = do x' <- st x
		       return (Throw x')
     st (Except x y) = do x' <- st x
			  y' <- st y
			  return (Except x' y')
     st (InferPrint e t f l) = do 
       e' <- st e
       case (subst phi t) of
            (Prim Number) -> return $ PrintNum e'
	    (Prim StringType) -> return $ PrintStr e'
	    (Prim Exception) -> return $ PrintExc e'
	    _ -> fail $ f ++ ":" ++ show l ++ ":Can't print type " ++ show t
     st (InferInfix op e1 e2 (t1,t2,t3) f l) = do
	 e1' <- st e1
	 e2' <- st e2
	 checkInfix mod ctxt op e1' e2' (subst phi t1) (subst phi t2) (subst phi t3) f l
-- 	InferInfix op (st e1) (st e2) (subst phi t1,subst phi t2,subst phi t3)
-- 		   f l
     st (Append e1 e2) = do
	 e1' <- st e1
	 e2' <- st e2
	 return $ Append e1' e2'
     st (InferUnary op e1 (t1,t2) f l) = do
         e1' <- st e1
	 checkUnary op e1' (subst phi t1) (subst phi t2) f l
-- 	InferUnary op (st e1) (subst phi t1,subst phi t2) f l
     st (InferCoerce t1 t2 e f l) = do 
          e' <- st e
	  checkCoerce (subst phi t1) (subst phi t2) e' f l
     st (Case e1 e2) = do e1' <- st e1
			  e2' <- stalt e2
			  return $ Case e1' e2'
          where stalt [] = return []
                stalt ((Default ex):xs) =
                    do ex' <- st ex
                       rest <- stalt xs
                       return $ (Default ex'):rest
                stalt ((ConstAlt pt c ex):xs) =
                    do ex' <- st ex
                       rest <- stalt xs
                       return $ (ConstAlt pt c ex'):rest
		stalt ((Alt n t exps ex):xs) = 
		    do ex' <- st ex
		       exps' <- mapM st exps
		       rest <- stalt xs
		       return $ (Alt n t exps' ex'):rest
		stalt ((ArrayAlt exps ex):xs) = 
		    do ex' <- st ex
		       exps' <- mapM st exps
		       rest <- stalt xs
		       return $ (ArrayAlt exps' ex'):rest
     st (ArrayInit e) = do e' <- mapM st e
			   return $ ArrayInit e'
     st (If e1 e2 e3) = do e1' <- st e1
			   e2' <- st e2
			   e3' <- st e3
			   return $ If e1' e2' e3'
     st (Index e1 e2) = do e1' <- st e1
			   e2' <- st e2
			   return $ Index e1' e2'
     st (Field e n a t) = do e' <- st e
			     return $ Field e' n a t
     st (Annotation (DynCheck t) e) 
         = do e' <- st e
	      return $ Annotation (DynCheck (subst phi t)) e'
     st (Annotation a e) = do e' <- st e
			      return $ Annotation a e'
     st x = return x

checkInfix :: Monad m => Name -> Context -> Op -> Expr Name -> Expr Name -> 
	                 Type -> Type -> Type -> 
			 String -> Int -> m (Expr Name)
-- If the types are different, try to insert a coercion
checkInfix mod ctxt op l r (Prim x) (Prim y) ret file line
    | x `tlt` y = do col <- implicitCoerce x y l file line
		     checkInfix mod ctxt op col r (Prim y) (Prim y) ret file line
    | y `tlt` x = do cor <- implicitCoerce y x r file line
		     checkInfix mod ctxt op l cor (Prim x) (Prim x) ret file line
checkInfix mod ctxt op l r (Prim StringType) (Prim StringType) (Prim Boolean) file line
  | (op==Equal || op == NEqual) =
    return $ CmpStr op l r
checkInfix mod ctxt Plus l r (Prim StringType) (Prim StringType) (Prim StringType) file line
 = return $ Append l r
checkInfix mod ctxt op l r (Prim Number) (Prim Number) (Prim Number) file line
  | (op==Plus || op==Minus || op==Times || op==Divide || op==Modulo || 
     op==Power || op==OpAnd || op==OpOr || op==OpXOR || 
     op==OpShLeft || op==OpShRight)
      = return $ Infix op l r
checkInfix mod ctxt op l r (Prim RealNum) (Prim RealNum) (Prim RealNum) file line
  | (op==Plus || op==Minus || op==Times || op==Divide || 
     op==Power || op==OpAnd || op==OpOr)
      = return $ RealInfix op l r
checkInfix mod ctxt op l r (Prim Number) (Prim Number) (Prim Boolean) file line
  | (op==Equal || op==NEqual || op==OpLT || op==OpGT ||
     op==OpLE || op==OpGE)
      = return $ Infix op l r
checkInfix mod ctxt op l r (Prim RealNum) (Prim RealNum) (Prim Boolean) file line
  | (op==Equal || op==NEqual || op==OpLT || op==OpGT ||
     op==OpLE || op==OpGE)
      = return $ RealInfix op l r
checkInfix mod ctxt op l r (Prim Character) (Prim Character) (Prim Boolean) file line
  | (op==Equal || op==NEqual || op==OpLT || op==OpGT ||
     op==OpLE || op==OpGE)
      = return $ Infix op l r
checkInfix mod ctxt op l r (Prim Boolean) (Prim Boolean) (Prim Boolean) file line
  | (op==Equal || op==NEqual || op==OpAndBool || op==OpOrBool)
      = return $ Infix op l r
checkInfix mod ctxt op l r (Prim Exception) (Prim Exception) (Prim Boolean) file line
  | (op==Equal || op==NEqual)
      = return $ CmpExcept op l r

-- Defaults for equality, pass through to built in equal function
checkInfix mod ctxt Equal l r t1 t2 (Prim Boolean) file line
      | t1==t2 = return $ Apply (Global eqfun eqmangle 2) [l,r]
checkInfix mod ctxt NEqual l r t1 t2 (Prim Boolean) file line
      | t1==t2 = return $ Unary Not (Apply (Global eqfun eqmangle 2) [l,r])
{-
Operator overloading: It works but I'm still not switching it on until
I've either worked out proper general overloading or decided we shouldn't
worry about it.
checkInfix mod ctxt op l r tl tr ret file line
   | Just (nm,ty@(Fn _ _ rty)) <- 
       ctxtlookup mod (OP op) ctxt (Just (Fn [] [tl,tr] ret)) []
      = if (rty == ret) then 
           return $ Apply (Global nm (mangling ty) (argSpace ty)) [l,r]
           else fail $ file ++ ":" ++ show line ++ ":Can't apply operator '" ++ show op ++ "' to " ++ show tl ++ " and " ++ show tr ++ " to give " ++ show ret
-}

checkInfix mod ctxt op l r tl tr ret file line = fail $ file ++ ":" ++ show line ++ ":Can't apply operator '" ++ show op ++ "' to " ++ show tl ++ " and " ++ show tr ++ " to give " ++ show ret

checkUnary :: Monad m => UnOp -> Expr Name -> 
	                 Type -> Type -> 
			 String -> Int -> m (Expr Name)
checkUnary Not l (Prim Boolean) (Prim Boolean) file line = 
    return $ Unary Not l
checkUnary Neg l (Prim Number) (Prim Number) file line = 
    return $ Unary Neg l
checkUnary Neg l (Prim RealNum) (Prim RealNum) file line = 
    return $ RealUnary Neg l
checkUnary op l tl ret file line = fail $ file ++ ":" ++ show line ++ ":Can't apply operator '" ++ show op ++ "' to " ++ show tl ++ " to give " ++ show ret

checkCoerce :: Monad m => Type -> Type -> Expr Name -> String -> Int ->
	       m (Expr Name)
checkCoerce t1 t2 e file line
  | (t1==(Prim Number) && t2==(Prim StringType)) ||
    (t1==(Prim StringType) && t2==(Prim Number)) ||
    (t1==(Prim RealNum) && t2==(Prim StringType)) ||
    (t1==(Prim StringType) && t2==(Prim RealNum)) ||
    (t1==(Prim Character) && t2==(Prim StringType)) ||
    (t1==(Prim Boolean) && t2==(Prim StringType)) ||
    (t1==(Prim RealNum) && t2==(Prim Number)) ||
    (t1==(Prim Number) && t2==(Prim RealNum)) ||
    (t1==(Prim Character) && t2==(Prim Number)) ||
    (t1==(Prim Number) && t2==(Prim Character))
	= return $ Coerce t1 t2 e
  | otherwise = fail $ file ++ ":" ++ show line ++ ":Can't coerce from " ++ show t1 ++ " to " ++ show t2

implicitCoerce :: Monad m => PrimType -> PrimType -> Expr Name -> 
		  String -> Int -> m (Expr Name)
implicitCoerce x y e f l = checkCoerce (Prim x) (Prim y) e f l

{-
mkCtxt :: ParseResult -> Tags -> Types -> Context
mkCtxt [] tags syns = []
mkCtxt ((FB (x,xt,_)):xs) tags syns 
  = let xft = appsyn syns xt in
      ((x,xft):(mkCtxt xs))
mkCtxt (_:xs) tags syns = mkCtxt xs
-}

type InferError = String

-- Main inference function; go through all of the definitions and get
-- their types.
inferAll :: MonadPlus m => Name -> -- Current module name
	    Context -> [InferError] -> GContext -> EContext ->
            Tags -> Types -> Fields ->
	    Bool -> [RawDecl] -> Options ->
	        m (Program, [InferError], Context, GContext, EContext, 
                   Tags, Types)
-- Finished
inferAll mod ctxt errs globs excs tags syns flds dump [] copts
    = return ([], [], ctxt,globs,excs,tags,syns)

-- C Includes
inferAll mod ctxt errs globs excs tags syns flds dump ((CInc str):xs) copts = 
  do (rest, errs, ctxt', globs', excs', tags',syns') <- inferAll mod ctxt errs globs excs tags syns flds dump xs copts
     return $ ((CInclude str):rest, errs, ctxt', globs', excs', tags',syns')
-- Function map names (lifted functions)
inferAll mod ctxt errs globs excs tags syns flds dump ((FMN str):xs) copts = 
  do (rest, errs, ctxt', globs', excs', tags',syns') <- inferAll mod ctxt errs globs excs tags syns flds dump xs copts
     return $ ((FMName str):rest, errs, ctxt', globs', excs', tags',syns')

-- Import statements
inferAll mod ctxt errs globs excs tags syns flds dump ((Imp str):xs) copts = 
  do (rest, errs, ctxt', globs', excs', tags',syns') <- inferAll mod ctxt errs globs excs tags syns flds dump xs copts
     return $ ((Imported str):rest, errs, ctxt', globs', excs', tags',syns')

-- Import searches (ignoreable)
inferAll mod ctxt errs globs excs tags syns flds dump ((SearchImport str):xs) copts = 
  do inferAll mod ctxt errs globs excs tags syns flds dump xs copts

-- Link directives
inferAll mod ctxt errs globs excs tags syns flds dump ((Link str):xs) copts = 
  do (rest, errs, ctxt', globs', excs', tags',syns') <- inferAll mod ctxt errs globs excs tags syns flds dump xs copts
     return $ ((Linker str):rest, errs, ctxt', globs', excs', tags',syns')

-- Global variables
inferAll mod ctxt errs globs excs tags syns flds dump ((GlobDecl file line (n,t,v)):xs) copts =
  do st <- normalise False file line mod syns t
     let gid = length globs
     (rest, errs, ctxt', globs', excs', tags',syns') <- 
	 inferAll mod ctxt errs ((n,(st,gid)):globs) excs tags syns flds dump xs copts
     vval <- checkGlob file line mod ctxt' globs excs tags syns flds v st copts
     return ((Glob (n,st,gid,vval):rest), errs, ctxt', ((n,(st,gid)):globs), excs', tags', syns')

-- Constant functions with no type label. We need to do these separately,
-- because we need to determine their type before typechecking other functions
-- (usually we know the type of everything in advance)
inferAll mod ctxt errs globs excs tags syns flds dump ((FB (file,line,x,Fn [] [] UnknownType,fopts,Defined xr) comm):xs) copts = 
  do let xft' = Fn [] [] (TyVar (MN ("ret",0)))
     let xrdec = insertdecl mod excs globs (addName ctxt x xft' fopts) xr
     case infer mod ctxt globs excs tags syns flds xrdec 
                xft' copts of
        Failure err f l -> do
              -- check the rest anyway to see if we can get more errors
             (rest, errs', ctxt', globs', excs', tags',syns') <- 
	         inferAll mod ctxt errs globs excs tags 
                          syns flds dump xs copts
             return (rest, err:errs', ctxt, globs, excs, tags, syns)
        Success (xrv,xeq) -> do
             xeq' <- return $! 
                      (if dump then (trace (showeqns x xft' xeq) xeq) else xeq)
	     phi' <- {- trace (show xrv) $ -} mkSubst xeq'
	     xfn <- substTerm mod ctxt phi' xrv
	     let xinft = subst phi' xft'
             (rest, errs', ctxt', globs', excs', tags',syns') <- 
	         inferAll mod (addName ctxt x xinft fopts) errs globs excs tags 
                          syns flds dump xs copts
 	     let xannot = Annotation (FnBody (showuser x) file line) xfn
             return ((FunBind (file,line,x,xinft,fopts,Defined xannot) comm xinft):rest,
                     errs',
		    (addName ctxt' x xinft fopts), globs', excs', tags', syns')

-- Function definitions
inferAll mod ctxt errs globs excs tags syns flds dump ((FB (file,line,x,xt,fopts,Defined xr) comm):xs) copts = 
  do let xftin = appsyn syns xt
     xft <- normalise False file line mod syns xftin
--     trace (showuser x++":"++show xft) $ return ()
     -- If it's been defined before, and it's a DefaultDef, just ignore it.
     if (DefaultDef `elem` fopts) && (defined ctxt x)
       then inferAll mod ctxt errs globs excs tags syns flds dump xs copts
       else do
	    checkRpt file line x xft ctxt (Repeatable `elem` fopts)
--            checkDefaultArgs xft mod ctxt globs tags syns flds
            (rest, errs, ctxt', globs', excs', tags', syns') <- 
	         case inferAll mod (addName ctxt x xft fopts) errs globs excs tags syns flds dump xs copts of
                    Success x -> return x
                    Failure err f l -> return ([], err:errs, ctxt, globs, excs, tags, syns)

            let (xft',errs') = safedefaults mod ctxt' file line xft errs
	    let xrdec = insertdecl mod excs globs (addName ctxt' x xft' fopts) xr
	    case infer mod (addName ctxt' x xft' fopts) 
                                 globs' excs' tags' syns' flds xrdec xft' copts of
               Failure err f l ->
                   return (rest, err:errs', ctxt', globs', excs', tags', syns')
               Success (xrv,xeq) -> do
	        xeq' <- return $! 
                          (if dump then (trace (showeqns x xft' xeq) xeq) else xeq)
	        phi' <- {- trace (show xrv) $ -} mkSubst xeq'
	        xfn <- substTerm mod ctxt phi' xrv
	        let xinft = subst phi' xft'
	        checkEq file line xinft xft'
	        checkReturn file line (showuser x) xinft xfn
	        let xannot = Annotation (FnBody (showuser x) file line) xfn
                -- We ought to return xinft as the type, since that's what
                -- we inferred. Alas, we currently need to use xft' instead
                -- since we already put it in the context when we checked the
                -- rest of the module. Need to rethink this whole process 
                -- really...
	        return {-$ trace ((show xrv)++"\n"++(show xfn)) $ -}
                   ((FunBind (file,line,x,xft',fopts,Defined xannot) comm xt):rest,
                     errs',
		    (addName ctxt' x xft' fopts), globs', excs', tags', syns')
 where mkfuntype f@(Fn _ _ _) = f
       mkfuntype x = (Fn [] [] x)

       checkDefaultArgs (Fn defs tys rt) mod ctxt globs tags 
                        syns flds = cda defs tys 
           where cda [] [] = return ()
                 cda ((Just d):ds) (t:tys) =
                     do (_,_) <- infertype mod ctxt globs excs tags syns flds
                                           d (Prim Void) t copts
                        cda ds tys
                 cda (_:ds) (_:tys) = cda ds tys
                 cda _ _ = fail "Can't happen (cda)"
       checkDefaultArgs _ _ _ _ _ _ _ = fail "Can't happen (checkDefaultArgs)"

-- Imported function declaration
inferAll mod ctxt errs globs excs tags syns flds dump ((FB (file,line,x,xt,fopts,Unbound) comm):xs) copts =
  do let xftin = appsyn syns (mkfuntype xt)
     xft <- normalise False file line mod syns xftin
--     let xft = trace (show xt)mkfuntype xt
     let (newctxt,newopts) = mergeIntoCtxt x xt fopts ctxt
     (rest, errs, ctxt', globs', excs', tags', syns') <- inferAll mod (addName newctxt x xft newopts) errs globs excs tags syns flds dump xs copts
     return $ ((FunBind (file,line,x,xft,newopts,Unbound) comm xft):rest, errs,
               addName ctxt' x xft newopts, globs', excs', tags', syns')
 where mkfuntype f@(Fn _ _ _) = f
       mkfuntype x = (Fn [] [] x)

-- Imported and inlinable function declaration
inferAll mod ctxt errs globs excs tags syns flds dump ((FB (file,line,x,xt,fopts, ExtInlinable xr) comm):xs) copts =
  do let xftin = appsyn syns (mkfuntype xt)
     xft <- normalise False file line mod syns xftin
--     let xft = trace (show xt)mkfuntype xt
     let (newctxt,newopts) = mergeIntoCtxt x xt fopts ctxt
     (rest, errs, ctxt', globs', excs', tags', syns') <- inferAll mod (addName newctxt x xft newopts) errs globs excs tags syns flds dump xs copts
     let xrdec = insertdecl mod excs globs (addName ctxt' x xft fopts) xr
     case infer mod (addName ctxt' x xft fopts) 
                globs' excs' tags' syns' flds xrdec xft copts of
         Failure err f l ->
             return (rest, err:errs, ctxt', globs', excs', tags', syns')
         Success (xrv,xeq) -> do
             phi' <- {- trace (show xrv) $ -} mkSubst xeq
             xfn <- substTerm mod ctxt phi' xrv
             let xinft = subst phi' xft
             checkEq file line xinft xft
             checkReturn file line (showuser x) xft xfn
             return $ ((FunBind (file,line,x,xft,newopts,ExtInlinable xfn) comm xft):rest, errs,
               addName ctxt' x xft newopts, globs', excs', tags', syns')
 where mkfuntype f@(Fn _ _ _) = f
       mkfuntype x = (Fn [] [] x)

-- Type synonyms
inferAll mod ctxt errs globs excs tags tydefs flds dump ((TSyn (file,line,n,ps,ty,exp)):xs) copts = 
  do let def = Syn (map getname ps) ty
  -- All typevars in <ty> must be listed in <ps>
     checkTyVars file line ps ty
  -- If it's a duplicate, check it's identical to what we already had.
     newdefs <- checkDefined file line n tydefs def
     (rest, errs, ctxt', globs', excs', tags',syns') <- 
	 inferAll mod ctxt errs globs excs tags newdefs flds dump xs copts
     -- normalise to check for cycles
     foo <- normalise False file line mod syns' (TyApp (User n) ps)
     return $ ((TySyn (file,line,n,(map getname ps),ty,exp):rest), errs, 
               ctxt', globs', excs', tags', syns')
  where getname (TyVar x) = x
--    fail $ file ++ ":" ++ show line ++ ":Type synonyms are broken"
--   inferAll ctxt globs tags ((n,ty):syns) flds dump xs

-- Data declarations
inferAll mod ctxt errs globs excs tags tydefs flds dump ((DDecl f l dopts n tys consin comm):xs) copts =
  do let newdefs = addToCtxt tydefs n (UserData tys)
     -- Check it's not already defined
--     trace (show newdefs) $ return ()
     cons <- normcons consin newdefs
     checkData f l newdefs tys cons
     (fbs, newflds, codegen) <- getFuns ctxt f l mod cons newdefs 0
--     trace (show fbs) $ return ()
     checkRptFlds f l newflds n
     if (codegen && n `elem` (getNames tydefs)) 
	then fail $ f ++ ":" ++ show l ++ ": Data type " ++ 
	            showuser n ++ " already defined"
	else return ()
     let ctxt' = addNames ctxt (map (mkCtxtEntry [Public,Constructor]) 
                                        (gettys newdefs fbs))
     let tags' = (gettags fbs (length cons))++tags
     (rest, errs, ctxt'', globs'', excs'', tags'', syns') 
         <- inferAll mod ctxt' errs globs excs tags' newdefs 
                     (flds ++ newflds) dump xs copts
--     return $ (fbs++(DataDecl n tys cons):rest)
     checkUserData f l mod syns' cons
     return $ ([DataDecl f l dopts n tys cons comm]++fbs++rest, errs, ctxt'', globs'', excs'', tags'', syns')
 where gettys s [] = []
       gettys s ((FunBind (f,l,n,ty,_,_) _ _):xs) = 
         ({-trace ((show n) ++ ":" ++ show ty) -}(n,appsyn s ty)):(gettys s xs)

       gettags [] l = []
       gettags ((FunBind (_,_,n,_,_,(DataCon t a _)) _ _):xs) l = (n,(t,l)):(gettags xs l)
       normcons [] n = return []
       normcons (x:xs) n = do rest <- normcons xs n
                              ncon <- normcon x n
                              return $ ncon:rest
       normcon (Con n ty ns b) newdefs = 
           do normty <- normalise False f l mod newdefs (appsyn newdefs ty)
              return $ Con n normty ns b

-- Exception declarations
inferAll mod ctxt errs globs excs tags tydefs flds dump ((ExtExc f l n tys):xs) copts =
  do let exfnty = Fn [] tys (Prim Exception)
     let exfnbody = FunBind (f, l, n, exfnty, [Public,Generated],
                            ExceptionFn n (length tys) False) "" exfnty
     let exctxt = addName ctxt n exfnty [Public,Generated]
     let newexcs = addToCtxt excs n tys
     (rest, errs, ctxt', globs', excs', tags',syns') <- 
	 inferAll mod exctxt errs globs newexcs tags tydefs flds dump xs copts
     return $ (exfnbody:rest, errs, ctxt', globs', excs', tags', syns')
inferAll mod ctxt errs globs excs tags tydefs flds dump ((ExcDecl f l n tysin comm):xs) copts =
  do tys <- mapM (normalise False f l mod tydefs) tysin
     let fulln = NS mod n
     let newexcs = addToCtxt excs fulln tys
     -- add a function of called n of type Exception(tys), which constructs
     -- the actual exception structure (TODO)
     let exfnty = Fn [] tys (Prim Exception)
     let exfnbody = FunBind (f, l, fulln, exfnty, [Public,Generated],
                            ExceptionFn fulln (length tys) True) "" exfnty
     let exctxt = addName ctxt fulln exfnty [Public,Generated]
     (rest, errs, ctxt', globs', excs', tags',syns') <- 
	 inferAll mod exctxt errs globs newexcs tags tydefs flds dump xs copts
     return ((ExceptDecl f l fulln tys comm):exfnbody:rest, errs, ctxt', globs', excs', tags', syns')
{-
inferAll ctxt tags syns ((CDecl n ty i t ar):xs) =
  do (rest,ctxt',tags',syns') <- inferAll ctxt tags syns xs
     let tags'' = (n,(i,t)):tags
     return $ ((FunBind (n,ty,DataCon i ar)):rest, ctxt', tags'', syns')
-} 

-- check that a default parameter is actually a constant
-- this is a bit too conservative and needs to do name lookups on RVar
safedefaults :: Name -> -- module name
                Context -> String -> Int -> Type -> [InferError] -> (Type,[InferError])
safedefaults mod ctxt f l (Fn defs tys t) errs = ((Fn defs tys t),(safedefaults' mod ctxt f l defs errs))
safedefaults mod ctxt f l t errs = (t,errs)

safedefaults' :: Name -> Context -> String -> Int -> [Maybe Raw] -> [InferError] -> [InferError]
safedefaults' mod ctxt f l [] errs = errs
safedefaults' mod ctxt f l (d:ds) errs = safedefaults' mod ctxt f l ds (safedefaults'' mod ctxt f l d errs)

safedefaults'' :: Name -> Context -> String -> Int -> Maybe Raw -> [InferError] -> [InferError]
safedefaults'' mod ctxt f l Nothing errs = errs
safedefaults'' mod ctxt f l (Just v) errs = case (safedefault mod ctxt f l v) of
                                               [] -> errs
                                               xs -> concat([xs,errs]);

safedefault :: Name -> Context -> String -> Int -> Raw -> [InferError]
safedefault mod ctxt fi li (RConst f l v) = []
safedefault mod ctxt fi li (RClosure f l as v) = safedefault mod ctxt f l v
safedefault mod ctxt fi li (RApply f l fn args) = concat (map (safedefault mod ctxt f l) args)
safedefault mod ctxt fi li (RPartial f l fn args) = concat (map (safedefault mod ctxt f l) args)
safedefault mod ctxt fi li (RInfix f l op v v') = concat [(safedefault mod ctxt f l v),(safedefault mod ctxt f l v')]
safedefault mod ctxt fi li (RUnary f l op v) = safedefault mod ctxt f l v
safedefault mod ctxt fi li (RIndex f l vs idx) = concat [(safedefault mod ctxt f l vs),(safedefault mod ctxt f l idx)]
safedefault mod ctxt fi li (RField f l v n) = safedefault mod ctxt f l v
safedefault mod ctxt fi li (RArrayInit f l vs) = concat (map (safedefault mod ctxt f l) vs)
-- this would work if all the functions in the current module got
-- added to the context first...
safedefault mod ctxt fi li (RVar f l n) = case lookupname mod n ctxt of 
                                          [] -> [fi ++ ":" ++ show li ++ ": Default argument " ++ show n ++ " is not a constant"]
                                          _ -> []
safedefault mod ctxt fi li v = [fi ++ ":" ++ show li ++ ": Default argument is not a constant"]


-- Return the function declarations and field names from a constructor
-- declaration
-- Also returns whether this needs code generating or not.
getFuns :: Monad m => Context -> String -> Int -> Name -> [ConDecl] -> 
	   Types -> Int -> m (Program, Fields, Bool)
getFuns ctxt f l mod [] syns i = return ([], [], False)
getFuns ctxt f l mod ((Con n ty an codegen):xs) syns i
  = do (rest, flds, _) <- getFuns ctxt f l mod xs syns (i+1)
       if codegen 
	  then checkRpt f l n ty ctxt False -- Check the name isn't used elsewhere
	  else return () -- Do nothing if it's from somewhere else
       normty <- normalise False f l mod syns (appsyn syns ty)
     --  trace (showuser n ++ ":" ++ show normty) $ return ()
       return (((FunBind (f,l,n,normty,[Inline,Pure,Public,Constructor],DataCon i (getarglen ty) codegen) "" normty):rest),
	       (getFields (appsyn syns ty) an 0 i) ++ flds, codegen)
  where getarglen (Fn _ tys _) = length tys
	getarglen _ = 0

        getFields (Fn _ ty tn) as argn tag = gf' ty as argn tag tn
        gf' (x:xs) (a:as) argn tag tn = 
	    ((a,tn),(x,argn,tag)):(gf' xs as (argn+1) tag tn)
	gf' _ _ _ _ _ = []
		   
-- Check that field names are not repeated within a type definition
checkRptFlds :: Monad m => String -> Int ->
		Fields -> Name -> m ()
checkRptFlds f l [] n = return ()
checkRptFlds f l (((fld,t),_):xs) n
   | fld /= None && elem fld (map (fst.fst) xs)
       = fail $ f ++ ":" ++ show l ++ ":" ++
	    "Field " ++ showuser fld ++ " is duplicated in type " ++ showuser n
   | otherwise = checkRptFlds f l xs n


-- Check that a function which returns non-void does indeed return something
-- on all possible branches.
checkReturn :: Monad m => String -> Int ->
	       String -> -- User description of function name
	       Type -> -- Function type
	       (Expr Name) -> 
	       m ()-- Function body
checkReturn _ _ _ (Fn _ _ (Prim Void)) _ 
    = return () -- Don't care, it's a void.
checkReturn file line n _ body 
    | containsReturn body = return ()
    | otherwise = fail $ file ++ ":" ++ show line ++ 
		  ":not all branches of " ++ n ++ " return a value"

checkDefined :: Monad m => String -> Int -> Name -> Types -> 
		TypeInfo ->
		m Types
checkDefined f l n tys def
    = case lookupname None n tys of
         [(_,x)] -> if (x==def) then return tys
		       else fail $ f ++ ":" ++ show l ++ ":" ++
			    "Type "++showuser n++" already defined"
	 _ -> return (addToCtxt tys n def)

checkTyVars :: Monad m => String -> Int -> [Type] -> Type -> m ()
checkTyVars f l ts t = ct t where
   ct (Fn ds ts t) = do mapM_ ct ts
			ct t
   ct (Array t) = ct t
   ct (TyApp t ts) = do ct t
                        mapM_ ct ts
   ct t@(TyVar _) | t `elem` ts = return ()
		  | otherwise = fail $ f ++ ":" ++ show l ++ ":" ++
				          show t ++ 
				         " not declared as a parameter"
   ct _ = return ()


checkData :: Monad m => String -> Int -> Types -- Synonyms/Datatypes
	     -> [Type] -- Parameters
	     -> [ConDecl] -- Constructor declarations
	     -> m () -- Just check it's okay
checkData f l syns tys [] = return ()
checkData f l syns tys (c:cs) = do checkConDecl f l syns tys c
				   checkData f l syns tys cs
				   
checkConDecl f l syns tys (Con n ty _ _) = 
    do --normty <- normalise False f l syns ty
       allDeclared f l n syns tys ty

allDeclared f l n dtys tys ty = {- trace (show ty) $ -} ad ty
  where ad (Fn _ ts t) = mapM_ ad (t:ts)
	ad (Array t) = ad t
	ad (TyApp t ts) = do ad t
                             mapM_ ad ts
	ad (TyVar x) | (TyVar x) `elem` tys = return ()
		     | otherwise = fail $ f ++ ":" ++ show l ++ ":" ++
				   "undeclared type variable " ++ showuser x
	ad _ = return ()

checkUserData :: Monad m => String -> Int -> Name -> -- Module
		 Types -- Synonyms/Datatypes
	     -> [ConDecl] -- Constructor declarations
	     -> m () -- Just check it's okay
checkUserData f l mod syns [] = return ()
checkUserData f l mod syns (c:cs) = do checkUserDecl f l mod syns c
				       checkUserData f l mod syns cs
				   
checkUserDecl f l mod syns (Con n ty _ _) 
  = do normty <- normalise False f l mod syns ty
       userDeclared f l n syns normty

userDeclared f l n dtys ty = ad ty
  where ad (Fn _ ts t) = mapM_ ad (t:ts)
	ad (Array t) = ad t
        ad (User n) = case (typelookup (UN "foo") n dtys) of
                         (Got _) -> return ()
			 _ -> fail $ f ++ ":" ++ show l ++ ":" ++
                                     "unknown type "++ showuser n
	ad (TyApp t ts) = do ad t
                             mapM_ ad ts
	ad (TyVar x) = return ()
	ad _ = return ()

checkGlob :: MonadPlus m => String -> Int ->
                  Name -> Context -> GContext -> EContext -> Tags -> Types ->
                  Fields -> Maybe Raw -> Type -> Options -> m (Maybe (Expr Name))
checkGlob f l mod ctxt globs excs tags tys flds (Just expr) (Prim Void) copts = 
    fail $ f ++ ":" ++ show l ++ ":Can't have a Void global variable"
checkGlob f l mod ctxt globs excs tags tys flds (Just expr) ty copts = 
   do (val,_) <- infertype mod ctxt globs excs tags tys flds expr (Prim Void) ty copts
      return $ Just val
checkGlob _ _ _ _ _ _ _ _ _ Nothing _ _ = return Nothing

-- Given a polymorphic type, and an instance, get what types the variables
-- refer to (as a substitution)
getVarTypes :: Monad m => Type -> Type -> String -> m Subst
getVarTypes t1 t2 ctxt = do tvm <- cg t1 t2 []
		            (_,s) <- mkFSubst tvm
		            return s
  where
     mkFSubst [] = return ideq
     mkFSubst ((l,r):xs) = 
	 do xsubs <- mkFSubst xs
	    addEq "" 0 (TyVar l, r, ctxt) xsubs

-- mkSubst $ map (\ (x,y) -> (TyVar x,y,"",0)) xs

     cg (TyVar x) y tvm = 
	 case (lookup x tvm) of
	   (Just z) -> if y==z then return tvm
		        else fail "Type error"
	   Nothing -> return $ (x,y):tvm
     cg t (TyVar y) tvm = fail "Type error"
     cg (Array x) (Array y) tvm = cg x y tvm
     cg (Fn ns ts t) (Fn ns' ts' t') tvm = do
          tvm' <- cg t t' tvm
	  cgl ts ts' tvm'
     cg (User n) (User n') tvm | n == n' = return tvm
                               | otherwise = fail "Type error"
     cg (TyApp t ts) (TyApp t' ts') tvm = do tvm' <- cg t t' tvm
                                             cgl ts ts' tvm'
     cg (Prim x) (Prim y) tvm | x == y = return tvm
			      | otherwise = fail "Type error"
     cg _ _ tvm = fail "Type error"

     cgl [] [] tvm = return tvm
     cgl (x:xs) (y:ys) tvm = do tvm' <- cg x y tvm
				cgl xs ys tvm'
     cgl _ _ tvm = fail "Type error"


checkRpt :: Monad m => String -> Int -> Name -> Type -> Context -> Bool -> m ()
checkRpt f l x ty xs rptable
    = case lookupname None x xs of
          [(_,(ty', _))] -> if (ty' == ty && (not rptable))
                            then fail $ f ++ ":" ++ show l ++ ":" ++ showuser x ++ " already defined"
                            else return ()
	  _ -> return ()

showtree :: Program -> String
showtree [] = ""
showtree ((FunBind (_,_,n,ty,fopts,Defined tr) _ _):xs) =
    showuser n ++ " :: " ++ show ty ++ " " ++ show fopts ++ "\n" ++ show tr ++ "\n\n" ++ showtree xs
showtree ((FunBind (_,_,n,ty,fopts,ExceptionFn nm i True) _ _):xs) =
    showuser n ++ " :: " ++ show ty ++ " " ++ show fopts ++ " = exception\n\n" ++ showtree xs
showtree (_:xs) = showtree xs

showeqns :: Name -> Type -> Equation -> String
showeqns n ty (es,_) = showuser n ++ " :: " ++ show ty ++ ":\n" ++ se' es
  where se' [] = ""
	se' ((t1,t2,f,l,ctxt):xs) = show t1 ++ " = " ++ show t2 ++ 
			            " ("++f++":"++show l++", " ++ ctxt ++ 
                                    ")\n" ++ se' xs