/*
 * Licensed to Julian Hyde under one or more contributor license
 * agreements.  See the NOTICE file distributed with this work
 * for additional information regarding copyright ownership.
 * Julian Hyde licenses this file to you under the Apache
 * License, Version 2.0 (the "License"); you may not use this
 * file except in compliance with the License.  You may obtain a
 * copy of the License at
 *
 * http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing,
 * software distributed under the License is distributed on an
 * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND,
 * either express or implied.  See the License for the specific
 * language governing permissions and limitations under the
 * License.
 */
package net.hydromatic.morel.compile;

import static com.google.common.base.Preconditions.checkArgument;
import static java.lang.String.join;
import static java.util.Objects.requireNonNull;
import static net.hydromatic.morel.ast.AstBuilder.ast;
import static net.hydromatic.morel.type.RecordType.mutableMap;
import static net.hydromatic.morel.util.Ord.forEachIndexed;
import static net.hydromatic.morel.util.Pair.forEach;
import static net.hydromatic.morel.util.Static.last;
import static net.hydromatic.morel.util.Static.skip;
import static net.hydromatic.morel.util.Static.transform;
import static net.hydromatic.morel.util.Static.transformEager;
import static org.apache.calcite.util.Util.firstDuplicate;

import com.google.common.base.Suppliers;
import com.google.common.collect.ImmutableList;
import com.google.common.collect.Iterables;
import com.google.common.collect.Lists;
import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.Deque;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
import java.util.NavigableMap;
import java.util.NavigableSet;
import java.util.SortedMap;
import java.util.TreeMap;
import java.util.TreeSet;
import java.util.concurrent.atomic.AtomicBoolean;
import java.util.function.BiConsumer;
import java.util.function.Consumer;
import java.util.function.Function;
import java.util.function.Supplier;
import net.hydromatic.morel.ast.Ast;
import net.hydromatic.morel.ast.AstNode;
import net.hydromatic.morel.ast.Op;
import net.hydromatic.morel.ast.Pos;
import net.hydromatic.morel.ast.Visitor;
import net.hydromatic.morel.type.Binding;
import net.hydromatic.morel.type.DataType;
import net.hydromatic.morel.type.FnType;
import net.hydromatic.morel.type.ForallType;
import net.hydromatic.morel.type.Keys;
import net.hydromatic.morel.type.ListType;
import net.hydromatic.morel.type.PrimitiveType;
import net.hydromatic.morel.type.RecordType;
import net.hydromatic.morel.type.TupleType;
import net.hydromatic.morel.type.Type;
import net.hydromatic.morel.type.TypeSystem;
import net.hydromatic.morel.type.TypeVar;
import net.hydromatic.morel.type.TypedValue;
import net.hydromatic.morel.util.MapList;
import net.hydromatic.morel.util.MartelliUnifier;
import net.hydromatic.morel.util.Ord;
import net.hydromatic.morel.util.Pair;
import net.hydromatic.morel.util.PairList;
import net.hydromatic.morel.util.Tracers;
import net.hydromatic.morel.util.Unifier;
import org.apache.calcite.util.Holder;
import org.checkerframework.checker.nullness.qual.Nullable;

/** Resolves the type of an expression. */
@SuppressWarnings("StaticPseudoFunctionalStyleMethod")
public class TypeResolver {
  private final TypeSystem typeSystem;
  private final Unifier unifier = new MartelliUnifier();
  private final List<TermVariable> terms = new ArrayList<>();
  private final Map<AstNode, Unifier.Term> map = new HashMap<>();
  private final Map<Unifier.Variable, Unifier.Action> actionMap =
      new HashMap<>();
  private final PairList<Unifier.Variable, PrimitiveType> preferredTypes =
      PairList.of();

  static final String TUPLE_TY_CON = "tuple";
  static final String LIST_TY_CON = "list";
  static final String RECORD_TY_CON = "record";
  static final String FN_TY_CON = "fn";

  /** A field of this name indicates that a record type is progressive. */
  static final String PROGRESSIVE_LABEL = "z$dummy";

  private TypeResolver(TypeSystem typeSystem) {
    this.typeSystem = requireNonNull(typeSystem);
  }

  /** Deduces the datatype of a declaration. */
  public static Resolved deduceType(
      Environment env, Ast.Decl decl, TypeSystem typeSystem) {
    final TypeResolver typeResolver = new TypeResolver(typeSystem);
    int attempt = 0;
    for (; ; ) {
      int original = typeSystem.expandCount.get();
      final TypeResolver.Resolved resolved =
          typeResolver.deduceType_(env, decl);
      if (typeSystem.expandCount.get() == original || attempt++ > 1) {
        return resolved;
      }
    }
  }

  /** Converts a type AST to a type. */
  public static Type toType(Ast.Type type, TypeSystem typeSystem) {
    return typeSystem.typeFor(toTypeKey(type));
  }

  /** Converts a type AST to a type key. */
  public static Type.Key toTypeKey(Ast.Type type) {
    return new Foo().toTypeKey(type);
  }

  private Resolved deduceType_(Environment env, Ast.Decl decl) {
    final TypeEnvHolder typeEnvs = new TypeEnvHolder(EmptyTypeEnv.INSTANCE);
    BuiltIn.forEach(
        typeSystem,
        (builtIn, type) -> {
          if (builtIn.structure == null) {
            typeEnvs.accept(builtIn.mlName, type);
          }
          if (builtIn.alias != null) {
            typeEnvs.accept(builtIn.alias, type);
          }
        });
    BuiltIn.forEachStructure(
        typeSystem, (structure, type) -> typeEnvs.accept(structure.name, type));
    env.forEachType(typeSystem, typeEnvs);
    final TypeEnv typeEnv = typeEnvs.typeEnv;
    final Map<Ast.IdPat, Unifier.Term> termMap = new LinkedHashMap<>();
    final Ast.Decl node2 = deduceDeclType(typeEnv, decl, termMap);
    final boolean debug = false;
    @SuppressWarnings("ConstantConditions")
    final Unifier.Tracer tracer =
        debug ? Tracers.printTracer(System.out) : Tracers.nullTracer();

    // Deduce types. The loop will retry, just once, if there are certain kinds
    // of errors.
    tryAgain:
    for (; ; ) {
      final List<Unifier.TermTerm> termPairs = new ArrayList<>();
      terms.forEach(
          tv -> termPairs.add(new Unifier.TermTerm(tv.term, tv.variable)));
      final Unifier.Result result = unifier.unify(termPairs, actionMap, tracer);
      if (!(result instanceof Unifier.Substitution)) {
        final String extra =
            ";\n"
                + " term pairs:\n"
                + join("\n", transform(terms, Object::toString));
        throw new TypeException("Cannot deduce type: " + result, Pos.ZERO);
      }
      final TypeMap typeMap =
          new TypeMap(typeSystem, map, (Unifier.Substitution) result);
      while (!preferredTypes.isEmpty()) {
        Map.Entry<Unifier.Variable, PrimitiveType> x = preferredTypes.remove(0);
        final Type type =
            typeMap.termToType(typeMap.substitution.resultMap.get(x.getKey()));
        if (type instanceof TypeVar) {
          equiv(toTerm(x.getValue()), x.getKey());
          continue tryAgain;
        }
      }

      final AtomicBoolean progressive = new AtomicBoolean();
      forEachUnresolvedField(
          node2,
          typeMap,
          apply -> {
            final Type type = typeMap.getType(apply.arg);
            if (type.isProgressive()) {
              progressive.set(true);
            }
          },
          apply -> {},
          apply -> {});
      if (progressive.get()) {
        node2.accept(FieldExpander.create(typeSystem, env));
      } else {
        checkNoUnresolvedFieldRefs(node2, typeMap);
      }
      return Resolved.of(env, decl, node2, typeMap);
    }
  }

  /**
   * Checks that there are no field references "x.y" or "#y x" where "x" has an
   * unresolved type. Throws if there are unresolved field references.
   */
  private static void checkNoUnresolvedFieldRefs(
      Ast.Decl decl, TypeMap typeMap) {
    forEachUnresolvedField(
        decl,
        typeMap,
        apply -> {
          throw new TypeException(
              "unresolved flex record (can't tell "
                  + "what fields there are besides "
                  + apply.fn
                  + ")",
              apply.arg.pos);
        },
        apply -> {
          throw new TypeException(
              "reference to field "
                  + ((Ast.RecordSelector) apply.fn).name
                  + " of non-record type "
                  + typeMap.getType(apply.arg),
              apply.arg.pos);
        },
        apply -> {
          throw new TypeException(
              "no field '"
                  + ((Ast.RecordSelector) apply.fn).name
                  + "' in type '"
                  + typeMap.getType(apply.arg)
                  + "'",
              apply.arg.pos);
        });
  }

