root/trunk/ProjectFortress/src/com/sun/fortress/compiler/typechecker/TypeChecker.java @ 3292

/*******************************************************************************
    Copyright 2008 Sun Microsystems, Inc.,
    4150 Network Circle, Santa Clara, California 95054, U.S.A.
    All rights reserved.

    U.S. Government Rights - Commercial software.
    Government users are subject to the Sun Microsystems, Inc. standard
    license agreement and applicable provisions of the FAR and its supplements.

    Use is subject to license terms.

    This distribution may include materials developed by third parties.

    Sun, Sun Microsystems, the Sun logo and Java are trademarks or registered
    trademarks of Sun Microsystems, Inc. in the U.S. and other countries.
 ******************************************************************************/

package com.sun.fortress.compiler.typechecker;


import static com.sun.fortress.exceptions.InterpreterBug.bug;
import static com.sun.fortress.exceptions.StaticError.errorMsg;
import static edu.rice.cs.plt.tuple.Option.none;
import static edu.rice.cs.plt.tuple.Option.some;
import static edu.rice.cs.plt.tuple.Option.wrap;
import static edu.rice.cs.plt.iter.IterUtil.tripleFirsts;
import static edu.rice.cs.plt.iter.IterUtil.tripleSeconds;
import static edu.rice.cs.plt.iter.IterUtil.tripleThirds;
import static edu.rice.cs.plt.iter.IterUtil.pairFirsts;
import static edu.rice.cs.plt.iter.IterUtil.pairSeconds;
import static edu.rice.cs.plt.collect.CollectUtil.makeList;

import java.math.BigInteger;
import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.ListIterator;
import java.util.Map;
import java.util.Set;

import com.sun.fortress.compiler.IndexBuilder;
import com.sun.fortress.compiler.Types;
import com.sun.fortress.compiler.disambiguator.ExprDisambiguator.HierarchyHistory;
import com.sun.fortress.compiler.index.CompilationUnitIndex;
import com.sun.fortress.compiler.index.DeclaredVariable;
import com.sun.fortress.compiler.index.Functional;
import com.sun.fortress.compiler.index.FunctionalMethod;
import com.sun.fortress.compiler.index.Method;
import com.sun.fortress.compiler.index.ObjectTraitIndex;
import com.sun.fortress.compiler.index.ParamVariable;
import com.sun.fortress.compiler.index.ProperTraitIndex;
import com.sun.fortress.compiler.index.TraitIndex;
import com.sun.fortress.compiler.index.TypeConsIndex;
import com.sun.fortress.compiler.index.Variable;
import com.sun.fortress.compiler.typechecker.TypeAnalyzer.SubtypeHistory;
import com.sun.fortress.compiler.typechecker.TypeEnv.BindingLookup;
import com.sun.fortress.compiler.typechecker.TypesUtil.ArgList;
import com.sun.fortress.exceptions.InterpreterBug;
import com.sun.fortress.exceptions.StaticError;
import com.sun.fortress.exceptions.TypeError;
import com.sun.fortress.nodes.*;
import com.sun.fortress.nodes_util.ExprFactory;
import com.sun.fortress.nodes_util.NodeFactory;
import com.sun.fortress.nodes_util.NodeUtil;
import com.sun.fortress.nodes_util.OprUtil;
import com.sun.fortress.nodes_util.Span;
import com.sun.fortress.parser_util.FortressUtil;
import com.sun.fortress.useful.NI;
import com.sun.fortress.useful.Useful;

import edu.rice.cs.plt.collect.CollectUtil;
import edu.rice.cs.plt.collect.ConsList;
import edu.rice.cs.plt.collect.EmptyRelation;
import edu.rice.cs.plt.collect.IndexedRelation;
import edu.rice.cs.plt.collect.Relation;
import edu.rice.cs.plt.collect.UnionRelation;
import edu.rice.cs.plt.iter.IterUtil;
import edu.rice.cs.plt.lambda.Box;
import edu.rice.cs.plt.lambda.Lambda;
import edu.rice.cs.plt.lambda.Lambda2;
import edu.rice.cs.plt.tuple.Option;
import edu.rice.cs.plt.tuple.Pair;
import edu.rice.cs.plt.tuple.Triple;

import static com.sun.fortress.compiler.typechecker.TypeNormalizer.normalize;

/**
 * The fortress typechecker.<br>
 *
 * Notes/Invariants:<br>
 * - The typechecker can either be in inference mode ({@code postInference==false}) or
 *   post-inference mode ({@code postInference == true}). In post-inference mode, all of the
 *   cases of the typechecker that create open constraints must close those constraints immediately.<br>
 */
public class TypeChecker extends NodeDepthFirstVisitor<TypeCheckerResult> {

    private static boolean isPostInference(FunctionalRef opref) {
        return opref.getOverloadings().isSome();
    }

    private static TypeChecker addSelf(Option<APIName> api_, Id name, TypeChecker newChecker, List<StaticParam> static_params){
        Id type_name;
        if( api_.isSome() )
            type_name = NodeFactory.makeId(api_.unwrap(), name);
        else
            type_name = name;

        TraitType self_type = NodeFactory.makeTraitType(type_name,TypeEnv.staticParamsToArgs(static_params));
        return newChecker.extend(Collections.singletonList(NodeFactory.makeLValue("self", self_type)));
    }
    /** Returns an error result if item is NOT an ExprMI */
    private static Option<TypeCheckerResult> expectExprMI(MathItem item) {
        boolean is_expr_item = isExprMI(item);
        if( !is_expr_item ) {
            String err = "Item at this location must be an expression, not an operator.";
            TypeCheckerResult err_result = new TypeCheckerResult(item,TypeError.make(err, item));
            return Option.some(err_result);
        }
        else {
            return Option.none();
        }
    }
    /** Returns an error result if item is NOT a ParenthesisDelimitedMI */
    private static Option<TypeCheckerResult> expectParenedExprItem(MathItem item) {
        boolean is_parened = isParenedExprItem(item);
        if( !is_parened ) {
            String err = "Argument to function must be parenthesized.";
            TypeCheckerResult err_result = new TypeCheckerResult(item, TypeError.make(err, item));
            return Option.some(err_result);
        }
        else {
            return Option.none();
        }
    }
    static private Type getTypeOfLValue(LValue lval) {
            return lval.getIdType().unwrap();
    }
    private static boolean isExprMI(MathItem item) {
        return item.accept(new NodeDepthFirstVisitor<Boolean>(){
            @Override public Boolean defaultCase(Node that) { return false; }
            @Override public Boolean forNonParenthesisDelimitedMI(NonParenthesisDelimitedMI that) { return true; }
            @Override public Boolean forParenthesisDelimitedMI(ParenthesisDelimitedMI that) { return true; }
        });
    }
    private static boolean isParenedExprItem(MathItem item) {
        return item.accept(new NodeDepthFirstVisitor<Boolean>(){
            @Override public Boolean defaultCase(Node that) { return false; }
            @Override public Boolean forParenthesisDelimitedMI(ParenthesisDelimitedMI that) { return true; }
        });
    }

    private static Type typeFromLValues(Span span, List<LValue> bindings) {
        List<Type> results = new ArrayList<Type>();

        for (LValue binding: bindings) {
            if (binding.getIdType().isSome()) {
                results.add(binding.getIdType().unwrap());
            } else
                bug(binding, "Missing type.");
        }
        return NodeFactory.makeTupleType(span, results);
    }

    private final CompilationUnitIndex compilationUnit;

    private final Map<Id, Option<Set<Type>>> labelExitTypes; // Note: this is mutable state.

    private final boolean postInference; // Is this pass of the typechecker a post-inference pass?

    private final TypeAnalyzer subtypeChecker;

    private TraitTable table;

    private TypeEnv typeEnv;

    // An informative constraint passed down the ast
    private final ConstraintFormula downwardConstraint;

    public TypeChecker(TraitTable table,
            TypeEnv typeEnv,
            CompilationUnitIndex compilationUnit,
            boolean postInference) {
        this.table = table;
        this.typeEnv = typeEnv;
        this.compilationUnit = compilationUnit;
        this.subtypeChecker = TypeAnalyzer.make(table);
        this.labelExitTypes = new HashMap<Id, Option<Set<Type>>>();
        this.postInference = postInference;
        this.downwardConstraint = ConstraintFormula.TRUE;
    }

    private TypeChecker(TraitTable table,
            TypeEnv typeEnv,
            CompilationUnitIndex compilationUnit,
            TypeAnalyzer subtypeChecker,
            Map<Id, Option<Set<Type>>> labelExitTypes,
            boolean postInference,
            ConstraintFormula downwardsConstraint) {
        this.table = table;
        this.typeEnv = typeEnv;
        this.compilationUnit = compilationUnit;
        this.subtypeChecker = subtypeChecker;
        this.labelExitTypes = labelExitTypes;
        this.postInference = postInference;
        this.downwardConstraint = downwardsConstraint;
    }

    /**
     * Checks whether all the expressions in the block have type void.
     * List of Exprs passed in so that error messages can be more accurate.
     */
    private List<TypeCheckerResult> allVoidButLast(List<TypeCheckerResult> results, List<Expr> block){
        // every other expression except for the last must be void
        List<TypeCheckerResult> all_results = new ArrayList<TypeCheckerResult>();
        String void_err = "All expressions except the last in a block must have () type.";
        for( int i=0; i<results.size()-1; i++ ) {
            TypeCheckerResult r_i = results.get(i);
            if( r_i.type().isSome() ) {
                all_results.add(this.checkSubtype(r_i.type().unwrap(),
                        Types.VOID, block.get(i), void_err));
            }
        }
        return all_results;
    }

    /**
     * For method calls, return a constraint formula matching the parameters to
     * the type of the argument. Assumes that this is being used for a method call,
     * because it makes some assumptions about the type of the argument.
     */
    private ConstraintFormula argsMatchParams(List<Param> params, Type arg_type) {
        final int arg_size;
        if( arg_type instanceof TupleType )
            arg_size = ((TupleType)arg_type).getElements().size();
        else
            arg_size = 1;

        //handle domain
        Type domain_type;
        if(!params.isEmpty()) {

            // Regular parameters & var args
            List<Type> param_types =
                IterUtil.fold(params, new LinkedList<Type>(), new Lambda2<LinkedList<Type>,Param,LinkedList<Type>>(){
                    // How many types have we accumulated thus far?
                    int typeCount = 0;

                    public LinkedList<Type> value(LinkedList<Type> arg0, Param arg1) {
                                            if( ! NodeUtil.isVarargsParam(arg1) ) {
                            typeCount++;
                            arg0.add(arg1.getIdType().unwrap());
                            return arg0;
                        }
                                            else { // a varargs param, add until the sizes are equal
                            int to_add = arg_size - typeCount;
                            while( to_add > 0 ) {
                                                            arg0.add(arg1.getVarargsType().unwrap());
                                to_add--;
                            }
                            return arg0;
                        }
                    }});

            //handle defaults (nyi)
            if( NodeUtil.isVarargsParam(params.get(params.size()-1))
                           && params.get(params.size()-1).getDefaultExpr().isSome()){
                return NI.nyi();
            }

            domain_type = NodeFactory.makeTupleType(NodeUtil.getSpan(arg_type),param_types);
        }
        else {
            //is void
            domain_type = Types.VOID;
        }
        return this.subtypeChecker.subtype(arg_type, domain_type);
    }

    /**
     * Return a failing TypecheckerResult with error message if the given type {@code t} is
     * not a trait.
     */
    private TypeCheckerResult assertTrait(BaseType t, Node ast, String msg, Node error_loc) {
        TypeCheckerResult err_result = new TypeCheckerResult(ast, TypeError.make(msg, error_loc));

        if( !(t instanceof TraitType) )
            return err_result;

        Option<TypeConsIndex> type_cons_ = this.table.typeCons(((TraitType)t).getName());
        if( type_cons_.isSome() && type_cons_.unwrap() instanceof ProperTraitIndex ) {
            return new TypeCheckerResult(ast);
        }
        else {
            return err_result;
        }
    }

    // Checks the chunk given, and returns the result and a new expression.
    // Requires that all TypeCheckerResults passed in actually have a type.
    // Must be called on non-empty list.
    private Pair<TypeCheckerResult,Expr> checkChunk(List<Pair<TypeCheckerResult,Expr>> chunk, FunctionalRef infix_juxt) {
        assert(!chunk.isEmpty());
        // The non-functions in each chunk, if any, are replaced by a single element consisting of the non-functions grouped
        // left-associatively into binary juxtapositions.
        Option<Expr> last_non_fn = Option.none();
        List<Expr> fns = new LinkedList<Expr>();
        for( Pair<TypeCheckerResult,Expr> chunk_element : chunk ) {
            if( !TypesUtil.isArrows(chunk_element.first().type().unwrap()) ) {
                // If we've already seen an expr, created a binary juxt with previous
                if( last_non_fn.isNone() )
                    last_non_fn = Option.some(chunk_element.second());
                else
                    last_non_fn = Option.<Expr>some(ExprFactory.makeOpExpr(infix_juxt,
                                                                                               last_non_fn.unwrap(),
                                                                                               chunk_element.second()));
            }
            else {
                fns.add(chunk_element.second());
            }
        }
        // What remains in each chunk is then grouped right-associatively, as fn applications.
        Option<Expr> result_expr = last_non_fn;
        Collections.reverse(fns); // reverse so right assoc becomes left assoc
        for( Expr fn : fns ) {
            if( result_expr.isNone() )
                result_expr = Option.some(fn);
            else
                result_expr = Option.<Expr>some(ExprFactory.make_RewriteFnApp(fn, result_expr.unwrap()));
        }
        // We are done. result_expr must be some or this method wasn't implemented correctly.
        TypeCheckerResult result = TypeCheckerResult.compose(result_expr.unwrap(), subtypeChecker,
                CollectUtil.makeList(IterUtil.pairFirsts(chunk)));
        return Pair.make(result, result_expr.unwrap());
    }

    /**
     * Check the subtype relation for the given types.  If subtype <: supertype, then a TypeCheckerResult
     * for the given node and corresponding type constraints will be returned.  Otherwise, a TypeCheckerResult
     * for the given node with a generic error message will be returned.
     */
    private TypeCheckerResult checkSubtype(Type subtype, Type supertype, Node ast) {
        return checkSubtype(subtype,
                supertype,
                ast,
                errorMsg("Expected expression of type ", supertype, " ",
                        "but was type ", subtype));
    }

    /**
     * Check the subtype relation for the given types.  If subtype <: supertype, then a TypeCheckerResult
     * for the given node and corresponding type constraints will be returned.  Otherwise, a TypeCheckerResult
     * for the given node with the a TypeError and the given error message will be returned.
     */
    private TypeCheckerResult checkSubtype(Type subtype, Type supertype, Node ast, String error) {
        ConstraintFormula constraint = subtypeChecker.subtype(subtype, supertype);
        if( !constraint.isSatisfiable() ) {
            // note that if it's satisfiable, it could still be later found to not be
            return new TypeCheckerResult(ast, TypeError.make(error, ast));
        } else {
            return new TypeCheckerResult(ast, constraint);
        }
    }

    /**
     * Check the subtype relation for the given types.  If subtype <: supertype, then a TypeCheckerResult
     * for the given node and corresponding type constraints will be returned, and the type of this node
     * will be the given type resultType.  Otherwise, a TypeCheckerResult
     * for the given node with the a TypeError and the given error message will be returned.
     */
    private TypeCheckerResult checkSubtype(Type subtype, Type supertype, Node ast, Type resultType, String error) {
        ConstraintFormula constraint = subtypeChecker.subtype(subtype, supertype);
        if( !constraint.isSatisfiable() ) {
            // note that if it's satisfiable, it could still be later found to not be
            return new TypeCheckerResult(ast, resultType, TypeError.make(error, ast));
        } else {
            return new TypeCheckerResult(ast, resultType, constraint);
        }
    }


    @Override
    public TypeCheckerResult defaultCase(Node that) {
        return new TypeCheckerResult(that);
    }

    private List<TraitIndex> expectTraitIndeces(List<TraitType> traits) {
        List<TraitIndex> result = new ArrayList<TraitIndex>(traits.size());
        for( TraitType type : traits ) {
            result.add(expectTraitIndex(type));
        }
        return result;
    }

    /**
     * Look up the index of the given type, expecting it to exist. If it
     * does not, that represents a bug.
     */
    private TraitIndex expectTraitIndex(TraitType trait) {
        Option<TypeConsIndex> tc_ = table.typeCons(trait.getName());
        if( tc_.isNone() || !(tc_.unwrap() instanceof TraitIndex) ) {
            return bug("This should never be anything but a legitimate trait index.");
        }
        else {
            return (TraitIndex)tc_.unwrap();
        }
    }

    /** Check for ^ followed by ^ or ^ followed by [], both static errors. */
    private Option<TypeCheckerResult> exponentiationStaticCheck(Node ast, List<MathItem> items) {

        //Visitor checks for two exponentiations or an exponentiation and a subscript in a row
        NodeDepthFirstVisitor<TypeCheckerResult> static_error = new NodeDepthFirstVisitor<TypeCheckerResult>() {
            Option<Node> exponent = Option.none();
            @Override
            public TypeCheckerResult defaultCase(Node that) {
                exponent=Option.none();
                return new TypeCheckerResult(that);
            }

            @Override
            public TypeCheckerResult forExponentiationMI(ExponentiationMI that) {
                if(exponent.isNone()){
                    exponent=Option.<Node>some(that);
                    return new TypeCheckerResult(that);
                }
                else{
                    String err_message = "Two consecutive ^s";
                    StaticError err=TypeError.make(err_message,
                                                                       new Span(NodeUtil.getSpan((ASTNode)exponent.unwrap()),
                                                                                NodeUtil.getSpan(that)).toString());
                    return new TypeCheckerResult(that,err);
                }
            }

            @Override
            public TypeCheckerResult forSubscriptingMI(SubscriptingMI that) {
                if(exponent.isNone()){
                    return new TypeCheckerResult(that);
                }
                else{
                    String err_message = "Exponentiation followed by subscripting is illegal";
                    StaticError err=TypeError.make(err_message,
                                                                       new Span(NodeUtil.getSpan((ASTNode)exponent.unwrap()),
                                                                                NodeUtil.getSpan(that)).toString());
                    exponent = Option.none();
                    return new TypeCheckerResult(that,err);
                }
            }
        };
        List<TypeCheckerResult> static_errors = static_error.recurOnListOfMathItem(items);
        TypeCheckerResult static_error_result = TypeCheckerResult.compose(ast, subtypeChecker, static_errors);
        if(!static_error_result.isSuccessful()){
            return Option.some(static_error_result);
        }
        else {
            return Option.none();
        }
    }

    private TypeChecker extend(List<LValue> bindings) {
        return new TypeChecker(table,
                typeEnv.extendWithLValues(bindings),
                compilationUnit,
                subtypeChecker,
                labelExitTypes,
                postInference,
                downwardConstraint);
    }

    private TypeChecker extend(List<StaticParam> newStaticParams, List<Param> newParams, Option<WhereClause> whereClause) {
        return new TypeChecker(table,
                typeEnv.extendWithParams(newParams).extendWithStaticParams(newStaticParams),
                compilationUnit,
                subtypeChecker.extend(newStaticParams, whereClause),
                labelExitTypes,
                postInference,
                downwardConstraint);
    }

    private TypeChecker extend(List<StaticParam> newStaticParams, Option<List<Param>> newParams, Option<WhereClause> whereClause) {
        return new TypeChecker(table,
                typeEnv.extend(newParams).extendWithStaticParams(newStaticParams),
                compilationUnit,
                subtypeChecker.extend(newStaticParams, whereClause),
                labelExitTypes,
                postInference,
                downwardConstraint);
    }

    private TypeChecker extend(List<StaticParam> newStaticParams, Option<WhereClause> whereClause) {
        return new TypeChecker(table,
                typeEnv.extendWithStaticParams(newStaticParams),
                compilationUnit,
                subtypeChecker.extend(newStaticParams, whereClause),
                labelExitTypes,
                postInference,
                downwardConstraint);
    }