  private static void forEachUnresolvedField(
      Ast.Decl decl,
      TypeMap typeMap,
      Consumer<Ast.Apply> variableConsumer,
      Consumer<Ast.Apply> notRecordTypeConsumer,
      Consumer<Ast.Apply> noFieldConsumer) {
    decl.accept(
        new Visitor() {
          @Override
          protected void visit(Ast.Apply apply) {
            if (apply.fn.op == Op.RECORD_SELECTOR) {
              final Ast.RecordSelector recordSelector =
                  (Ast.RecordSelector) apply.fn;
              if (typeMap.typeIsVariable(apply.arg)) {
                variableConsumer.accept(apply);
              } else {
                final Collection<String> fieldNames =
                    typeMap.typeFieldNames(apply.arg);
                if (fieldNames == null) {
                  notRecordTypeConsumer.accept(apply);
                } else {
                  if (!fieldNames.contains(recordSelector.name)) {
                    // "#f r" is valid if "r" is a record type with a field "f"
                    noFieldConsumer.accept(apply);
                  }
                }
              }
            }
            super.visit(apply);
          }
        });
  }

  private <E extends AstNode> E reg(
      E node, Unifier.Variable variable, Unifier.Term term) {
    requireNonNull(node);
    requireNonNull(term);
    map.put(node, term);
    if (variable != null) {
      equiv(term, variable);
    }
    return node;
  }

  private Ast.Exp deduceType(TypeEnv env, Ast.Exp node, Unifier.Variable v) {
    final List<Ast.Exp> args2;
    final Unifier.Variable v2;
    final Map<Ast.IdPat, Unifier.Term> termMap;
    switch (node.op) {
      case BOOL_LITERAL:
        return reg(node, v, toTerm(PrimitiveType.BOOL));

      case CHAR_LITERAL:
        return reg(node, v, toTerm(PrimitiveType.CHAR));

      case INT_LITERAL:
        return reg(node, v, toTerm(PrimitiveType.INT));

      case REAL_LITERAL:
        return reg(node, v, toTerm(PrimitiveType.REAL));

      case STRING_LITERAL:
        return reg(node, v, toTerm(PrimitiveType.STRING));

      case UNIT_LITERAL:
        return reg(node, v, toTerm(PrimitiveType.UNIT));

      case ANNOTATED_EXP:
        final Ast.AnnotatedExp annotatedExp = (Ast.AnnotatedExp) node;
        final Type type = toType(annotatedExp.type, typeSystem);
        final Ast.Exp exp2 = deduceType(env, annotatedExp.exp, v);
        final Ast.AnnotatedExp annotatedExp2 =
            annotatedExp.copy(exp2, annotatedExp.type);
        return reg(annotatedExp2, v, toTerm(type, Subst.EMPTY));

      case ANDALSO:
      case ORELSE:
      case IMPLIES:
        return infix(env, (Ast.InfixCall) node, v, PrimitiveType.BOOL);

      case TUPLE:
        final Ast.Tuple tuple = (Ast.Tuple) node;
        final List<Unifier.Term> types = new ArrayList<>();
        args2 = new ArrayList<>();
        for (Ast.Exp arg : tuple.args) {
          final Unifier.Variable vArg = unifier.variable();
          args2.add(deduceType(env, arg, vArg));
          types.add(vArg);
        }
        return reg(tuple.copy(args2), v, tuple(types));

      case LIST:
        final Ast.ListExp list = (Ast.ListExp) node;
        final Unifier.Variable vArg2 = unifier.variable();
        args2 = new ArrayList<>();
        for (Ast.Exp arg : list.args) {
          args2.add(deduceType(env, arg, vArg2));
        }
        return reg(list.copy(args2), v, unifier.apply(LIST_TY_CON, vArg2));

      case RECORD:
        final Ast.Record record = (Ast.Record) node;
        final NavigableMap<String, Unifier.Term> labelTypes = new TreeMap<>();
        final NavigableMap<String, Ast.Exp> map2 = new TreeMap<>();
        record.args.forEach(
            (name, exp) -> {
              final Unifier.Variable vArg = unifier.variable();
              final Ast.Exp e2 = deduceType(env, exp, vArg);
              labelTypes.put(name, vArg);
              map2.put(name, e2);
            });
        if (record.with == null) {
          return reg(record.copy(null, map2), v, record(labelTypes));
        } else {
          final Unifier.Variable v3 = unifier.variable();
          final Ast.Exp with2 = deduceType(env, record.with, v3);
          return reg(record.copy(with2, map2), v, v3);
        }

      case LET:
        final Ast.Let let = (Ast.Let) node;
        termMap = new LinkedHashMap<>();
        TypeEnv env2 = env;
        final List<Ast.Decl> decls = new ArrayList<>();
        for (Ast.Decl decl : let.decls) {
          decls.add(deduceDeclType(env2, decl, termMap));
          env2 = bindAll(env2, termMap);
          termMap.clear();
        }
        final Ast.Exp e2 = deduceType(env2, let.exp, v);
        final Ast.Let let2 = let.copy(decls, e2);
        return reg(let2, null, v);

      case RECORD_SELECTOR:
        final Ast.RecordSelector recordSelector = (Ast.RecordSelector) node;
        throw new RuntimeException(
            "Error: unresolved flex record\n"
                + "   (can't tell what fields there are besides #"
                + recordSelector.name
                + ")");

      case IF:
        // TODO: check that condition has type boolean
        // TODO: check that ifTrue has same type as ifFalse
        final Ast.If if_ = (Ast.If) node;
        v2 = unifier.variable();
        final Ast.Exp condition2 = deduceType(env, if_.condition, v2);
        equiv(v2, toTerm(PrimitiveType.BOOL));
        final Ast.Exp ifTrue2 = deduceType(env, if_.ifTrue, v);
        final Ast.Exp ifFalse2 = deduceType(env, if_.ifFalse, v);
        final Ast.If if2 = if_.copy(condition2, ifTrue2, ifFalse2);
        return reg(if2, null, v);

      case CASE:
        return deduceCaseType(env, (Ast.Case) node, v);

      case FROM:
      case EXISTS:
      case FORALL:
        // "(from exp: v50 as id: v60 [, exp: v51 as id: v61]...
        //  [where filterExp: v5] [yield yieldExp: v4]): v"
        // "(exists exp: v50 as id: v60 [, exp: v51 as id: v61]...
        //  [where filterExp: v5] [yield yieldExp: v4]): v" (v boolean)
        // "(forall exp: v50 as id: v60 [, exp: v51 as id: v61]...
        //   require requireExp: v21): v" (v boolean)
        final Ast.Query query = (Ast.Query) node;
        Unifier.Variable v3 = unifier.variable();
        TypeEnv env3 = env;
        final Map<Ast.Id, Unifier.Variable> fieldVars = new LinkedHashMap<>();
        final List<Ast.FromStep> fromSteps = new ArrayList<>();
        for (Ord<Ast.FromStep> step : Ord.zip(query.steps)) {
          Pair<TypeEnv, Unifier.Variable> p =
              deduceStepType(env, step.e, v3, env3, fieldVars, fromSteps);
          switch (step.e.op) {
            case COMPUTE:
            case INTO:
            case REQUIRE:
              if (step.e.op == Op.REQUIRE && query.op != Op.FORALL
                  || step.e.op == Op.COMPUTE && query.op != Op.FROM
                  || step.e.op == Op.INTO && query.op != Op.FROM) {
                String message =
                    String.format(
                        "'%s' step must not occur in '%s'",
                        step.e.op.lowerName(), query.op.lowerName());
                throw new CompileException(message, false, step.e.pos);
              }
              if (step.i != query.steps.size() - 1) {
                String message =
                    String.format(
                        "'%s' step must be last in '%s'",
                        step.e.op.lowerName(), query.op.lowerName());
                throw new CompileException(
                    message, false, query.steps.get(step.i + 1).pos);
              }
              break;
          }
          env3 = p.left;
          v3 = p.right;
        }
        if (query.op == Op.FORALL) {
          AstNode step = query.steps.isEmpty() ? query : last(query.steps);
          if (step.op != Op.REQUIRE) {
            throw new CompileException(
                "last step of 'forall' must be 'require'", false, step.pos);
          }
        }
        final Ast.Exp yieldExp2;
        if (query.implicitYieldExp != null) {
          v3 = unifier.variable();
          yieldExp2 = deduceType(env3, query.implicitYieldExp, v3);
        } else {
          requireNonNull(v3);
          yieldExp2 = null;
        }
        final Ast.Query query2 = query.copy(fromSteps, yieldExp2);
        return reg(
            query2,
            v,
            node.op == Op.EXISTS
                ? toTerm(PrimitiveType.BOOL)
                : node.op == Op.FORALL
                    ? toTerm(PrimitiveType.BOOL)
                    : query.isCompute() || query.isInto()
                        ? v3
                        : unifier.apply(LIST_TY_CON, v3));

      case ID:
        final Ast.Id id = (Ast.Id) node;
        final Unifier.Term term =
            env.get(
                typeSystem,
                id.name,
                name ->
                    new CompileException(
                        "unbound variable or constructor: " + name,
                        false,
                        id.pos));
        return reg(id, v, term);

      case FN:
        final Ast.Fn fn = (Ast.Fn) node;
        final Unifier.Variable resultVariable = unifier.variable();
        final List<Ast.Match> matchList = new ArrayList<>();
        for (Ast.Match match : fn.matchList) {
          matchList.add(
              deduceMatchType(env, match, new HashMap<>(), v, resultVariable));
        }
        final Ast.Fn fn2b = fn.copy(matchList);
        return reg(fn2b, null, v);

      case APPLY:
        return deduceApplyType(env, (Ast.Apply) node, v);

      case AT:
      case CARET:
      case COMPOSE:
      case PLUS:
      case MINUS:
      case TIMES:
      case DIVIDE:
      case DIV:
      case MOD:
      case EQ:
      case NE:
      case GE:
      case GT:
      case LE:
      case LT:
      case ELEM:
      case NOT_ELEM:
      case CONS:
      case UNION:
      case INTERSECT:
      case EXCEPT:
        return infix(env, (Ast.InfixCall) node, v);

      case NEGATE:
        return prefix(env, (Ast.PrefixCall) node, v);

      default:
        throw new AssertionError("cannot deduce type for " + node.op);
    }
  }

  private Pair<TypeEnv, Unifier.Variable> deduceStepType(
      TypeEnv env,
      Ast.FromStep step,
      Unifier.Variable v,
      final TypeEnv env2,
      Map<Ast.Id, Unifier.Variable> fieldVars,
      List<Ast.FromStep> fromSteps) {
    requireNonNull(v);
    switch (step.op) {
      case SCAN:
        final Ast.Scan scan = (Ast.Scan) step;
        final Ast.Exp scanExp;
        final boolean eq;
        final Ast.Exp scanExp3;
        final Unifier.Variable v15 = unifier.variable();
        final Unifier.Variable v16 = unifier.variable();
        final Map<Ast.IdPat, Unifier.Term> termMap1 = new HashMap<>();
        if (scan.exp == null) {
          scanExp = null;
          eq = false;
          scanExp3 = null;
        } else if (scan.exp.op == Op.FROM_EQ) {
          scanExp = ((Ast.PrefixCall) scan.exp).a;
          eq = true;
          final Ast.Exp scanExp2 = deduceType(env2, scanExp, v15);
          scanExp3 = ast.fromEq(scanExp2);
        } else {
          scanExp = scan.exp;
          eq = false;
          scanExp3 = deduceType(env2, scanExp, v15);
        }
        final Ast.Pat pat2 = deducePatType(env2, scan.pat, termMap1, null, v16);
        if (scanExp != null) {
          reg(scanExp, v15, eq ? v16 : unifier.apply(LIST_TY_CON, v16));
        }
        TypeEnv env4 = env2;
        for (Map.Entry<Ast.IdPat, Unifier.Term> e : termMap1.entrySet()) {
          env4 = env4.bind(e.getKey().name, e.getValue());
          fieldVars.put(
              ast.id(Pos.ZERO, e.getKey().name),
              (Unifier.Variable) e.getValue());
        }
        v = fieldVar(fieldVars);
        final Ast.Exp scanCondition2;
        if (scan.condition != null) {
          final Unifier.Variable v5 = unifier.variable();
          scanCondition2 = deduceType(env4, scan.condition, v5);
          equiv(v5, toTerm(PrimitiveType.BOOL));
        } else {
          scanCondition2 = null;
        }
        fromSteps.add(scan.copy(pat2, scanExp3, scanCondition2));
        return Pair.of(env4, v);

      case WHERE:
        final Ast.Where where = (Ast.Where) step;
        final Unifier.Variable v5 = unifier.variable();
        final Ast.Exp filter2 = deduceType(env2, where.exp, v5);
        equiv(v5, toTerm(PrimitiveType.BOOL));
        fromSteps.add(where.copy(filter2));
        return Pair.of(env2, v);

      case REQUIRE:
        final Ast.Require require = (Ast.Require) step;
        final Unifier.Variable v21 = unifier.variable();
        final Ast.Exp filter3 = deduceType(env2, require.exp, v21);
        equiv(v21, toTerm(PrimitiveType.BOOL));
        fromSteps.add(require.copy(filter3));
        return Pair.of(env2, v);

      case DISTINCT:
        final Ast.Distinct distinct = (Ast.Distinct) step;
        fromSteps.add(distinct);
        return Pair.of(env2, v);

      case SKIP:
        final Ast.Skip skip = (Ast.Skip) step;
        final Unifier.Variable v11 = unifier.variable();
        final Ast.Exp skipCount = deduceType(env2, skip.exp, v11);
        equiv(v11, toTerm(PrimitiveType.INT));
        fromSteps.add(skip.copy(skipCount));
        return Pair.of(env2, v);

      case TAKE:
        final Ast.Take take = (Ast.Take) step;
        final Unifier.Variable v12 = unifier.variable();
        final Ast.Exp takeCount = deduceType(env2, take.exp, v12);
        equiv(v12, toTerm(PrimitiveType.INT));
        fromSteps.add(take.copy(takeCount));
        return Pair.of(env2, v);

      case YIELD:
        final Ast.Yield yield = (Ast.Yield) step;
        final Unifier.Variable v6 = unifier.variable();
        v = v6;
        final Ast.Exp yieldExp2 = deduceType(env2, yield.exp, v6);
        fromSteps.add(yield.copy(yieldExp2));
        if (yieldExp2.op == Op.RECORD
            && ((Ast.Record) yieldExp2).with == null) {
          final Unifier.Sequence sequence =
              (Unifier.Sequence) map.get(yieldExp2);
          final Ast.Record record2 = (Ast.Record) yieldExp2;
          final TypeEnv[] envs = {env};
          forEach(
              record2.args.keySet(),
              sequence.terms,
              (name, term) -> envs[0] = envs[0].bind(name, term));
          return Pair.of(envs[0], v);
        } else {
          return Pair.of(env2, v);
        }

      case ORDER:
        final Ast.Order order = (Ast.Order) step;
        final List<Ast.OrderItem> orderItems = new ArrayList<>();
        for (Ast.OrderItem orderItem : order.orderItems) {
          orderItems.add(
              orderItem.copy(
                  deduceType(env2, orderItem.exp, unifier.variable()),
                  orderItem.direction));
        }
        fromSteps.add(order.copy(orderItems));
        return Pair.of(env2, v);

      case GROUP:
      case COMPUTE:
        final Ast.Group group = (Ast.Group) step;
        validateGroup(group);
        TypeEnv env3 = env;
        fieldVars.clear();
        final PairList<Ast.Id, Ast.Exp> groupExps = PairList.of();
        for (Map.Entry<Ast.Id, Ast.Exp> groupExp : group.groupExps) {
          final Ast.Id id = groupExp.getKey();
          final Ast.Exp exp = groupExp.getValue();
          final Unifier.Variable v7 = unifier.variable();
          final Ast.Exp exp2 = deduceType(env2, exp, v7);
          reg(id, null, v7);
          env3 = env3.bind(id.name, v7);
          fieldVars.put(id, v7);
          groupExps.add(id, exp2);
        }
        final List<Ast.Aggregate> aggregates = new ArrayList<>();
        for (Ast.Aggregate aggregate : group.aggregates) {
          final Ast.Id id = aggregate.id;
          final Unifier.Variable v8 = unifier.variable();
          reg(id, null, v8);
          final Unifier.Variable v9 = unifier.variable();
          final Ast.Exp aggregateFn2 =
              deduceType(env2, aggregate.aggregate, v9);
          final Ast.Exp arg2;
          final Unifier.Variable v10;
          if (aggregate.argument == null) {
            arg2 = null;
            v10 = v;
          } else {
            v10 = unifier.variable();
            arg2 = deduceType(env2, aggregate.argument, v10);
          }
          reg(aggregate.aggregate, null, v9);
          equiv(
              unifier.apply(FN_TY_CON, unifier.apply(LIST_TY_CON, v10), v8),
              v9);
          env3 = env3.bind(id.name, v8);
          fieldVars.put(id, v8);
          final Ast.Aggregate aggregate2 =
              aggregate.copy(aggregateFn2, arg2, aggregate.id);
          aggregates.add(aggregate2);
          reg(aggregate2, null, v8);
        }
        fromSteps.add(
            step.op == Op.GROUP
                ? group.copy(groupExps, aggregates)
                : ((Ast.Compute) step).copy(aggregates));
        return Pair.of(env3, v);

      case INTO:
        // from i in [1,2,3] into f
        //   f: int list -> string
        //   expression: string
        final Ast.Into into = (Ast.Into) step;
        final Unifier.Variable v13 = unifier.variable();
        final Unifier.Variable v14 = unifier.variable();
        final Ast.Exp intoExp = deduceType(env2, into.exp, v14);
        equiv(
            unifier.apply(FN_TY_CON, unifier.apply(LIST_TY_CON, v), v13), v14);
        fromSteps.add(into.copy(intoExp));
        return Pair.of(EmptyTypeEnv.INSTANCE, v13);

      case THROUGH:
        // from i in [1,2,3] through p in f
        //   f: int list -> string list
        //   expression: string list
        // v: int (i)
        // v20: int list
        // v17: int list -> string list (f)
        // v18: string (p)
        // v19: string list (from i in [1,2,3] through p in f)
        final Ast.Through through = (Ast.Through) step;
        final Unifier.Variable v17 = unifier.variable();
        final Unifier.Variable v18 = unifier.variable();
        final Unifier.Variable v19 = unifier.variable();
        final Unifier.Variable v20 = unifier.variable();
        equiv(unifier.apply(LIST_TY_CON, v), v20);

        final Map<Ast.IdPat, Unifier.Term> termMap = new HashMap<>();
        final Ast.Pat throughPat =
            deducePatType(env, through.pat, termMap, null, v18);
        final Ast.Exp throughExp = deduceType(env2, through.exp, v17);
        equiv(unifier.apply(LIST_TY_CON, v18), v19);
        equiv(unifier.apply(FN_TY_CON, v20, v19), v17);
        fromSteps.add(through.copy(throughPat, throughExp));
        TypeEnv env5 = env;
        fieldVars.clear();
        for (Map.Entry<Ast.IdPat, Unifier.Term> e : termMap.entrySet()) {
          env5 = env5.bind(e.getKey().name, e.getValue());
          fieldVars.put(
              ast.id(Pos.ZERO, e.getKey().name),
              (Unifier.Variable) e.getValue());
        }
        return Pair.of(env5, v18);

      default:
        throw new AssertionError("unknown step type " + step.op);
    }
  }