    private TypeChecker extend(LocalVarDecl decl) {
        return new TypeChecker(table,
                typeEnv.extend(decl),
                compilationUnit,
                subtypeChecker,
                labelExitTypes,
                postInference,
                downwardConstraint);
    }

    private TypeChecker extend(Param newParam) {
        return new TypeChecker(table,
                typeEnv.extend(newParam),
                compilationUnit,
                subtypeChecker,
                labelExitTypes,
                postInference,
                downwardConstraint);
    }

    private TypeChecker extend(Option<WhereClause> whereClause) {
        return new TypeChecker(table,
                typeEnv,
                compilationUnit,
                subtypeChecker.extend(Collections.<StaticParam>emptyList(), whereClause),
                labelExitTypes,
                postInference,
                downwardConstraint);
    }

    public TypeChecker extendWithFnDecls(Relation<IdOrOpOrAnonymousName, FnDecl> fns) {
        return new TypeChecker(table,
                typeEnv.extendWithFnDecls(fns),
                compilationUnit,
                subtypeChecker,
                labelExitTypes,
                postInference,
                downwardConstraint);
    }

    public TypeChecker extendWithFunctions(Relation<IdOrOpOrAnonymousName, FunctionalMethod> methods) {
        return new TypeChecker(table,
                typeEnv.extendWithFunctions(methods),
                compilationUnit,
                subtypeChecker,
                labelExitTypes,
                postInference,
                downwardConstraint);
    }

    public TypeChecker extendWithMethods(Relation<IdOrOpOrAnonymousName, Method> methods) {
        return new TypeChecker(table,
                typeEnv.extendWithMethods(methods),
                compilationUnit,
                subtypeChecker,
                labelExitTypes,
                postInference,
                downwardConstraint);
    }

    public TypeChecker extendWithout(Node declSite, Set<? extends IdOrOpOrAnonymousName> names) {
        return new TypeChecker(table,
                typeEnv.extendWithout(declSite, names),
                compilationUnit,
                subtypeChecker,
                labelExitTypes,
                postInference,
                downwardConstraint);
    }

    public TypeChecker extendWithConstraints(Iterable<ConstraintFormula> constraints) {
        constraints = IterUtil.compose(downwardConstraint, constraints);
        ConstraintFormula new_constraint = ConstraintFormula.bigAnd(constraints,
                subtypeChecker.new SubtypeHistory());
        return new TypeChecker(table,
                typeEnv,
                compilationUnit,
                subtypeChecker,
                labelExitTypes,
                postInference,
                new_constraint);
    }

    private Option<Type> findFieldInTraitHierarchy(List<TraitType> supers, FieldRef that) {

        List<TraitType> new_supers = new ArrayList<TraitType>();
        for( TraitType my_super : supers ) {
            TraitIndex index = expectTraitIndex(my_super);

            final List<StaticParam> trait_static_params = index.staticParameters();
            final List<StaticArg> trait_static_args = my_super.getArgs();

            // Map to list of supertypes
            for( TraitTypeWhere ttw : index.extendsTypes() ) {
                Type t = ttw.getBaseType();
                Type t_ = (Type)t.accept(new StaticTypeReplacer(trait_static_params, trait_static_args));
                new_supers.addAll(traitTypesCallable(t_));
            }

            // check if trait has a getter
            Map<Id,Method> getters=index.getters();
            if(getters.containsKey(that.getField())) {
                Method field=(Method)getters.get(that.getField()).instantiate(trait_static_params, trait_static_args);
                return Option.some(field.getReturnType());
            }
            else {
                //check if trait is an object
                if(index instanceof ObjectTraitIndex) {
                    //Check if object has field
                    ObjectTraitIndex object_index=(ObjectTraitIndex)index;
                    Map<Id,Variable> fields=object_index.fields();
                    if(fields.containsKey(that.getField())){
                        Variable field=fields.get(that.getField());

                        if( field instanceof ParamVariable ) {
                            ParamVariable param = (ParamVariable)field;
                            Param field_node = param.ast();

                            Type field_type =
                                field_node.accept(new NodeAbstractVisitor<Type>() {
                                    @Override
                                    public Type forParam(Param that) {
                                                                            if ( NodeUtil.isVarargsParam(that) )
                                                                                return that.getIdType().unwrap();
                                                                            else
                                                                                return that.getVarargsType().unwrap();
                                                                        }
                                });

                            return Option.some(field_type);
                        }
                        else if( field instanceof DeclaredVariable ) {
                            DeclaredVariable var = (DeclaredVariable)field;
                            LValue bind = var.ast();
                            return Option.some(bind.getIdType().unwrap());
                        }
                        else {
                            return bug("Field of an object should not be a Singleton Object." + field);
                        }
                    }
                }
                //error no such field

            }
        }

        if(!new_supers.isEmpty() ) {
            // recur
            return this.findFieldInTraitHierarchy(new_supers, that);
        }
        else {
            return Option.none();
        }
    }

    // This method does a lot: Basically all of the hard work of finding an appropriate overloading, including looking
    // in parent traits.
    // TODO: This method is in need of a serious overhaul. It is way too similar to
    // TypesUtil.applicationType...
    private Pair<List<Method>,List<TypeCheckerResult>> findMethodsInTraitHierarchy(final IdOrOpOrAnonymousName method_name, List<TraitType> supers,
            Type arg_type, List<StaticArg> in_static_args,
            final Node that) {
        final List<TypeCheckerResult> all_results= new ArrayList<TypeCheckerResult>();
        List<Method> candidates=new ArrayList<Method>();
        List<TraitType> new_supers=new ArrayList<TraitType>();
        SubtypeHistory history = subtypeChecker.new SubtypeHistory();

        for(TraitType type: supers) {
            TraitIndex trait_index = expectTraitIndex(type);

            final List<StaticArg> extended_type_args = type.getArgs();
            final List<StaticParam> extended_type_params = trait_index.staticParameters();
            // get all of the types this type extends. Note that because we can extend types with our own static args,
            // we must visit the extended type with a static type replacer.
            for( TraitTypeWhere ttw : trait_index.extendsTypes() ) {
                Type t = (Type)ttw.getBaseType().accept(new StaticTypeReplacer(extended_type_params, extended_type_args));
                new_supers.addAll(traitTypesCallable(t));
            }

            // Get methods with the right name:
            // Add all dotted methods,
            Set<Method> methods_with_name = trait_index.dottedMethods().matchFirst(method_name);

            for( Method m : methods_with_name ) {
                List<StaticArg> static_args = new ArrayList<StaticArg>(in_static_args);
                // same number of static args
                if( m.staticParameters().size() > 0 && in_static_args.size() == 0 ) {
                    // we need to infer static arguments

                    List<StaticArg> static_inference_params =
                        CollectUtil.makeList(
                                IterUtil.map(m.staticParameters(), new Lambda<StaticParam,StaticArg>(){
                                    public StaticArg value(StaticParam arg0) {
                                        // TODO if parameters are anything but TypeParam, we don't know
                                        // how to infer it yet.
                                        // Otherwise, we've got all static parameters
                                                                            if( NodeUtil.isTypeParam(arg0) ){
                                            Set<BaseType> bounds = CollectUtil.asSet(arg0.getExtendsClause());
                                            Type ivt = NodeFactory.make_InferenceVarType(NodeUtil.getSpan(method_name));
                                            ConstraintFormula constraint=TypeChecker.this.subtypeChecker.subtype(ivt, NodeFactory.makeIntersectionType(bounds));
                                            all_results.add(new TypeCheckerResult(that, Option.<Type>none(), constraint));
                                            return NodeFactory.makeTypeArg(NodeFactory.makeSpan(ivt), ivt);
                                        }
                                        else{
                                            return NI.nyi();
                                        }
                                    }}));
                    static_args = static_inference_params;
                }
                else if(m.staticParameters().size()!=static_args.size()) {
                    // we don't need to infer, and they have different numbers of args
                    continue;
                }
                // instantiate method params with method and type args
                Functional im_maybe = m.instantiate(Useful.concat(m.staticParameters(), extended_type_params),
                        Useful.concat(static_args, extended_type_args));
                // we know this cast works, instantiate contract
                Method im = (Method)im_maybe;
                // Do they have the same number of parameters, or at least can they be matched.
                ConstraintFormula mc = this.argsMatchParams(im.parameters(), arg_type);
                // constraint & any relevent downward constraints satisfiable?
                if(mc.and(downwardConstraint, history) .isSatisfiable()) {
                    //add method to candidates
                    candidates.add(im);
                    all_results.add(new TypeCheckerResult(that,Option.<Type>none(),mc));
                }

            }
        }
        //If you have a super type check it for overloadings
        if(!new_supers.isEmpty()){

            Pair<List<Method>, List<TypeCheckerResult>> temp = findMethodsInTraitHierarchy(method_name, new_supers, arg_type, in_static_args, that);
            candidates.addAll(temp.first());
            all_results.addAll(all_results);
        }
        return Pair.make(candidates,all_results);
    }

    private TypeCheckerResult findSetterInTraitHierarchy(IdOrOpOrAnonymousName field_name, List<TraitType> supers,
            Type arg_type, Node ast){
        List<TraitType> new_supers = new ArrayList<TraitType>();
        for( TraitType my_super : supers ) {
            TraitIndex trait_index = expectTraitIndex(my_super);


            // Map to list of supertypes
            for( TraitTypeWhere ttw : trait_index.extendsTypes() ) {
                new_supers.addAll(traitTypesCallable(ttw.getBaseType()));
            }

            // check if trait has a getter
            Map<Id,Method> setters=trait_index.setters();
            if(setters.containsKey(field_name)) {
                Method field=setters.get(field_name);
                ConstraintFormula works =  argsMatchParams(field.parameters(),arg_type);
                if(!works.isSatisfiable()){
                    String errmes = "Argument to setter has wrong type";
                    StaticError err = TypeError.make(errmes, ast);
                    return new TypeCheckerResult(ast,Option.<Type>none(),Collections.singletonList(err),works);
                }
                else{
                    return new TypeCheckerResult(ast,works);
                }
            }
            else {
                // we used to check for a field but we don't think that's right.
                //check if trait is an object
                //                 if(trait_index instanceof ObjectTraitIndex){
                //                 //Check if object has field
                //                 ObjectTraitIndex object_index=(ObjectTraitIndex)trait_index;
                //                 Map<Id,Variable> fields=object_index.fields();
                //                 if(fields.containsKey(field_name)){
                //                 Variable field=fields.get(field_name);
                //                 Option<BindingLookup> type=this.typeEnv.binding(field_name);
                //                 return this.checkSubtype(arg_type,type.unwrap().getType().unwrap(),ast, "Argument to field has wrong type");
                //                 }
                //                 }
                //error no such field
            }
            //error receiver not a trait
        }

        if(!new_supers.isEmpty() ) {
            // recur
            return this.findSetterInTraitHierarchy(field_name, new_supers, arg_type, ast );
        }
        else {
            String errmes = "Setter for field "+ field_name +" not found.";
            return new TypeCheckerResult(ast,TypeError.make(errmes, ast));
        }

    }

    /**
     * Given a list of functional refs and the argument to which they are to be applied, find the FunctionalRef
     * whose type is the statically most applicable to the given arg.
     */
    private TypeCheckerResult findStaticallyMostApplicableFn(List<? extends Pair<? extends FunctionalRef, Type>> fns, Type arg_type, FunctionalRef ref, IdOrOp name) {
        final List<Pair<FunctionalRef, Type>> pruned_fns = new ArrayList<Pair<FunctionalRef, Type>>(fns.size());
        // prune down the list of fns to just the ones that apply
        for( Pair<? extends FunctionalRef, Type> fn : fns ) {
            // If applicationType indicates the method applies, we keep it in pruned_fns
            Type fn_type = fn.second();
            Option<?> applies = TypesUtil.applicationType(subtypeChecker, fn_type, new ArgList(arg_type), downwardConstraint);
            if( applies.isSome() )
                pruned_fns.add(Pair.<FunctionalRef, Type>make(fn.first(), fn_type));
        }

        if( pruned_fns.isEmpty() ){
            //No statically most applicable Fn
            String err = "No applicable overloading of " + name + " exists for argument of type " + arg_type.toString();
            TypeCheckerResult err_result = new TypeCheckerResult(ref, TypeError.make(err, ref));
            return TypeCheckerResult.compose(ref, subtypeChecker, err_result);
        }
        // then, find the one with out of that group with the most specific arguments.
        final Box<Option<Pair<FunctionalRef, Type>>> most_applicable = new Box<Option<Pair<FunctionalRef, Type>>>(){
            private Option<Pair<FunctionalRef, Type>> ma = none();
            public void set(Option<Pair<FunctionalRef, Type>> arg0) { ma = arg0; }
            public Option<Pair<FunctionalRef, Type>> value() { return ma; }
        };
        // Loops through all the pruned_fns finding one with the most specific arg type
        for( final Pair<FunctionalRef, Type> pruned_fn : pruned_fns ) {
            Type cur_type_ = pruned_fn.second();
            for( final Type cur_type : TypesUtil.conjuncts(cur_type_) ) {
                cur_type.accept(new TypeAbstractVisitor_void() {
                    @Override
                    public void forArrowType(final ArrowType cur_type) {
                        if( most_applicable.value().isNone() ) {
                            most_applicable.set(some(Pair.<FunctionalRef,Type>make(pruned_fn.first(), cur_type)));
                            return;
                        }
                        // do some gnarly double dispatch
                        most_applicable.value().unwrap().second().accept(new TypeAbstractVisitor_void() {
                            @Override
                            public void forArrowType(ArrowType most_appl) {
                                // Where is arg of cur_type <: arg of most_appl?
                                ConstraintFormula sub =
                                    subtypeChecker.subtype(Types.stripKeywords(cur_type.getDomain()),
                                            Types.stripKeywords(most_appl.getDomain()));
                                if( sub.solve().isTrue() ) {
                                    // TODO: We should actually throw an error if they are equal!
                                    most_applicable.set(some(Pair.<FunctionalRef,Type>make(pruned_fn.first(), cur_type)));
                                }
                            }
                            @Override public void forType(Type that) { bug("An applicable function should have an arrow type: " + that); }
                        });
                    }
                    @Override public void forType(Type that) {
                        bug("An applicable function should have an arrow type: " + that);
                    }
                });
            }
        }
        // Unwrap should always work b/c we already tested pruned_fns for empty, and
        // on the first iteration of the loop, most_applicable is always set to some.
        return new TypeCheckerResult(most_applicable.value().unwrap().first(), most_applicable.value().unwrap().second());
    }

    private static List<Pair<FunctionalRef, Type>> destructFnOverloadings(List<FunctionalRef> overloadings) {
        List<Pair<FunctionalRef, Type>> result = new ArrayList<Pair<FunctionalRef, Type>>(overloadings.size());
        for( FunctionalRef overloading : overloadings ) {
                    if ( overloading.getOverloadingType().isNone() )
                        bug(overloading,
                            "Type checker should have type for the overloading of "
                            + overloading.getOriginalName());
                    result.add(Pair.make(overloading, overloading.getOverloadingType().unwrap()));
        }
        return result;
    }

    @Override
    public TypeCheckerResult for_RewriteFnApp(_RewriteFnApp that) {
        TypeCheckerResult arg_result = recur(that.getArgument());

        if( postInference && that.getFunction() instanceof FnRef &&
                    isPostInference((FnRef)that.getFunction()) ) {
                    FnRef fns = (FnRef)that.getFunction();
            // if we have finished typechecking, and we have encountered a reference to an overloaded function

            if( !arg_result.isSuccessful() ) {
                return TypeCheckerResult.compose(that, subtypeChecker, arg_result);
            }

            Type arg_type = arg_result.type().unwrap();
            TypeCheckerResult fn_result = findStaticallyMostApplicableFn(destructFnOverloadings(fns.getOverloadings().unwrap()),
                                                                                     arg_type, fns, fns.getOriginalName());
            // Now just check the rewritten expression by the normal means
            return for_RewriteFnAppOnly(that, Option.<TypeCheckerResult>none(), fn_result, arg_result);
        }
        else {
            // Add constraints from the arguments, since they may affect overloading choice
                    TypeCheckerResult fn_result = recur(that.getFunction());
            Iterable<ConstraintFormula> arg_constraint = Collections.singletonList(arg_result.getNodeConstraints());
            //debugging
            ConstraintFormula temp = ConstraintFormula.TRUE;
            for(ConstraintFormula i: arg_constraint){
                temp.and(i, this.subtypeChecker.new SubtypeHistory());
            }
            Boolean blah = temp.isSatisfiable();
            //end debugging
            return this.extendWithConstraints(arg_constraint).for_RewriteFnAppOnly(that,
                    Option.<TypeCheckerResult>none(), fn_result, arg_result);
        }
    }

    public TypeCheckerResult for_RewriteFnAppOnly(_RewriteFnApp that, Option<TypeCheckerResult> exprType_result,
            TypeCheckerResult function_result, TypeCheckerResult argument_result) {
        // check sub expressions
        if( function_result.type().isNone() || argument_result.type().isNone() )
            return TypeCheckerResult.compose(that, subtypeChecker, function_result, argument_result);
        Option<Pair<Type,ConstraintFormula>> app_result =
            TypesUtil.applicationType(subtypeChecker, function_result.type().unwrap(),
                    new ArgList(argument_result.type().unwrap()), downwardConstraint);
        Option<Type> result_type;
        TypeCheckerResult result;

        if( app_result.isSome() ) {
            result = new TypeCheckerResult(that,app_result.unwrap().second());
            result_type = Option.some(app_result.unwrap().first());
        }
        else {
            String err = "Applicable overloading of function " + that.getFunction() +
                " could not be found for argument type " + normalize(argument_result.type().unwrap()); // error message needs work
            result = new TypeCheckerResult(that, TypeError.make(err, that));
            result_type = Option.none();
        }

        _RewriteFnApp new_node = ExprFactory.make_RewriteFnApp(NodeUtil.getSpan(that),
                NodeUtil.isParenthesized(that),
                result_type,
                (Expr) function_result.ast(),
                (Expr) argument_result.ast());

        // On the post-inference pass, an application could produce Inference vars
        TypeCheckerResult successful = new TypeCheckerResult(that);
        if( postInference && TypesUtil.containsInferenceVarTypes(new_node) ) {
            // close constraints
            Pair<Boolean,Node> temp1 = TypesUtil.closeConstraints(new_node, subtypeChecker, function_result, argument_result, result);
            new_node = (_RewriteFnApp)temp1.second();
            Boolean ok = temp1.first();
            if(result_type.isSome()){
                Pair<Boolean,Node> temp2 = TypesUtil.closeConstraints(result_type.unwrap(), subtypeChecker, function_result, argument_result, result);
                result_type = Option.some((Type)temp2.second());
                ok&=temp2.first();
            }
            if(!ok){
                String err = "Applicable overloading of function " + that.getFunction() + " could not be found for argument type " + argument_result.type();
                successful = new TypeCheckerResult(that,TypeError.make(err, that));
            }
        }

        return TypeCheckerResult.compose(new_node, result_type,
                subtypeChecker, function_result, argument_result, result, successful);
    }