  /**
   * Validates a {@code Group}. Throws if there are duplicate names among the
   * keys and aggregates.
   */
  private void validateGroup(Ast.Group group) {
    final List<String> names = new ArrayList<>();
    group.groupExps.leftList().forEach(id -> names.add(id.name));
    group.aggregates.forEach(aggregate -> names.add(aggregate.id.name));
    int duplicate = firstDuplicate(names);
    if (duplicate >= 0) {
      throw new RuntimeException(
          "Duplicate field name '" + names.get(duplicate) + "' in group");
    }
  }

  private Unifier.Variable fieldVar(Map<Ast.Id, Unifier.Variable> fieldVars) {
    switch (fieldVars.size()) {
      case 0:
        return equiv(toTerm(PrimitiveType.UNIT), unifier.variable());
      case 1:
        return Iterables.getOnlyElement(fieldVars.values());
      default:
        final TreeMap<String, Unifier.Variable> map = new TreeMap<>();
        fieldVars.forEach((k, v) -> map.put(k.name, v));
        return equiv(record(map), unifier.variable());
    }
  }

  private Unifier.Term record(
      NavigableMap<String, ? extends Unifier.Term> labelTypes) {
    if (labelTypes.isEmpty()) {
      return toTerm(PrimitiveType.UNIT);
    } else if (TypeSystem.areContiguousIntegers(labelTypes.navigableKeySet())
        && labelTypes.size() != 1) {
      return unifier.apply(TUPLE_TY_CON, labelTypes.values());
    } else {
      final StringBuilder b = new StringBuilder(RECORD_TY_CON);
      for (String label : labelTypes.navigableKeySet()) {
        b.append(':').append(label);
      }
      return unifier.apply(b.toString(), labelTypes.values());
    }
  }

  private Unifier.Term tuple(List<Unifier.Term> types) {
    if (types.isEmpty()) {
      return toTerm(PrimitiveType.UNIT);
    } else {
      return unifier.apply(TUPLE_TY_CON, types);
    }
  }

  private Ast.Apply deduceApplyType(
      TypeEnv env, Ast.Apply apply, Unifier.Variable v) {
    final Unifier.Variable vFn = unifier.variable();
    final Unifier.Variable vArg = unifier.variable();
    equiv(unifier.apply(FN_TY_CON, vArg, v), vFn);
    final Ast.Exp arg2;
    if (apply.arg instanceof Ast.RecordSelector) {
      // node is "f #field" and has type "v"
      // "f" has type "vArg -> v" and also "vFn"
      // "#field" has type "vArg" and also "vRec -> vField"
      // When we resolve "vRec" we can then deduce "vField".
      final Unifier.Variable vRec = unifier.variable();
      final Unifier.Variable vField = unifier.variable();
      deduceRecordSelectorType(
          env, vField, vRec, (Ast.RecordSelector) apply.arg);
      arg2 = reg(apply.arg, vArg, unifier.apply(FN_TY_CON, vRec, vField));
    } else {
      arg2 = deduceType(env, apply.arg, vArg);
    }
    final Ast.Exp fn2;
    if (apply.fn instanceof Ast.RecordSelector) {
      // node is "#field arg" and has type "v"
      // "#field" has type "vArg -> v"
      // "arg" has type "vArg"
      // When we resolve "vArg" we can then deduce "v".
      fn2 =
          deduceRecordSelectorType(env, v, vArg, (Ast.RecordSelector) apply.fn);
    } else {
      fn2 = deduceType(env, apply.fn, vFn);
    }
    if (fn2 instanceof Ast.Id) {
      final BuiltIn builtIn = BuiltIn.BY_ML_NAME.get(((Ast.Id) fn2).name);
      if (builtIn != null) {
        builtIn.prefer(t -> preferredTypes.add(v, t));
      }
    }
    return reg(apply.copy(fn2, arg2), null, v);
  }

  private Ast.RecordSelector deduceRecordSelectorType(
      TypeEnv env,
      Unifier.Variable vResult,
      Unifier.Variable vArg,
      Ast.RecordSelector recordSelector) {
    final String fieldName = recordSelector.name;
    actionMap.put(
        vArg,
        (v, t, substitution, termPairs) -> {
          // We now know that the type arg, say "{a: int, b: real}".
          // So, now we can declare that the type of vResult, say "#b", is
          // "real".
          if (t instanceof Unifier.Sequence) {
            final Unifier.Sequence sequence = (Unifier.Sequence) t;
            final List<String> fieldList = fieldList(sequence);
            if (fieldList != null) {
              int i = fieldList.indexOf(fieldName);
              if (i >= 0) {
                final Unifier.Term result2 = substitution.resolve(vResult);
                final Unifier.Term term = sequence.terms.get(i);
                final Unifier.Term term2 = substitution.resolve(term);
                termPairs.accept(result2, term2);
              }
            }
          }
        });
    return recordSelector;
  }

  static List<String> fieldList(final Unifier.Sequence sequence) {
    if (sequence.operator.equals(RECORD_TY_CON)) {
      return ImmutableList.of();
    } else if (sequence.operator.startsWith(RECORD_TY_CON + ":")) {
      final String[] fields = sequence.operator.split(":");
      return skip(Arrays.asList(fields));
    } else if (sequence.operator.equals(TUPLE_TY_CON)) {
      final int size = sequence.terms.size();
      return TupleType.ordinalNames(size);
    } else {
      return null;
    }
  }

  private Ast.Match deduceMatchType(
      TypeEnv env,
      Ast.Match match,
      Map<Ast.IdPat, Unifier.Term> termMap,
      Unifier.Variable argVariable,
      Unifier.Variable resultVariable) {
    final Unifier.Variable vPat = unifier.variable();
    Ast.Pat pat2 = deducePatType(env, match.pat, termMap, null, vPat);
    TypeEnv env2 = bindAll(env, termMap);
    Ast.Exp e2 = deduceType(env2, match.exp, resultVariable);
    Ast.Match match2 = match.copy(pat2, e2);
    return reg(
        match2, argVariable, unifier.apply(FN_TY_CON, vPat, resultVariable));
  }