    public TypeCheckerResult for_RewriteObjectRefOnly(VarRef that, TypeCheckerResult exprType_result,
                                                          TypeCheckerResult obj_result,
                                                          List<TypeCheckerResult> staticArgs_result) {
            Type t;
            ConstraintFormula accumulated_constraints = ConstraintFormula.TRUE;
            if( obj_result.type().isNone() ) {
                return TypeCheckerResult.compose(that, subtypeChecker, obj_result,
                                                 TypeCheckerResult.compose(that, subtypeChecker, staticArgs_result));
            }
            else if( (obj_result.type().unwrap() instanceof TraitType) ) {
                t=obj_result.type().unwrap();
                TraitType _t = (TraitType)t;

                if ( NodeUtil.isGenericSingletonType(_t) ) {
                    // instantiate with static parameters
                    Option<ConstraintFormula> constraint = StaticTypeReplacer.argsMatchParams(that.getStaticArgs(),
                                                                                              _t.getStaticParams(),
                                                                                              this.subtypeChecker);
                    if(constraint.isSome()) {
                        // make a trait type that is GenericType instantiated
                        t = NodeFactory.makeTraitType(NodeUtil.getSpan(_t),
                                                      NodeUtil.isParenthesized(_t),
                                                      _t.getName(),
                                                      that.getStaticArgs());
                        accumulated_constraints = constraint.unwrap();
                    }
                    else {
                        // error
                        String err = "Generic object, " + _t + " instantiated with invalid arguments, " + that.getStaticArgs();
                        TypeCheckerResult e_result = new TypeCheckerResult(that, TypeError.make(err, that));
                        return TypeCheckerResult.compose(that, subtypeChecker, obj_result, e_result,
                                                         TypeCheckerResult.compose(that, subtypeChecker, staticArgs_result));
                    }
                }
            }
            else {
                return bug("Unexpected type for ObjectRef.");
            }

            Node new_node = ExprFactory.makeVarRef(NodeUtil.getSpan(that), NodeUtil.isParenthesized(that),
                                                   Option.<Type>some(t),
                                                   (Id) obj_result.ast(),
                                                   (List<StaticArg>) TypeCheckerResult.astFromResults(staticArgs_result),
                                                   that.getLexicalDepth());
            return TypeCheckerResult.compose(new_node, t, subtypeChecker, obj_result,
                                             TypeCheckerResult.compose(that, subtypeChecker, staticArgs_result),
                                             new TypeCheckerResult(new_node,accumulated_constraints));
    }

    @Override
    public TypeCheckerResult forAmbiguousMultifixOpExpr(final AmbiguousMultifixOpExpr that) {
        // See if we can successfully typecheck this expression as a multifix one.
        TypeCheckerResult multi_result =
            (ExprFactory.makeOpExpr(NodeUtil.getSpan(that),
                                                NodeUtil.isParenthesized(that),
                                                NodeUtil.getExprType(that),
                                                that.getMultifix_op(),
                                                that.getArgs()).accept(this));

        if( multi_result.isSuccessful() ) {
            return multi_result;
        }
        else {
            if( that.getArgs().size() < 2 )
                bug("This never should have been neither multifix nor infix.");

            // If not, do it as a collection of left-associated infix expressions
            return
            IterUtil.fold(IterUtil.skipFirst(that.getArgs()), IterUtil.first(that.getArgs()),
                    new Lambda2<Expr,Expr,Expr>(){
                public Expr value(Expr arg0, Expr arg1) {
                    return ExprFactory.makeOpExpr(that.getInfix_op(), arg0, arg1);
                }}).accept(this);
        }

        //I am pretty sure this method rebuilds the ast correctly and fills in the exprType field without any changes

    }

    @Override
    public TypeCheckerResult forAnyType(AnyType that) {
        return new TypeCheckerResult(that);
    }

    @Override
    public TypeCheckerResult forAPIName(APIName that) {
        return new TypeCheckerResult(that);
    }

    // This case is only called for single element arrays ( e.g., [5] )
    // and not for pieces of ArrayElements
    @Override
    public TypeCheckerResult forArrayElementOnly(ArrayElement that, TypeCheckerResult exprType_result,
            List<TypeCheckerResult> staticArgs_result,
            TypeCheckerResult element_result) {

        if( element_result.type().isNone() ) {
            return TypeCheckerResult.compose(that, subtypeChecker, element_result,
                    TypeCheckerResult.compose(that, subtypeChecker, staticArgs_result));
        }

        List<StaticArg> staticArgs = that.getStaticArgs();
        Id array = Types.getArrayKName(1);
        Option<TypeConsIndex> ind=table.typeCons(array);
        if(ind.isNone()){
            array = Types.ARRAY_NAME;
            ind = table.typeCons(array);
            if(ind.isNone()){
                bug(array+"not in table");
            }
        }
        TraitIndex index = (TraitIndex)ind.unwrap();
        if(staticArgs.isEmpty()){
            TypeArg elem = NodeFactory.makeTypeArg(element_result.type().unwrap());
            IntArg lower = NodeFactory.makeIntArgVal(NodeUtil.getSpan(that),""+0);
            IntArg size = NodeFactory.makeIntArgVal(NodeUtil.getSpan(that),""+1);
            Type t=Types.makeArrayKType(1, Useful.list(elem, lower, size));
            Node new_node=ExprFactory.makeArrayElement(NodeUtil.getSpan(that), NodeUtil.isParenthesized(that),
                                                                   Option.some(t),
                                                                   (List<StaticArg>) TypeCheckerResult.astFromResults(staticArgs_result),
                                                                   (Expr) element_result.ast());
            return TypeCheckerResult.compose(new_node,t,this.subtypeChecker, element_result);
        }
        else{
            Option<ConstraintFormula> constraint = StaticTypeReplacer.argsMatchParams(that.getStaticArgs(), index.staticParameters(), this.subtypeChecker);
            if(constraint.isSome()){
                TypeCheckerResult res=this.checkSubtype(element_result.type().unwrap(),
                        ((TypeArg)that.getStaticArgs().get(0)).getTypeArg(), that,
                        element_result.type().unwrap()+" must be a subtype of "+((TypeArg)that.getStaticArgs().get(0)).getTypeArg());
                Type t=Types.makeArrayKType(1, that.getStaticArgs());
                Node new_node=ExprFactory.makeArrayElement(NodeUtil.getSpan(that), NodeUtil.isParenthesized(that),
                                                                           Option.some(t),
                                                                           (List<StaticArg>) TypeCheckerResult.astFromResults(staticArgs_result),
                                                                           (Expr) element_result.ast());
                return TypeCheckerResult.compose(new_node,t,this.subtypeChecker, element_result, res,
                        TypeCheckerResult.compose(new_node,this.subtypeChecker,staticArgs_result),
                        new TypeCheckerResult(new_node, constraint.unwrap()));
            }
            else{
                String err = "Explicit static arguments do not match required arguments for Array1 (" + index.staticParameters() + ".)";
                TypeCheckerResult err_result = new TypeCheckerResult(that, TypeError.make(err, that));
                return TypeCheckerResult.compose(that, subtypeChecker, err_result, element_result,
                        TypeCheckerResult.compose(that, subtypeChecker, staticArgs_result));
            }
        }
    }


    // This method is pretty long because we have to create a new visitor that visits ArrayElements and ArrayElement
    // knowing that we are inside of another ArrayElement.

    private static Pair<Type,List<BigInteger>> getTypeAndBoundsFromArray(Type that){
        TraitType type;
        if(that instanceof TraitType){
            type=(TraitType)that;
        }
        else{
            return InterpreterBug.bug("Not an Array");
        }
        if(type.getName().toString().startsWith("FortressLibrary.Array")){
            List<BigInteger> dims = new ArrayList<BigInteger>();
            for(int i=2; i<type.getArgs().size(); i+=2){
                StaticArg arg = type.getArgs().get(i);
                if(arg instanceof IntArg){
                    IntExpr iexpr = ((IntArg)arg).getIntVal();
                    if(iexpr instanceof IntBase){
                        IntLiteralExpr dim = ((IntBase) iexpr).getIntVal();
                        BigInteger n = dim.getIntVal();
                        dims.add(n);
                    }
                    else{
                        return NI.nyi();
                    }
                }
                else{
                    return InterpreterBug.bug("Array type changed");
                }
            }
            Type t;
            if(type.getArgs().get(0) instanceof TypeArg){
                t = ((TypeArg)type.getArgs().get(0)).getTypeArg();
            }
            else{
                return InterpreterBug.bug("Array type changed");
            }
            return Pair.make(t, dims);
        }
        else{
            return InterpreterBug.bug("Not an Array");
        }
    }

    @Override
    public TypeCheckerResult forArrayElements(ArrayElements that){
            Span span = NodeUtil.getSpan(that);
        List<TypeCheckerResult> subarrays = this.recurOnListOfArrayExpr(that.getElements());
        Lambda<TypeCheckerResult,Option<Pair<Type,List<BigInteger>>>> get = new Lambda<TypeCheckerResult,Option<Pair<Type,List<BigInteger>>>>(){
            public Option<Pair<Type, List<BigInteger>>> value(TypeCheckerResult arg0) {
                if(arg0.type().isSome()){
                    return Option.some(TypeChecker.this.getTypeAndBoundsFromArray(arg0.type().unwrap()));
                }
                else{
                    return Option.none();
                }
            }
        };
        Iterable <Option<Pair<Type, List<BigInteger>>>> temp = IterUtil.map(subarrays, get);
        List<Type> types = new ArrayList<Type>();
        List<List<BigInteger>> dims = new ArrayList<List<BigInteger>>();
        boolean failed=false;
        List<TypeCheckerResult> all_results = new ArrayList<TypeCheckerResult>(subarrays);
        for(Option<Pair<Type,List<BigInteger>>> i: temp){
            if(i.isNone()){
                //one of your subarrays already failed
                failed=true;
            }
            else{
                types.add(i.unwrap().first());
                dims.add(i.unwrap().second());
            }
        }
        List<BigInteger> first = dims.get(0);
        Boolean same_size = true;
        for(List<BigInteger> f: dims){
            same_size&=f.equals(first);
        }
        Type array_type = this.subtypeChecker.join(types);

        if(!same_size){
            all_results.add(new TypeCheckerResult(that, TypeError.make("Not all subarrays the same size ", that)));
        }



        // Now try to get array type for the dimension we have
        int dim = that.getDimension();
        Id array = Types.getArrayKName(dim);
        Option<TypeConsIndex> ind=table.typeCons(array);
        if(ind.isNone()){
            array = Types.ARRAY_NAME;
            ind = table.typeCons(array);
            if(ind.isNone()){
                bug(array+"not in table");
            }
        }

        TraitIndex trait_index = (TraitIndex)ind.unwrap();


        Type return_type;
        ConstraintFormula accumulated_constraints = ConstraintFormula.TRUE;
        if(that.getStaticArgs().isEmpty()){
            if(failed || !same_size){
                return TypeCheckerResult.compose(that, subtypeChecker, all_results);
            }
            // then we just use what we determine to be true
            List<StaticArg> inferred_args = new ArrayList<StaticArg>(1+dim*2);
            inferred_args.add(NodeFactory.makeTypeArg(array_type));
            IntArg lower_bound = NodeFactory.makeIntArgVal(span,"0");
            IntArg size = NodeFactory.makeIntArgVal(span,
                                                                ((Integer)subarrays.size()).toString());
            inferred_args.add(lower_bound);
            inferred_args.add(size);
            for(int i=0;i<dim-1;i++) {
                BigInteger s = first.get(i);
                lower_bound = NodeFactory.makeIntArgVal(span,"0");
                size = NodeFactory.makeIntArgVal(span,s.toString());
                inferred_args.add(lower_bound);
                inferred_args.add(size);
            }
            // then instantiate and return
            return_type = Types.makeArrayKType(dim, inferred_args);
        }
        else{
            List<StaticArg> sargs = that.getStaticArgs();
            Option<ConstraintFormula> constraints = StaticTypeReplacer.argsMatchParams(sargs, trait_index.staticParameters(), this.subtypeChecker);
            if(constraints.isSome()) {
                // First arg MUST BE a TypeArg, and it must be a supertype of the elements
                Type declared_type = ((TypeArg)that.getStaticArgs().get(0)).getTypeArg();
                all_results.add(this.checkSubtype(array_type, declared_type, that, "Array elements must be a subtype of explicity declared type" + declared_type + "."));
                //Check infered dims against explicit dims
                return_type = Types.makeArrayKType(dim, sargs);
                accumulated_constraints=constraints.unwrap();
            }
            else {
                // wrong args passed
                all_results.add(new TypeCheckerResult(that, TypeError.make("Explicit static arguments don't matched required arguments for " + trait_index + ".", that)));
                return TypeCheckerResult.compose(that ,subtypeChecker, all_results);
            }
            if(failed || !same_size){
                return TypeCheckerResult.compose(that, Option.some(return_type) ,subtypeChecker, all_results);
            }
        }



        Lambda<TypeCheckerResult,ArrayExpr> get_expr = new Lambda<TypeCheckerResult,ArrayExpr>(){
            public ArrayExpr value(TypeCheckerResult arg0) {
                return (ArrayExpr)arg0.ast();
            }
        };
        ArrayElements new_node=ExprFactory.makeArrayElements(NodeUtil.getSpan(that),
                                                                     NodeUtil.isParenthesized(that),
                                                                     Option.some(return_type) ,
                                                                     that.getStaticArgs(),
                                                                     that.getDimension(),
                                                                     Useful.list(IterUtil.map(subarrays, get_expr)),
                                                                     that.isOutermost());

        all_results.add(new TypeCheckerResult(new_node, accumulated_constraints));

        return TypeCheckerResult.compose(new_node, Option.some(return_type) ,subtypeChecker, all_results);

    }

    @Override
    public TypeCheckerResult forAsExpr(AsExpr that) {
        Type ascriptedType = that.getAnnType();
        TypeCheckerResult expr_result = that.getExpr().accept(this);
        Type exprType = expr_result.type().isSome() ? expr_result.type().unwrap() : Types.BOTTOM;
        // node rebuilding handled in forTypeAnnotatedExprOnly
        return forTypeAnnotatedExprOnly(that,
                expr_result,
                errorMsg("Attempt to ascribe expression of type ",
                        exprType, " to non-supertype ", ascriptedType));
    }

    @Override
    public TypeCheckerResult forAsIfExpr(AsIfExpr that) {
        Type assumedType = that.getAnnType();
        TypeCheckerResult expr_result = that.getExpr().accept(this);
        Type exprType = expr_result.type().isSome() ? expr_result.type().unwrap() : Types.BOTTOM;
        // node rebuilding handled in forTypeAnnotatedExprOnly
        return forTypeAnnotatedExprOnly(that,
                expr_result,
                errorMsg("Attempt to assume type ", assumedType,
                        " from non-subtype ", exprType));
    }

    @Override
    public TypeCheckerResult forAssignment(Assignment that) {
            if ( that.getOpsForLhs().isSome() ) // postInference pass
                return for_Assignment( that );

        Pair<List<Type>, TypeCheckerResult> tuple_types_ = requireTupleType(that.getRhs(), that.getLhs().size());

        // Get the types for the RHS, which must be a tuple if the LHS is
        TypeCheckerResult rhs_result = tuple_types_.second();
        List<Type> rhs_types = tuple_types_.first();

        if( !rhs_result.isSuccessful() )
            return TypeCheckerResult.compose(that, subtypeChecker, rhs_result);
        if( rhs_types.size() != that.getLhs().size() )
            return bug("requireTupleType should always return a list of types equal to the size it is passed.");

        List<TypeCheckerResult> lhs_results = new ArrayList<TypeCheckerResult>(that.getLhs().size());
        List<FunctionalRef> op_refs = that.getAssignOp().isSome() ? new ArrayList<FunctionalRef>(that.getLhs().size()) : Collections.<FunctionalRef>emptyList();

        // Go through LHS, checking each one
        Iterator<Type> rhs_type_iter = rhs_types.iterator();
        for( Lhs lhs : that.getLhs() ) {
            Type rhs_type = rhs_type_iter.next();
            Pair<Option<FunctionalRef>, TypeCheckerResult> p = checkLhsAssignment(lhs, rhs_type, that.getAssignOp());
            lhs_results.add(p.second());

            if( p.first().isSome() )
                op_refs.add(p.first().unwrap());
        }

        Assignment new_node;
        if( that.getAssignOp().isSome() ) {
            // Create a new Assignment, with an FunctionalRef for each LHS
            new_node = ExprFactory.makeAssignment(NodeUtil.getSpan(that),
                                                  NodeUtil.isParenthesized(that),
                                                  Option.<Type>some(Types.VOID),
                                                  (List<Lhs>)TypeCheckerResult.astFromResults(lhs_results),
                                                  that.getAssignOp(),
                                                  (Expr)rhs_result.ast(),
                                                  Option.<List<FunctionalRef>>some(op_refs));
        }
        else {
            // Create a new Assignment
            new_node = ExprFactory.makeAssignment(NodeUtil.getSpan(that),
                    NodeUtil.isParenthesized(that),
                    Option.<Type>some(Types.VOID),
                    (List<Lhs>)TypeCheckerResult.astFromResults(lhs_results),
                    that.getAssignOp(),
                    (Expr)rhs_result.ast(),
                                        Option.<List<FunctionalRef>>none());
        }
        // This case could not result in open constraints: If there is an FunctionalRef, this must not be
        // the postInference pass, because AssignmentNodes should exist instead. If there is
        // no FunctionalRef, then no open constraints can be created.
        return TypeCheckerResult.compose(new_node, Types.VOID, subtypeChecker, rhs_result,
                TypeCheckerResult.compose(new_node, subtypeChecker, lhs_results));
    }

    private TypeCheckerResult for_Assignment(Assignment that) {
        Pair<List<Type>, TypeCheckerResult> tuple_types_ = requireTupleType(that.getRhs(), that.getLhs().size());

        // Get the types for the RHS, which must be a tuple if the LHS is
        TypeCheckerResult rhs_result = tuple_types_.second();
        List<Type> rhs_types = tuple_types_.first();

        if( !rhs_result.isSuccessful() )
            return TypeCheckerResult.compose(that, subtypeChecker, rhs_result);
        if( rhs_types.size() != that.getLhs().size() )
            return bug("requireTupleType should always return a list of types equal to the size it is passed.");

        List<TypeCheckerResult> lhs_results = new ArrayList<TypeCheckerResult>(that.getLhs().size());
        List<FunctionalRef> op_refs = that.getAssignOp().isSome() ? new ArrayList<FunctionalRef>(that.getLhs().size()) : Collections.<FunctionalRef>emptyList();

        // Go through LHS, checking each one
        Iterator<Type> rhs_type_iter = rhs_types.iterator();
        for( Lhs lhs : that.getLhs() ) {
            Type rhs_type = rhs_type_iter.next();
            Pair<Option<FunctionalRef>, TypeCheckerResult> p = checkLhsAssignment(lhs, rhs_type, that.getAssignOp());
            lhs_results.add(p.second());

            if( p.first().isSome() )
                op_refs.add(p.first().unwrap());
        };

        // Create a Assignment, with an FunctionalRef for each LHS
        Assignment new_node = ExprFactory.makeAssignment(NodeUtil.getSpan(that),
                                                     NodeUtil.isParenthesized(that),
                                                     Option.<Type>some(Types.VOID),
                                                     (List<Lhs>)TypeCheckerResult.astFromResults(lhs_results),
                                                     that.getAssignOp(),
                                                     (Expr)rhs_result.ast(),
                                                     Option.<List<FunctionalRef>>some(op_refs));

        TypeCheckerResult result = TypeCheckerResult.compose(new_node, Types.VOID, subtypeChecker, rhs_result,
                TypeCheckerResult.compose(new_node, subtypeChecker, lhs_results));

        // The application of operators could cause Inference Vars to be introduced
        TypeCheckerResult successful = new TypeCheckerResult(that);
        if( postInference && TypesUtil.containsInferenceVarTypes(new_node) ) {
            Pair<Boolean,Node> temp = TypesUtil.closeConstraints(new_node, result);
            new_node = (Assignment)temp.second();
            if(!temp.first()){
                String err = "No overloading for " + that.getAssignOp().unwrap();
                successful = new TypeCheckerResult(that, TypeError.make(err,that));
            }
        }
        return TypeCheckerResult.compose(new_node, Types.VOID, subtypeChecker, result, successful);
    }
    /**
     * Checks that something of type rhs_type can be assigned to the given lhs. If opr is some, we have to
     * take that in to account as well. This method is still pretty complicated...
     */
    private Pair<Option<FunctionalRef>, TypeCheckerResult> checkLhsAssignment(final Lhs lhs, final Type rhs_type, final Option<FunctionalRef> opr) {

        // Different assignment rules for each type of LHS...
        Pair<TypeCheckerResult, Type> result_and_arg_type = lhs.accept(new NodeAbstractVisitor<Pair<TypeCheckerResult, Type>>(){
            @Override public Pair<TypeCheckerResult, Type> forFieldRef(FieldRef that) {
                TypeCheckerResult obj_result = recur(that.getObj());
                TypeCheckerResult field_result = recur(that); // only used for ast, and type if opr is SOME
                if( !obj_result.isSuccessful() )
                    return Pair.<TypeCheckerResult,Type>make(TypeCheckerResult.compose(that, subtypeChecker, obj_result), Types.BOTTOM);

                Type obj_type = obj_result.type().unwrap();
                List<TraitType> traits = traitTypesCallable(obj_type);
                TypeCheckerResult r = findSetterInTraitHierarchy(that.getField(), traits, rhs_type, that);

                if( opr.isSome() && field_result.isSuccessful() ) {
                    // Return the type of the field for opr application
                    return Pair.<TypeCheckerResult,Type>make(TypeCheckerResult.compose(field_result.ast(), subtypeChecker, r, field_result, obj_result), field_result.type().unwrap());
                }
                else if( opr.isSome() && !field_result.isSuccessful() ) {
                    return Pair.<TypeCheckerResult,Type>make(TypeCheckerResult.compose(that, subtypeChecker, r, field_result, obj_result), Types.BOTTOM);
                }
                else {
                    return Pair.<TypeCheckerResult, Type>make(TypeCheckerResult.compose(field_result.ast(), subtypeChecker, r, obj_result), Types.BOTTOM);
                }
            }

            @Override public Pair<TypeCheckerResult, Type> forLValue(LValue that) {
                if( !that.isMutable() ) {
                    String err = "Left-hand side of assignment must be mutable.";
                    return Pair.<TypeCheckerResult,Type>make(new TypeCheckerResult(that, TypeError.make(err, that)), Types.BOTTOM);
                }
                else {
                    Type lhs_type = that.getIdType().unwrap();
                    return Pair.make(checkSubtype(rhs_type,
                            lhs_type, that,
                            "Type of right-hand side of assignment, " + rhs_type + ", must be a sub-type of left-hand side, " + lhs_type + "."),
                            lhs_type);
                }
            }

            @Override
            public Pair<TypeCheckerResult, Type> forParam(Param that) {
                            if ( ! NodeUtil.isVarargsParam(that) ) {
                if( !NodeUtil.isMutable(that) ) {
                    String err = "Left-hand side of assignment must be mutable.";
                    return Pair.<TypeCheckerResult,Type>make(new TypeCheckerResult(that, TypeError.make(err, that)), Types.BOTTOM);
                }
                else {
                    Type lhs_type = that.getIdType().unwrap();
                    return Pair.make(checkSubtype(rhs_type,
                            lhs_type, that,
                            "Type of right-hand side of assignment, " + rhs_type + ", must be a sub-type of left-hand side, " + lhs_type + "."),
                            lhs_type);
                }
                            } else
                                return bug(that, "Varargs parameter should not appear in the left-hand side of an assignment.");
            }

            @Override
            public Pair<TypeCheckerResult, Type> forSubscriptExpr(SubscriptExpr that) {
                // If there is an op, we must typechecker that as a normal read reference
                TypeCheckerResult read_result = recur(that); // only used if opr is SOME

                // make sure there is a subscript setter for type
                // This method is very similar to forSubscriptExprOnly in Typechecker
                // except that we must graft the new RHS type onto the end of subs_types
                // to see if there is an appropriate setter method.
                TypeCheckerResult obj_result = that.getObj().accept(TypeChecker.this);
                List<TypeCheckerResult> subs_result = TypeChecker.this.recurOnListOfExpr(that.getSubs());
                // ignore op_result...
                List<TypeCheckerResult> staticArgs_result = TypeChecker.this.recurOnListOfStaticArg(that.getStaticArgs());

                TypeCheckerResult all_result =
                    TypeCheckerResult.compose(that, subtypeChecker, obj_result,
                            TypeCheckerResult.compose(that, subtypeChecker, subs_result),
                            TypeCheckerResult.compose(that, subtypeChecker, staticArgs_result));

                if( obj_result.type().isNone() ) return Pair.<TypeCheckerResult,Type>make(all_result,Types.BOTTOM);
                for( TypeCheckerResult r : subs_result )
                    if( r.type().isNone() ) return Pair.<TypeCheckerResult,Type>make(all_result,Types.BOTTOM);

                // get types
                Type obj_type = obj_result.type().unwrap();
                List<Type> subs_types = CollectUtil.makeList(IterUtil.map(subs_result, new Lambda<TypeCheckerResult,Type>(){
                    public Type value(TypeCheckerResult arg0) { return arg0.type().unwrap(); }}));
                // put rhs type on the end
                subs_types = Useful.concat(subs_types, Collections.singletonList(rhs_type));

                TypeCheckerResult final_result =
                    TypeChecker.this.subscriptHelper(that, that.getOp(), obj_type, subs_types, that.getStaticArgs());

                SubscriptExpr new_node = (SubscriptExpr)read_result.ast();

                if(opr.isSome() && read_result.isSuccessful() ) {
                    return Pair.<TypeCheckerResult,Type>make(TypeCheckerResult.compose(new_node,
                            read_result.type(), subtypeChecker, read_result, final_result, all_result), Types.BOTTOM);
                }
                else if( opr.isSome()) {
                    return Pair.make(TypeCheckerResult.compose(new_node,
                            read_result.type(), subtypeChecker, read_result, final_result, all_result), read_result.type().unwrap());
                }
                else {
                    return Pair.<TypeCheckerResult,Type>make(TypeCheckerResult.compose(new_node,
                            read_result.type(), subtypeChecker, final_result, all_result), Types.BOTTOM);
                }
            }

            @Override
            public Pair<TypeCheckerResult, Type> forVarRef(VarRef that) {
                TypeCheckerResult var_result = recur(that);
                if( !var_result.isSuccessful() ) return Pair.<TypeCheckerResult, Type>make(var_result, Types.BOTTOM);

                TypeCheckerResult sub_result = checkSubtype(rhs_type, var_result.type().unwrap(), lhs,
                        "Type of right-hand side of assignment, " +rhs_type+ ", must be subtype of left-hand side, " + var_result.type() + ".");

                TypeEnv env = that.getVarId().getApiName().isSome() ? returnTypeEnvForApi(that.getVarId().getApiName().unwrap()) : typeEnv;
                Option<BindingLookup> bl = env.binding(that.getVarId());
                if( bl.isNone() ) return bug("Inconsistent results from TypeEnv and typechecking VarRef");

                // make sure it's immutable
                if( !(bl.unwrap().isMutable()) ) {
                    String err = "Left-hand side of assignment must be mutable.";
                    return Pair.<TypeCheckerResult,Type>make(new TypeCheckerResult(that, TypeError.make(err, that)), Types.BOTTOM);
                }
                else {
                    return Pair.make(TypeCheckerResult.compose(var_result.ast(), subtypeChecker, sub_result, var_result), var_result.type().unwrap());
                }
            }

        });

        final Type arg_type = result_and_arg_type.second();
        // Find the arrow type of the opr, if it is some
        Option<TypeCheckerResult> opr_type = (new NodeDepthFirstVisitor<TypeCheckerResult>() {
            @Override public TypeCheckerResult forFnRef(FnRef that) {
                            return TypeChecker.this.recur(that);
                        }
            @Override public TypeCheckerResult forOpRef(OpRef that) {
                            if ( isPostInference(that) ) {
                                Type args_type = NodeFactory.makeTupleType(NodeUtil.getSpan(that),
                                                                           Useful.list(arg_type, rhs_type));
                                return findStaticallyMostApplicableFn(TypeChecker.destructOpOverLoading(that.getOverloadings().unwrap()),
                                                                      args_type, that, that.getOriginalName());
                            }

                            TypeCheckerResult op_result = TypeChecker.this.recur(that);
                            if( !op_result.isSuccessful() ) return op_result;

                            Option<Pair<Type, ConstraintFormula>> app_result =
                            TypesUtil.applicationType(subtypeChecker, op_result.type().unwrap(), new ArgList(arg_type, rhs_type), downwardConstraint);

                            if( app_result.isNone() ) {
                                String err = "No overloading of " + that.getOriginalName() + " can be found that applies to types " +
                                    arg_type + " and " + rhs_type + ".";
                                return new TypeCheckerResult(that, TypeError.make(err, that));
                            }
                            else {
                                TypeCheckerResult app_result_ = new TypeCheckerResult(that, app_result.unwrap().second());
                                return TypeCheckerResult.compose(op_result.ast(), subtypeChecker, app_result_, op_result);
                            }
                        }
                    }).recurOnOptionOfFunctionalRef(opr);

        TypeCheckerResult result = TypeCheckerResult.compose(result_and_arg_type.first().ast(), subtypeChecker, result_and_arg_type.first(),
                                                                     TypeCheckerResult.compose(result_and_arg_type.first().ast(), subtypeChecker, opr_type));

        return Pair.<Option<FunctionalRef>,TypeCheckerResult>make((Option<FunctionalRef>)TypeCheckerResult.astFromResult(opr_type), result);
    }

    /**
     * An assertion that the type of the given expression should be a tuple type of the given size.
     * If it is of a different size, an error will be reported. If is not an instance of TupleType,
     * a tuple of inference variables will be created instead, with the restriction that it must have the
     * same type as e's type.
     */
    private Pair<List<Type>, TypeCheckerResult> requireTupleType(final Expr e, int size) {
        final List<Type> inference_var_types = NodeFactory.make_InferenceVarTypes(NodeUtil.getSpan(e), size); // may not be used
        final TypeCheckerResult e_result = recur(e);

        if( !e_result.isSuccessful() )
            return Pair.make(inference_var_types, e_result);

        if( size == 1 ) {
            return Pair.make(Collections.singletonList(e_result.type().unwrap()), e_result);
        }

        return e_result.type().unwrap().accept(new TypeAbstractVisitor<Pair<List<Type>, TypeCheckerResult>>() {
            @Override
            public Pair<List<Type>, TypeCheckerResult> forTupleType(TupleType that) {
                return Pair.make(that.getElements(), e_result);
            }
            @Override
            public Pair<List<Type>, TypeCheckerResult> forType(Type that) {
                Type tuple_type = NodeFactory.makeTupleType(NodeUtil.getSpan(that),
                                                                            inference_var_types);
                TypeCheckerResult sub_1 = checkSubtype(tuple_type, that, e);
                TypeCheckerResult sub_2 = checkSubtype(that, tuple_type, e);
                TypeCheckerResult tcr = TypeCheckerResult.compose(e, subtypeChecker, sub_1, sub_2, e_result);
                return Pair.make(inference_var_types, tcr);
            }
        });
    }


    private TypeCheckerResult forAtomic(Expr body, final String errorMsg) {
        TypeChecker newChecker = new TypeChecker(table,
                //staticParamEnv,
                typeEnv,
                compilationUnit,
                subtypeChecker,
                labelExitTypes,
                postInference,
                downwardConstraint) {
            @Override public TypeCheckerResult forSpawn(Spawn that) {
                // Use TypeChecker's forSpawn method, but compose an error onto the result
                return TypeCheckerResult.compose(
                        that,
                        subtypeChecker,
                        new TypeCheckerResult(that,
                                TypeError.make(errorMsg,
                                        that)), that.accept(TypeChecker.this));
            }
        };
        return body.accept(newChecker);
    }

    @Override
    public TypeCheckerResult forAtomicExpr(AtomicExpr that) {
        TypeCheckerResult expr_result =
            forAtomic(that.getExpr(),
                    errorMsg("A 'spawn' expression must not occur inside an 'atomic' expression."));

        AtomicExpr new_node = ExprFactory.makeAtomicExpr(NodeUtil.getSpan(that),
                NodeUtil.isParenthesized(that),
                expr_result.type(),
                (Expr)expr_result.ast());
        return TypeCheckerResult.compose(new_node, expr_result.type(), subtypeChecker, expr_result);
    }

    @Override
    public TypeCheckerResult forBigFixity(BigFixity that) {
        return new TypeCheckerResult(that);
    }

    @Override
    public TypeCheckerResult forCaseExpr(CaseExpr that) {
        Option<TypeCheckerResult> param_result = this.recurOnOptionOfExpr(that.getParam());
        Option<TypeCheckerResult> compare_result = this.recurOnOptionOfFunctionalRef(that.getCompare());
        TypeCheckerResult equalsOp_result = that.getEqualsOp().accept(this);
        TypeCheckerResult inOp_result = that.getInOp().accept(this);
        NodeDepthFirstVisitor<Triple<CaseClause, TypeCheckerResult,TypeCheckerResult>> temp = new NodeDepthFirstVisitor<Triple<CaseClause, TypeCheckerResult,TypeCheckerResult>>() {
            @Override
            public Triple<CaseClause, TypeCheckerResult, TypeCheckerResult> forCaseClause(
                    CaseClause that) {
                TypeCheckerResult match_result = that.getMatchClause().accept(TypeChecker.this);
                TypeCheckerResult body_result = that.getBody().accept(TypeChecker.this);
                CaseClause new_node = NodeFactory.makeCaseClause(NodeUtil.getSpan(that), (Expr)match_result.ast(), (Block)body_result.ast(),
                                                                     that.getOp());
                return Triple.<CaseClause,TypeCheckerResult,TypeCheckerResult>make(new_node, match_result, body_result);
            }
        };
        List<Triple<CaseClause, TypeCheckerResult,TypeCheckerResult>> clauses_result = temp.recurOnListOfCaseClause(that.getClauses());
        Option<TypeCheckerResult> elseClause_result = recurOnOptionOfBlock(that.getElseClause());

        // Checker that clauses all typechecked properly
        for(Triple<CaseClause, TypeCheckerResult,TypeCheckerResult> clause_result: clauses_result){
            if(clause_result.second().type().isNone() || clause_result.third().type().isNone()) {
                return TypeCheckerResult.compose(that, subtypeChecker,
                        TypeCheckerResult.compose(that, subtypeChecker, CollectUtil.makeList(IterUtil.tripleSeconds(clauses_result))),
                        TypeCheckerResult.compose(that, subtypeChecker, CollectUtil.makeList(IterUtil.tripleThirds(clauses_result))));
            }
        }

        // Check that compare typechecked, if it exists
        if( compare_result.isSome()) {
            if(compare_result.unwrap().type().isNone()){
                return TypeCheckerResult.compose(that, subtypeChecker, compare_result.unwrap());
            }
        }
        // Check elseClause
        if(elseClause_result.isSome()){
            if(elseClause_result.unwrap().type().isNone()){
                return TypeCheckerResult.compose(that, subtypeChecker, elseClause_result.unwrap());
            }
        }
        // Check if we are dealing with a normal case (i.e. not an extremum)
        if (that.getParam().isSome()) {
            if(param_result.unwrap().type().isNone()){
                return TypeCheckerResult.compose(that, subtypeChecker, param_result.unwrap());
            }

            if(equalsOp_result.type().isNone() || inOp_result.type().isNone()){
                return bug("Equals or In does not have a type");
            }

            return forCaseExprNormal(that);
        } else {
            return forExtremumOnly(that, compare_result.unwrap(), clauses_result);
        }
    }

    // Handle regular (non-extremum) case expressions
    private TypeCheckerResult forCaseExprNormal(CaseExpr that) {
        Option<TypeCheckerResult> else_result_ = recurOnOptionOfBlock(that.getElseClause());
        Option<TypeCheckerResult> param_result_ = recurOnOptionOfExpr(that.getParam());
        Option<TypeCheckerResult> compare_result_ = recurOnOptionOfFunctionalRef(that.getCompare());
        TypeCheckerResult equals_result = recur(that.getEqualsOp());
        TypeCheckerResult in_result = recur(that.getInOp());

        // Check all of these subexpressions
        if( (else_result_.isSome() && !else_result_.unwrap().isSuccessful()) || (param_result_.isSome() && !param_result_.unwrap().isSuccessful()) ||
                (compare_result_.isSome() && !compare_result_.unwrap().isSuccessful()) || !equals_result.isSuccessful() || !in_result.isSuccessful() ) {
            TypeCheckerResult.compose(that, subtypeChecker, equals_result, in_result,
                    TypeCheckerResult.compose(that, subtypeChecker, else_result_, param_result_, compare_result_));
        }

        List<TypeCheckerResult> clause_results = new ArrayList<TypeCheckerResult>(that.getClauses().size());
        List<Type> clause_types = new ArrayList<Type>(that.getClauses().size());

        for( CaseClause clause : that.getClauses() ) {
            Type param_type = param_result_.unwrap().type().unwrap(); // assured by the fact that we are caseExprNormal

            if( postInference ) {
                // after inference, the case clause had better have the op field set
                            if( clause.getOp().isNone() )
                                    return bug("All case clauses should be rewritten to reflect the chosen compare op.");

                Pair<Type, TypeCheckerResult> p = for_CaseClauseGetType(clause, param_result_);
                clause_results.add(p.second());
                clause_types.add(p.first());
            }
            else {
                // during inference, we'll try to apply the given compare op (if there is one) and otherwise try
                // equals and in. We will set the op field with a chosen opr.
                Pair<Type, TypeCheckerResult> p = forCaseClauseRewriteAndGetType(clause, param_result_, compare_result_, equals_result, in_result);
                clause_results.add(p.second());
                clause_types.add(p.first());
            }
        }

        // Also, do else block if necessary
        if( else_result_.isSome() ) {
            clause_types.add(else_result_.unwrap().type().unwrap());
        }

        Type result_type = NodeFactory.makeIntersectionType(CollectUtil.asSet(clause_types));
        CaseExpr new_node = ExprFactory.makeCaseExpr(NodeUtil.getSpan(that),
                NodeUtil.isParenthesized(that),
                some(result_type),
                (Option<Expr>)TypeCheckerResult.astFromResult(param_result_),
                (Option<FunctionalRef>)TypeCheckerResult.astFromResult(compare_result_),
                (FunctionalRef)equals_result.ast(),
                (FunctionalRef)in_result.ast(),
                (List<CaseClause>)TypeCheckerResult.astFromResults(clause_results),
                (Option<Block>)TypeCheckerResult.astFromResult(else_result_));
        TypeCheckerResult result = TypeCheckerResult.compose(new_node, subtypeChecker, equals_result, in_result,
                TypeCheckerResult.compose(new_node, subtypeChecker, clause_results),
                TypeCheckerResult.compose(new_node, subtypeChecker, param_result_, compare_result_, else_result_));

        // The application of operators (IN, EQUALS) could cause Inference Vars to be introduced
        TypeCheckerResult successful = new TypeCheckerResult(that);
        if( postInference && TypesUtil.containsInferenceVarTypes(new_node) ) {
            Pair<Boolean,Node> temp1 = TypesUtil.closeConstraints(new_node, result);
            new_node = (CaseExpr)temp1.second();
            Pair<Boolean,Node> temp2 = TypesUtil.closeConstraints(result_type, result);
            result_type = (Type)temp2.second();
            if(!temp1.first() || !temp2.first()){
                String err = "No overloading of " + (that.getCompare().isSome()? that.getCompare().unwrap() + "." : that.getEqualsOp() + " or " + that.getInOp() + ".");
                successful = new TypeCheckerResult(that, TypeError.make(err,that));
            }
        }
        return TypeCheckerResult.compose(new_node, result_type, subtypeChecker, result);
    }