  private List<Ast.Match> deduceMatchListType(
      TypeEnv env,
      List<Ast.Match> matchList,
      NavigableSet<String> labelNames,
      Unifier.Variable argVariable,
      Unifier.Variable resultVariable) {
    for (Ast.Match match : matchList) {
      if (match.pat instanceof Ast.RecordPat) {
        labelNames.addAll(((Ast.RecordPat) match.pat).args.keySet());
      }
    }
    final List<Ast.Match> matchList2 = new ArrayList<>();
    for (Ast.Match match : matchList) {
      final Map<Ast.IdPat, Unifier.Term> termMap = new HashMap<>();
      final Ast.Pat pat2 =
          deducePatType(env, match.pat, termMap, labelNames, argVariable);
      final TypeEnv env2 = bindAll(env, termMap);
      final Ast.Exp e2 = deduceType(env2, match.exp, resultVariable);
      matchList2.add(match.copy(pat2, e2));
    }
    return matchList2;
  }

  private Ast.Case deduceCaseType(
      TypeEnv env, Ast.Case case_, Unifier.Variable v) {
    final Unifier.Variable v2 = unifier.variable();
    final Ast.Exp e2b = deduceType(env, case_.exp, v2);
    final NavigableSet<String> labelNames = new TreeSet<>();
    final Unifier.Term argType = map.get(e2b);
    if (argType instanceof Unifier.Sequence) {
      final List<String> fieldList = fieldList((Unifier.Sequence) argType);
      if (fieldList != null) {
        labelNames.addAll(fieldList);
      }
    }
    final List<Ast.Match> matchList2 =
        deduceMatchListType(env, case_.matchList, labelNames, v2, v);
    return reg(case_.copy(e2b, matchList2), null, v);
  }

  private AstNode deduceValBindType(
      TypeEnv env,
      Ast.ValBind valBind,
      Map<Ast.IdPat, Unifier.Term> termMap,
      Unifier.Variable vPat) {
    deducePatType(env, valBind.pat, termMap, null, vPat);
    final Ast.Exp e2 = deduceType(env, valBind.exp, vPat);
    final Ast.ValBind valBind2 = valBind.copy(valBind.pat, e2);
    map.put(valBind2, toTerm(PrimitiveType.UNIT));
    return valBind2;
  }

  private static TypeEnv bindAll(
      TypeEnv env, Map<Ast.IdPat, Unifier.Term> termMap) {
    for (Map.Entry<Ast.IdPat, Unifier.Term> entry : termMap.entrySet()) {
      env = env.bind(entry.getKey().name, entry.getValue());
    }
    return env;
  }

  private Ast.Decl deduceDeclType(
      TypeEnv env, Ast.Decl node, Map<Ast.IdPat, Unifier.Term> termMap) {
    switch (node.op) {
      case VAL_DECL:
        return deduceValDeclType(env, (Ast.ValDecl) node, termMap);

      case FUN_DECL:
        final Ast.ValDecl valDecl = toValDecl(env, (Ast.FunDecl) node);
        return deduceValDeclType(env, valDecl, termMap);

      case DATATYPE_DECL:
        final Ast.DatatypeDecl datatypeDecl = (Ast.DatatypeDecl) node;
        return deduceDataTypeDeclType(env, datatypeDecl, termMap);

      default:
        throw new AssertionError(
            "cannot deduce type for " + node.op + " [" + node + "]");
    }
  }

  private Ast.Decl deduceDataTypeDeclType(
      TypeEnv env,
      Ast.DatatypeDecl datatypeDecl,
      Map<Ast.IdPat, Unifier.Term> termMap) {
    final List<Keys.DataTypeKey> keys = new ArrayList<>();
    for (Ast.DatatypeBind bind : datatypeDecl.binds) {
      final Foo foo = new Foo();
      bind.tyVars.forEach(foo::toTypeKey);

      final SortedMap<String, Type.Key> tyCons = new TreeMap<>();
      deduceDatatypeBindType(bind, tyCons);

      keys.add(
          Keys.datatype(
              bind.name.name, Keys.ordinals(foo.tyVarMap.size()), tyCons));
    }
    final List<Type> types = typeSystem.dataTypes(keys);

    forEach(
        datatypeDecl.binds,
        types,
        (datatypeBind, type) -> {
          final DataType dataType =
              (DataType)
                  (type instanceof DataType ? type : ((ForallType) type).type);
          for (Ast.TyCon tyCon : datatypeBind.tyCons) {
            final Type tyConType;
            if (tyCon.type != null) {
              final Type.Key conKey = toTypeKey(tyCon.type);
              tyConType =
                  typeSystem.fnType(conKey.toType(typeSystem), dataType);
            } else {
              tyConType = dataType;
            }
            termMap.put(
                (Ast.IdPat) ast.idPat(tyCon.pos, tyCon.id.name),
                toTerm(tyConType, Subst.EMPTY));
            map.put(tyCon, toTerm(tyConType, Subst.EMPTY));
          }
        });

    map.put(datatypeDecl, toTerm(PrimitiveType.UNIT));
    return datatypeDecl;
  }

  private Ast.Decl deduceValDeclType(
      TypeEnv env, Ast.ValDecl valDecl, Map<Ast.IdPat, Unifier.Term> termMap) {
    final Holder<TypeEnv> envHolder = Holder.of(env);
    final Map<Ast.ValBind, Supplier<Unifier.Variable>> map0 =
        new LinkedHashMap<>();
    //noinspection FunctionalExpressionCanBeFolded
    valDecl.valBinds.forEach(
        b -> map0.put(b, Suppliers.memoize(unifier::variable)::get));
    map0.forEach(
        (valBind, vPatSupplier) -> {
          // If recursive, bind each value (presumably a function) to its type
          // in the environment before we try to deduce the type of the
          // expression.
          if (valDecl.rec && valBind.pat instanceof Ast.IdPat) {
            envHolder.set(
                envHolder
                    .get()
                    .bind(((Ast.IdPat) valBind.pat).name, vPatSupplier.get()));
          }
        });
    final List<Ast.ValBind> valBinds = new ArrayList<>();
    final TypeEnv env2 = envHolder.get();
    map0.forEach(
        (valBind, vPatSupplier) ->
            valBinds.add(
                (Ast.ValBind)
                    deduceValBindType(
                        env2, valBind, termMap, vPatSupplier.get())));
    Ast.Decl node2 = valDecl.copy(valBinds);
    map.put(node2, toTerm(PrimitiveType.UNIT));
    return node2;
  }

  private void deduceDatatypeBindType(
      Ast.DatatypeBind datatypeBind, SortedMap<String, Type.Key> tyCons) {
    Foo foo = new Foo();
    for (Ast.TyCon tyCon : datatypeBind.tyCons) {
      tyCons.put(
          tyCon.id.name,
          tyCon.type == null ? Keys.dummy() : foo.toTypeKey(tyCon.type));
    }
  }

  /** Workspace for converting types to keys. */
  private static class Foo {
    final Map<String, Integer> tyVarMap = new HashMap<>();

    /** Converts an AST type into a type key. */
    Type.Key toTypeKey(Ast.Type type) {
      switch (type.op) {
        case TUPLE_TYPE:
          final Ast.TupleType tupleType = (Ast.TupleType) type;
          return Keys.tuple(toTypeKeys(tupleType.types));

        case RECORD_TYPE:
          final Ast.RecordType recordType = (Ast.RecordType) type;
          final SortedMap<String, Type.Key> argNameTypes = mutableMap();
          final AtomicBoolean progressive = new AtomicBoolean(false);
          recordType.fieldTypes.forEach(
              (name, t) -> {
                if (name.equals(PROGRESSIVE_LABEL)) {
                  progressive.set(true);
                } else {
                  argNameTypes.put(name, toTypeKey(t));
                }
              });
          return progressive.get()
              ? Keys.progressiveRecord(argNameTypes)
              : Keys.record(argNameTypes);

        case FUNCTION_TYPE:
          final Ast.FunctionType functionType = (Ast.FunctionType) type;
          final Type.Key paramType = toTypeKey(functionType.paramType);
          final Type.Key resultType = toTypeKey(functionType.resultType);
          return Keys.fn(paramType, resultType);

        case NAMED_TYPE:
          final Ast.NamedType namedType = (Ast.NamedType) type;
          final List<Type.Key> typeList = toTypeKeys(namedType.types);
          if (namedType.name.equals(LIST_TY_CON) && typeList.size() == 1) {
            // TODO: make 'list' a regular generic type
            return Keys.list(typeList.get(0));
          }
          if (typeList.isEmpty()) {
            return Keys.name(namedType.name);
          } else {
            return Keys.apply(Keys.name(namedType.name), typeList);
          }

        case TY_VAR:
          final Ast.TyVar tyVar = (Ast.TyVar) type;
          return Keys.ordinal(
              tyVarMap.computeIfAbsent(tyVar.name, name -> tyVarMap.size()));

        default:
          throw new AssertionError(
              "cannot convert type " + type + " " + type.op);
      }
    }