    /**
     * Typecheck the clause, using one of the ops (compare, equals, or in), return the type of the right-hand side block, and
     * rewrite the CaseClause to set the op field. All TypeCheckerResults must contain types, and must contain the AST type
     * that is reflected by their name.
     */
    private Pair<Type, TypeCheckerResult> forCaseClauseRewriteAndGetType(CaseClause clause, Option<TypeCheckerResult> param_result_,
            Option<TypeCheckerResult> compare_result_, TypeCheckerResult equals_result, TypeCheckerResult in_result) {
        TypeCheckerResult match_result = recur(clause.getMatchClause());
        TypeCheckerResult block_result = recur(clause.getBody());

        // make sure subexpressions were well-typed
        if( !match_result.isSuccessful() || !block_result.isSuccessful() )
            return Pair.<Type,TypeCheckerResult>make(Types.BOTTOM, TypeCheckerResult.compose(clause, subtypeChecker, match_result, block_result));

        Type match_type = match_result.type().unwrap();
        Type block_type = block_result.type().unwrap();
        FunctionalRef chosen_op;
        Option<Pair<Type, ConstraintFormula>> application_result;
        Type param_type = param_result_.unwrap().type().unwrap();
        ArgList args = new ArgList(param_type, match_type);

        // If compare is some, we use that operator
        if( compare_result_.isSome() ) {
            chosen_op = (FunctionalRef)compare_result_.unwrap().ast();
            Type compare_type = compare_result_.unwrap().type().unwrap();
            application_result = TypesUtil.applicationType(subtypeChecker, compare_type, args, downwardConstraint);
        }
        else {
            // Check both = and IN operators
            // we first want to do <: generator test.
            // If both are sat, we use =, if only gen_subtype_c is sat, we use IN
            ConstraintFormula gen_subtype_c =
                subtypeChecker.subtype(match_type, Types.makeGeneratorType(NodeFactory.make_InferenceVarType(NodeUtil.getSpan(clause))));
            ConstraintFormula gen_subtype_p =
                subtypeChecker.subtype(param_type, Types.makeGeneratorType(NodeFactory.make_InferenceVarType(NodeUtil.getSpan(clause))));

            if( gen_subtype_c.isSatisfiable() && !gen_subtype_p.isSatisfiable() ) {
                // Implicit IN
                chosen_op = (FunctionalRef)in_result.ast();
                Type in_type = in_result.type().unwrap();
                application_result = TypesUtil.applicationType(subtypeChecker, in_type, args, downwardConstraint);
            }
            else {
                // Implicit =
                chosen_op = (FunctionalRef)equals_result.ast();
                Type equals_type = equals_result.type().unwrap();
                application_result = TypesUtil.applicationType(subtypeChecker, equals_type, args, downwardConstraint);
            }
        }

        if( application_result.isNone() ) {
            // error
            String err = "No overloading of the operator " + chosen_op + " could be found for arguments of type " +
            param_type + " (Param Type)  and " + match_type + " (Match Type).";
            TypeCheckerResult e_r = new TypeCheckerResult(clause, TypeError.make(err, clause));
            return Pair.<Type,TypeCheckerResult>make(block_type, TypeCheckerResult.compose(clause, subtypeChecker, e_r, match_result, block_result));
        }
        else {
            CaseClause new_node = NodeFactory.makeCaseClause(NodeUtil.getSpan(clause),
                                                             (Expr)match_result.ast(),
                                                             (Block)block_result.ast(),
                                                             Option.<FunctionalRef>some(chosen_op));
            TypeCheckerResult app_result = new TypeCheckerResult(new_node, application_result.unwrap().second());
            Type app_type = application_result.unwrap().first();
            // We still must ensure the type of the application is a Boolean
            TypeCheckerResult bool_result = checkSubtype(app_type, Types.BOOLEAN, new_node,
                    "Result of application of " + chosen_op + " to param and match expression must have type boolean, but had type " + app_type + ".");
            return Pair.make(block_type, TypeCheckerResult.compose(new_node, subtypeChecker, bool_result, app_result, match_result, block_result));
        }
    }
    /**
         * pointInference pass
     * Typecheck the clause AND return the type of the right-hand side.
     */
    private Pair<Type, TypeCheckerResult> for_CaseClauseGetType(CaseClause clause, Option<TypeCheckerResult> param_result_) {
            // after inference, the case clause had better have the op field set
            if( clause.getOp().isNone() )
                return bug("All case clauses should be rewritten to reflect the chosen compare op.");

            FunctionalRef op = clause.getOp().unwrap();

        TypeCheckerResult match_result = recur(clause.getMatchClause());
        TypeCheckerResult block_result = recur(clause.getBody());

        // make sure subexpressions were well-typed
        if( !match_result.isSuccessful() || !block_result.isSuccessful() )
            return Pair.<Type,TypeCheckerResult>make(Types.BOTTOM, TypeCheckerResult.compose(clause, subtypeChecker, match_result, block_result));

        Type match_type = match_result.type().unwrap();
        Type block_type = block_result.type().unwrap();
        Type param_type = param_result_.unwrap().type().unwrap();

        if( isPostInference(op) ) {
            // Our operator is an overloading, so we should find the statically most applicable one and rewrite
            Type arg_type = NodeFactory.makeTupleType(NodeUtil.getSpan(clause),
                                                                  Useful.list(param_type, match_type));
            TypeCheckerResult app_result_1 =
                            findStaticallyMostApplicableFn(destructOpOverLoading(op.getOverloadings().unwrap()),
                                                           arg_type, op, op.getOriginalName());

            if( app_result_1.isSuccessful() ) {
                Type arrow_type = app_result_1.type().unwrap();
                Option<Pair<Type, ConstraintFormula>> app_result_2 =
                    TypesUtil.applicationType(subtypeChecker, arrow_type, new ArgList(param_type, match_type), downwardConstraint);

                if( app_result_2.isSome() ) {
                    CaseClause new_node = NodeFactory.makeCaseClause(NodeUtil.getSpan(clause),
                                                                             (Expr)match_result.ast(),
                                                                             (Block)block_result.ast(),
                                                                             Option.<FunctionalRef>some((FunctionalRef)app_result_1.ast()));
                    TypeCheckerResult app_result_3 = new TypeCheckerResult(new_node, app_result_2.unwrap().second());
                    Type app_type = app_result_2.unwrap().first();
                    // We still must ensure the type of the application is a Boolean
                    TypeCheckerResult bool_result = checkSubtype(app_type, Types.BOOLEAN, new_node,
                                                                                     "Result of application of " + op + " to param and match expression must have type boolean, but had type " + app_type + ".");
                    return Pair.make(block_type, TypeCheckerResult.compose(new_node, subtypeChecker, bool_result, app_result_3, match_result, block_result));
                }
                else {
                    // should be impossible, unless applicationType and findStaticallyMostApplicable don't agree...
                    return bug("applicationType and findStaticallyMostApplicable do not agree to function applicability. " + clause);
                }
            }
            else {
                return Pair.make(block_type, TypeCheckerResult.compose(clause, subtypeChecker, app_result_1, match_result, block_result, param_result_.unwrap()));
            }
        }
        else {
            // no overloading, so just do the normal thing
                    TypeCheckerResult op_result = recur(op);
            if( !op_result.isSuccessful() ) return Pair.make(block_type, TypeCheckerResult.compose(clause, subtypeChecker, op_result));
            Option<Pair<Type, ConstraintFormula>> app_result_1 =
                TypesUtil.applicationType(subtypeChecker, op_result.type().unwrap(), new ArgList(param_type, match_type), downwardConstraint);
            if( app_result_1.isSome() ) {
                CaseClause new_node = NodeFactory.makeCaseClause(NodeUtil.getSpan(clause),
                                                                     (Expr)match_result.ast(),
                                                                     (Block)block_result.ast(),
                                                                     Option.<FunctionalRef>some((FunctionalRef)op_result.ast()));
                TypeCheckerResult app_result_2 = new TypeCheckerResult(new_node, app_result_1.unwrap().second());
                Type app_type = app_result_1.unwrap().first();
                // We still must ensure the type of the application is a Boolean
                TypeCheckerResult bool_result = checkSubtype(app_type, Types.BOOLEAN, new_node,
                                                                             "Result of application of " + op + " to param and match expression must have type boolean, but had type " + app_type + ".");
                return Pair.make(block_type, TypeCheckerResult.compose(new_node, subtypeChecker, bool_result, app_result_2, match_result, block_result));
            }
            else {
                // error
                            String err = "No overloading of the operator " + op + " could be found for arguments of type " +
                param_type + " (Param Type)  and " + match_type + " (Match Type).";
                TypeCheckerResult e_r = new TypeCheckerResult(clause, TypeError.make(err, clause));
                return Pair.<Type,TypeCheckerResult>make(block_type, TypeCheckerResult.compose(clause, subtypeChecker, e_r, match_result, block_result));
            }
        }
    }


    @Override
    public TypeCheckerResult forCatch(Catch that) {
        // We have to pass the name down so it can be bound to each exn type in turn
        Id bound_name = that.getName();
        List<TypeCheckerResult> clause_results =
            recurOnCatchClausesWithIdToBind(that.getClauses(),bound_name);
        // Gather all the types of the catch clauses
        List<Type> clause_types = new ArrayList<Type>(clause_results.size());
        for( TypeCheckerResult r : clause_results ) {
            if( r.type().isSome() )
                clause_types.add(r.type().unwrap());
        }
        // resulting type is the join of those types
        Type result_type = subtypeChecker.join(clause_types);

        Catch new_node = NodeFactory.makeCatch(NodeUtil.getSpan(that),
                that.getName(),
                (List<CatchClause>)TypeCheckerResult.astFromResults(clause_results));

        return TypeCheckerResult.compose(new_node, result_type,
                subtypeChecker, clause_results).addNodeTypeEnvEntry(new_node, typeEnv);
    }

    /**
     * Given the CatchClause and an Id, the Id will be bound to the exception type that the catch
     * clause declares to catch, and then its body will be type-checked.
     */
    private TypeCheckerResult forCatchClauseWithIdToBind(CatchClause that,
            Id id_to_bind) {
        TypeCheckerResult match_result = that.getMatchType().accept(this);
        // type must be an exception
        TypeCheckerResult is_exn_result = checkSubtype(that.getMatchType(), Types.EXCEPTION, that.getMatchType(),
                "Catch clauses must catch sub-types of Exception, but " + that.getMatchType() + " is not.");

        // bind id and check the body
        LValue lval = NodeFactory.makeLValue(id_to_bind, that.getMatchType());
        TypeChecker extend_tc = this.extend(Collections.singletonList(lval));
        TypeCheckerResult body_result = that.getBody().accept(extend_tc);

        // result has body type
        Option<Type> result_type = body_result.type();

        CatchClause new_node = NodeFactory.makeCatchClause(NodeUtil.getSpan(that),
                (BaseType)match_result.ast(),
                (Block)body_result.ast());

        return TypeCheckerResult.compose(new_node, result_type, subtypeChecker, match_result, is_exn_result, body_result);
    }

    @Override
    public TypeCheckerResult forChainExpr(ChainExpr that) {
        TypeCheckerResult first_result = that.getFirst().accept(this);
        List<TypeCheckerResult> bool_exprs = new ArrayList<TypeCheckerResult>(that.getLinks().size());
        List<TypeCheckerResult> link_result = new ArrayList<TypeCheckerResult>(that.getLinks().size());
        List<TypeCheckerResult> temps_result = new ArrayList<TypeCheckerResult>(that.getLinks().size());

        Expr prev = that.getFirst();

        for(Link link : that.getLinks()) {
            FunctionalRef op = link.getOp();
            Expr next = link.getExpr();

            link_result.add(link.accept(this));

            // Check a temporary binary op, to see if the result is <: Boolean
            OpExpr tempOpExpr = ExprFactory.makeOpExpr(FortressUtil.spanTwo(prev,next),
                                                                   op, prev, next);
            TypeCheckerResult temp_op_result = tempOpExpr.accept(this);
            temps_result.add(temp_op_result);

            if(temp_op_result.type().isSome()) {
                bool_exprs.add(this.checkSubtype(temp_op_result.type().unwrap(), Types.BOOLEAN, tempOpExpr));
            }
            prev = next;
        }

        ChainExpr new_node = ExprFactory.makeChainExpr(NodeUtil.getSpan(that),
                NodeUtil.isParenthesized(that),
                Option.<Type>some(Types.BOOLEAN),
                (Expr)first_result.ast(),
                (List<Link>)TypeCheckerResult.astFromResults(link_result));

        return TypeCheckerResult.compose(new_node, Types.BOOLEAN, subtypeChecker, first_result,
                TypeCheckerResult.compose(new_node, subtypeChecker, link_result),
                TypeCheckerResult.compose(new_node, subtypeChecker, bool_exprs),
                TypeCheckerResult.compose(new_node, subtypeChecker, temps_result));
    }

    @Override
    public TypeCheckerResult forCharLiteralExpr(CharLiteralExpr that) {
        CharLiteralExpr new_node = ExprFactory.makeCharLiteralExpr(NodeUtil.getSpan(that),
                                                                           NodeUtil.isParenthesized(that),
                                                                           Option.<Type>some(Types.CHAR),
                                                                           that.getText(),
                                                                           that.getCharVal());
        return new TypeCheckerResult(new_node, Types.CHAR);
    }

    @Override
    public TypeCheckerResult forComponentOnly(Component that,
                                                  TypeCheckerResult info,
                                                  TypeCheckerResult name_result,
                                                  List<TypeCheckerResult> imports_result,
                                                  List<TypeCheckerResult> decls_result,
                                                  List<TypeCheckerResult> exports_result) {
        Component new_comp =
                    NodeFactory.makeComponent(NodeUtil.getSpan(that),
                                              (APIName)name_result.ast(),
                                              (List<Import>)TypeCheckerResult.astFromResults(imports_result),
                                              (List<Decl>)TypeCheckerResult.astFromResults(decls_result),
                                              that.is_native(),
                                              (List<APIName>)TypeCheckerResult.astFromResults(exports_result));

        return TypeCheckerResult.compose(new_comp,
                subtypeChecker,
                name_result,
                TypeCheckerResult.compose(new_comp, subtypeChecker, imports_result),
                TypeCheckerResult.compose(new_comp, subtypeChecker, exports_result),
                TypeCheckerResult.compose(new_comp, subtypeChecker, decls_result));
    }

    @Override
    public TypeCheckerResult forContractOnly(Contract that,
                                                 TypeCheckerResult info,
            Option<List<TypeCheckerResult>> requires_result,
            Option<List<TypeCheckerResult>> ensures_result,
            Option<List<TypeCheckerResult>> invariants_result) {
        TypeCheckerResult result = new TypeCheckerResult(that);

        // Check that each 'requires' expression is Boolean
        if (requires_result.isSome()) {
            for (TypeCheckerResult r : requires_result.unwrap()) {
                if (r.type().isNone()) continue;
                Type exprType = r.type().unwrap();
                result = TypeCheckerResult.compose(
                        that,
                        subtypeChecker,
                        result, checkSubtype(exprType,
                                Types.BOOLEAN,
                                r.ast(),
                                errorMsg("Attempt to use expression of type ", exprType,
                                        " in a 'requires' clause, instead of ",Types.BOOLEAN)));
            }
        }

        Contract new_node = NodeFactory.makeContract(NodeUtil.getSpan(that),
                (Option<List<Expr>>)TypeCheckerResult.astFromResults(requires_result),
                (Option<List<EnsuresClause>>)TypeCheckerResult.astFromResults(ensures_result),
                (Option<List<Expr>>)TypeCheckerResult.astFromResults(invariants_result));

        return TypeCheckerResult.compose(new_node,
                subtypeChecker,
                TypeCheckerResult.compose(new_node, subtypeChecker, requires_result),
                TypeCheckerResult.compose(new_node, subtypeChecker, ensures_result),
                TypeCheckerResult.compose(new_node, subtypeChecker, invariants_result), result);
    }

    public TypeCheckerResult forBlock(Block that) {
            if ( that.isAtomicBlock() )
                return forAtomic(ExprFactory.makeBlock(NodeUtil.getSpan(that), NodeUtil.isParenthesized(that),
                                                       NodeUtil.getExprType(that), that.getLoc(),
                                                       false, that.isWithinDo(), that.getExprs()),
                                                 errorMsg("A 'spawn' expression must not occur inside",
                                                          "an 'atomic' do block."));

            Option<TypeCheckerResult> loc_result_ = this.recurOnOptionOfExpr(that.getLoc());
            TypeCheckerResult loc_result = loc_result_.isNone() ? new TypeCheckerResult(that) :
                loc_result_.unwrap();

            TypeCheckerResult region_result = new TypeCheckerResult(that);
            if (loc_result_.isSome() && loc_result_.unwrap().type().isSome()) {
                Type locType = loc_result_.unwrap().type().unwrap();
                region_result = checkSubtype(locType,
                                             Types.REGION,
                                             that.getLoc().unwrap(),
                                             errorMsg("Location of 'do' block must ",
                                                      "have type Region: ", locType));
            }
            List<TypeCheckerResult> exprs_result = this.recurOnListOfExpr(that.getExprs());
            // Type is type of last expression or void if none.
            Option<Type> result_type;
            List<Expr> es;
            List<TypeCheckerResult> body_void;
            if ( exprs_result.isEmpty() ) {
                result_type = Option.<Type>some(Types.VOID);
                es = Collections.<Expr>emptyList();
                body_void = Collections.<TypeCheckerResult>emptyList();
            } else {
                result_type = IterUtil.last(exprs_result).type();
                es = (List<Expr>)TypeCheckerResult.astFromResults(exprs_result);
                body_void = allVoidButLast(exprs_result,that.getExprs());
            }
            Block new_node = ExprFactory.makeBlock(NodeUtil.getSpan(that),
                                                   NodeUtil.isParenthesized(that),
                                                   result_type,
                                                   (Option<Expr>)TypeCheckerResult.astFromResult(loc_result_),
                                                   that.isAtomicBlock(), that.isWithinDo(),
                                                   (List<Expr>)TypeCheckerResult.astFromResults(exprs_result));
            return TypeCheckerResult.compose(new_node,
                                             result_type,
                                             subtypeChecker,
                                             TypeCheckerResult.compose(new_node, subtypeChecker, body_void),
                                             loc_result,
                                             region_result,
                                             TypeCheckerResult.compose(new_node, subtypeChecker, exprs_result));
    }

    @Override
    public TypeCheckerResult forDoOnly(Do that, TypeCheckerResult exprType_result, List<TypeCheckerResult> fronts_result) {
        // Get union of all clauses' types
        List<Type> frontTypes = new ArrayList<Type>();
        for (TypeCheckerResult frontResult : fronts_result) {
            if (frontResult.type().isSome()) {
                frontTypes.add(frontResult.type().unwrap());
            }
        }

        Type result_type = subtypeChecker.join(frontTypes);
        Do new_node = ExprFactory.makeDo(NodeUtil.getSpan(that),
                NodeUtil.isParenthesized(that),
                some(result_type),
                (List<Block>)TypeCheckerResult.astFromResults(fronts_result));

        return TypeCheckerResult.compose(new_node, result_type, subtypeChecker, fronts_result);
    }

    @Override
    public TypeCheckerResult forEnclosingFixity(EnclosingFixity that) {
        return new TypeCheckerResult(that);
    }

    @Override
    public TypeCheckerResult forExit(Exit that) {
        assert (that.getTarget().isSome()); // Filled in by disambiguator
        Id labelName = that.getTarget().unwrap();
        Option<BindingLookup> b = typeEnv.binding(labelName);
        assert (that.getReturnExpr().isSome()); // Filled in by disambiguator
        if (b.isNone()) {
            TypeCheckerResult withResult = that.getReturnExpr().unwrap().accept(this);
            return TypeCheckerResult.compose(
                    that,
                    Types.BOTTOM,
                    subtypeChecker,
                    new TypeCheckerResult(that,
                            TypeError.make(errorMsg("Could not find 'label' expression with name: ",
                                    labelName),
                                    labelName)), withResult);
        }
        Type targetType = b.unwrap().getType().unwrap(null);
        if (!(targetType instanceof LabelType)) {
            TypeCheckerResult withResult = that.getReturnExpr().unwrap().accept(this);
            return TypeCheckerResult.compose(
                    that,
                    Types.BOTTOM,
                    subtypeChecker,
                    new TypeCheckerResult(that,
                            TypeError.make(errorMsg("Target of 'exit' expression is not a label name: ",
                                    labelName),
                                    labelName)), withResult);
        }

        // Append the 'with' type to the list for this label
        TypeCheckerResult withResult = that.getReturnExpr().unwrap().accept(this);
        if (withResult.type().isNone()) {
            labelExitTypes.put(labelName, Option.<Set<Type>>none());
        } else {
            assert (labelExitTypes.get(labelName).isSome());
            labelExitTypes.get(labelName).unwrap().add(withResult.type().unwrap());
        }

        Exit new_node = ExprFactory.makeExit(NodeUtil.getSpan(that),
                NodeUtil.isParenthesized(that),
                Option.<Type>some(Types.BOTTOM),
                that.getTarget(),
                some((Expr)withResult.ast()));

        return TypeCheckerResult.compose(new_node, Types.BOTTOM, subtypeChecker, withResult);
    }

    // Works for extremum expressions
    // case most < of ... end
    private TypeCheckerResult forExtremumOnly(CaseExpr that, TypeCheckerResult compare_result,
            List<Triple<CaseClause, TypeCheckerResult, TypeCheckerResult>> clauses_result) {

        Iterable<Type> candidate_types =
            IterUtil.map(IterUtil.tripleSeconds(clauses_result), new Lambda<TypeCheckerResult,Type>(){
                public Type value(TypeCheckerResult arg0) { return arg0.type().unwrap(); }});

        Iterable<Type> rhs_types =
            IterUtil.map(IterUtil.tripleThirds(clauses_result), new Lambda<TypeCheckerResult,Type>(){
                public Type value(TypeCheckerResult arg0) { return arg0.type().unwrap(); }});

        Type union_of_candidate_types = this.subtypeChecker.join(candidate_types);
        Type total_op_order = Types.makeTotalOperatorOrder(union_of_candidate_types,
                                                                   (Op)that.getCompare().unwrap().getOriginalName());

        TypeCheckerResult total_result = checkSubtype(union_of_candidate_types, total_op_order, that,
                "In an extremum expression, the union of all candidate types must be a subtype of " +
                "TotalOperatorOrder[union,<,<=,>=,>,"+that.getCompare().unwrap().getOriginalName()+"] but it is not. " +
                "The union is " + union_of_candidate_types);

        Type result_type = subtypeChecker.join(rhs_types);
        CaseExpr new_node = ExprFactory.makeCaseExpr(NodeUtil.getSpan(that),
                NodeUtil.isParenthesized(that),
                some(result_type),
                that.getParam(), // implicitly NONE
                that.getCompare(),
                that.getEqualsOp(),
                that.getInOp(),
                CollectUtil.makeList(IterUtil.tripleFirsts(clauses_result)),
                that.getElseClause());

        return TypeCheckerResult.compose(new_node, result_type, subtypeChecker, total_result, compare_result,
                TypeCheckerResult.compose(new_node, subtypeChecker, CollectUtil.makeList(IterUtil.tripleSeconds(clauses_result))),
                TypeCheckerResult.compose(new_node, subtypeChecker, CollectUtil.makeList(IterUtil.tripleThirds(clauses_result))));
    }

    @Override
    public TypeCheckerResult forFieldRefOnly(FieldRef that, TypeCheckerResult exprType_result,
            TypeCheckerResult obj_result, TypeCheckerResult field_result) {

        // We need the type of the receiver
        if( obj_result.type().isNone() ) {
            return TypeCheckerResult.compose(that, subtypeChecker, obj_result);
        }
        //check whether receiver can have fields
        Type recvr_type=obj_result.type().unwrap();
        TypeCheckerResult result;
        Option<Type> result_type;

        List<TraitType> trait_types = traitTypesCallable(recvr_type);

        if( !trait_types.isEmpty() ) {
            Option<Type> f_type = this.findFieldInTraitHierarchy(trait_types, that);
            if( f_type.isSome() ) {
                result = new TypeCheckerResult(that);
                result_type = f_type;
            }
            else {
                String no_field = "Field " + that.getField() + " could not be found in type" +
                recvr_type + ".";
                result = new TypeCheckerResult(that, TypeError.make(no_field, that));
                result_type = Option.none();
            }
        }
        else {
            String not_trait = "Receiver of field expression must be a trait or object, but "
                + recvr_type + " is neither.";
            result = new TypeCheckerResult(that, TypeError.make(not_trait, that));
            result_type = Option.none();
        }

        FieldRef new_node = ExprFactory.makeFieldRef(NodeUtil.getSpan(that),
                NodeUtil.isParenthesized(that),
                result_type,
                (Expr)obj_result.ast(),
                that.getField());

        return TypeCheckerResult.compose(new_node, result_type, this.subtypeChecker, obj_result, result);
    }

    @Override
    public TypeCheckerResult forFloatLiteralExpr(FloatLiteralExpr that) {
        return new TypeCheckerResult(that, Types.FLOAT_LITERAL);
    }

    @Override
    public TypeCheckerResult forFnDecl(FnDecl that) {
                if (NodeUtil.getBody(that).isNone())
                    return super.forFnDecl(that);

        TypeChecker newChecker = this.extend(NodeUtil.getStaticParams(that), NodeUtil.getParams(that), NodeUtil.getWhereClause(that));

        TypeCheckerResult result = new TypeCheckerResult(that);
        TypeCheckerResult contractResult;
        Option<Contract> contract;
        if ( NodeUtil.getContract(that).isSome() ) {
            contractResult = NodeUtil.getContract(that).unwrap().accept(newChecker);
            contract = Option.some((Contract)contractResult.ast());
        } else {
            contractResult = result;
            contract = Option.<Contract>none();
        }
        TypeCheckerResult bodyResult = NodeUtil.getBody(that).unwrap().accept(newChecker);

        if( !contractResult.isSuccessful() || !bodyResult.isSuccessful() ) {
            return TypeCheckerResult.compose(that, subtypeChecker, result, bodyResult, contractResult);
        }



        Option<Type> returnType = NodeUtil.getReturnType(that);
        if (bodyResult.type().isSome()) {
            Type bodyType = bodyResult.type().unwrap();
            if (returnType.isNone()) {
                returnType = wrap(bodyType);
            }

//                         System.err.println("Location: " + NodeUtil.getSpan(that));
//                         System.err.println("body type: " + bodyType.getClass() + ":" + bodyType);
//                         if (bodyType instanceof TraitType) {
//                             System.err.println("name: " + ((TraitType)bodyType).getName());
//                             System.err.println("args:" + ((TraitType)bodyType).getArgs());
//                         }
//                         System.err.println("return type: " + returnType.unwrap().getClass() + ":" + returnType.unwrap());
//                         if (returnType.unwrap() instanceof TraitType) {
//                             System.err.println("name: " + ((TraitType)returnType.unwrap()).getName());
//                             System.err.println("args:" + ((TraitType)returnType.unwrap()).getArgs());
//                         }
//                         System.err.println("equal? " + bodyType.equals(returnType.unwrap()));
            result = newChecker.checkSubtype(normalize(bodyType),
                                             normalize(returnType.unwrap()),
                                             that,
                                             errorMsg("Function body has type ", normalize(bodyType), ", but ",
                                                      "declared return type is ", normalize(returnType.unwrap())));
        }

        FnDecl new_node = NodeFactory.makeFnDecl(NodeUtil.getSpan(that),
                                                         NodeUtil.getMods(that),
                                                         NodeUtil.getName(that),
                                                         NodeUtil.getStaticParams(that),
                                                         NodeUtil.getParams(that),
                                                         returnType,
                                                         NodeUtil.getThrowsClause(that),
                                                         NodeUtil.getWhereClause(that),
                                                         contract,
                                                         Option.<Expr>some((Expr)bodyResult.ast()));
        return TypeCheckerResult.compose(new_node, subtypeChecker, contractResult,
                bodyResult, result)
                .addNodeTypeEnvEntry(new_node, typeEnv)
                .removeStaticParamsFromScope(NodeUtil.getStaticParams(that));
    }

    @Override
    public TypeCheckerResult forFnExpr(FnExpr that) {
        // Fn expressions have arrow type. They cannot have static arguments.
        // They cannot have where clauses.

        Option<TypeCheckerResult> returnType_result = recurOnOptionOfType(NodeUtil.getReturnType(that));

        List<TypeCheckerResult> all_results = new ArrayList<TypeCheckerResult>();

        Option<List<TypeCheckerResult>> throwsClause_result = recurOnOptionOfListOfBaseType(NodeUtil.getThrowsClause(that));


        List<TypeCheckerResult> params_result = recurOnListOfParam(NodeUtil.getParams(that));
        // Grab bindings and introduce them. For the time-being, they must have types.
        TypeChecker extended_checker = this;
        for( Param p : NodeUtil.getParams(that) ) {
            extended_checker = extended_checker.extend(p);
        }
        TypeCheckerResult body_result = that.getBody().accept(extended_checker);
        // Get all results together
        all_results.addAll(params_result);
        all_results.add(body_result);
        //get domain type
        List<Type> dlist = new ArrayList<Type>();
        Boolean varargs=false;
        for(Param p: NodeUtil.getParams(that)){
                    if( ! NodeUtil.isVarargsParam(p) ){
                        if(p.getIdType().isSome()){
                            dlist.add(p.getIdType().unwrap());
                        }
                        else{
                            NI.nyi();
                        }
                    } else {
                        dlist.add(p.getVarargsType().unwrap());
                        varargs=true;
                    }
        }
        TupleType domain;
        if(varargs){
            Type var = dlist.remove(dlist.size()-1);
            domain = NodeFactory.makeTupleType(NodeUtil.getSpan(that), false, dlist,
                                                           Option.<Type>some(var),
                                                           Collections.<KeywordType>emptyList());
        }
        else{
            domain = NodeFactory.makeTupleType(NodeUtil.getSpan(that), dlist);
        }

        if( returnType_result.isSome() )
            all_results.add(returnType_result.unwrap());
        if( throwsClause_result.isSome() )
            all_results.addAll(throwsClause_result.unwrap());

        // If return type is given, we check that it is a supertype of the inferred super-type
        // and we use it, otherwise the return type is what we infer.
        Type return_type;
        if( body_result.type().isNone() ) {
            // We've got errors in the body
            return_type = Types.BOTTOM;
        }
        else if( NodeUtil.getReturnType(that).isSome() ) {
            return_type = NodeUtil.getReturnType(that).unwrap();
            TypeCheckerResult subtype_result =
                this.checkSubtype(body_result.type().unwrap(), return_type, that.getBody(),
                        "Type of body of Fn expression must be a subtype of declared return type ("+
                        return_type +") but is " + body_result.type().unwrap() +".");
            all_results.add(subtype_result);
        }
        else {
            return_type = body_result.type().unwrap();
        }

        // All throws types must be a subtype of exception
        if( NodeUtil.getThrowsClause(that).isSome() ) {
            for( BaseType exn : NodeUtil.getThrowsClause(that).unwrap() ) {
                all_results.add(this.checkSubtype(exn, Types.CHECKED_EXCEPTION, that,
                        "Types in throws clause must be subtypes of CheckedException, but "+
                        exn + " is not."));
            }
        }

        ArrowType arr = NodeFactory.makeArrowType(FortressUtil.spanTwo(domain, return_type),
                domain, return_type);
        FnExpr new_node = ExprFactory.makeFnExpr(NodeUtil.getSpan(that),
                NodeUtil.isParenthesized(that),
                NodeUtil.getExprType(that),
                NodeUtil.getName(that),
                NodeUtil.getStaticParams(that),
                NodeUtil.getParams(that),
                (Option<Type>)TypeCheckerResult.astFromResult(returnType_result),
                NodeUtil.getWhereClause(that),
                (Option<List<BaseType>>)TypeCheckerResult.astFromResults(throwsClause_result),
                (Expr)body_result.ast() );

        return TypeCheckerResult.compose(new_node, arr,
                this.subtypeChecker, all_results).addNodeTypeEnvEntry(new_node, typeEnv);
    }

    @Override
    public TypeCheckerResult forFnRefOnly(final FnRef that, TypeCheckerResult exprType_result,
                                              List<TypeCheckerResult> staticArgs_result,
                                              TypeCheckerResult originalName_result,
                                              List<TypeCheckerResult> fns_result,
                                              Option<List<TypeCheckerResult>> overloadings_result,
                                              Option<TypeCheckerResult> type_result) {

        // Could we give a type to each of our fns?
        for( TypeCheckerResult r : fns_result ) {
            if( !r.isSuccessful() )
                return TypeCheckerResult.compose(that, subtypeChecker, fns_result);
        }

        // Gather types of all overloadings
        List<Type> overloaded_types = CollectUtil.makeList(IterUtil.map(fns_result, new Lambda<TypeCheckerResult, Type>() {
            public Type value(TypeCheckerResult arg0) { return arg0.type().unwrap(); }}));

        Node new_node;
        Option<Type> type;
        ConstraintFormula constraints=ConstraintFormula.TRUE;

        // if no static args are provided, and we have several overloadings, we
        // will create a FnRef with the overloadings field set
        if( that.getStaticArgs().isEmpty()  && TypesUtil.overloadingRequiresStaticArgs(overloaded_types) ) {
            // if there is an overloading that requires static args, and we don't have any, we'll
            // create a _FnInstantitedOverloading
            List<FunctionalRef> fn_overloadings = new ArrayList<FunctionalRef>();
            List<Type> arrow_types = new ArrayList<Type>();
            ConstraintFormula accumulated_constraints = ConstraintFormula.TRUE;
            for( Type overloaded_type : overloaded_types ) {
                for( Type overloading : TypesUtil.conjuncts(overloaded_type) ) {
                    // If type needs static args, create inference vars, and apply to the signature
                    Option<Pair<Pair<Type,ConstraintFormula>,List<StaticArg>>> new_type_and_args_ =
                        overloading.accept(new TypeAbstractVisitor<Option<Pair<Pair<Type,ConstraintFormula>,List<StaticArg>>>>() {
                            @Override
                            public Option<Pair<Pair<Type,ConstraintFormula>, List<StaticArg>>> forArrowType(
                                    ArrowType gen_arr_type) {
                                // If the arrow type is generic, it needs static args, so make up inference variables
                                List<StaticArg> new_args =
                                    TypesUtil.staticArgsFromTypes(NodeFactory.make_InferenceVarTypes(NodeUtil.getSpan(that), NodeUtil.getStaticParams(gen_arr_type).size()));
                                Option<Pair<Type,ConstraintFormula>> instantiated_type = TypesUtil.applyStaticArgsIfPossible(gen_arr_type, new_args, TypeChecker.this.subtypeChecker);

                                if( instantiated_type.isNone() )
                                    return none();
                                else
                                    return some(Pair.make(instantiated_type.unwrap(), new_args));
                            }

                            @Override
                            public Option<Pair<Pair<Type,ConstraintFormula>, List<StaticArg>>> forType(Type that) {
                                // any other sort of Type does not get rewritten, and has no args
                                return some(Pair.make(Pair.make(that, ConstraintFormula.TRUE), Collections.<StaticArg>emptyList()));
                            }
                        });

                    // For now, we don't consider overloadings that require inference of bools/nats/ints
                    if( new_type_and_args_.isNone() ) continue;
                    Type new_type = new_type_and_args_.unwrap().first().first();
                    List<StaticArg> new_args = new_type_and_args_.unwrap().second();
                    // create new FnRef for this application of static params
                    FnRef fn_ref = ExprFactory.makeFnRef(NodeUtil.getSpan(that),
                                                                             NodeUtil.isParenthesized(that),
                                                                             some(new_type),
                                                                             new_args,
                                                                             that.getLexicalDepth(),
                                                                             that.getOriginalName(),
                                                                             that.getNames(),
                                                                             that.getOverloadings(),
                                                                             Option.<Type>none());
                    fn_overloadings.add(ExprFactory.make_RewriteFnRefOverloading(NodeUtil.getSpan(that), fn_ref, new_type));
                    arrow_types.add(new_type);
                    accumulated_constraints=accumulated_constraints.and(new_type_and_args_.unwrap().first().second(),this.subtypeChecker.new SubtypeHistory());
                }
            }

            type = (arrow_types.isEmpty()) ?
                    Option.<Type>none() :
                        Option.<Type>some(NodeFactory.makeIntersectionType(NodeFactory.makeSetSpan("impossible", arrow_types), arrow_types));
                    constraints = accumulated_constraints;
                    new_node = ExprFactory.makeFnRef(NodeUtil.getSpan(that),
                                                                         NodeUtil.isParenthesized(that),
                                                                         type,
                                                                         that.getStaticArgs(),
                                                                         that.getLexicalDepth(),
                                                                         that.getOriginalName(),
                                                                         that.getNames(),
                                                                         Option.<List<FunctionalRef>>some(fn_overloadings),
                                                                         Option.<Type>none());
        }
        else {
            // otherwise, we just operate according to the normal procedure, apply args or none were necessary
            List<Type> arrow_types = new ArrayList<Type>();
            ConstraintFormula accumulated_constraints=ConstraintFormula.TRUE;
            for( Type ty : overloaded_types ) {
                Option<Pair<Type,ConstraintFormula>> instantiated_type = TypesUtil.applyStaticArgsIfPossible(ty, that.getStaticArgs(), this.subtypeChecker);
                if( instantiated_type.isSome() ){
                    arrow_types.add(instantiated_type.unwrap().first());
                    accumulated_constraints=accumulated_constraints.and(instantiated_type.unwrap().second(),this.subtypeChecker.new SubtypeHistory());
                }
            }
            if (arrow_types.isEmpty()) {
                type = Option.<Type>none();
            } else if (arrow_types.size() == 1) { // special case to allow for simpler types
                type = Option.<Type>some(arrow_types.get(0));
            } else {
                type = Option.<Type>some(NodeFactory.makeIntersectionType(NodeFactory.makeSetSpan("impossible", arrow_types), arrow_types));
            }

            type = (arrow_types.isEmpty()) ?
                    Option.<Type>none() :
                        Option.<Type>some(NodeFactory.makeIntersectionType(NodeFactory.makeSetSpan("impossible", arrow_types), arrow_types));
                    constraints = accumulated_constraints;
                    new_node = ExprFactory.makeFnRef(NodeUtil.getSpan(that),
                                                                         NodeUtil.isParenthesized(that),
                                                                         type,
                                                                         that.getStaticArgs(),
                                                                         that.getLexicalDepth(),
                                                                         that.getOriginalName(),
                                                                         that.getNames(),
                                                                         Option.<List<FunctionalRef>>none(),
                                                                         Option.<Type>none());
        }

        return TypeCheckerResult.compose(new_node, type, subtypeChecker,
                TypeCheckerResult.compose(new_node, subtypeChecker, fns_result),
                TypeCheckerResult.compose(new_node, subtypeChecker, staticArgs_result),
                new TypeCheckerResult(new_node, constraints));
    }

    @Override
    public TypeCheckerResult forFor(For that) {
        Pair<List<TypeCheckerResult>,List<LValue>> pair = recurOnListsOfGeneratorClauseBindings(that.getGens());
        Option<TypeCheckerResult> type_result = recurOnOptionOfType(NodeUtil.getExprType(that));
        TypeChecker extend = this.extend(pair.second());
        TypeCheckerResult body_result = that.getBody().accept(extend);
        return forForOnly(that, type_result, pair.first(), body_result);
    }

    public TypeCheckerResult forForOnly(For that, Option<TypeCheckerResult> exprType_result, List<TypeCheckerResult> gens_result, TypeCheckerResult body_result) {

        if( body_result.type().isNone() ) {
            return TypeCheckerResult.compose(that, Types.VOID, subtypeChecker, body_result,
                    TypeCheckerResult.compose(that, Types.VOID, subtypeChecker, gens_result));
        }

        // Body must be a void type
        String err = "Body type of a for loop must have type VOID but has type " + body_result.type().unwrap();
        TypeCheckerResult body_void = this.checkSubtype(body_result.type().unwrap(), Types.VOID, that.getBody(), err);

        For for_ = ExprFactory.makeFor(NodeUtil.getSpan(that),
                NodeUtil.isParenthesized(that),
                Option.<Type>some(Types.VOID),
                (List<GeneratorClause>)TypeCheckerResult.astFromResults(gens_result),
                (Block)body_result.ast());

        TypeCheckerResult result = TypeCheckerResult.compose(for_, subtypeChecker, body_void, body_result,
                TypeCheckerResult.compose(for_, subtypeChecker, gens_result)).addNodeTypeEnvEntry(for_, typeEnv);

        return TypeCheckerResult.compose(for_, Types.VOID, subtypeChecker, result);
    }