    List<Type.Key> toTypeKeys(Iterable<? extends Ast.Type> types) {
      return transformEager(types, this::toTypeKey);
    }
  }

  /**
   * Converts a function declaration to a value declaration. In other words,
   * {@code fun} is syntactic sugar, and this is the de-sugaring machine.
   *
   * <p>For example, {@code fun inc x = x + 1} becomes {@code val rec inc = fn x
   * => x + 1}.
   *
   * <p>If there are multiple arguments, there is one {@code fn} for each
   * argument: {@code fun sum x y = x + y} becomes {@code val rec sum = fn x =>
   * fn y => x + y}.
   *
   * <p>If there are multiple clauses, we generate {@code case}:
   *
   * <pre>
   * {@code fun gcd a 0 = a | gcd a b = gcd b (a mod b)}
   * </pre>
   *
   * <p>becomes
   *
   * <pre>{@code val rec gcd = fn x => fn y =>
   * case (x, y) of
   *     (a, 0) => a
   *   | (a, b) = gcd b (a mod b)}</pre>
   */
  private Ast.ValDecl toValDecl(TypeEnv env, Ast.FunDecl funDecl) {
    final List<Ast.ValBind> valBindList = new ArrayList<>();
    for (Ast.FunBind funBind : funDecl.funBinds) {
      valBindList.add(toValBind(env, funBind));
    }
    return ast.valDecl(funDecl.pos, true, valBindList);
  }

  private Ast.ValBind toValBind(TypeEnv env, Ast.FunBind funBind) {
    final List<Ast.Pat> vars;
    Ast.Exp exp;
    Ast.Type returnType = null;
    if (funBind.matchList.size() == 1) {
      final Ast.FunMatch funMatch = funBind.matchList.get(0);
      exp = funMatch.exp;
      vars = funMatch.patList;
      returnType = funMatch.returnType;
    } else {
      final List<String> varNames =
          MapList.of(
              funBind.matchList.get(0).patList.size(), index -> "v" + index);
      vars = Lists.transform(varNames, v -> ast.idPat(Pos.ZERO, v));
      final List<Ast.Match> matchList = new ArrayList<>();
      Pos prevReturnTypePos = null;
      for (Ast.FunMatch funMatch : funBind.matchList) {
        matchList.add(
            ast.match(
                funMatch.pos, patTuple(env, funMatch.patList), funMatch.exp));
        if (funMatch.returnType != null) {
          if (returnType != null && !returnType.equals(funMatch.returnType)) {
            throw new CompileException(
                "parameter or result constraints of "
                    + "clauses don't agree [tycon mismatch]",
                false,
                prevReturnTypePos.plus(funMatch.pos));
          }
          returnType = funMatch.returnType;
          prevReturnTypePos = funMatch.pos;
        }
      }
      exp = ast.caseOf(Pos.ZERO, idTuple(varNames), matchList);
    }
    if (returnType != null) {
      exp = ast.annotatedExp(exp.pos, exp, returnType);
    }
    final Pos pos = funBind.pos;
    for (Ast.Pat var : Lists.reverse(vars)) {
      exp = ast.fn(pos, ast.match(pos, var, exp));
    }
    return ast.valBind(pos, ast.idPat(pos, funBind.name), exp);
  }

  /**
   * Converts a list of variable names to a variable or tuple.
   *
   * <p>For example, ["x"] becomes "{@code x}" (an {@link Ast.Id}), and ["x",
   * "y"] becomes "{@code (x, y)}" (a {@link Ast.Tuple} of {@link Ast.Id Ids}).
   */
  private static Ast.Exp idTuple(List<String> vars) {
    final List<Ast.Id> idList = Lists.transform(vars, v -> ast.id(Pos.ZERO, v));
    if (idList.size() == 1) {
      return idList.get(0);
    }
    return ast.tuple(Pos.ZERO, idList);
  }

  /** Converts a list of patterns to a singleton pattern or tuple pattern. */
  @SuppressWarnings("SwitchStatementWithTooFewBranches")
  private Ast.Pat patTuple(TypeEnv env, List<Ast.Pat> patList) {
    final List<Ast.Pat> list2 = new ArrayList<>();
    for (int i = 0; i < patList.size(); i++) {
      final Ast.Pat pat = patList.get(i);
      switch (pat.op) {
        case ID_PAT:
          final Ast.IdPat idPat = (Ast.IdPat) pat;
          if (env.has(idPat.name)
              && typeSystem.lookupTyCon(idPat.name) != null) {
            final Unifier.Term term =
                env.get(
                    typeSystem,
                    idPat.name,
                    name ->
                        new RuntimeException(
                            "oops, should have " + idPat.name));
            if (term instanceof Unifier.Sequence
                && ((Unifier.Sequence) term).operator.equals(FN_TY_CON)) {
              list2.add(
                  ast.conPat(
                      idPat.pos,
                      ast.id(idPat.pos, idPat.name),
                      patList.get(++i)));
            } else {
              list2.add(ast.con0Pat(idPat.pos, ast.id(idPat.pos, idPat.name)));
            }
            break;
          }
          // fall through
        default:
          list2.add(pat);
      }
    }
    if (list2.size() == 1) {
      return list2.get(0);
    } else {
      return ast.tuplePat(Pos.sum(list2), list2);
    }
  }