    private Pair<TypeCheckerResult, List<LValue>> forGeneratorClauseGetBindings(GeneratorClause that,
            boolean mustBeCondition) {
        TypeCheckerResult init_result = that.getInit().accept(this);
        final Pair<TypeCheckerResult, List<LValue>> p = forGeneratorClauseOnlyGetBindings(that, init_result, mustBeCondition);

        if( postInference ) {
            Boolean ok = true;
            List<LValue> closed_binds = new ArrayList<LValue>();
            for(LValue b : p.second()){
                Pair<Boolean,Node> temp = TypesUtil.closeConstraints(b, subtypeChecker, p.first());
                closed_binds.add((LValue)temp.second());
                ok&=temp.first();
            }
            TypeCheckerResult successful = new TypeCheckerResult(that);
            if(!ok){
                String err = "Couldn't close binding.";
                successful = new TypeCheckerResult(that,TypeError.make(err,that));
            }
            return Pair.make(TypeCheckerResult.compose(that, this.subtypeChecker, p.first(), successful), closed_binds);
        }
        else {
            return p;
        }
    }

    private Pair<TypeCheckerResult, List<LValue>> forGeneratorClauseOnlyGetBindings(GeneratorClause that,
            TypeCheckerResult init_result, boolean mustBeCondition) {

        if( that.getBind().isEmpty()) {
            GeneratorClause new_node = NodeFactory.makeGeneratorClause(NodeUtil.getSpan(that),
                    that.getBind(),
                    (Expr)init_result.ast());


            // If bindings are empty, then init_result must be of type boolean, a filter, 13.14
                        TypeCheckerResult bool_result;

                        if (init_result.type().isNone()) {
                            String err = "Filter expressions in generator clauses must have type boolean, but " +
                                that.getInit() + " was not well typed.";
                            bool_result = new TypeCheckerResult(that.getInit(), TypeError.make(err, that.getInit()));
                        } else {
                            bool_result =
                this.checkSubtype(init_result.type().unwrap(), Types.BOOLEAN, that.getInit(),
                        "Filter expressions in generator clauses must have type " + Types.BOOLEAN + ", but " +
                        that.getInit() + " had type " + init_result.type().unwrap() + ".");
                        }
            return Pair.make(TypeCheckerResult.compose(new_node, subtypeChecker, init_result, bool_result),
                    Collections.<LValue>emptyList());
        }

        // Otherwise, we may actually have bindings!
        int bindings_count = that.getBind().size();

        List<LValue> result_bindings;
        Type lhstype;
        // Now create the bindings

        if( bindings_count == 1 ){
            // Just one binding
            lhstype = NodeFactory.make_InferenceVarType(NodeUtil.getSpan(that.getBind().get(0)));
            LValue lval = NodeFactory.makeLValue(that.getBind().get(0), lhstype);
            result_bindings = Collections.singletonList(lval);
        }
        else {
            // Because generator_type is almost certainly a _InferenceVar, we have to declare a new tuple
            // that is the size of the binding and declare one to be a sub-type of the other.
            List<Type> inference_vars = new ArrayList<Type>(bindings_count);
            for( int i = 0; i<bindings_count;i++ ) {
                inference_vars.add(NodeFactory.make_InferenceVarType(NodeUtil.getSpan(that.getBind().get(i))));
            }
            lhstype=Types.makeTuple(inference_vars);
            // Now just create the lvalues with the newly created inference variable type
            Iterator<Id> id_iter = that.getBind().iterator();
            result_bindings = new ArrayList<LValue>(bindings_count);
            for( Type inference_var : inference_vars ) {
                result_bindings.add(NodeFactory.makeLValue(id_iter.next(), inference_var));
            }
        }

        TypeCheckerResult this_result = TypeCheckerResult.compose(that, subtypeChecker, init_result);
        GeneratorClause new_node=that;
        if(init_result.type().isSome()){
            Type init_type = init_result.type().unwrap();
            String type_err_msg = "Init expression of generator must be a sub-type of " +
            (mustBeCondition ? "Condition" : "Generator") +
            " but is type " + init_result.type().unwrap() + ".";
            // Get the type of the Generator

            Pair<TypeCheckerResult, Type> generator_pair = mustBeCondition ? this.getConditionType(init_type, that.getInit(), type_err_msg) :
                this.getGeneratorType(init_type, that.getInit(), type_err_msg);

            Type generator_type = generator_pair.second();
            String tup_err_msg = "If more than one variable is bound in a generator, generator must have tuple type "+
            "but " + that.getInit() + " does not or has different number of arguments.";
            TypeCheckerResult subtype=this.checkSubtype(lhstype, generator_type, that.getInit(),tup_err_msg);
            TypeCheckerResult suptype=this.checkSubtype(generator_type, lhstype, that.getInit(),tup_err_msg);
            this_result = TypeCheckerResult.compose(that, subtypeChecker, suptype, subtype, generator_pair.first());
            new_node = NodeFactory.makeGeneratorClause(NodeUtil.getSpan(that),
                    that.getBind(),
                    (Expr)init_result.ast());
        }
        return Pair.make(TypeCheckerResult.compose(new_node, subtypeChecker, this_result, init_result), result_bindings);
    }

    @Override
    public TypeCheckerResult forId(Id name) {
        Option<APIName> apiName = name.getApiName();
        if (apiName.isSome()) {
            APIName api = apiName.unwrap();
            TypeEnv apiTypeEnv = returnTypeEnvForApi(api);

            Option<Type> type = apiTypeEnv.type(name);
            if (type.isSome()) {
                Type _type = type.unwrap();
                if (_type instanceof NamedType) { // Do we need to qualify?
                    NamedType _namedType = (NamedType)_type;

                    // Type was declared in that API, so it's not qualified;
                    // prepend it with the API.
                    if (_namedType.getName().getApiName().isNone()) {
                        _type = NodeFactory.makeNamedType(api, (NamedType) type.unwrap());
                    }
                }
                return new TypeCheckerResult(name, _type);
            } else {
                // Operators are never qualified in source code, so if 'name' is qualified and not
                // found, it must be a Id, not a Op.
                StaticError error = TypeError.make(errorMsg("Attempt to reference unbound variable: ", name),
                        name);
                return new TypeCheckerResult(name, error);
            }
        }
        Option<Type> type = typeEnv.type(name);
        if (type.isSome()) {
            Type _type = type.unwrap();
            if (_type instanceof LabelType) { // then name must be an Id
                return new TypeCheckerResult(name, makeLabelNameError((Id)name));
            } else {
                return new TypeCheckerResult(name, _type);
            }
        } else {
            StaticError error;
            error = TypeError.make(errorMsg("Variable '", name, "' not found."),
                    name);
            return new TypeCheckerResult(name, error);
        }
    }

    // This method not only typechecks an IfClause, but also returns the type of that clause's
    // body. We don't include this in the TypeCheckerResult because an IfClause is not an Expr
    // and we didn't want to confuse things by giving it a type.
    private Pair<TypeCheckerResult, Option<Type>> forIfClauseWithType(IfClause that) {
        // For generalized 'if' we must introduce new bindings.
        Pair<TypeCheckerResult, List<LValue>> result_and_binds =
            this.forGeneratorClauseGetBindings(that.getTestClause(), true);

        // Destruct result
        TypeCheckerResult test_result = result_and_binds.first();
        List<LValue> bindings = result_and_binds.second();

        // Check body with new bindings
        TypeChecker tc_with_new_bindings = this.extend(bindings);
        TypeCheckerResult body_result = that.getBody().accept(tc_with_new_bindings);
        //return forIfClauseOnly(that, test_result, body_result);

        Option<Type> result_type = body_result.type();
        IfClause new_node = NodeFactory.makeIfClause(NodeUtil.getSpan(that),
                (GeneratorClause)test_result.ast(),
                (Block)body_result.ast());

        TypeCheckerResult tcr = TypeCheckerResult.compose(new_node,
                subtypeChecker, test_result, body_result).addNodeTypeEnvEntry(new_node, typeEnv);

        return Pair.make(tcr, result_type);
    }

    @Override
    public TypeCheckerResult forIf(If that) {

        Option<TypeCheckerResult> elseClause_result = this.recurOnOptionOfBlock(that.getElseClause());
        List<Pair<TypeCheckerResult,Option<Type>>> clauses_result_ = new ArrayList<Pair<TypeCheckerResult,Option<Type>>>(that.getClauses().size());
        for( IfClause clause : that.getClauses() ) {
            clauses_result_.add(this.forIfClauseWithType(clause));
        }
        List<TypeCheckerResult> clauses_result = CollectUtil.makeList(IterUtil.pairFirsts(clauses_result_));
        List<Option<Type>> clause_types_ = CollectUtil.makeList(IterUtil.pairSeconds(clauses_result_));

        Type result_type;
        List<TypeCheckerResult> clauses_void;

        if (elseClause_result.isSome()) {
            List<Type> clause_types = new ArrayList<Type>(that.getClauses().size());
            TypeCheckerResult elseResult = elseClause_result.unwrap();

            // Get union of all clauses' types
            for (Option<Type> clause_type_ : clause_types_) {
                if (clause_type_.isSome()) {
                    clause_types.add(clause_type_.unwrap());
                }
            }
            if (elseResult.type().isSome()) {
                clause_types.add(elseResult.type().unwrap());
            }
            clauses_void = Collections.emptyList();
            result_type = subtypeChecker.join(clause_types);
        } else {
            // Check that each if/elif clause has void type
            clauses_void = new ArrayList<TypeCheckerResult>(that.getClauses().size());
            for (Option<Type> clause_type_ : clause_types_) {
                if ( clause_type_.isSome() ) {
                    Type clause_type = clause_type_.unwrap();
                    clauses_void.add(checkSubtype(clause_type, Types.VOID, that,
                            errorMsg("An 'if' clause without corresponding 'else' has type ",
                                    clause_type, " instead of type ()")));
                }
            }
            result_type = Types.VOID;
        }

        TypeCheckerResult elseClause_result_ = elseClause_result.isNone() ? new TypeCheckerResult(that) : elseClause_result.unwrap();

        If new_node = ExprFactory.makeIf(NodeUtil.getSpan(that),
                NodeUtil.isParenthesized(that),
                some(result_type),
                (List<IfClause>)TypeCheckerResult.astFromResults(clauses_result),
                (Option<Block>)TypeCheckerResult.astFromResult(elseClause_result));

        return TypeCheckerResult.compose(new_node, result_type, subtypeChecker,
                TypeCheckerResult.compose(new_node, subtypeChecker, clauses_result),
                TypeCheckerResult.compose(new_node, subtypeChecker, clauses_void),
                elseClause_result_);
    }

    @Override
    public TypeCheckerResult forImportStar(ImportStar that) {
        return new TypeCheckerResult(that);
    }

    @Override
    public TypeCheckerResult forInFixity(InFixity that) {
        return new TypeCheckerResult(that);
    }

    @Override
    public TypeCheckerResult forIntArgOnly(IntArg that,
                                               TypeCheckerResult info,
                                               TypeCheckerResult val_result) {
        return new TypeCheckerResult(that);
    }

    @Override
    public TypeCheckerResult forIntLiteralExpr(IntLiteralExpr that) {
        IntLiteralExpr new_node = ExprFactory.makeIntLiteralExpr(NodeUtil.getSpan(that),
                                                                         NodeUtil.isParenthesized(that),
                                                                         Option.<Type>some(Types.INT_LITERAL),
                                                                         that.getText(), that.getIntVal());
        return new TypeCheckerResult(new_node, Types.INT_LITERAL);
    }

    @Override
    public TypeCheckerResult forLabel(Label that) {

        // Make sure this label isn't already bound
        Option<BindingLookup> b = typeEnv.binding(that.getName());
        if (b.isSome()) {
            TypeCheckerResult bodyResult = that.getBody().accept(this);
            return TypeCheckerResult.compose(that,
                    subtypeChecker,
                    new TypeCheckerResult(that, TypeError.make(errorMsg("Cannot use an existing identifier ",
                            "for a 'label' expression: ",
                            that.getName()),
                            that)), bodyResult);
        }

        // Check for nested label of same name
        if (labelExitTypes.containsKey(that.getName())) {
            TypeCheckerResult bodyResult = that.getBody().accept(this);
            return TypeCheckerResult.compose(that,
                    subtypeChecker,
                    new TypeCheckerResult(that, TypeError.make(errorMsg("Name of 'label' expression ",
                            "already in scope: ", that.getName()),
                            that)), bodyResult);
        }

        // Initialize the set of exit types
        labelExitTypes.put(that.getName(), some((Set<Type>)new HashSet<Type>()));

        // Extend the checker with this label name in the type env
        TypeChecker newChecker = this.extend(Collections.singletonList(NodeFactory.makeLValue(that.getName(), Types.LABEL)));
        TypeCheckerResult bodyResult = that.getBody().accept(newChecker);

        // If the body was typed, union all the exit types with it.
        // If any exit type is none, then don't type this label.
        Option<Type> labelType = none();
        if (bodyResult.type().isSome()) {
            Option<Set<Type>> exitTypes = labelExitTypes.get(that.getName());
            if (exitTypes.isSome()) {
                Set<Type> _exitTypes = exitTypes.unwrap();
                _exitTypes.add(bodyResult.type().unwrap());
                labelType = some(subtypeChecker.join(_exitTypes));
            }
        }

        // Destroy the mappings for this label
        labelExitTypes.remove(that.getName());

        Label new_node = ExprFactory.makeLabel(NodeUtil.getSpan(that),
                NodeUtil.isParenthesized(that),
                labelType,
                that.getName(),
                (Block)bodyResult.ast());

        return TypeCheckerResult.compose(new_node, labelType,
                subtypeChecker, bodyResult).addNodeTypeEnvEntry(new_node, typeEnv);
    }

    @Override
    public TypeCheckerResult forLetFn(LetFn that) {
        Relation<IdOrOpOrAnonymousName, FnDecl> fnDefs = new IndexedRelation<IdOrOpOrAnonymousName, FnDecl>(false);
        for (FnDecl fnDef : that.getFns()) {
            fnDefs.add(NodeUtil.getName(fnDef), fnDef);
        }

        TypeChecker newChecker = this.extendWithFnDecls(fnDefs);
        List<TypeCheckerResult> fn_results = newChecker.recurOnListOfFnDecl(that.getFns());

        // A LetFn is like a let. It has a body, and it's type is the type of the body
        List<TypeCheckerResult> body_results = newChecker.recurOnListOfExpr(that.getBody());
        List<TypeCheckerResult> body_void = newChecker.allVoidButLast(body_results, that.getBody());
        Option<Type> body_type = that.getBody().size() == 0 ?
                Option.<Type>some(Types.VOID) :
                    body_results.get(body_results.size()-1).type();

                LetFn new_node = ExprFactory.makeLetFn(NodeUtil.getSpan(that),
                        NodeUtil.isParenthesized(that),
                        body_type,
                        (List<Expr>)TypeCheckerResult.astFromResults(body_results),
                        (List<FnDecl>)TypeCheckerResult.astFromResults(fn_results));

                TypeCheckerResult result =
                    TypeCheckerResult.compose(new_node, body_type, subtypeChecker,
                            TypeCheckerResult.compose(new_node, subtypeChecker, body_results),
                            TypeCheckerResult.compose(new_node, subtypeChecker, body_void),
                            TypeCheckerResult.compose(new_node, subtypeChecker, fn_results));

                return result.addNodeTypeEnvEntry(new_node, typeEnv);
    }

    @Override
    public TypeCheckerResult forLocalVarDecl(LocalVarDecl that) {
        TypeCheckerResult result = new TypeCheckerResult(that);

        // Create type for LHS
        Type lhs_type =
            Types.MAKE_TUPLE.value(IterUtil.map(that.getLhs(), new Lambda<LValue,Type>(){
                public Type value(LValue arg0) { return getTypeOfLValue(arg0); }}));

        Option<TypeCheckerResult> _rhs_result = this.recurOnOptionOfExpr(that.getRhs());
        if ( _rhs_result.isSome() ) {
            TypeCheckerResult rhs_result = _rhs_result.unwrap();
            result = TypeCheckerResult.compose(that, subtypeChecker, result, rhs_result);

            if( rhs_result.type().isSome() ) {
                Type rhs_type = rhs_result.type().unwrap();
                result = TypeCheckerResult.compose(that, subtypeChecker, result,
                        checkSubtype(rhs_type, lhs_type, that,
                                "Right-hand side, " + rhs_type + ", must be a subtype of left-hand side, " + lhs_type + "."));
            }
        }

        // Extend typechecker with new bindings and with constraints from the RHS types
        TypeChecker newChecker = this.extend(that);
        Iterable<ConstraintFormula> rhs_constraint = IterUtil.make(result.getNodeConstraints());
        newChecker = newChecker.extendWithConstraints(rhs_constraint);

        // A LocalVarDecl is like a let. It has a body, and it's type is the type of the body
        List<TypeCheckerResult> body_results = newChecker.recurOnListOfExpr(that.getBody());
        List<TypeCheckerResult> body_void = newChecker.allVoidButLast(body_results, that.getBody());
        Option<Type> body_type = that.getBody().size() == 0 ?
                Option.<Type>some(Types.VOID) :
                    body_results.get(body_results.size()-1).type();

                LocalVarDecl new_node = ExprFactory.makeLocalVarDecl(NodeUtil.getSpan(that),
                        NodeUtil.isParenthesized(that),
                        body_type,
                        (List<Expr>)TypeCheckerResult.astFromResults(body_results),
                        that.getLhs(),
                        (Option<Expr>)TypeCheckerResult.astFromResult(_rhs_result));
                return TypeCheckerResult.compose(new_node,
                        body_type, subtypeChecker, result,
                        TypeCheckerResult.compose(new_node, subtypeChecker, _rhs_result),
                        TypeCheckerResult.compose(new_node, subtypeChecker, body_results),
                        TypeCheckerResult.compose(new_node, subtypeChecker, body_void)).addNodeTypeEnvEntry(new_node, typeEnv);
    }

    @Override
        public TypeCheckerResult forJuxt(Juxt that) {
            if ( that.isTight() ) {
                // Just create a MathPrimary
                Expr front = that.getExprs().get(0);

                // If this juxt is actually a fn app, then rewrite to a fn app.
                if (that.isFnApp()) {
                    // Make sure it is just two exprs.
                    if (that.getExprs().size() != 2) {
                        bug(String.format("TightJuxt denoted as function application but has %d (!= 2) exprs.",
                                          that.getExprs().size()));
                    }
                    Expr arg = that.getExprs().get(1);
                    _RewriteFnApp fnApp = ExprFactory.make_RewriteFnApp(front, arg);

                    // Simulate a TypeCheckerResult for the front, giving it a fresh arrow type.
                    Type freshArrow = NodeFactory.makeArrowType(NodeUtil.getSpan(that),
                                                                NodeFactory.make_InferenceVarType(NodeUtil.getSpan(that)),
                                                                NodeFactory.make_InferenceVarType(NodeUtil.getSpan(that)));
                    TypeCheckerResult front_result = new TypeCheckerResult(front, freshArrow);

                    // Type check the other nodes and recur on the fn app.
                    Option<TypeCheckerResult> exprType_result = this.recurOnOptionOfType(NodeUtil.getExprType(that));
                    TypeCheckerResult arg_result = arg.accept(this);
                    TypeCheckerResult fnApp_result = this.for_RewriteFnAppOnly(fnApp,
                                                                               exprType_result,
                                                                               front_result,
                                                                               arg_result);
                    return TypeCheckerResult.compose(that,
                                                     fnApp_result.type(),
                                                     subtypeChecker,
                                                     fnApp_result);
                }

                Iterable<Expr> rest = IterUtil.skipFirst(that.getExprs());
                List<MathItem> items = CollectUtil.makeList(IterUtil.map(rest, new Lambda<Expr,MathItem>(){
                            public MathItem value(Expr arg0) {
                                if( NodeUtil.isParenthesized(arg0) || arg0 instanceof TupleExpr || arg0 instanceof VoidLiteralExpr)
                                    return ExprFactory.makeParenthesisDelimitedMI(NodeUtil.getSpan(arg0),arg0);
                                else
                                    return ExprFactory.makeNonParenthesisDelimitedMI(NodeUtil.getSpan(arg0),arg0);
                            }}));
                MathPrimary new_primary = ExprFactory.makeMathPrimary(NodeUtil.getSpan(that),
                                                               NodeUtil.isParenthesized(that),
                                                               NodeUtil.getExprType(that),
                                                               that.getMultiJuxt(),
                                                               that.getInfixJuxt(),
                                                               front, items);
        return new_primary.accept(this);
            } else
                return super.forJuxt(that);
        }

    @Override
    public TypeCheckerResult forJuxtOnly(Juxt that, TypeCheckerResult exprType_result,
                                             TypeCheckerResult multiJuxt_result,
                                             TypeCheckerResult infixJuxt_result,
                                             List<TypeCheckerResult> exprs_result) {
            if (! that.isTight() ) {
                // The implementation of this method is very similar to tight juxt except
                // the ordering of association is different.
                // Notice also that tightJuxt has to be recursive, but loose juxt is not, due to specification.

                // Did any subexpressions fail to typecheck?
                for( TypeCheckerResult r : exprs_result ) {
                    if( r.type().isNone())
                        return TypeCheckerResult.compose(that, subtypeChecker, exprs_result);
                }

                if( that.getExprs().size() != exprs_result.size() ) {
                    bug("Number of types don't match number of sub-expressions");
                }
                // Specification describes chunks, which are elements group together. Chunking process goes first.
                List<Pair<TypeCheckerResult,Expr>> checked_chunks = new LinkedList<Pair<TypeCheckerResult,Expr>>();
                {
                    List<Pair<TypeCheckerResult,Expr>> cur_chunk = new LinkedList<Pair<TypeCheckerResult,Expr>>();
                    Iterator<Expr> expr_iter = that.getExprs().iterator();
                    boolean seen_non_fn = false;
                    // First the loose juxtaposition is broken into nonempty chunks; wherever there is a non-function element followed
                    // by a function element, the latter begins a new chunk. Thus a chunk consists of some number (possibly zero) of
                    // functions followed by some number (possibly zero) of non-functions.
                    for( TypeCheckerResult r : exprs_result ) {
                        boolean is_arrow = TypesUtil.isArrows(r.type().unwrap());
                        if( is_arrow && seen_non_fn ) {
                            // finished last chunk
                            Pair<TypeCheckerResult,Expr> checked_chunk = this.checkChunk(cur_chunk, that.getInfixJuxt());
                            checked_chunks.add(checked_chunk);
                            cur_chunk.clear();
                            seen_non_fn = false;
                        }
                        if( is_arrow ){
                            cur_chunk.add(Pair.make(r, expr_iter.next()));
                        }
                        else {
                            seen_non_fn = true;
                            cur_chunk.add(Pair.make(r, expr_iter.next()));
                        }
                    }
                    // Last chunk needs to be checked, if there is one
                    if( !cur_chunk.isEmpty() ) {
                        checked_chunks.add(checkChunk(cur_chunk, that.getInfixJuxt()));
                    }
                }
                // After chunking
                List<Expr> new_juxt_exprs = CollectUtil.makeList(IterUtil.pairSeconds(checked_chunks));
                List<TypeCheckerResult> new_juxt_results = CollectUtil.makeList(IterUtil.pairFirsts(checked_chunks));

                if( checked_chunks.size() == 1 ) {
                    Expr expr = new_juxt_exprs.get(0);
                    TypeCheckerResult expr_result = expr.accept(this); // Is it bad to re-typecheck all args?
                    return TypeCheckerResult.compose(expr_result.ast(), expr_result.type(), subtypeChecker, expr_result,
                                                     TypeCheckerResult.compose(expr_result.ast(), subtypeChecker, new_juxt_results));
                }
                // (1) If any element that remains has type String, then it is a static error if any two adjacent elements are not of type String.
                // TODO: Separate pass?
                // (2) Treat the sequence that remains as a multifix application of the juxtaposition operator. The rules for multifix operators then apply:
                OpExpr multi_op_expr = ExprFactory.makeOpExpr(NodeUtil.getSpan(that),
                                                              NodeUtil.isParenthesized(that),
                                                              NodeUtil.getExprType(that),
                                                              that.getMultiJuxt(),
                                                              new_juxt_exprs);
                TypeCheckerResult multi_op_result = multi_op_expr.accept(this);
                if( multi_op_result.type().isSome() ) {
                    return TypeCheckerResult.compose(multi_op_result.ast(), multi_op_result.type(), subtypeChecker,
                                                     TypeCheckerResult.compose(multi_op_result.ast(), subtypeChecker, new_juxt_results));
                }
                // if an applicable method cannot be found for the entire expression, then it is left-associated.
                Iterator<Expr> expr_iter = new_juxt_exprs.iterator();
                Expr expr_1 = expr_iter.next(); // the fact that >= two items are here is guaranteed from above.
                Expr expr_2 = expr_iter.next();
                OpExpr cur_op_expr = ExprFactory.makeOpExpr(FortressUtil.spanTwo(expr_1,expr_2),
                                                            that.getInfixJuxt(),
                                                            expr_1, expr_2);
                while( expr_iter.hasNext() ) {
                    Expr next_expr = expr_iter.next();
                    cur_op_expr = ExprFactory.makeOpExpr(FortressUtil.spanTwo(cur_op_expr,next_expr),
                                                         that.getInfixJuxt(),
                                                         cur_op_expr, next_expr);
                }
                // typecheck this result instead
                TypeCheckerResult op_expr_result = cur_op_expr.accept(this); // Is it bad to re-typecheck all args?
                return TypeCheckerResult.compose(op_expr_result.ast(), op_expr_result.type(), subtypeChecker, op_expr_result,
                                                 TypeCheckerResult.compose(op_expr_result.ast(), subtypeChecker, new_juxt_results));
            } else {
                return super.forJuxtOnly(that, exprType_result,
                                         multiJuxt_result, infixJuxt_result,
                                         exprs_result);
            }
        }

    // Math primary, which is the more general case, is going to be called for both TightJuxt and MathPrimary
    @Override
    public TypeCheckerResult forMathPrimary(MathPrimary that) {

        // Base case of recursion: If there is no 'rest', return the Expr
        Expr front = that.getFront();
        if( that.getRest().isEmpty() ) {
            return front.accept(this);
        }
        // See if simple static errors exist
        Option<TypeCheckerResult> static_result = exponentiationStaticCheck(that, that.getRest());
        if( static_result.isSome() ) {
            return static_result.unwrap();
        }

        // HANDLE THE FRONT ITEM
        {
            // Create a new list of MathItems that is a copy of the old one
            List<MathItem> new_items = new ArrayList<MathItem>(that.getRest());
            ListIterator<MathItem> item_iter = new_items.listIterator();

            TypeCheckerResult front_result = front.accept(this);
            MathItem first_of_rest = item_iter.next();
            if( front_result.type().isNone() )
                return TypeCheckerResult.compose(that, subtypeChecker, front_result);

            // If front is a fn followed by an expr, we reassociate
            if( TypesUtil.isArrows(front_result.type().unwrap()) && isExprMI(first_of_rest) ) {
                MathItem arg = first_of_rest;
                // It is a static error if either the argument is not parenthesized,
                Option<TypeCheckerResult> is_error = expectParenedExprItem(arg);
                if( is_error.isSome() ) {
                    return TypeCheckerResult.compose(that, subtypeChecker, is_error.unwrap());
                }
                item_iter.remove(); // remove arg from item list
                // static error if the argument is immediately followed by a non-expression element.
                if( item_iter.hasNext() ) {
                    Option<TypeCheckerResult> is_expr_error = expectExprMI(item_iter.next());
                    if( is_expr_error.isSome() ) {
                        return TypeCheckerResult.compose(that, subtypeChecker, is_expr_error.unwrap());
                    }
                }
                // Otherwise, make a new MathPrimary that is one element shorter, and recur
                _RewriteFnApp fn = ExprFactory.make_RewriteFnApp(front,
                                                                                 ((ExprMI)arg).getExpr());
                MathPrimary new_primary = ExprFactory.makeMathPrimary(NodeUtil.getSpan(that),
                                                                                      NodeUtil.isParenthesized(that),
                                                                                      NodeUtil.getExprType(that),
                                                                                      that.getMultiJuxt(),
                                                                                      that.getInfixJuxt(),
                                                                                      fn,
                                                                                      new_items);
                return new_primary.accept(this);
            }
        }
        // THE FRONT ITEM WAS NOT A FN FOLLOWED BY AN EXPR, REASSOCIATE REST
        {

            Expr last_expr_ = front;
            boolean last_expr_is_front = true;
            // Create a new list of MathItems that is a copy of the old one
            List<MathItem> new_items = new ArrayList<MathItem>(that.getRest());
            ListIterator<MathItem> item_iter = new_items.listIterator();

            while( item_iter.hasNext() ) {
                MathItem cur_item = item_iter.next();
                final Expr last_expr = last_expr_;
                // For each expression element determine whether it is a function immediately followed by an expr
                if( isExprMI(cur_item) ) {
                    TypeCheckerResult expr_result = ((ExprMI)cur_item).getExpr().accept(this);
                    if( expr_result.type().isNone() )
                        return TypeCheckerResult.compose(that, subtypeChecker, expr_result);

                    Option<MathItem> next_item = item_iter.hasNext() ? Option.<MathItem>some(item_iter.next()) : Option.<MathItem>none();
                    if( TypesUtil.isArrows(expr_result.type().unwrap()) && next_item.isSome() && isExprMI(next_item.unwrap()) ) {
                        // Yes. We have a function followed by an expr
                        MathItem arg = next_item.unwrap();
                        // It is a static error if either the argument is not parenthesized,
                        Option<TypeCheckerResult> is_error = expectParenedExprItem(arg);
                        if( is_error.isSome() ) {
                            return TypeCheckerResult.compose(that, subtypeChecker, is_error.unwrap());
                        }
                        item_iter.remove(); // remove arg from item list
                        item_iter.previous();
                        item_iter.remove(); // remove fn from item list
                        // replace both with fn appication
                        _RewriteFnApp fn = ExprFactory.make_RewriteFnApp(front, ((ExprMI)arg).getExpr());
                        item_iter.add(ExprFactory.makeNonParenthesisDelimitedMI(NodeUtil.getSpan(fn),fn));
                        // static error if the argument is immediately followed by a non-expression element.
                        if( item_iter.hasNext() ) {
                            Option<TypeCheckerResult> is_expr_error = expectExprMI(item_iter.next());
                            if( is_expr_error.isSome() ) {
                                return TypeCheckerResult.compose(that, subtypeChecker, is_expr_error.unwrap());
                            }
                        }
                        // Otherwise, make a new MathPrimary that is one element shorter, and recur
                        MathPrimary new_primary = ExprFactory.makeMathPrimary(NodeUtil.getSpan(that),
                                                                                                      NodeUtil.isParenthesized(that),
                                                                                                      NodeUtil.getExprType(that),
                                                                                                      that.getMultiJuxt(),
                                                                                                      that.getInfixJuxt(),
                                                                                                      that.getFront(),
                                                                                                      new_items);
                        return new_primary.accept(this);
                    } else {
                        // Continues to next expression...
                        last_expr_ = ((ExprMI)cur_item).getExpr();
                        last_expr_is_front = false;
                    }
                }
                else {
                    // If there is any non-expression element then replace the first such element and the
                    // element immediately preceding it (which must be an expression) with a single element that does the appropriate
                    // operator application.
                    NodeDepthFirstVisitor<Expr> op_visitor = new NodeDepthFirstVisitor<Expr>() {
                        @Override
                        public Expr forExponentiationMI(ExponentiationMI that) {
                            // how could an expression not exist in an exponentiation?
                            return ExprFactory.makeOpExpr(that.getOp(), last_expr, that.getExpr().unwrap());
                        }
                        @Override
                        public Expr forSubscriptingMI(SubscriptingMI that) {
                            Span span = new Span(NodeUtil.getSpan(last_expr),NodeUtil.getSpan(that));
                            return ExprFactory.makeSubscriptExpr(span, last_expr, that.getExprs(), Option.some(that.getOp()), that.getStaticArgs());
                        }
                    };
                    Expr new_expr = cur_item.accept(op_visitor);
                    item_iter.remove(); // remove NonExprMI
                    if( last_expr_is_front ) {
                        // in our new MathPrimary, place this expression at the front
                        MathPrimary new_primary = ExprFactory.makeMathPrimary(NodeUtil.getSpan(that),
                                                                                                      NodeUtil.isParenthesized(that),
                                                                                                      NodeUtil.getExprType(that),
                                                                                                      that.getMultiJuxt(),
                                                                                                      that.getInfixJuxt(),
                                                                                                      new_expr, new_items);
                        return new_primary.accept(this);
                    }
                    else {
                        // in our new MathPrimary, place this expression where it is
                        item_iter.previous();
                        item_iter.remove(); // remove the previous expression in the list.
                        MathItem new_item = ExprFactory.makeParenthesisDelimitedMI(NodeUtil.getSpan(new_expr),new_expr);
                        item_iter.add(new_item); // replace both item with new item
                        MathPrimary new_primary = ExprFactory.makeMathPrimary(NodeUtil.getSpan(that),
                                                                                                      NodeUtil.isParenthesized(that),
                                                                                                      NodeUtil.getExprType(that),
                                                                                                      that.getMultiJuxt(),
                                                                                                      that.getInfixJuxt(),
                                                                                                      that.getFront(),
                                                                                                      new_items);
                        return new_primary.accept(this);
                    }
                }
            }
        }

        // If you've made is this far, there are only expressions left in the math primary.
        // helper method handles the last two rules
        return juxtaposeMathPrimary(that);
    }





    @Override
    public TypeCheckerResult forMethodInvocation(MethodInvocation that) {
        Option<TypeCheckerResult> exprType_result = recurOnOptionOfType(NodeUtil.getExprType(that));
        TypeCheckerResult obj_result = recur(that.getObj());
        TypeCheckerResult method_result = recur(that.getMethod());
        List<TypeCheckerResult> staticArgs_result = recurOnListOfStaticArg(that.getStaticArgs());
        TypeCheckerResult arg_result = recur(that.getArg());

        // Use constraints from arguments to extend typechecker. This will allow for
        // better choices of overloadings during the first typechecking phase.
        Iterable<ConstraintFormula> arg_constraint = IterUtil.make(arg_result.getNodeConstraints());
        TypeChecker new_checker = this.extendWithConstraints(arg_constraint);
        return new_checker.forMethodInvocationOnly(that, exprType_result, obj_result, method_result, staticArgs_result, arg_result);
    }

    public TypeCheckerResult forMethodInvocationOnly(MethodInvocation that, Option<TypeCheckerResult> exprType_result,
            TypeCheckerResult obj_result, TypeCheckerResult DONTUSE,
            List<TypeCheckerResult> staticArgs_result,
            TypeCheckerResult arg_result) {

        // Did the arguments typecheck?
        if( arg_result.type().isNone() ) {
            return TypeCheckerResult.compose(that, subtypeChecker, obj_result, arg_result,
                    TypeCheckerResult.compose(that, subtypeChecker, staticArgs_result));
        }
        // We need the type of the receiver
        if( obj_result.type().isNone() ) {
            return TypeCheckerResult.compose(that, subtypeChecker, obj_result, arg_result,
                    TypeCheckerResult.compose(that, subtypeChecker, staticArgs_result));
        }
        // Check whether receiver can have methods
        Type recvr_type=obj_result.type().unwrap();
        List<TraitType> traits = traitTypesCallable(recvr_type);
        if( traits.isEmpty() ) {
            //error receiver not a trait
            String trait_err = "Target of a method invocation must have trait type, while this receiver has type " + recvr_type + ".";
            TypeCheckerResult trait_result = new TypeCheckerResult(that.getObj(), TypeError.make(trait_err, that.getObj()));
            return TypeCheckerResult.compose(that, subtypeChecker, obj_result, arg_result, trait_result,
                    TypeCheckerResult.compose(that, subtypeChecker, staticArgs_result));
        }
        else {
            Pair<List<Method>,List<TypeCheckerResult>> candidate_pair =
                findMethodsInTraitHierarchy(that.getMethod(), traits, arg_result.type().unwrap(),that.getStaticArgs(),that);

            // Now we meet together the results, or return an error if there are no candidates.
            List<Method> candidates = candidate_pair.first();
            if(candidates.isEmpty()) {
                String err = "No candidate methods found for '" + that.getMethod() + "' with argument types (" + arg_result.type().unwrap() + ").";
                TypeCheckerResult no_methods = new TypeCheckerResult(that,TypeError.make(err,that));

                return TypeCheckerResult.compose(that, subtypeChecker, obj_result, arg_result, no_methods,
                        TypeCheckerResult.compose(that, subtypeChecker, staticArgs_result));
            }

            List<Type> ranges = CollectUtil.makeList(IterUtil.map(candidates, new Lambda<Method,Type>(){
                public Type value(Method arg0) {
                    return arg0.getReturnType();
                }}));

            Type range = subtypeChecker.meet(ranges);
            range = subtypeChecker.normalize(range);
            MethodInvocation new_node = ExprFactory.makeMethodInvocation(NodeUtil.getSpan(that),
                                                                                     NodeUtil.isParenthesized(that),
                                                                                     Option.<Type>some(range),
                                                                                     (Expr)obj_result.ast(),
                                                                                     that.getMethod(),
                    (List<StaticArg>)TypeCheckerResult.astFromResults(staticArgs_result),
                    (Expr)arg_result.ast());

            TypeCheckerResult result = TypeCheckerResult.compose(new_node, range, subtypeChecker, obj_result, arg_result,
                    TypeCheckerResult.compose(that, subtypeChecker, staticArgs_result),
                    TypeCheckerResult.compose(new_node, subtypeChecker, candidate_pair.second()));

            // On the post-inference pass, an application could produce Inference vars
            TypeCheckerResult successful = new TypeCheckerResult(that);
            if( postInference && TypesUtil.containsInferenceVarTypes(new_node) ) {
                // close constraints

                Pair<Boolean,Node> temp1 = TypesUtil.closeConstraints(new_node, subtypeChecker, result);
                new_node = (MethodInvocation)temp1.second();
                Pair<Boolean,Node> temp2 = TypesUtil.closeConstraints(range, subtypeChecker, result);
                range = (Type)temp2.second();
                if(!temp1.first() || !temp2.first()){
                    String err = "No candidate methods found for '" + that.getMethod() + "' with argument types (" + arg_result.type().unwrap() + ").";
                    successful = new TypeCheckerResult(that, TypeError.make(err,that));
                }
            }

            return TypeCheckerResult.compose(new_node, range, subtypeChecker, result, successful);
        }
    }

    @Override
    public TypeCheckerResult forMultiFixity(MultiFixity that) {
        // No checks needed to be performed on a MultiFixity.
        return new TypeCheckerResult(that);
    }

    @Override
    public TypeCheckerResult forNoFixity(NoFixity that) {
        // No checks needed to be performed on a NoFixity.
        return new TypeCheckerResult(that);
    }

    @Override
    public TypeCheckerResult forParam(Param that) {
        // No checks needed to be performed on a Param.
        return new TypeCheckerResult(that);
    }

    @Override
    public TypeCheckerResult forIntBaseOnly(IntBase that,
                                                TypeCheckerResult info,
                                                TypeCheckerResult val_result) {
        return new TypeCheckerResult(that);
    }

    @Override
    public TypeCheckerResult forObjectDecl(final ObjectDecl that) {
        TypeChecker checker_with_sparams = this.extend(NodeUtil.getStaticParams(that), NodeUtil.getParams(that), NodeUtil.getWhereClause(that));
        TypeCheckerResult nameResult = NodeUtil.getName(that).accept(checker_with_sparams);
        List<TypeCheckerResult> extendsClauseResult = checker_with_sparams.recurOnListOfTraitTypeWhere(NodeUtil.getExtendsClause(that));
        TypeCheckerResult whereResult;
        Option<WhereClause> where;