  /**
   * Derives a type term for a pattern, collecting the names of pattern
   * variables.
   *
   * @param env Compile-time environment
   * @param pat Pattern AST
   * @param termMap Map from names to bound terms, populated by this method
   * @param labelNames List of names of labels in this pattern and sibling
   *     patterns in a {@code |} match, or null if not a record pattern
   * @param v Type variable that this method should equate the type term that it
   *     derives for this pattern
   */
  private Ast.Pat deducePatType(
      TypeEnv env,
      Ast.Pat pat,
      Map<Ast.IdPat, Unifier.Term> termMap,
      NavigableSet<String> labelNames,
      Unifier.Variable v) {
    switch (pat.op) {
      case BOOL_LITERAL_PAT:
        return reg(pat, v, toTerm(PrimitiveType.BOOL));

      case CHAR_LITERAL_PAT:
        return reg(pat, v, toTerm(PrimitiveType.CHAR));

      case INT_LITERAL_PAT:
        return reg(pat, v, toTerm(PrimitiveType.INT));

      case REAL_LITERAL_PAT:
        return reg(pat, v, toTerm(PrimitiveType.REAL));

      case STRING_LITERAL_PAT:
        return reg(pat, v, toTerm(PrimitiveType.STRING));

      case ID_PAT:
        final Ast.IdPat idPat = (Ast.IdPat) pat;
        final Pair<DataType, Type.Key> pair1 =
            typeSystem.lookupTyCon(idPat.name);
        if (pair1 != null) {
          // It is a zero argument constructor, e.g. the LESS constructor of the
          // 'order' type.
          final DataType dataType0 = pair1.left;
          return reg(pat, v, toTerm(dataType0, Subst.EMPTY));
        }
        termMap.put(idPat, v);
        // fall through

      case WILDCARD_PAT:
        return reg(pat, null, v);

      case AS_PAT:
        final Ast.AsPat asPat = (Ast.AsPat) pat;
        termMap.put(asPat.id, v);
        deducePatType(env, asPat.pat, termMap, null, v);
        return reg(pat, null, v);

      case ANNOTATED_PAT:
        final Ast.AnnotatedPat annotatedPat = (Ast.AnnotatedPat) pat;
        final Type type = toType(annotatedPat.type, typeSystem);
        deducePatType(env, annotatedPat.pat, termMap, null, v);
        return reg(pat, v, toTerm(type, Subst.EMPTY));

      case TUPLE_PAT:
        final List<Unifier.Term> typeTerms = new ArrayList<>();
        final Ast.TuplePat tuple = (Ast.TuplePat) pat;
        for (Ast.Pat arg : tuple.args) {
          final Unifier.Variable vArg = unifier.variable();
          deducePatType(env, arg, termMap, null, vArg);
          typeTerms.add(vArg);
        }
        return reg(pat, v, tuple(typeTerms));

      case RECORD_PAT:
        // First, determine the set of field names.
        //
        // If the pattern is in a 'case', we know the field names from the
        // argument. But if we are in a function, we require at least one of the
        // patterns to not be a wildcard and not have an ellipsis. For example,
        // in
        //
        //  fun f {a=1,...} = 1 | f {b=2,...} = 2
        //
        // we cannot deduce whether a 'c' field is allowed.
        final Ast.RecordPat recordPat = (Ast.RecordPat) pat;
        final NavigableMap<String, Unifier.Term> labelTerms =
            RecordType.mutableMap();
        if (labelNames == null) {
          labelNames = new TreeSet<>(recordPat.args.keySet());
        }
        final SortedMap<String, Ast.Pat> args = RecordType.mutableMap();
        for (String labelName : labelNames) {
          final Unifier.Variable vArg = unifier.variable();
          labelTerms.put(labelName, vArg);
          final Ast.Pat argPat = recordPat.args.get(labelName);
          if (argPat != null) {
            args.put(
                labelName, deducePatType(env, argPat, termMap, null, vArg));
          }
        }
        final Unifier.Term record = record(labelTerms);
        final Ast.RecordPat recordPat2 =
            recordPat.copy(recordPat.ellipsis, args);
        if (!recordPat.ellipsis) {
          return reg(recordPat2, v, record);
        }
        final Unifier.Variable v2 = unifier.variable();
        equiv(record, v2);
        actionMap.put(
            v,
            (v3, t, substitution, termPairs) -> {
              // We now know the type of the source record, say
              // "{a: int, b: real}". So, now we can fill out the ellipsis.
              assert v == v3;
              if (t instanceof Unifier.Sequence) {
                final Unifier.Sequence sequence = (Unifier.Sequence) t;
                final List<String> fieldList = fieldList(sequence);
                if (fieldList != null) {
                  final NavigableMap<String, Unifier.Term> labelTerms2 =
                      RecordType.mutableMap();
                  forEachIndexed(
                      fieldList,
                      (fieldName, i) -> {
                        if (labelTerms.containsKey(fieldName)) {
                          labelTerms2.put(fieldName, sequence.terms.get(i));
                        }
                      });
                  final Unifier.Term result2 = substitution.resolve(v2);
                  final Unifier.Term term2 = record(labelTerms2);
                  termPairs.accept(result2, term2);
                }
              }
            });
        return reg(recordPat2, null, record);

      case CON_PAT:
        final Ast.ConPat conPat = (Ast.ConPat) pat;
        // e.g. "SOME x" has type "int option", "x" has type "int"
        final Pair<DataType, Type.Key> pair =
            typeSystem.lookupTyCon(conPat.tyCon.name);
        if (pair == null) {
          throw new AssertionError("not found: " + conPat.tyCon.name);
        }
        final DataType dataType = pair.left;
        final Type argType = pair.right.toType(typeSystem);
        final Unifier.Variable vArg = unifier.variable();
        deducePatType(env, conPat.pat, termMap, null, vArg);
        final Unifier.Term argTerm = toTerm(argType, Subst.EMPTY);
        equiv(vArg, argTerm);
        final Unifier.Term term = toTerm(dataType, Subst.EMPTY);
        if (argType instanceof TypeVar) {
          // E.g. Suppose arg is "NODE 'b"
          // (therefore argType is "'b", argTerm is "T7"),
          // datatype is "('a,'b) tree"
          // (therefore term is "tree(T8,T9)").
          // We can say that argTerm (T7) is equivalent to
          // the second type parameter (T9).
          //
          // TODO: handle more complex types, e.g. "NODE (int * 'b)"
          equiv(
              argTerm,
              ((Unifier.Sequence) term).terms.get(((TypeVar) argType).ordinal));
        }
        return reg(pat, v, term);

      case CON0_PAT:
        final Ast.Con0Pat con0Pat = (Ast.Con0Pat) pat;
        final Pair<DataType, Type.Key> pair0 =
            typeSystem.lookupTyCon(con0Pat.tyCon.name);
        if (pair0 == null) {
          throw new AssertionError();
        }
        final DataType dataType0 = pair0.left;
        return reg(pat, v, toTerm(dataType0, Subst.EMPTY));

      case LIST_PAT:
        final Ast.ListPat list = (Ast.ListPat) pat;
        final Unifier.Variable vArg2 = unifier.variable();
        for (Ast.Pat arg : list.args) {
          deducePatType(env, arg, termMap, null, vArg2);
        }
        return reg(list, v, unifier.apply(LIST_TY_CON, vArg2));

      case CONS_PAT:
        final Unifier.Variable elementType = unifier.variable();
        final Ast.InfixPat call = (Ast.InfixPat) pat;
        deducePatType(env, call.p0, termMap, null, elementType);
        deducePatType(env, call.p1, termMap, null, v);
        return reg(call, v, unifier.apply(LIST_TY_CON, elementType));

      default:
        throw new AssertionError("cannot deduce type for pattern " + pat.op);
    }
  }

  /** Registers an infix operator whose type is a given type. */
  private Ast.Exp infix(
      TypeEnv env, Ast.InfixCall call, Unifier.Variable v, Type type) {
    final Unifier.Term term = toTerm(type, Subst.EMPTY);
    final Ast.Exp a0 = deduceType(env, call.a0, v);
    final Ast.Exp a1 = deduceType(env, call.a1, v);
    return reg(call.copy(a0, a1), v, term);
  }

  /** Registers an infix operator. */
  private Ast.Exp infix(TypeEnv env, Ast.InfixCall call, Unifier.Variable v) {
    return deduceType(
        env,
        ast.apply(
            ast.id(Pos.ZERO, call.op.opName),
            ast.tuple(Pos.ZERO, ImmutableList.of(call.a0, call.a1))),
        v);
  }

  /** Registers a prefix operator. */
  private Ast.Exp prefix(TypeEnv env, Ast.PrefixCall call, Unifier.Variable v) {
    return deduceType(
        env, ast.apply(ast.id(Pos.ZERO, call.op.opName), call.a), v);
  }

  private Unifier.Variable equiv(Unifier.Term term, Unifier.Variable v) {
    terms.add(new TermVariable(term, v));
    return v;
  }

  private void equiv(Unifier.Term term, Unifier.Term term2) {
    if (term2 instanceof Unifier.Variable) {
      equiv(term, (Unifier.Variable) term2);
    } else if (term instanceof Unifier.Variable) {
      equiv(term2, (Unifier.Variable) term);
    } else {
      final Unifier.Variable variable = unifier.variable();
      equiv(term, variable);
      equiv(term2, variable);
    }
  }

  private List<Unifier.Term> toTerms(List<? extends Type> types, Subst subst) {
    return transformEager(types, type -> toTerm(type, subst));
  }

  private Unifier.Term toTerm(PrimitiveType type) {
    return unifier.atom(type.moniker);
  }

  private Unifier.Term toTerm(Type type, Subst subst) {
    switch (type.op()) {
      case ID:
        return toTerm((PrimitiveType) type);
      case TY_VAR:
        final Unifier.Variable variable = subst.get((TypeVar) type);
        return variable != null ? variable : unifier.variable();
      case DATA_TYPE:
        final DataType dataType = (DataType) type;
        return unifier.apply(
            dataType.name(), toTerms(dataType.arguments, subst));
      case FUNCTION_TYPE:
        final FnType fnType = (FnType) type;
        return unifier.apply(
            FN_TY_CON,
            toTerm(fnType.paramType, subst),
            toTerm(fnType.resultType, subst));
      case TUPLE_TYPE:
        final TupleType tupleType = (TupleType) type;
        return unifier.apply(
            TUPLE_TY_CON,
            transform(tupleType.argTypes, type1 -> toTerm(type1, subst)));
      case RECORD_TYPE:
        final RecordType recordType = (RecordType) type;
        SortedMap<String, Type> argNameTypes = recordType.argNameTypes;
        if (recordType.isProgressive()) {
          argNameTypes = new TreeMap<>(argNameTypes);
          argNameTypes.put(PROGRESSIVE_LABEL, PrimitiveType.UNIT);
        }
        @SuppressWarnings({"rawtypes", "unchecked"})
        final NavigableSet<String> labelNames =
            (NavigableSet) argNameTypes.keySet();
        final String result;
        if (labelNames.isEmpty()) {
          result = PrimitiveType.UNIT.name();
        } else if (TypeSystem.areContiguousIntegers(labelNames)) {
          result = TUPLE_TY_CON;
        } else {
          final StringBuilder b = new StringBuilder(RECORD_TY_CON);
          for (String label : labelNames) {
            b.append(':').append(label);
          }
          result = b.toString();
        }
        final List<Unifier.Term> args =
            transformEager(argNameTypes.values(), t -> toTerm(t, subst));
        return unifier.apply(result, args);
      case LIST:
        final ListType listType = (ListType) type;
        return unifier.apply(LIST_TY_CON, toTerm(listType.elementType, subst));
      case FORALL_TYPE:
        final ForallType forallType = (ForallType) type;
        Subst subst2 = subst;
        for (int i = 0; i < forallType.parameterCount; i++) {
          subst2 = subst2.plus(typeSystem.typeVariable(i), unifier.variable());
        }
        return toTerm(forallType.type, subst2);
      default:
        throw new AssertionError("unknown type: " + type.moniker());
    }
  }

  /** Empty type environment. */
  enum EmptyTypeEnv implements TypeEnv {
    INSTANCE;

    @Override
    public Unifier.Term get(
        TypeSystem typeSystem,
        String name,
        Function<String, RuntimeException> exceptionFactory) {
      throw exceptionFactory.apply(name);
    }

    @Override
    public boolean has(String name) {
      return false;
    }

    @Override
    public TypeEnv bind(
        String name, Function<TypeSystem, Unifier.Term> termFactory) {
      return new BindTypeEnv(name, termFactory, this);
    }

    @Override
    public String toString() {
      return "[]";
    }
  }

  /** Type environment. */
  interface TypeEnv {
    Unifier.Term get(
        TypeSystem typeSystem,
        String name,
        Function<String, RuntimeException> exceptionFactory);

    boolean has(String name);

    TypeEnv bind(String name, Function<TypeSystem, Unifier.Term> termFactory);

    default TypeEnv bind(String name, Unifier.Term term) {
      return bind(
          name,
          new Function<TypeSystem, Unifier.Term>() {
            @Override
            public Unifier.Term apply(TypeSystem typeSystem) {
              return term;
            }

            @Override
            public String toString() {
              return term.toString();
            }
          });
    }
  }

  /** Pair consisting of a term and a variable. */
  private static class TermVariable {
    final Unifier.Term term;
    final Unifier.Variable variable;

    private TermVariable(Unifier.Term term, Unifier.Variable variable) {
      this.term = term;
      this.variable = variable;
    }

    @Override
    public String toString() {
      return term + " = " + variable;
    }
  }

  /**
   * A type environment that consists of a type environment plus one binding.
   */
  private static class BindTypeEnv implements TypeEnv {
    private final String definedName;
    private final Function<TypeSystem, Unifier.Term> termFactory;
    private final TypeEnv parent;

    BindTypeEnv(
        String definedName,
        Function<TypeSystem, Unifier.Term> termFactory,
        TypeEnv parent) {
      this.definedName = requireNonNull(definedName);
      this.termFactory = requireNonNull(termFactory);
      this.parent = requireNonNull(parent);
    }

    @Override
    public Unifier.Term get(
        TypeSystem typeSystem,
        String name,
        Function<String, RuntimeException> exceptionFactory) {
      for (BindTypeEnv e = this; ; e = (BindTypeEnv) e.parent) {
        if (e.definedName.equals(name)) {
          return e.termFactory.apply(typeSystem);
        }
        if (!(e.parent instanceof BindTypeEnv)) {
          return e.parent.get(typeSystem, name, exceptionFactory);
        }
      }
    }

    @Override
    public boolean has(String name) {
      return name.equals(definedName) || parent.has(name);
    }

    @Override
    public TypeEnv bind(
        String name, Function<TypeSystem, Unifier.Term> termFactory) {
      return new BindTypeEnv(name, termFactory, this);
    }

    @Override
    public String toString() {
      final Map<String, String> map = new LinkedHashMap<>();
      for (BindTypeEnv e = this; ; ) {
        map.putIfAbsent(e.definedName, e.termFactory.toString());
        if (e.parent instanceof BindTypeEnv) {
          e = (BindTypeEnv) e.parent;
        } else {
          return map.toString();
        }
      }
    }
  }

  /**
   * Contains a {@link TypeEnv} and adds to it by calling {@link
   * TypeEnv#bind(String, Function)}.
   */
  private class TypeEnvHolder implements BiConsumer<String, Type> {
    private TypeEnv typeEnv;

    TypeEnvHolder(TypeEnv typeEnv) {
      this.typeEnv = requireNonNull(typeEnv);
    }

    @Override
    public void accept(String name, Type type) {
      typeEnv =
          typeEnv.bind(
              name,
              new Function<TypeSystem, Unifier.Term>() {
                @Override
                public Unifier.Term apply(TypeSystem typeSystem_) {
                  return TypeResolver.this.toTerm(type, Subst.EMPTY);
                }

                @Override
                public String toString() {
                  return type.moniker();
                }
              });
    }
  }

  /** Result of validating a declaration. */
  public static class Resolved {
    public final Environment env;
    public final Ast.Decl originalNode;
    public final Ast.Decl node;
    public final TypeMap typeMap;

    private Resolved(
        Environment env,
        Ast.Decl originalNode,
        Ast.Decl node,
        TypeMap typeMap) {
      this.env = env;
      this.originalNode = requireNonNull(originalNode);
      this.node = requireNonNull(node);
      this.typeMap = requireNonNull(typeMap);
      checkArgument(
          originalNode instanceof Ast.FunDecl
              ? node instanceof Ast.ValDecl
              : originalNode.getClass() == node.getClass());
    }

    static Resolved of(
        Environment env,
        Ast.Decl originalNode,
        Ast.Decl node,
        TypeMap typeMap) {
      return new Resolved(env, originalNode, node, typeMap);
    }

    public Ast.Exp exp() {
      if (node instanceof Ast.ValDecl) {
        final Ast.ValDecl valDecl = (Ast.ValDecl) this.node;
        if (valDecl.valBinds.size() == 1) {
          final Ast.ValBind valBind = valDecl.valBinds.get(0);
          return valBind.exp;
        }
      }
      throw new AssertionError("not an expression: " + node);
    }
  }

  /** Substitution. */
  private abstract static class Subst {
    static final Subst EMPTY = new EmptySubst();

    Subst plus(TypeVar typeVar, Unifier.Variable variable) {
      return new PlusSubst(this, typeVar, variable);
    }

    abstract Unifier.Variable get(TypeVar typeVar);
  }

  /** Empty substitution. */
  private static class EmptySubst extends Subst {
    @Override
    public String toString() {
      return "[]";
    }

    @Override
    Unifier.Variable get(TypeVar typeVar) {
      return null;
    }
  }

  /**
   * Substitution that adds one (type, variable) assignment to a parent
   * substitution.
   */
  private static class PlusSubst extends Subst {
    final Subst parent;
    final TypeVar typeVar;
    final Unifier.Variable variable;

    PlusSubst(Subst parent, TypeVar typeVar, Unifier.Variable variable) {
      this.parent = parent;
      this.typeVar = typeVar;
      this.variable = variable;
    }

    @Override
    Unifier.Variable get(TypeVar typeVar) {
      return typeVar.equals(this.typeVar) ? variable : parent.get(typeVar);
    }

    @Override
    public String toString() {
      final Map<TypeVar, Unifier.Term> map = new LinkedHashMap<>();
      for (PlusSubst e = this; ; ) {
        map.putIfAbsent(e.typeVar, e.variable);
        if (e.parent instanceof PlusSubst) {
          e = (PlusSubst) e.parent;
        } else {
          return map.toString();
        }
      }
    }
  }

  /** Error while deducing type. */
  public static class TypeException extends CompileException {
    public TypeException(String message, Pos pos) {
      super(message, false, pos);
    }
  }

  /**
   * Visitor that expands progressive types if they are used in field
   * references.
   */
  static class FieldExpander extends EnvVisitor {
    static FieldExpander create(TypeSystem typeSystem, Environment env) {
      return new FieldExpander(typeSystem, env, new ArrayDeque<>());
    }

    private FieldExpander(
        TypeSystem typeSystem, Environment env, Deque<FromContext> fromStack) {
      super(typeSystem, env, fromStack);
    }

    @Override
    protected EnvVisitor push(Environment env) {
      return new FieldExpander(typeSystem, env, fromStack);
    }

    @Override
    protected void visit(Ast.Apply apply) {
      super.visit(apply);
      expandField(env, apply);
    }

    @Override
    protected void visit(Ast.Id id) {
      super.visit(id);
      expandField(env, id);
    }

    private @Nullable TypedValue expandField(Environment env, Ast.Exp exp) {
      switch (exp.op) {
        case APPLY:
          final Ast.Apply apply = (Ast.Apply) exp;
          if (apply.fn.op == Op.RECORD_SELECTOR) {
            final Ast.RecordSelector selector = (Ast.RecordSelector) apply.fn;
            final TypedValue typedValue = expandField(env, apply.arg);
            if (typedValue != null) {
              typedValue.discoverField(typeSystem, selector.name);
              return typedValue.fieldValueAs(selector.name, TypedValue.class);
            }
          }
          return null;

        case ID:
          final Binding binding = env.getOpt(((Ast.Id) exp).name);
          if (binding != null && binding.value instanceof TypedValue) {
            return (TypedValue) binding.value;
          }
          // fall through

        default:
          return null;
      }
    }
  }
}

// End TypeResolver.java
