Merge lp:~mgiuca/mars/newtypes into lp:mars

[Matt Giuca]

Ready to merge. All type system changes are complete.

[Matt Giuca (mgiuca)]

review: Approve

=== modified file 'doc/intro.rst'
--- doc/intro.rst	2010-05-07 09:02:21 +0000
+++ doc/intro.rst	2010-05-10 05:50:41 +0000
@@ -192,9 +192,9 @@
 
 .. highlight:: mars
 
-Variables must be explicitly declared, using the :keyword:`var` keyword
-(because Mars doesn't currently have type inference). All declarations must
-come at the top of the function.
+Mars will automatically infer the type of any variable assigned in the body of
+a function. Variables may also be explicitly declared, using the
+:keyword:`var` keyword. All declarations must come at the top of the function.
 
 You can use a while loop just as you might expect. Assignment statements are
 also quite straightforward, using the :keyword:`=` operator, much to the

=== modified file 'doc/ref/procedures.rst'
--- doc/ref/procedures.rst	2009-02-05 23:38:09 +0000
+++ doc/ref/procedures.rst	2010-05-10 05:50:41 +0000
@@ -166,9 +166,21 @@
 Local variables
 ---------------
 
-Mars currently requires all local variables to be declared before use. For
-simplicity, all declarations must appear before any statements. Declarations
-have the following syntax:
+Mars distinguishes between local and global variables. All local variables are
+scoped to the entire procedure body (there is no block scope). A name refers
+to a local variable if and only if it:
+
+* Is a formal parameter, or
+* Is explicitly declared with the :keyword:`var` keyword, or
+* Appears on the left-hand side of an assignment statement, or
+* Appears in a pattern.
+
+Local variables may be given the same name as a global constant or function.
+In this case, the local variable shadows the global constant of the same name.
+
+Local variables may optionally be explicitly declared. For simplicity, all
+declarations must appear before any statements. Declarations have the
+following syntax:
 
 .. productionlist::
    var_decl: "var" `var_name` "::" `type` NEWLINE
@@ -179,8 +191,13 @@
 name as a formal parameter, or if two local variables are declared with the
 same name.
 
-Local variables may be given the same name as a global constant or function.
-In this case, the local variable shadows the global constant of the same name.
+.. Launchpad bug #482947:
+
+It is currently an error to declare a local variable with a type which
+includes a type variable not found in the procedure header. This is generally
+not a useful thing (since type variables are monomorphic; see :ref:`type
+unification <ref-type-unification>`), but if it is desired, the variable
+cannot be explicitly declared.
 
 Local variables (other than parameters) are not initialised with any
 particular value. The compiler is required to guarantee that variables are not
@@ -192,7 +209,7 @@
 ====================
 
 The evaluation of procedures is the heart of the Mars execution model. Mars
-procetures are evaluated eagerly, and arguments are passed by-value.
+procedures are evaluated eagerly, and arguments are passed by-value.
 
 Global constant references
 --------------------------

=== modified file 'doc/ref/types.rst'
--- doc/ref/types.rst	2009-11-23 05:40:42 +0000
+++ doc/ref/types.rst	2010-05-10 05:50:41 +0000
@@ -189,6 +189,130 @@
   * This is a classic "curried style" function, as may be found in Haskell.
   * This type may also be written as :class:`->(a, ->(b, c))`.
 
+.. _ref-type-unification:
+
+Type unification
+----------------
+
+Unification is the main algorithm Mars uses for type checking and type
+inference. For a general overview of unification, see
+`Unification <http://en.wikipedia.org/wiki/Unification>`_ on Wikipedia.
+
+When two or more values are expected to have the same type, their types are
+unified. The specification explicitly states when types should be unified. If
+the two types are the same, they successfully unify. Otherwise, they fail to
+unify, and the program must be rejected (due to a type error).
+
+For example, the type :class:`Int` will unify with the type :class:`Int`, but
+fail to unify with the type :class:`Array(Int)`.
+
+This is complicated by type variables. Each type variable is either **free**,
+**bound** or **rigid**.
+
+* A **free** type variable *a* will successfully unify with any type *t*, but
+  once unified, *a* is bound to *t* for the entirety of the function.
+* A **bound** type variable *a*, bound to type *t*, will unify with *s* if and
+  only if *t* unifies with *s*.
+* A **rigid** type variable *a* is never bound, and unifies only with *a*.
+
+For example, the type :class:`a` (if *a* is a free type variable) will unify
+with the type :class:`Int`, but result in *a* being bound to :class:`Int`. In
+future unifications within the same function, :class:`a` will unify only with
+:class:`Int`.
+
+Type variables explicitly named in the header or body of a procedure are
+**rigid**, and will not unify with any type other than themselves. For
+example, this code is invalid::
+
+ def to_int(x :: a) :: Int:
+     return x                # Type error
+
+It is invalid because the header specifies that the caller may pass an
+argument of non-:class:`Int` type, but in that case, it won't be able to
+return an :class:`Int`. Thus the type variable *a* is rigid; the procedure is
+only valid if *a* is not unified with any other type.
+
+Non-rigid type variables are introduced by implicitly-typed variables (for
+type inference) or by expressions with polymorphic types (such as the empty
+array literal, or global variables and functions with polymorphic types). For
+example::
+
+ def singleton(x :: Int) :: Array(Int):
+     v = []
+     return array_add(v, x)
+
+In this example, the variable `v` is given the free type variable *a* when it
+is first assigned. During the call to :func:`array_add`, its type is unified
+with :class:`Int`. It would be a type error to treat `v` as a different type
+elsewhere, even though it hasn't got any data in it (once its type is bound,
+it is bound for the entire body of the function; type variables in Mars are
+*monomorphic*), as in the following example::
+
+ def monomorphic(x :: Int) :: Array(Int):
+     v = []
+     r = array_add(v, x)
+     w = array_add(v, [1])   # Type error
+     return r
+
+The unification rules are as follows (note all rules are symmetric):
+
+* Type variable *a* unifies with type *t* with the rules as above (regardless
+  of whether *t* is a type name, a type variable or a type application). If
+  successful, this results in variable *a* becoming bound.
+* Type name *x* unifies with type name *x*, and no other type name.
+* Type names do not unify with type applications.
+* Type application *t* ( *t1*, ..., *tn* ) unifies with type application *s*
+  ( *s1*, ..., *sn* ) if and only if *t* unifies with *s* and *ti* unifies
+  with *si* for all *i* <= *n*. Any bindings made in the recursive
+  unifications apply.
+
+Polymorphism in global constants
+++++++++++++++++++++++++++++++++
+
+The example above shows that type variables in Mars are monomorphic. This is
+true only for local variables. As a special rule, global constants (including
+functions and data constructors) in Mars are polymorphic, meaning they can be
+given a different binding upon each use.
+
+The type of each global constant is "generalised" by taking each type variable
+in its original type, and universally quantifying it. A variable of type *t*
+containing type variables *a1*, ..., *an* is generalised as "∀ *a1*, ...,
+*an*. *t*"
+
+A successful unification of a type with a universal quantification will *not*
+cause the quantified variables to become bound, so they may be unified again
+as a free variable.
+
+The example above can be "fixed" by making `v` a global constant::
+
+ def v :: Array(a) = []
+
+ def monomorphic(x :: Int) :: Array(Int):
+     r = array_add(v, x)
+     w = array_add(v, [1])
+     return r
+
+Now `v` has type :class:`∀a. Array(a)`. The first unification between
+:class:`∀a. Array(a)` and :class:`Array(Int)` succeeds without binding *a*.
+Thus, the second unification between :class:`∀a. Array(a)` and
+:class:`Array(Array(Int))` also succeeds.
+
+The polymorphic / monomorphic distinction is important when dealing with
+polymorphic functions. Consider::
+
+ def twomaps(f :: a -> b, g :: a -> c, x :: Array(a)) :: Pair(Array(b), Array(c)):
+     y = array_map(f, x)
+     z = array_map(g, x)
+     return Pair(y, z)
+
+Contrast with::
+
+ def twomaps(f :: a -> b, g :: a -> c, x :: Array(a)) :: Pair(Array(b), Array(c)):
+     mymap = array_map
+     y = mymap(f, x)
+     z = mymap(g, x)     # Type error
+     return Pair(y, z)
+
 Built-In Types
 --------------
 
@@ -266,10 +390,10 @@
 must have a name (an identifier beginning with an uppercase letter), and at
 least one constructor.
 
-A type may optionally have zero or more parameters. If a type does not have
-parameters, its kind is :class:`*`. If a type has *n* parameters, its kind is
-:class:`(*1, *2, ..., *n) -> *`. Any parameter variables may be used in the
-types of the constructor parameters.
+A type may optionally have zero or more type parameters. If a type does not
+have parameters, its kind is :class:`*`. If a type has *n* parameters, its
+kind is :class:`(*1, *2, ..., *n) -> *`. Any parameter variables may be used
+in the types of the constructor parameters.
 
 This statement only creates type constructors of the form
 :class:`(*,*,...,*) -> *`. It is not possible to create a user-defined type
@@ -291,7 +415,30 @@
 Types have one or more constructors. Each constructor has a globally-unique
 name, and zero or more parameters. The constructor declares a
 globally-available function of the same name, which takes the given arguments
-as inputs, and returns a value of the type being declared.
+as inputs, and returns a value of the type being declared. Each constructor
+parameter may optionally have a name. No two parameters of a constructor may
+have the same name. The same parameter name *may* appear in multiple
+constructors, but it MUST have the same type in all constructors.
+
+For example, the following type is illegal, as a constructor has two
+parameters with the same name::
+
+ type Foo:
+     X(v :: Int, v :: Array(Int))        # Error: Duplicate field name
+
+The following type is valid, as the name `v` appears in multiple constructors,
+but has the same type in all instances::
+
+ type Foo:
+     X(u :: Int, v :: Int)
+     Y(v :: Int)
+
+The following type is illegal, as the name `v` appears in multiple
+constructors with differing types::
+
+ type Foo:
+     A(u :: Int, v :: Int)
+     B(v :: Array(Int))                  # Error: Duplicate field name
 
 .. note::
    A constructor without parameters is, in effect, declaring a global

=== modified file 'lib/prelude.mar'
--- lib/prelude.mar	2010-05-06 13:26:56 +0000
+++ lib/prelude.mar	2010-05-10 05:50:41 +0000
@@ -216,8 +216,8 @@
     switch x:
         case Nil:
             return y
-        case Cons(x, xs):
-            return Cons(x, append(xs, y))
+        case Cons(h, t):
+            return Cons(h, append(t, y))
 
 # Returns the index of the first occurence of a particular element in a
 # list, or -1 if not found.

=== modified file 'src/ast_cfg.m'
--- src/ast_cfg.m	2010-05-06 13:13:04 +0000
+++ src/ast_cfg.m	2010-05-10 05:50:41 +0000
@@ -80,10 +80,13 @@
 :- import_module integer.
 :- import_module bool.
 :- import_module require.
+:- import_module varset.
 
 :- import_module cfg.
+:- import_module types.
 :- import_module context.
 :- import_module util.
+:- import_module pretty.
 
 prog_to_cfg(PT, program(Nodes0), program(Nodes)) :-
     prog_nodes_to_cfg(PT, Nodes0, Nodes).
@@ -120,6 +123,26 @@
 def_map_insert_local(Name-_, !DefMap) :-
     map.det_insert(!.DefMap, Name, unbound, !:DefMap).
 
+% Take the union of two type maps. It is an error if they have overlapping
+% keys.
+:- func type_map_union(type_map, type_map) = type_map.
+type_map_union(X, Y) = map.union(
+    %(func(_,_) = _ :- error(string.format(
+    %    "ast_cfg.type_map_union: Keys not disjoint (%s versus %s)",
+    %    [s(string.join_list(", ",
+    %        map(ir.varname_to_string_noescape, map.keys(X)))),
+    %     s(string.join_list(", ",
+    %        map(ir.varname_to_string_noescape, map.keys(Y))))]))),
+    % XXX Possibility of binding the same variable name twice (bug #578068)
+    % For now, just allow overlapping keys, and take the first (should always
+    % be the same type anyway)
+    (func(Z,_) = Z),
+    X, Y).
+
+% Take the union of all the type maps in a list.
+:- func type_map_union_list(list(type_map)) = type_map.
+type_map_union_list(Ts) = foldl(type_map_union, Ts, map.init).
+
 func_to_cfg(PT, !Func) :-
     % Create a new defmap with all of the params.
     new_def_map(DefMap0),
@@ -127,33 +150,41 @@
     (
         % No parameters
         Params = no,
-        DefMap = DefMap0
+        DefMap = DefMap0,
+        Types = map.init
     ;
         Params = yes(YesParams),
-        foldl(def_map_insert_param, YesParams, DefMap0, DefMap)
+        foldl(def_map_insert_param, YesParams, DefMap0, DefMap),
+        Types = map.from_assoc_list(map(func({N,T,_}) = svname(N)-T,
+                                        YesParams))
     ),
-    func_body_to_cfg(PT, DefMap, !.Func ^ func_context, !.Func ^ func_body,
-        CFGBody),
+    func_body_to_cfg(PT, DefMap, !.Func^func_varset, Types,
+        !.Func ^ func_context, !.Func ^ func_body, CFGBody),
     !:Func = !.Func ^ func_body := CFGBody.
 
 % Note: def_map argument should have all of the function's parameters already
-% bound in the map.
-:- pred func_body_to_cfg(progtable::in, def_map::in, context::in,
-    func_body::in, func_body::out) is det.
-func_body_to_cfg(_PT, _DefMap, _Ctx, B@func_builtin, B).
-func_body_to_cfg(_PT, _DefMap, _Ctx, B@func_body_cfg(_,_), B).
-func_body_to_cfg(PT, DefMap0, Ctx, func_body_ast(Decls,Stmts), NewFuncBody) :-
-    NewFuncBody = 'new func_body_cfg'(Decls, CFG),
+% bound in the map. Likewise, type_map should have the type of each of the
+% function's parameters' types.
+:- pred func_body_to_cfg(progtable::in, def_map::in, varset::in, type_map::in,
+    context::in, func_body::in, func_body::out) is det.
+func_body_to_cfg(_PT, _DefMap, _Varset, _Types, _Ctx, B@func_builtin, B).
+func_body_to_cfg(_PT, _DefMap, _Vset, _Types, _Ctx, B@func_body_cfg(_,_), B).
+func_body_to_cfg(PT, DefMap0, Varset, Types0, Ctx,
+    func_body_ast(Decls0,Stmts), NewFuncBody):-
+    NewFuncBody = 'new func_body_cfg'(Types, CFG),
     % Insert all of the function's locals into the defmap, unbound
-    foldl(def_map_insert_local, Decls, DefMap0, DefMap),
-    ast_to_cfg(PT, DefMap, Ctx, Stmts, CFG).
+    foldl(def_map_insert_local, Decls0, DefMap0, DefMap),
+    ast_to_cfg(PT, DefMap, Ctx, Stmts, Types1, CFG),
+    Types_Raw = type_map_union(Types0, Types1),
+    % Dereference all the types
+    map.map_values_only(types.deref(Varset), Types_Raw, Types).
 
 % ast_to_cfg(DefMap, Stmts, CFG) converts a statement block (AST form) to a
 % control flow graph, translating the code.
 % This also performs error checking (see func_to_cfg).
 :- some [S] pred ast_to_cfg(progtable::in, def_map::in, context::in,
-    stmt_block::in, cfg(S)::out) is det.
-ast_to_cfg(PT, DefMap, Ctx, Stmts, CFG) :-
+    stmt_block::in, type_map::out, cfg(S)::out) is det.
+ast_to_cfg(PT, DefMap, Ctx, Stmts, Types, CFG) :-
     some [!CFG]
     (
         % Need to create the entry block and exit block so that
@@ -162,7 +193,7 @@
         !:CFG = cfg.new_cfg,
         Entry = cfg.get_entry(!.CFG),
         Exit = cfg.get_exit(!.CFG),
-        stmt_block_to_cfg(PT, Stmts, Entry, Exit, DefMap,
+        stmt_block_to_cfg(PT, Stmts, Entry, Exit, DefMap, Types,
             map.init,AfterPredMap, map.init, ExitPredMap, !CFG),
         % The union of AfterPredMap and ExitPredMap contains information about
         % all predecessors to Exit. Use this to compute phi instructions for
@@ -228,6 +259,10 @@
 % have a key in the map.
 :- type subscript_map == map(varname, int).
 
+% type_map
+% Map SSA variable names to types.
+:- type type_map == map(varname, typeval).
+
 % new_ssa_variable(BlockID, VarName, QualVarName, !SubscriptMap, !DefMap).
 % Given an unqualified variable name, produces a new qualified variable name
 % which is unique, and updates the subscript map accordingly.
@@ -404,6 +439,10 @@
         )
     ;
         % Disagreement. See if the variable is bound for all predecessors.
+        % XXX This assumes that all predecessors have an entry in the PredMap,
+        % which is only true for all predecessors in which this variable was
+        % in-scope (this is only true because Mars has no block-level scopes,
+        % but wasn't always true -- see Launchpad bug #567082).
         ( foldl((pred(X-bound(V)::in, Map0::in, Map::out) is semidet :-
             map.set(Map0, X, V, Map)),
             PredAssoc, map.init, BoundAssoc) ->
@@ -459,7 +498,7 @@
         map.det_insert(!.Map, U, TVMap, !:Map)
     ).
 
-% stmt_block_to_cfg(+Stmts, +BBCurrent, +BBAfter, +DefMap,
+% stmt_block_to_cfg(+Stmts, +BBCurrent, +BBAfter, +DefMap, -Types,
 %   !AfterPredMap, !ExitPredMap, !CFG).
 % Compiles a statement block into basic blocks. Begins inserting statements
 % into BBCurrent, and may create more blocks as necessary.
@@ -471,39 +510,41 @@
 % AfterPredMap contains information about predecessors to the BBAfter block --
 % this may append to the map information about blocks which branch to BBAfter,
 % for the purpose of computing phis.
+% Returns the types of all assigned variables in Types.
 % Throws a context error if there is an attempt to read from a variable which
 % may not have been assigned on some or all code paths.
 :- pred stmt_block_to_cfg(progtable::in, stmt_block::in, bbref(S)::in,
-    bbref(S)::in, def_map::in, pred_map(S)::in, pred_map(S)::out,
-    pred_map(S)::in, pred_map(S)::out, cfg(S)::in, cfg(S)::out)
-    is det.
-stmt_block_to_cfg(PT, Stmts, BBCurrent, BBAfter, DefMap, !AfterPredMap,
-    !ExitPredMap, !CFG) :-
+    bbref(S)::in, def_map::in, type_map::out,
+    pred_map(S)::in, pred_map(S)::out, pred_map(S)::in, pred_map(S)::out,
+    cfg(S)::in, cfg(S)::out) is det.
+stmt_block_to_cfg(PT, Stmts, BBCurrent, BBAfter, DefMap, Types,
+    !AfterPredMap, !ExitPredMap, !CFG) :-
     map.init(SubscriptMap),
     stmt_block_to_cfg(PT, Stmts, BBCurrent, BBAfter, SubscriptMap, DefMap,
-        !AfterPredMap, !ExitPredMap, !CFG).
+        Types, !AfterPredMap, !ExitPredMap, !CFG).
 
 :- pred stmt_block_to_cfg(progtable::in, stmt_block::in, bbref(S)::in,
-    bbref(S)::in,
-    subscript_map::in, def_map::in, pred_map(S)::in, pred_map(S)::out,
+    bbref(S)::in, subscript_map::in, def_map::in, type_map::out,
+    pred_map(S)::in, pred_map(S)::out,
     pred_map(S)::in, pred_map(S)::out, cfg(S)::in, cfg(S)::out) is det.
-stmt_block_to_cfg(_PT, [], BBCurrent, BBAfter, _SubscriptMap, DefMap,
-    !AfterPredMap, !ExitPredMap, !CFG) :-
+stmt_block_to_cfg(_PT, [], BBCurrent, BBAfter, _SubscriptMap,
+    DefMap, map.init, !AfterPredMap, !ExitPredMap, !CFG) :-
     % Special case for empty block - just branch to BBAfter.
     add_to_pred_map(BBCurrent, DefMap, BBAfter, !AfterPredMap, !CFG),
     cfg.set_terminator(BBCurrent, branch(BBAfter, blank_context), !CFG).
-stmt_block_to_cfg(PT, [S], BBCurrent, BBAfter, SubscriptMap, DefMap,
+stmt_block_to_cfg(PT, [S], BBCurrent, BBAfter, SubscriptMap, DefMap, Types,
     !AfterPredMap, !ExitPredMap, !CFG) :-
     % Base-case for the last statement in a block - compile statement into
     % BBCurrent, but end up by branching to BBAfter.
-    stmt_to_cfg_last(PT, S, BBCurrent, BBAfter, SubscriptMap, DefMap,
+    stmt_to_cfg_last(PT, S, BBCurrent, BBAfter, SubscriptMap, DefMap, Types,
         !AfterPredMap, !ExitPredMap, !CFG).
-stmt_block_to_cfg(PT, [S|Ss@[_|_]], BBCurrent, BBAfter, SubscriptMap0,DefMap0,
-    !AfterPredMap, !ExitPredMap, !CFG) :-
+stmt_block_to_cfg(PT, [S|Ss@[_|_]], BBCurrent, BBAfter, SubscriptMap0,
+    DefMap0, Types, !AfterPredMap, !ExitPredMap, !CFG) :-
     % Compile a single statement into BBCurrent. BBContinue is the block to
     % compile subsequent statements into (may be equal to BBCurrent).
-    stmt_to_cfg(PT, S, BBCurrent, BBContinue, Terminated,
-        SubscriptMap0, SubscriptMap, DefMap0, DefMap, !ExitPredMap, !CFG),
+    stmt_to_cfg(PT, S, BBCurrent, BBContinue, Terminated, Types0,
+        SubscriptMap0, SubscriptMap, DefMap0, DefMap, !ExitPredMap,
+        !CFG),
     % Compile subsequent statements into BBContinue, if not terminated.
     % If Terminated is 'yes', the rest of this block is inaccessible, so DO
     % NOT generate code for it. This doesn't just save time -- it is NECESSARY
@@ -511,16 +552,18 @@
     % contain local variables -- this can cause malformed code generation --
     % see bug #517403.
     (
-        Terminated = yes
+        Terminated = yes,
+        Types = Types0
     ;
         Terminated = no,
         stmt_block_to_cfg(PT, Ss, BBContinue, BBAfter, SubscriptMap, DefMap,
-            !AfterPredMap, !ExitPredMap, !CFG)
+            Types1, !AfterPredMap, !ExitPredMap, !CFG),
+        Types = type_map_union(Types0, Types1)
     ).
 
 %%% HIGH-LEVEL STATEMENT-COMPILATION PREDICATES %%%
 
-% stmt_to_cfg(+Stmt, +BBCurrent, -BBAfter, -Terminated, !SubscriptMap,
+% stmt_to_cfg(+Stmt, +BBCurrent, -BBAfter, -Terminated, -Types, !SubscriptMap,
 %     !DefMap, !ExitPredMap, !CFG).
 % Compiles a single statement into basic blocks. Assumes this statement is NOT
 % the last statement in its containing block (if it is, no harm, but may
@@ -537,18 +580,18 @@
 % and therefore, the rest of the block is inaccessible.
 % May also update def_map with any new variable definitions.
 :- pred stmt_to_cfg(progtable::in, stmt::in, bbref(S)::in, bbref(S)::out,
-        bool::out, subscript_map::in, subscript_map::out,
+        bool::out, type_map::out, subscript_map::in, subscript_map::out,
         def_map::in, def_map::out, pred_map(S)::in, pred_map(S)::out,
         cfg(S)::in, cfg(S)::out) is det.
-stmt_to_cfg(_PT, basic_stmt(S,Ctx), !BBRef, no, !SubscriptMap, !DefMap,
+stmt_to_cfg(_PT, basic_stmt(S,Ctx), !BBRef, no, Types, !SubscriptMap, !DefMap,
     !ExitPredMap, !CFG) :-
-    basic_stmt_to_cfg(S, Ctx, !.BBRef, !SubscriptMap, !DefMap, !CFG).
-stmt_to_cfg(PT, compound_stmt(S,Ctx), BBCurrent, BBAfter, Terminated,
+    basic_stmt_to_cfg(S, Ctx, !.BBRef, Types, !SubscriptMap, !DefMap, !CFG).
+stmt_to_cfg(PT, compound_stmt(S,Ctx), BBCurrent, BBAfter, Terminated, Types,
     !SubscriptMap, !DefMap, !ExitPredMap, !CFG) :-
     % Generate a target block for the compound statement to branch to
     cfg.new_basic_block(BBAfter, !CFG),
     compound_stmt_to_cfg(PT, S, Ctx, BBCurrent, BBAfter, !.SubscriptMap,
-        !.DefMap, map.init, AfterPredMap, !ExitPredMap, !CFG),
+        !.DefMap, Types, map.init, AfterPredMap, !ExitPredMap, !CFG),
     % AfterPredMap contains information about all predecessors to BBAfter.
     % Use this to compute phi instructions for BBAfter and update DefMap.
     AfterID = ref_id(BBAfter, !.CFG),
@@ -564,7 +607,7 @@
     cfg.set_phis(BBAfter, Phis, !CFG).
 
 % stmt_to_cfg_last(+Stmt, +BBCurrent, +BBAfter, +SubscriptMap, +DefMap,
-%     !AfterPredMap, !ExitPredMap, !CFG).
+%     -Types, !AfterPredMap, !ExitPredMap, !CFG).
 % Special version of stmt_to_cfg, used on the last statement in a statement
 % block to avoid generating redundant empty basic blocks.
 % Inserts the statement into BBCurrent, and ensures BBCurrent is complete.
@@ -576,31 +619,41 @@
 % May update DefMap with new bindings, but SubscriptMap is read-only (since it
 % will definitely branch to a new block).
 :- pred stmt_to_cfg_last(progtable::in, stmt::in, bbref(S)::in, bbref(S)::in,
-    subscript_map::in, def_map::in, pred_map(S)::in, pred_map(S)::out,
-    pred_map(S)::in, pred_map(S)::out, cfg(S)::in, cfg(S)::out) is det.
+    subscript_map::in, def_map::in, type_map::out,
+    pred_map(S)::in, pred_map(S)::out, pred_map(S)::in, pred_map(S)::out,
+    cfg(S)::in, cfg(S)::out) is det.
 stmt_to_cfg_last(_PT, basic_stmt(S,Ctx), BBCurrent, BBAfter, SubscriptMap,
-    DefMap, !AfterPredMap, !ExitPredMap, !CFG) :-
-    basic_stmt_to_cfg(S, Ctx, BBCurrent, SubscriptMap, _, DefMap, NewDefMap,
-        !CFG),
+    DefMap, Types, !AfterPredMap, !ExitPredMap, !CFG) :-
+    basic_stmt_to_cfg(S, Ctx, BBCurrent, Types, SubscriptMap, _, DefMap,
+        NewDefMap, !CFG),
     % Branch to the provided BBAfter
     add_to_pred_map(BBCurrent, NewDefMap, BBAfter, !AfterPredMap, !CFG),
     cfg.set_terminator(BBCurrent, branch(BBAfter, Ctx), !CFG).
 stmt_to_cfg_last(PT, compound_stmt(S,Ctx), BBCurrent, BBAfter, SubscriptMap,
-    DefMap, !AfterPredMap, !ExitPredMap, !CFG) :-
+    DefMap, Types, !AfterPredMap, !ExitPredMap, !CFG) :-
     compound_stmt_to_cfg(PT, S, Ctx, BBCurrent, BBAfter, SubscriptMap,
-        DefMap, !AfterPredMap, !ExitPredMap, !CFG).
+        DefMap, Types, !AfterPredMap, !ExitPredMap, !CFG).
 
 %%% LOW-LEVEL STATEMENT-COMPILATION PREDICATES %%%
 % Either of the above two statement compilation predicates may call either of
 % the two low-level predicates, which handle the compilation of each statement
 % kind.
 
-% exprs_to_instrs(+BlockID, +Ctx, +Exprs, -VarNames, -Instrs, !SubscriptMap).
+% Put an expression's type in a singleton typemap bound to V.
+% Raises an error if the expression has no type annotation.
+:- func expr_typemap(varname, expr) = type_map.
+expr_typemap(_, E@expr(_,no)) = _ :-
+        error("ast_cfg: Expression has no associated type: " ++
+              pretty.string_expr(E)).
+expr_typemap(V, expr(_, yes(T))) = map.from_assoc_list([V-T]).
+
+% exprs_to_instrs(+BlockID, +Ctx, +Exprs, -VarNames, -Instrs, -Types,
+%   !SubscriptMap).
 :- pred exprs_to_instrs(int::in, context::in, list(expr)::in,
-    list(varname)::out, list(instr)::out,
+    list(varname)::out, list(instr)::out, type_map::out,
     subscript_map::in, subscript_map::out) is det.
-exprs_to_instrs(BlockID, Ctx, Es, VarNames, Instrs, !SubscriptMap) :-
-    exprs_to_instrs_(BlockID, Ctx, Es, [], VarNamesRev, [], LLInstrsRev,
+exprs_to_instrs(BlockID, Ctx, Es, VarNames, Instrs, Types, !SubscriptMap) :-
+    exprs_to_instrs_(BlockID, Ctx, Es, Types, [], VarNamesRev, [],LLInstrsRev,
         !SubscriptMap),
     list.reverse(VarNamesRev, VarNames),
     list.reverse(LLInstrsRev, LLInstrs),
@@ -611,144 +664,176 @@
 % (so it ends up reversed).
 % Instrs is a list of lists (to be flattened). The outer list is reversed, the
 % inner list is not -- this is to allow prepending.
-:- pred exprs_to_instrs_(int::in, context::in, list(expr)::in,
+:- pred exprs_to_instrs_(int::in, context::in, list(expr)::in, type_map::out,
     list(varname)::in, list(varname)::out,
     list(list(instr))::in, list(list(instr))::out,
     subscript_map::in, subscript_map::out) is det.
-exprs_to_instrs_(_BlockID, _Ctx, [], !VarNames, !Instrs, !SubscriptMap).
-exprs_to_instrs_(BlockID, Ctx, [E|Es], !VarNames, !Instrs, !SubscriptMap) :-
+exprs_to_instrs_(_BlockID, _Ctx, [], map.init, !VarNames, !Instrs,
+                 !SubscriptMap).
+exprs_to_instrs_(BlockID,Ctx,[E|Es],Types,!VarNames,!Instrs,!SubscriptMap) :-
     % Create a new variable name and generate instructions for each expr
-    expr_to_instrs(BlockID, Ctx, E, V, Is, !SubscriptMap),
+    expr_to_instrs(BlockID, Ctx, E, V, Is, Types0, !SubscriptMap),
     !:VarNames = [V | !.VarNames],
     !:Instrs = [Is | !.Instrs],     % Do not flatten Is; keep as list of lists
-    exprs_to_instrs_(BlockID, Ctx, Es, !VarNames, !Instrs, !SubscriptMap).
+    exprs_to_instrs_(BlockID, Ctx, Es, Types1, !VarNames, !Instrs,
+                     !SubscriptMap),
+    Types = type_map_union(Types0, Types1).
 
 % expr_to_instrs(+BlockID, +Ctx, +Expr, -VarName, -Instrs, !SubscriptMap).
 % Converts a single expression into a sequence of low-level instructions
 % which compute the expression and assign it to a variable (possibly a
 % new temporary variable name). Returns the assigned variable name in VarName.
 :- pred expr_to_instrs(int::in, context::in, expr::in, varname::out,
-    list(instr)::out, subscript_map::in, subscript_map::out) is det.
-expr_to_instrs(BlockID, Ctx, E, V, Is, !SubscriptMap) :-
+    list(instr)::out, type_map::out, subscript_map::in, subscript_map::out)
+    is det.
+expr_to_instrs(BlockID, Ctx, E, V, Is, Types, !SubscriptMap) :-
     (E = expr(varref(Var), _) ->
         % Special case -- expr_to_instrs_as will generate a mov.
         % We can avoid this by not generating a temp var, and just returning
         % the variable name (with no instructions at all).
         V = Var,
-        Is = []
+        Is = [],
+        Types = map.init
     ;
         new_temp_variable(BlockID, V, !SubscriptMap),
-        expr_to_instrs_as(BlockID, Ctx, E, V, Is, !SubscriptMap)
+        expr_to_instrs_as(BlockID, Ctx, E, V, Is, Types, !SubscriptMap)
     ).
 
 expr_to_instrs(E, V, Is) :-
-    expr_to_instrs(0, context.blank_context, E, V, Is, map.init, _).
+    expr_to_instrs(0, context.blank_context, E, V, Is, _, map.init, _).
 
-% expr_to_instrs_as(+BlockID, +Ctx, +Expr, +VarName, -Instrs, !SubscriptMap).
+% expr_to_instrs_as(+BlockID, +Ctx, +Expr, +VarName, -Instrs, -Types,
+%   !SubscriptMap).
 % Like expr_to_instrs, but it assigns to a specific VarName as given.
 % (This is less efficient as it may generate a mov instruction).
 :- pred expr_to_instrs_as(int::in, context::in, expr::in, varname::in,
-    list(instr)::out, subscript_map::in, subscript_map::out) is det.
-expr_to_instrs_as(_BlockID, Ctx, expr(intlit(Val),_), V, Is, !SubscriptMap) :-
+    list(instr)::out, type_map::out, subscript_map::in, subscript_map::out)
+    is det.
+expr_to_instrs_as(_BlockID, Ctx, E@expr(intlit(Val),_), V, Is, Types,
+    !SubscriptMap) :-
+    Types = expr_typemap(V, E),
     Is = [instr(ld_intlit(V, Val), Ctx)].
-expr_to_instrs_as(BlockID, Ctx, expr(arraylit(Elems0),_), V, Is,
+expr_to_instrs_as(BlockID, Ctx, E@expr(arraylit(Elems0),_), V, Is, Types,
     !SubscriptMap) :-
-    exprs_to_instrs(BlockID, Ctx, Elems0, Elems, Is0, !SubscriptMap),
+    ( varname_is_global(V) ->
+        % Don't assign types to global variables
+        Types0 = map.init
+    ;
+        Types0 = expr_typemap(V, E)
+    ),
+    exprs_to_instrs(BlockID, Ctx, Elems0, Elems, Is0, Types1, !SubscriptMap),
+    Types = type_map_union(Types0, Types1),
     Is = Is0 ++ [instr(ld_arraylit(V, Elems), Ctx)].
-expr_to_instrs_as(_BlockID, Ctx, expr(varref(Var),_), V, Is, !SubscriptMap) :-
+expr_to_instrs_as(_BlockID, Ctx, E@expr(varref(Var),_), V, Is, Types,
+    !SubscriptMap) :-
+    Types = expr_typemap(V, E),
     Is = [instr(mov(V, Var), Ctx)].
-expr_to_instrs_as(_BlockID, Ctx, expr(ctorref(Name),_), V, Is,
+expr_to_instrs_as(_BlockID, Ctx, E@expr(ctorref(Name),_), V, Is, Types,
     !SubscriptMap) :-
+    Types = expr_typemap(V, E),
     Is = [instr(ld_ctor(V, Name), Ctx)].
-expr_to_instrs_as(BlockID, Ctx, expr(fieldref(Obj0, Field),_), V, Is,
+expr_to_instrs_as(BlockID, Ctx, E@expr(fieldref(Obj0, Field),_), V, Is, Types,
     !SubscriptMap) :-
-    expr_to_instrs(BlockID, Ctx, Obj0, Obj, Is0, !SubscriptMap),
+    Types0 = expr_typemap(V, E),
+    expr_to_instrs(BlockID, Ctx, Obj0, Obj, Is0, Types1, !SubscriptMap),
+    Types = type_map_union(Types0, Types1),
     Is = Is0 ++ [instr(ld_field(V, Obj, Field), Ctx)].
-expr_to_instrs_as(BlockID, Ctx, expr(app(Func0, Args0),_), V, Is,
+expr_to_instrs_as(BlockID, Ctx, E@expr(app(Func0, Args0),_), V, Is, Types,
     !SubscriptMap) :-
-    expr_to_instrs(BlockID, Ctx, Func0, Func, Is0, !SubscriptMap),
-    exprs_to_instrs(BlockID, Ctx, Args0, Args, Is1, !SubscriptMap),
+    Types0 = expr_typemap(V, E),
+    expr_to_instrs(BlockID, Ctx, Func0, Func, Is0, Types1, !SubscriptMap),
+    exprs_to_instrs(BlockID, Ctx, Args0, Args, Is1, Types2, !SubscriptMap),
+    Types = type_map_union(Types0, type_map_union(Types1, Types2)),
     Is2 = [instr(call(V, Func, Args), Ctx)],
     Is = Is0 ++ Is1 ++ Is2.
-expr_to_instrs_as(BlockID, Ctx, expr(parapp(Func0, Args0),_), V, Is,
+expr_to_instrs_as(BlockID, Ctx, E@expr(parapp(Func0, Args0),_), V, Is, Types,
     !SubscriptMap) :-
-    expr_to_instrs(BlockID, Ctx, Func0, Func, Is0, !SubscriptMap),
-    exprs_to_instrs(BlockID, Ctx, Args0, Args, Is1, !SubscriptMap),
+    Types0 = expr_typemap(V, E),
+    expr_to_instrs(BlockID, Ctx, Func0, Func, Is0, Types1, !SubscriptMap),
+    exprs_to_instrs(BlockID, Ctx, Args0, Args, Is1, Types2, !SubscriptMap),
+    Types = type_map_union(Types0, type_map_union(Types1, Types2)),
     Is2 = [instr(parcall(V, Func, Args), Ctx)],
     Is = Is0 ++ Is1 ++ Is2.
 
 basic_stmt_to_instrs(BasicStmt, Instrs) :-
-    basic_stmt_to_instrs(0, BasicStmt, context.blank_context, Instrs,
+    basic_stmt_to_instrs(0, BasicStmt, context.blank_context, _, Instrs,
         map.init, _).
 
-% basic_stmt_to_instrs(+BlockID, +BasicStmt, +Ctx, -Instrs, !SubscriptMap).
+% basic_stmt_to_instrs(+BlockID, +BasicStmt, +Ctx, -Types, -Instrs,
+%   !SubscriptMap).
 % Converts a single basic statement into a sequence of low-level instructions
 % which do the same thing. This will potentially assign many temporary
 % variables.
 :- pred basic_stmt_to_instrs(int::in, basic_stmt::in, context::in,
-    list(instr)::out, subscript_map::in, subscript_map::out) is det.
-basic_stmt_to_instrs(_BlockID, pass, _Ctx, [], !SubscriptMap).
-basic_stmt_to_instrs(BlockID, assign(V, E), Ctx, Is, !SubscriptMap) :-
-    expr_to_instrs_as(BlockID, Ctx, E, V, Is, !SubscriptMap).
-basic_stmt_to_instrs(BlockID, fieldset(Obj0, Field, Val0), Ctx, Is,
+    type_map::out, list(instr)::out, subscript_map::in, subscript_map::out)
+    is det.
+basic_stmt_to_instrs(_BlockID, pass, _Ctx, map.init, [], !SubscriptMap).
+basic_stmt_to_instrs(BlockID, assign(V, E), Ctx, Types, Is, !SubscriptMap) :-
+    expr_to_instrs_as(BlockID, Ctx, E, V, Is, Types, !SubscriptMap).
+basic_stmt_to_instrs(BlockID, fieldset(Obj0, Field, Val0), Ctx, Types, Is,
     !SubscriptMap) :-
-    expr_to_instrs(BlockID, Ctx, Obj0, Obj, Is0, !SubscriptMap),
-    expr_to_instrs(BlockID, Ctx, Val0, Val, Is1, !SubscriptMap),
+    expr_to_instrs(BlockID, Ctx, Obj0, Obj, Is0, Types0, !SubscriptMap),
+    expr_to_instrs(BlockID, Ctx, Val0, Val, Is1, Types1, !SubscriptMap),
+    Types = type_map_union(Types0, Types1),
     Is2 = [instr(i_fieldset(Obj, Field, Val), Ctx)],
     Is = Is0 ++ Is1 ++ Is2.
-basic_stmt_to_instrs(BlockID, fieldreplace(Obj0, Field, Val0), Ctx, Is,
+basic_stmt_to_instrs(BlockID, fieldreplace(Obj0, Field, Val0), Ctx, Types, Is,
     !SubscriptMap) :-
     % XXX fieldreplace statement is very weird (should be an expr).
     % Currently re-assign to the same variable.
-    expr_to_instrs(BlockID, Ctx, Obj0, Obj, Is0, !SubscriptMap),
-    expr_to_instrs(BlockID, Ctx, Val0, Val, Is1, !SubscriptMap),
+    expr_to_instrs(BlockID, Ctx, Obj0, Obj, Is0, Types0, !SubscriptMap),
+    expr_to_instrs(BlockID, Ctx, Val0, Val, Is1, Types1, !SubscriptMap),
+    Types = type_map_union(Types0, Types1),
     Is2 = [instr(i_fieldreplace(Obj, Obj, Field, Val), Ctx)],
     Is = Is0 ++ Is1 ++ Is2.
-basic_stmt_to_instrs(BlockID, eval(E), Ctx, Is, !SubscriptMap) :-
+basic_stmt_to_instrs(BlockID, eval(E), Ctx, Types, Is, !SubscriptMap) :-
     % The variable _T is assigned to, then thrown away.
-    expr_to_instrs(BlockID, Ctx, E, _T, Is, !SubscriptMap).
+    expr_to_instrs(BlockID, Ctx, E, _T, Is, Types, !SubscriptMap).
 
-% basic_stmt_to_cfg(+BasicStmt, +Ctx, +BBCurrent, !SubscriptMap, !DefMap,
-%   !CFG).
+% basic_stmt_to_cfg(+BasicStmt, +Ctx, +BBCurrent, -Types, !SubscriptMap,
+%   !DefMap, !CFG).
 % Compiles a single basic statement into a basic block. Appends the statement
 % to the end of BBCurrent. May also update SubscriptMap and DefMap with any
 % newly-defined variables.
 :- pred basic_stmt_to_cfg(basic_stmt::in, context::in, bbref(S)::in,
-    subscript_map::in, subscript_map::out, def_map::in, def_map::out,
-    cfg(S)::in, cfg(S)::out) is det.
+    type_map::out, subscript_map::in, subscript_map::out,
+    def_map::in, def_map::out, cfg(S)::in, cfg(S)::out) is det.
 % "pass" statements disappear at this point
-basic_stmt_to_cfg(pass, _Ctx, _BBCurrent, !SubscriptMap, !DefMap, !CFG).
-basic_stmt_to_cfg(assign(Var0, E0), Ctx, BBCurrent, !SubscriptMap, !DefMap,
-    !CFG) :-
+basic_stmt_to_cfg(pass, _Ctx, _BBCurrent, map.init, !SubscriptMap, !DefMap,
+    !CFG).
+basic_stmt_to_cfg(assign(Var0, E0), Ctx, BBCurrent, Types, !SubscriptMap,
+    !DefMap, !CFG) :-
     apply_def_map_to_expr(!.DefMap, Ctx, E0, E),
     BlockID = ref_id(BBCurrent, !.CFG),
     new_ssa_variable(BlockID, Var0, Var, !SubscriptMap, !DefMap),
-    basic_stmt_to_instrs(BlockID, assign(Var, E), Ctx, Instrs, !SubscriptMap),
+    basic_stmt_to_instrs(BlockID, assign(Var, E), Ctx, Types, Instrs,
+                         !SubscriptMap),
     cfg.append_instrs(BBCurrent, Instrs, !CFG).
-basic_stmt_to_cfg(fieldset(Target0,FieldName,Expr0), Ctx, BBCurrent,
+basic_stmt_to_cfg(fieldset(Target0,FieldName,Expr0), Ctx, BBCurrent, Types,
     !SubscriptMap, !DefMap, !CFG) :-
     apply_def_map_to_expr(!.DefMap, Ctx, Target0, Target),
     apply_def_map_to_expr(!.DefMap, Ctx, Expr0, Expr),
     BlockID = ref_id(BBCurrent, !.CFG),
     basic_stmt_to_instrs(BlockID, fieldset(Target, FieldName, Expr), Ctx,
-        Instrs, !SubscriptMap),
+        Types, Instrs, !SubscriptMap),
     cfg.append_instrs(BBCurrent, Instrs, !CFG).
 basic_stmt_to_cfg(fieldreplace(Target0,FieldName,Expr0), Ctx, BBCurrent,
-    !SubscriptMap, !DefMap, !CFG) :-
+    Types, !SubscriptMap, !DefMap, !CFG) :-
     apply_def_map_to_expr(!.DefMap, Ctx, Target0, Target),
     apply_def_map_to_expr(!.DefMap, Ctx, Expr0, Expr),
     BlockID = ref_id(BBCurrent, !.CFG),
     basic_stmt_to_instrs(BlockID, fieldreplace(Target, FieldName, Expr), Ctx,
-        Instrs, !SubscriptMap),
+        Types, Instrs, !SubscriptMap),
     cfg.append_instrs(BBCurrent, Instrs, !CFG).
-basic_stmt_to_cfg(eval(E0), Ctx, BBCurrent, !SubscriptMap, !DefMap, !CFG) :-
+basic_stmt_to_cfg(eval(E0), Ctx, BBCurrent, Types, !SubscriptMap, !DefMap,
+    !CFG) :-
     apply_def_map_to_expr(!.DefMap, Ctx, E0, E),
     BlockID = ref_id(BBCurrent, !.CFG),
-    basic_stmt_to_instrs(BlockID, eval(E), Ctx, Instrs, !SubscriptMap),
+    basic_stmt_to_instrs(BlockID, eval(E), Ctx, Types, Instrs, !SubscriptMap),
     cfg.append_instrs(BBCurrent, Instrs, !CFG).
 
 % compound_stmt_to_cfg(+CompoundStmt, +Ctx, +BBCurrent, +BBAfter,
-%   +SubscriptMap, +DefMap, !AfterPredMap, !ExitPredMap, !CFG).
+%   +SubscriptMap, +DefMap, -Types, !AfterPredMap, !ExitPredMap, !CFG).
 % Compiles a single compound statement into a basic block. Appends statements
 % to the end of BBCurrent and completes that block (with a terminator). May
 % generate new basic blocks, and ensures they are complete as well.
@@ -761,30 +846,33 @@
 % DefMap is read-only (the resulting def-maps should be appended to
 % AfterPredMap).
 :- pred compound_stmt_to_cfg(progtable::in, compound_stmt::in, context::in,
-    bbref(S)::in, bbref(S)::in, subscript_map::in, def_map::in,
+    bbref(S)::in, bbref(S)::in, subscript_map::in, def_map::in, type_map::out,
     pred_map(S)::in, pred_map(S)::out, pred_map(S)::in, pred_map(S)::out,
     cfg(S)::in, cfg(S)::out) is det.
 compound_stmt_to_cfg(_PT,return(Expr), Ctx, BBCurrent, _BBAfter, SubscriptMap,
-    DefMap0, !AfterPredMap, !ExitPredMap, !CFG) :-
+    DefMap0, Types, !AfterPredMap, !ExitPredMap, !CFG) :-
     % Return is expressed in CFG as $RET = expr, followed by a branch to the
     % exit block.
-    basic_stmt_to_cfg(assign(retvname, Expr), Ctx, BBCurrent,
+    basic_stmt_to_cfg(assign(retvname, Expr), Ctx, BBCurrent, Types,
         SubscriptMap, _, DefMap0, DefMap, !CFG),
     ExitBlock = cfg.get_exit(!.CFG),
     add_to_pred_map(BBCurrent, DefMap, ExitBlock, !ExitPredMap, !CFG),
     cfg.set_terminator(BBCurrent, branch(ExitBlock, Ctx), !CFG).
 compound_stmt_to_cfg(PT, switch(Ctrl0, Cases0), Ctx, BBCurrent, BBAfter,
-    SubscriptMap, DefMap, !AfterPredMap, !ExitPredMap, !CFG) :-
+    SubscriptMap, DefMap, Types, !AfterPredMap, !ExitPredMap, !CFG) :-
     % Calculate the condition expression at the end of BBCurrent
     apply_def_map_to_expr(DefMap, Ctx, Ctrl0, Ctrl),
     BlockID = ref_id(BBCurrent, !.CFG),
-    expr_to_instrs(BlockID, Ctx, Ctrl, CtrlVar, CtrlInstrs, SubscriptMap, _),
+    expr_to_instrs(BlockID, Ctx, Ctrl, CtrlVar, CtrlInstrs, Types0,
+                   SubscriptMap, _),
     cfg.append_instrs(BBCurrent, CtrlInstrs, !CFG),
     % Convert all patterns to use SSA variables, and generate CFG code for the
     % bodies of all case statements. The resulting Cases contains goto
     % statements for each generated block.
     list.map_foldl3(case_stmt_to_jmp(PT,BBCurrent,BBAfter,SubscriptMap,DefMap),
-        Cases0, Cases, !AfterPredMap, !ExitPredMap, !CFG),
+        Cases0, CasesTypes, !AfterPredMap, !ExitPredMap, !CFG),
+    Cases = map(fst, CasesTypes),
+    Types = type_map_union_list([Types0|map(snd, CasesTypes)]),
     % Now begin switch factoring transformation
     % Convert each case statement to a matcher (flatten the patterns)
     Matchers = list.map(case_to_matcher, Cases),
@@ -793,35 +881,39 @@
         SubscriptMap, Ctx, map.init, PhiTable, !CFG),
     map.foldl(generate_case_block_phis, PhiTable, !CFG).
 compound_stmt_to_cfg(PT, if_then_else(Cond0,ThenPart,ElsePart), Ctx,BBCurrent,
-    BBAfter, SubscriptMap, DefMap, !AfterPredMap, !ExitPredMap, !CFG) :-
+    BBAfter, SubscriptMap, DefMap, Types, !AfterPredMap, !ExitPredMap,
+    !CFG) :-
     % Calculate the condition expression at the end of BBCurrent
     apply_def_map_to_expr(DefMap, Ctx, Cond0, Cond),
     BlockID = ref_id(BBCurrent, !.CFG),
-    expr_to_instrs(BlockID, Ctx, Cond, CondVar, CondInstrs, SubscriptMap, _),
+    expr_to_instrs(BlockID, Ctx, Cond, CondVar, CondInstrs, Types0,
+                   SubscriptMap, _),
     cfg.append_instrs(BBCurrent, CondInstrs, !CFG),
     % Create a new basic block for the "then" part.
     cfg.new_basic_block(ThenEnter, !CFG),
     cfg.append_predecessor(ThenEnter, BBCurrent, !CFG),
-    stmt_block_to_cfg(PT, ThenPart, ThenEnter, BBAfter, DefMap, !AfterPredMap,
-        !ExitPredMap, !CFG),
+    stmt_block_to_cfg(PT, ThenPart, ThenEnter, BBAfter, DefMap, Types1,
+        !AfterPredMap, !ExitPredMap, !CFG),
     ( list.is_empty(ElsePart) ->
         % Branch straight to the "after" block if the condition fails
         add_to_pred_map(BBCurrent, DefMap, BBAfter, !AfterPredMap, !CFG),
         cfg.set_terminator(BBCurrent,
-            cond_branch(CondVar,ThenEnter,BBAfter,Ctx), !CFG)
+            cond_branch(CondVar,ThenEnter,BBAfter,Ctx), !CFG),
+        Types = type_map_union(Types0, Types1)
     ;
         % Create a new basic block for the "else" part.
         cfg.new_basic_block(ElseEnter, !CFG),
         cfg.append_predecessor(ElseEnter, BBCurrent, !CFG),
-        stmt_block_to_cfg(PT, ElsePart, ElseEnter, BBAfter, DefMap,
+        stmt_block_to_cfg(PT, ElsePart, ElseEnter, BBAfter, DefMap, Types2,
             !AfterPredMap, !ExitPredMap, !CFG),
         % Have the current block terminate by branching into the then/else
         % blocks
         cfg.set_terminator(BBCurrent,
-            cond_branch(CondVar,ThenEnter,ElseEnter,Ctx), !CFG)
+            cond_branch(CondVar,ThenEnter,ElseEnter,Ctx), !CFG),
+        Types = type_map_union(Types0, type_map_union(Types1, Types2))
     ).
 compound_stmt_to_cfg(PT, while(Cond0, Body), Ctx, BBCurrent, BBAfter,
-    SubscriptMap, DefMap, !AfterPredMap, !ExitPredMap, !CFG) :-
+    SubscriptMap, DefMap, Types, !AfterPredMap, !ExitPredMap, !CFG) :-
     % Create a new basic block for the condition and body
     cfg.new_basic_block(CondBlock, !CFG),
     cfg.new_basic_block(BodyEnter, !CFG),
@@ -840,7 +932,7 @@
 
     % Do the whole fixpoint. Updates CFG by setting CondBlock's phis, and
     % compiling Body.
-    while_fixpoint(PT, CondBlock, BodyEnter, Body, CondBlockPredMap,
+    while_fixpoint(PT, CondBlock, BodyEnter, Body, CondBlockPredMap, Types0,
         !ExitPredMap, DefMap, CondBlockDefMap, !CFG),
 
     % CondBlock branches to BodyBlock or BBAfter, based on the condition
@@ -853,36 +945,38 @@
     % Calculate the condition expression at the end of CondBlock
     apply_def_map_to_expr(CondBlockDefMap, Ctx, Cond0, Cond),
     BlockID = ref_id(CondBlock, !.CFG),
-    expr_to_instrs(BlockID, Ctx, Cond, CondVar, CondInstrs, SubscriptMap, _),
+    expr_to_instrs(BlockID, Ctx, Cond, CondVar, CondInstrs, Types1,
+                   SubscriptMap, _),
+    Types = type_map_union(Types0, Types1),
     cfg.append_instrs(CondBlock, CondInstrs, !CFG),
     cfg.set_terminator(CondBlock, cond_branch(CondVar,BodyEnter,BBAfter,Ctx),
                        !CFG).
 
-% while_fixpoint(CondBlock, BodyEnter, Body, CondPredMap, !ExitPredMap,
-%   !DefMap, !CFG).
+% while_fixpoint(CondBlock, BodyEnter, Body, CondPredMap, -Types,
+%   !ExitPredMap, !DefMap, !CFG).
 % Does fixpoint iteration over the condition and body block of the while loop
 % until they agree on the phi nodes for the condition block.
 % Updates the CFG as follows:
 %  - Sets the phis of CondBlock to the computed phi nodes.
 %  - Compiles the body into BodyEnter, branching to CondBlock.
 :- pred while_fixpoint(progtable::in, bbref(S)::in, bbref(S)::in,
-    stmt_block::in,
-    pred_map(S)::in, pred_map(S)::in, pred_map(S)::out,
+    stmt_block::in, pred_map(S)::in, type_map::out,
+    pred_map(S)::in, pred_map(S)::out,
     def_map::in, def_map::out, cfg(S)::in, cfg(S)::out) is det.
-while_fixpoint(PT, CondBlock, BodyEnter, Body, CondPredMap, !ExitPredMap,
-    !DefMap, !CFG) :-
+while_fixpoint(PT, CondBlock, BodyEnter, Body, CondPredMap, Types,
+    !ExitPredMap, !DefMap, !CFG) :-
     % First iteration, assume there are no phis
-    while_fixpoint_(PT, CondBlock, BodyEnter, Body, CondPredMap, [],
+    while_fixpoint_(PT, CondBlock, BodyEnter, Body, CondPredMap, [], Types,
         !ExitPredMap, !DefMap, !CFG).
 
 :- pred while_fixpoint_(progtable::in, bbref(S)::in, bbref(S)::in,
-    stmt_block::in,
-    pred_map(S)::in, list(phi(S))::in, pred_map(S)::in, pred_map(S)::out,
+    stmt_block::in, pred_map(S)::in, list(phi(S))::in, type_map::out,
+    pred_map(S)::in, pred_map(S)::out,
     def_map::in, def_map::out, cfg(S)::in, cfg(S)::out) is det.
-while_fixpoint_(PT, CondBlock, BodyEnter, Body, CondPredMap0, Phis0,
+while_fixpoint_(PT, CondBlock, BodyEnter, Body, CondPredMap0, Phis0, Types,
     !ExitPredMap, !CondDefMap, !CFG) :-
     % Compute CondPredMap (after another iteration of the body)
-    stmt_block_to_cfg(PT, Body, BodyEnter, CondBlock, !.CondDefMap,
+    stmt_block_to_cfg(PT, Body, BodyEnter, CondBlock, !.CondDefMap, Types0,
         CondPredMap0, CondPredMap, !ExitPredMap, !.CFG, PotentialFinalCFG),
     % Now we can compute the phis for the cond block
     CondBlockID = ref_id(CondBlock, !.CFG),
@@ -892,11 +986,12 @@
         !:CFG = PotentialFinalCFG,
         % Write the phi into the cond block
         cfg.set_phis(CondBlock, Phis, !CFG),
+        Types = Types0,
         !:CondDefMap = CondDefMap1
     ;
         % Now iterate till fixpoint
         while_fixpoint_(PT, CondBlock, BodyEnter, Body, CondPredMap, Phis,
-            !ExitPredMap, CondDefMap1, !:CondDefMap, !CFG)
+            Types, !ExitPredMap, CondDefMap1, !:CondDefMap, !CFG)
     ).
 
 % Intermediate representation of a case statement -- still contains recursive
@@ -1305,8 +1400,8 @@
             cfg.append_phi(TargetBlock, PhiInstr, CFG0, CFG)
         ), Phis, !CFG).
 
-% case_stmt_to_jmp(+BBAfter, +SubscriptMap, +DefMap, +CaseStmt, -CFGCaseStmt,
-%   !AfterPredMap, !ExitPredMap, !CFG).
+% case_stmt_to_jmp(+BBAfter, +SubscriptMap, +DefMap, +CaseStmt,
+%   -(CFGCaseStmt - Types), !AfterPredMap, !ExitPredMap, !CFG).
 % Compiles a case statement into a jmp case statement (which is
 % branch-oriented rather than sub-statement-block-oriented).
 % Compiles the sub-statement-block in the case statement to new basic blocks,
@@ -1319,51 +1414,68 @@
 % DefMap is read-only (the resulting def-maps should be appended to
 % AfterPredMap).
 :- pred case_stmt_to_jmp(progtable::in, bbref(S)::in, bbref(S)::in,
-    subscript_map::in, def_map::in, case_stmt::in, jmp_case_stmt(S)::out,
-    pred_map(S)::in, pred_map(S)::out, pred_map(S)::in, pred_map(S)::out,
-    cfg(S)::in, cfg(S)::out) is det.
+    subscript_map::in, def_map::in, case_stmt::in,
+    pair(jmp_case_stmt(S), type_map)::out, pred_map(S)::in, pred_map(S)::out,
+    pred_map(S)::in, pred_map(S)::out, cfg(S)::in, cfg(S)::out) is det.
 case_stmt_to_jmp(PT, BBCurrent, BBAfter, SubscriptMap, DefMap,
-    case_stmt(Pattern0, Stmts, Ctx), jmp_case_stmt(Pattern, BBFirst, Ctx),
-    !AfterPredMap, !ExitPredMap, !CFG) :-
+    case_stmt(Pattern0, Stmts, Ctx),
+    jmp_case_stmt(Pattern, BBFirst, Ctx) - Types, !AfterPredMap, !ExitPredMap,
+    !CFG) :-
     % Traverse the pattern and uniquely label each newly-introduced
     % variable, as well as adding them to DefMap.
     BlockID = ref_id(BBCurrent, !.CFG),
-    pattern_to_ssa(BlockID, Pattern0, Pattern, SubscriptMap, _, DefMap,
-        InnerScopeDefMap),
+    pattern_to_ssa(BlockID, Pattern0, Pattern-Types0, SubscriptMap, _,
+        DefMap, InnerScopeDefMap),
 
     cfg.new_basic_block(BBFirst, !CFG),
-    stmt_block_to_cfg(PT, Stmts, BBFirst, BBAfter, InnerScopeDefMap,
-        !AfterPredMap, !ExitPredMap, !CFG).
-
-% pattern_to_ssa(BlockID, !Pattern, !SubscriptMap, !DefMap).
+    stmt_block_to_cfg(PT, Stmts, BBFirst, BBAfter, InnerScopeDefMap, Types1,
+        !AfterPredMap, !ExitPredMap, !CFG),
+
+    Types = type_map_union(Types0, Types1).
+
+% pattern_to_ssa(BlockID, +Pattern, -(Pattern-Types), !SubscriptMap, !DefMap).
 % Converts a pattern to SSA form by replacing all of its introduced variables
 % with subscripted SSA variables.
 % BlockID: An int identifying the block the pattern is in (for computing
 % subscripts).
+% Types: Output -- Type map for all bound variables in the pattern.
 % SubscriptMap and DefMap are updated with the new variable definitions.
-:- pred pattern_to_ssa(int::in, pattern::in, pattern::out,
+:- pred pattern_to_ssa(int::in, pattern::in, pair(pattern, type_map)::out,
     subscript_map::in, subscript_map::out, def_map::in, def_map::out) is det.
-pattern_to_ssa(BlockID, pattern(Pat0, PatType), pattern(Pat, PatType),
+pattern_to_ssa(BlockID, pattern(Pat0, PatType), pattern(Pat, PatType) - Types,
     !SubscriptMap, !DefMap) :-
     (
+        PatType = yes(Type)
+    ;
+        PatType = no,
+        error("ast_cfg: Pattern has no associated type: " ++
+              pretty.string_pattern(pattern(Pat0, no)))
+    ),
+    (
         Pat0 = pat_any,
-        Pat = Pat0
+        Pat = Pat0,
+        Types = map.init
     ;
         Pat0 = pat_var(Var0),
         new_ssa_variable(BlockID, Var0, Var, !SubscriptMap, !DefMap),
-        Pat = pat_var(Var)
+        Pat = pat_var(Var),
+        Types = map.from_assoc_list([Var-Type])
     ;
         Pat0 = pat_ctor(CtorName, SubPatterns0),
         (
             SubPatterns0 = yes(YesSubPatterns0),
-            map_foldl2(pattern_to_ssa(BlockID), YesSubPatterns0, SubPatterns,
-                !SubscriptMap, !DefMap),
-            Pat = pat_ctor(CtorName, yes(SubPatterns))
+            map_foldl2(pattern_to_ssa(BlockID), YesSubPatterns0,
+                SubPatternsTypes, !SubscriptMap, !DefMap),
+            SubPatterns = map(fst, SubPatternsTypes),
+            Pat = pat_ctor(CtorName, yes(SubPatterns)),
+            Types = type_map_union_list(map(snd, SubPatternsTypes))
         ;
             SubPatterns0 = no,
-            Pat = pat_ctor(CtorName, no)
+            Pat = pat_ctor(CtorName, no),
+            Types = map.init
         )
     ;
         Pat0 = pat_intlit(_),
-        Pat = Pat0
+        Pat = Pat0,
+        Types = map.init
     ).

=== modified file 'src/builtins.m'
--- src/builtins.m	2009-11-26 08:09:50 +0000
+++ src/builtins.m	2010-05-10 05:50:41 +0000
@@ -110,7 +110,7 @@
 func_eq = function("eq", yes([{"x", types.variable(A), def_argmode},
                               {"y", types.variable(A), def_argmode}]),
                            types.const("Int"),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -119,7 +119,7 @@
 func_is = function("is", yes([{"x", types.variable(A), def_argmode},
                               {"y", types.variable(A), def_argmode}]),
                            types.const("Int"),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -128,7 +128,7 @@
 func_cmp = function("cmp", yes([{"x", types.const("Int"), def_argmode},
                                 {"y", types.const("Int"), def_argmode}]),
                             types.const("Int"),
-                            varset.init,
+                            varset.init, [],
                             func_builtin,
                             ctx).
 
@@ -138,7 +138,7 @@
 func_add = function("add", yes([{"x", types.const("Int"), def_argmode},
                                 {"y", types.const("Int"), def_argmode}]),
                            types.const("Int"),
-                           varset.init,
+                           varset.init, [],
                            func_builtin,
                            ctx).
 
@@ -146,7 +146,7 @@
 func_sub = function("sub", yes([{"x", types.const("Int"), def_argmode},
                                 {"y", types.const("Int"), def_argmode}]),
                            types.const("Int"),
-                           varset.init,
+                           varset.init, [],
                            func_builtin,
                            ctx).
 
@@ -154,7 +154,7 @@
 func_mul = function("mul", yes([{"x", types.const("Int"), def_argmode},
                                 {"y", types.const("Int"), def_argmode}]),
                            types.const("Int"),
-                           varset.init,
+                           varset.init, [],
                            func_builtin,
                            ctx).
 
@@ -162,7 +162,7 @@
 func_div = function("div", yes([{"x", types.const("Int"), def_argmode},
                                 {"y", types.const("Int"), def_argmode}]),
                            types.const("Int"),
-                           varset.init,
+                           varset.init, [],
                            func_builtin,
                            ctx).
 
@@ -170,7 +170,7 @@
 func_mod = function("mod", yes([{"x", types.const("Int"), def_argmode},
                                 {"y", types.const("Int"), def_argmode}]),
                            types.const("Int"),
-                           varset.init,
+                           varset.init, [],
                            func_builtin,
                            ctx).
 
@@ -182,7 +182,7 @@
                                 {"default", types.variable(A), def_argmode}]),
                            types.app(types.const("Array"),
                                [types.variable(A)]),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -194,7 +194,7 @@
                                         [types.variable(A)]), def_argmode},
                                 {"index", types.const("Int"), def_argmode}]),
                            types.variable(A),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -208,7 +208,7 @@
                                 {"value", types.variable(A), def_argmode}]),
                            types.app(types.const("Array"),
                                [types.variable(A)]),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -222,7 +222,7 @@
                                 {"value", types.variable(A), def_argmode}]),
                            types.app(types.const("Array"),
                                [types.variable(A)]),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -233,7 +233,7 @@
                                         types.const("Array"),
                                         [types.variable(A)]), def_argmode}]),
                            types.const("Int"),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -246,7 +246,7 @@
                             {"value", types.variable(A), def_argmode}]),
                            types.app(types.const("Array"),
                                [types.variable(A)]),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -261,7 +261,7 @@
                                         [types.variable(A)]), def_argmode}]),
                            types.app(types.const("Array"),
                                [types.variable(A)]),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -273,7 +273,7 @@
                                         [types.variable(A)]), def_argmode},
                                 {"value", types.variable(A), def_argmode}]),
                            types.app(types.const("Array"), [types.variable(A)]),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -287,7 +287,7 @@
                                         types.const("Array"),
                                         [types.variable(A)]), def_argmode}]),
                            types.app(types.const("Array"), [types.variable(A)]),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -300,7 +300,7 @@
                                 {"index", types.const("Int"), def_argmode}]),
                            types.app(types.const("Array"),
                                [types.variable(A)]),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -313,7 +313,7 @@
                                 {"index", types.const("Int"), def_argmode}]),
                            types.app(types.const("Array"),
                                [types.variable(A)]),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -324,7 +324,7 @@
 func_put_char = function("put_char",
                            yes([{"c", types.const("Int"), def_argmode}]),
                            types.const("Int"),
-                           varset.init,
+                           varset.init, [],
                            func_builtin,
                            ctx).
 
@@ -332,7 +332,7 @@
 func_get_char = function("get_char",
                            yes([]),
                            types.const("Int"),
-                           varset.init,
+                           varset.init, [],
                            func_builtin,
                            ctx).
 
@@ -343,7 +343,7 @@
                                                    def_argmode}]),
                            types.app(types.const("Array"),
                                      [types.const("Int")]),
-                           varset.init,
+                           varset.init, [],
                            func_builtin,
                            ctx).
 
@@ -353,7 +353,7 @@
 func_show = function("show", yes([{"x", types.variable(A), def_argmode}]),
                            types.app(types.const("Array"),
                                [types.const("Int")]),
-                           Varset,
+                           Varset, [],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).
@@ -364,7 +364,7 @@
                                               [types.const("Int")]),
                                               def_argmode}]),
                            types.variable(A),
-                           Varset,
+                           Varset, [A],
                            func_builtin,
                            ctx) :-
     varset.new_named_var(varset.init, "a", A, Varset).

=== modified file 'src/interactive.m'
--- src/interactive.m	2010-05-10 05:10:31 +0000
+++ src/interactive.m	2010-05-10 05:50:41 +0000
@@ -206,7 +206,7 @@
         parsem.parse_expr(Tokens, UserExpr),
         % Get the type of this expression
         typecheck.expr_type(Context, ProgTable, LocalTable,
-            !.State^st_localvarset, Varset, UserExpr, _, Type),
+            !.State^st_localvarset, Varset, [], UserExpr, _, Type),
         io.write_string(pretty.string_expr(UserExpr), !IO),
         io.write_string(" :: ", !IO),
         io.write_string(pretty.string_typeval(Varset, Type), !IO),
@@ -289,14 +289,14 @@
 assignment_update_locals(!BasicStmt, Ctx, !State) :-
     ( !.BasicStmt = assign(Target, Expr0) ->
         typecheck.expr_type(Ctx, !.State^st_progtable, !.State^st_localtable,
-            !.State^st_localvarset, NewVarset, Expr0, Expr, Type),
+            !.State^st_localvarset, NewVarset, [], Expr0, Expr, Type),
         tables.update_localtable(Target, Type, !.State^st_localtable, NewLT),
         !State^st_localvarset := NewVarset,
         !State^st_localtable := NewLT,
         !:BasicStmt = assign(Target, Expr)
     ;
         typecheck.check_basic_stmt(Ctx, !.State^st_progtable,
-            !.State^st_localtable, !.State^st_localvarset, _Varset,
+            !.State^st_localtable, !.State^st_localvarset, _Varset, [],
             !BasicStmt)
         % Note: Do not update localvarset (could do, but there wouldn't be
         % anything useful since we didn't add anything to localtable).

=== modified file 'src/ir.m'
--- src/ir.m	2010-04-28 05:20:46 +0000
+++ src/ir.m	2010-05-10 05:50:41 +0000
@@ -52,6 +52,7 @@
 :- import_module bool.
 :- import_module list.
 :- import_module assoc_list.
+:- import_module map.
 :- import_module maybe.
 :- import_module pair.
 
@@ -298,6 +299,8 @@
                 func_params   :: maybe(list({string, typeval, argmode})),
                 func_ret_type :: typeval,
                 func_varset   :: varset,
+                % Set of type vars which may not be unified in the body
+                func_rigids   :: list(var),
                 func_body     :: func_body,
                 func_context  :: context.context
             ).
@@ -314,7 +317,9 @@
             )
             % The function is represented by a CFG.
     ;       some [S] func_body_cfg(
-                list(pair(varname, typeval)),
+                % Type of each SSA variable and argument. Must not contain any
+                % references to unbound variables (must be dereferenced).
+                map(varname, typeval),
                 cfg(S)
             ).
 
@@ -402,7 +407,6 @@
 :- implementation.
 
 :- import_module int.
-:- import_module map.
 :- import_module require.
 
 :- func tab_width = int.

=== modified file 'src/mars.m'
--- src/mars.m	2010-04-28 05:59:37 +0000
+++ src/mars.m	2010-05-10 05:50:41 +0000
@@ -127,11 +127,11 @@
     MainExpr = expr(varref(svname(MainFuncName)),no),
     % Typecheck this expression (makes sure main exists, and get its type)
     typecheck.expr_type(blank_context, ProgTable, empty_localtable,
-        varset.init, VarSet, MainExpr, _, MainType),
+        varset.init, VarSet, [], MainExpr, _, MainType),
     % Ensure that MainType is () -> Int
     ExpType = app(functype, [const("Int")]),
     typecheck.det_unify(blank_context, MainFuncName, MainExpr, MainType,
-                        ExpType, VarSet, _NewVarset),
+                        ExpType, [], VarSet, _NewVarset),
     % MainInstr is the instruction "$T = MainFuncName()"
     MainInstr = instr(call(tempvname, gvname(MainFuncName), []),
                       context.blank_context),

=== modified file 'src/marsc.m'
--- src/marsc.m	2010-04-28 05:59:37 +0000
+++ src/marsc.m	2010-05-10 05:50:41 +0000
@@ -133,11 +133,11 @@
     MainExpr = expr(varref(svname(MainFunc)),no),
     % Typecheck this expression (makes sure main exists, and get its type)
     typecheck.expr_type(blank_context, PT, empty_localtable,
-        varset.init, VarSet, MainExpr, _, MainType),
+        varset.init, VarSet, [], MainExpr, _, MainType),
     % Ensure that MainType is () -> Int
     ExpType = app(functype, [const("Int")]),
     typecheck.det_unify(blank_context, MainFunc, MainExpr, MainType,
-                        ExpType, VarSet, _NewVarset).
+                        ExpType, [], VarSet, _NewVarset).
 
 % Does the whole program, (taking a filename as input), but does not catch
 % exceptions. Any context.error exceptions will be propagated upwards.

=== modified file 'src/parsem.m'
--- src/parsem.m	2010-03-29 08:58:37 +0000
+++ src/parsem.m	2010-05-10 05:50:41 +0000
@@ -417,7 +417,7 @@
 % Consumes a single function.
 :- pred function(function::out, tokenparser::in, tokenparser::out) is semidet.
 function(
-    function(FuncName, Params, RetType, Varset, Body, Context)) -->
+    function(FuncName, Params, RetType, Varset, Rigids, Body, Context)) -->
     some [!Varset, !VarNames] (
         {varset.init(!:Varset)},
         {map.init(!:VarNames)},
@@ -464,7 +464,12 @@
         ;
             throw_expected("lowercase identifier")
         ),
-        {Varset = !.Varset}
+        {Varset = !.Varset},
+        % The rigid type variables are all those which have been explicitly
+        % named.
+        % (If we support type inference, implicitly-typed variables will not
+        % have names, and should not be rigid, so this logic still applies.)
+        {Rigids = map.values(!.VarNames)}
     ).
 
 % func_param(Param, !Varset, !VarNames, !Parser).

=== modified file 'src/pretty.m'
--- src/pretty.m	2010-01-25 01:42:15 +0000
+++ src/pretty.m	2010-05-10 05:50:41 +0000
@@ -494,7 +494,8 @@
         foldl(print_stmt(Indent+1), Stmts, !IO)
     ;
         Func^func_body = func_body_cfg(Decls, CFG),
-        foldl(print_decl(Indent+1, Func^func_varset), Decls, !IO),
+        foldl(print_decl(Indent+1, Func^func_varset),
+              map.to_assoc_list(Decls), !IO),
         indent(Indent+1, !IO),
         io.write_string("# XXX CFG representation (not valid Mars code)\n",
                         !IO),

=== modified file 'src/tables.m'
--- src/tables.m	2010-04-28 05:29:04 +0000
+++ src/tables.m	2010-05-10 05:50:41 +0000
@@ -129,6 +129,7 @@
 :- import_module require.
 
 :- import_module context.
+:- import_module util.
 
 empty_progtable = progtable(map.init, map.init, map.init).
 empty_localtable = map.init.
@@ -199,7 +200,8 @@
     ( Func^func_body = func_body_ast(Decls,_) ->
         list.foldl(add_to_localtable(Func, "variable"), Decls, !Table)
     ; Func^func_body = func_body_cfg(Decls,_) ->
-        list.foldl(add_to_localtable(Func, "variable"), Decls, !Table)
+        map.foldl(pred(K::in,V::in,A0::in,A::out) is det :-
+            add_to_localtable(Func, "variable", K-V, A0, A), Decls, !Table)
     ;
         true
     ).
@@ -223,6 +225,16 @@
         Table = Table0
     ;
         Args = yes(YesArgs),
+        % Test for duplicate parameter names
+        filter_map(pred(yes(Name)-_::in, Name::out) is semidet,
+                   YesArgs, FieldNames),
+        ( util.list_first_duplicate(FieldNames, DupName) ->
+            % FieldNames contains duplicates
+            context.throw_error("Duplicate field name: " ++ DupName,
+                                Ctor ^ ctor_context)
+        ;
+            true
+        ),
         list.foldl(add_ctor_field_to_fieldtable(Ctor ^ ctor_context),
                    YesArgs, Table0, Table)
     ).

=== modified file 'src/typecheck.m'
--- src/typecheck.m	2010-05-10 05:15:01 +0000
+++ src/typecheck.m	2010-05-10 05:50:41 +0000
@@ -22,7 +22,9 @@
 
 :- interface.
 
+:- import_module list.
 :- import_module varset.
+:- use_module term.
 
 :- import_module ir.
 :- import_module tables.
@@ -42,7 +44,7 @@
 % Otherwise, succeeds. Note that this may bind variables, or create new
 % variables, which will be reflected in the output varset.
 :- pred expr_type(context::in, progtable::in, localtable::in,
-                    varset::in, varset::out,
+                    varset::in, varset::out, list(term.var)::in,
                     expr::in, expr::out, typeval::out)
                     is det.
 
@@ -63,14 +65,14 @@
 % Updates Stmt so its expressions hold their type values.
 % Throws a context.error on reference or type errors.
 :- pred check_stmt(progtable::in, localtable::in, typeval::in,
-                    varset::in, varset::out,
+                    varset::in, varset::out, list(term.var)::in,
                     stmt::in, stmt::out) is det.
 
 % check_basic_stmt(Context, ProgTable, LocalTable, !Varsete, !BasicStmt).
 % Checks to see if a basic statement is type-correct.
 % Does not require a function return type.
 :- pred check_basic_stmt(context::in, progtable::in, localtable::in,
-                    varset::in, varset::out,
+                    varset::in, varset::out, list(term.var)::in,
                     basic_stmt::in, basic_stmt::out) is det.
 
 % check_function(ProgTable, LocalTable, !Function).
@@ -100,7 +102,7 @@
 % Succeeds if they do, and possibly updates varset with new bindings.
 % "What" : see type_error
 :- pred det_unify(context::in, string::in, expr::in, typeval::in, typeval::in,
-                  varset::in, varset::out) is det.
+                  list(term.var)::in, varset::in, varset::out) is det.
 
 % -------------------------------------------------------------------------- %
 % -------------------------------------------------------------------------- %
@@ -112,9 +114,9 @@
 :- import_module string.
 :- import_module maybe.
 :- import_module pair.
-:- import_module list.
 :- import_module set.
 :- import_module svset.
+:- import_module assoc_list.
 :- import_module require.
 
 :- import_module pretty.
@@ -128,21 +130,21 @@
 % "What" : see type_error
 :- pred list_elem_type(context::in, progtable::in, localtable::in, string::in,
                         typeval::in, list(expr)::in, list(expr)::out,
-                        varset::in, varset::out) is det.
-list_elem_type(_Ctx, _PT, _LT, _What, _T1, [], [], !Varset).
-list_elem_type(Ctx, PT, LT, What, T1, [E0|Es0], [E|Es], !Varset) :-
-    expr_type(Ctx, PT, LT, !Varset, E0, E, EType),
-    det_unify(Ctx, What, E, EType, T1, !Varset),
-    list_elem_type(Ctx, PT, LT, What, T1, Es0, Es, !Varset).
+                        list(term.var)::in, varset::in, varset::out) is det.
+list_elem_type(_Ctx, _PT, _LT, _What, _T1, [], [], _Rigids, !Varset).
+list_elem_type(Ctx, PT, LT, What, T1, [E0|Es0], [E|Es], Rigids, !Varset) :-
+    expr_type(Ctx, PT, LT, !Varset, Rigids, E0, E, EType),
+    det_unify(Ctx, What, E, EType, T1, Rigids, !Varset),
+    list_elem_type(Ctx, PT, LT, What, T1, Es0, Es, Rigids, !Varset).
 
 % expr_type for expressions with a computed type.
 % Still check the type, unify to make sure the existing annotation was good,
 % and recurse (bug #578082).
-expr_type(Ctx, PT, LT, !Varset, expr(Expr0,yes(Type)),
+expr_type(Ctx, PT, LT, !Varset, Rigids, expr(Expr0,yes(Type)),
           expr(Expr,yes(Type)), Type) :-
-    expr_type_(Ctx, PT, LT, !Varset, Expr0, Expr, InfType),
+    expr_type_(Ctx, PT, LT, !Varset, Rigids, Expr0, Expr, InfType),
     % Match the existing annotation with the inferred type
-    ( types.unify(Type, InfType, !Varset) ->
+    ( types.unify(Type, InfType, Rigids, !Varset) ->
         true
     ;
         error(string.format("typecheck: Expression %s with existing type "
@@ -153,24 +155,27 @@
     ).
 % expr_type for expressions without a computed type.
 % Compute the type and store it in the output expr.
-expr_type(Ctx, PT, LT, !Varset, expr(Expr0,no), expr(Expr,yes(Type)), Type) :-
-    expr_type_(Ctx, PT, LT, !Varset, Expr0, Expr, Type).
+expr_type(Ctx, PT, LT, !Varset, Rigids, expr(Expr0,no), expr(Expr,yes(Type)),
+          Type) :-
+    expr_type_(Ctx, PT, LT, !Varset, Rigids, Expr0, Expr, Type).
 
 % expr_type_(ProgTable, LocalTable, !Varset, !Expr_, Type).
 % Determines the type of an expr_ (the data structure inside expr).
 :- pred expr_type_(context::in, progtable::in, localtable::in,
-                    varset::in, varset::out,
+                    varset::in, varset::out, list(term.var)::in,
                     expr_::in, expr_::out, typeval::out)
                     is det.
 % Type of intlit is Int.
-expr_type_(_Ctx, _PT, _LT, !Varset, E@intlit(_), E, types.const("Int")).
-expr_type_(Ctx, PT, LT, !Varset, E@arraylit(Elems0), arraylit(Elems),
+expr_type_(_Ctx, _PT, _LT, !Varset, _Rigids, E@intlit(_), E,
+            types.const("Int")).
+expr_type_(Ctx, PT, LT, !Varset, Rigids, E@arraylit(Elems0), arraylit(Elems),
             types.app(types.const("Array"), [ElemType])) :-
     % Find the type of each element. (Type error unless all unify).
     types.new_var(ElemType, !Varset),
     What = "expression '" ++ pretty.string_expr(expr(E,no)) ++ "'",
-    list_elem_type(Ctx, PT, LT, What, ElemType, Elems0, Elems, !Varset).
-expr_type_(Ctx, PT, LT, !Varset, E@varref(VarName), E, Type) :-
+    list_elem_type(Ctx, PT, LT, What, ElemType, Elems0, Elems, Rigids,
+                   !Varset).
+expr_type_(Ctx, PT, LT, !Varset, _Rigids, E@varref(VarName), E, Type) :-
     ( tables.lookup_local(LT, VarName, Type_) ->
         % Found in local table
         Type = Type_
@@ -187,7 +192,7 @@
         context.throw_error("Undefined variable: "
             ++ ir.varname_to_string_noescape(VarName), Ctx)
     ).
-expr_type_(Ctx, PT, _LT, !Varset, E@ctorref(VarName), E, Type) :-
+expr_type_(Ctx, PT, _LT, !Varset, _Rigids, E@ctorref(VarName), E, Type) :-
     ( tables.lookup_ctor(PT, VarName, TypeDef, _) ->
         % Found in global ctor table - get its type and varset
         ( ctor_type(TypeDef, VarName, CtorVarset, Type0) ->
@@ -201,9 +206,9 @@
     ;
         context.throw_error("Undefined variable: " ++ VarName, Ctx)
     ).
-expr_type_(Ctx, PT, LT, !Varset,
+expr_type_(Ctx, PT, LT, !Varset, Rigids,
             fieldref(Expr0, FieldName), fieldref(Expr, FieldName), Type) :-
-    expr_type(Ctx, PT, LT, !Varset, Expr0, Expr, ObjType0),
+    expr_type(Ctx, PT, LT, !Varset, Rigids, Expr0, Expr, ObjType0),
     types.deref(!.Varset, ObjType0, ObjType),
     % ObjType is the type which we are accessing
     ( ObjType = variable(_) ->
@@ -217,10 +222,10 @@
             ++ "references", Ctx)
     ),
     Type = ObjType.
-expr_type_(Ctx, PT, LT, !Varset, app(Func0, Args0), Expr@app(Func, Args),
-        RetType) :-
-    expr_type(Ctx, PT, LT, !Varset, Func0, Func, FuncType0),
-    expr_types(Ctx, PT, LT, !Varset, Args0, Args, ArgTypes),
+expr_type_(Ctx, PT, LT, !Varset, Rigids,
+        app(Func0, Args0), Expr@app(Func, Args), RetType) :-
+    expr_type(Ctx, PT, LT, !Varset, Rigids, Func0, Func, FuncType0),
+    expr_types(Ctx, PT, LT, !Varset, Rigids, Args0, Args, ArgTypes),
     types.deref(!.Varset, FuncType0, FuncType),
     What = "expression '" ++ pretty.string_expr(expr(Expr,no)) ++ "'",
     % Unify: FuncType = ArgType -> Type
@@ -231,7 +236,8 @@
         Arity = list.length(InputTypes),
         NumArgs = list.length(Args),
         ( Arity = NumArgs ->
-            det_unify_lists(Ctx, What, Args, ArgTypes, InputTypes, !Varset)
+            det_unify_lists(Ctx, What, Args, ArgTypes, InputTypes, Rigids,
+                            !Varset)
         ;
             type_error_arity(Ctx, !.Varset, What, Func, FuncType, Arity,
                 NumArgs)
@@ -241,16 +247,16 @@
         types.new_var(RetType, !Varset),
         det_unify(Ctx, What, Func, FuncType,
                   types.app(types.functype, ArgTypes ++ [RetType]),
-                  !Varset)
+                  Rigids, !Varset)
     ;
         % All other alternatives - not going to unify with ArgType -> Type.
         % Hence, "this is not a function" error.
         error_not_a_function(Ctx, !.Varset, What, Func, FuncType)
     ).
-expr_type_(Ctx, PT, LT, !Varset, parapp(Func0, Args0),
+expr_type_(Ctx, PT, LT, !Varset, Rigids, parapp(Func0, Args0),
         Expr@parapp(Func, Args), ResultType) :-
-    expr_type(Ctx, PT, LT, !Varset, Func0, Func, FuncType0),
-    expr_types(Ctx, PT, LT, !Varset, Args0, Args, ArgTypes),
+    expr_type(Ctx, PT, LT, !Varset, Rigids, Func0, Func, FuncType0),
+    expr_types(Ctx, PT, LT, !Varset, Rigids, Args0, Args, ArgTypes),
     types.deref(!.Varset, FuncType0, FuncType),
     What = "expression '" ++ pretty.string_expr(expr(Expr,no)) ++ "'",
     % Unify: FuncType = ArgType -> Type
@@ -264,7 +270,8 @@
             list.det_split_list(NumArgs, InputTypes, GotInputTypes,
                 RemInputTypes),
             % Unify all supplied args (remaining input types are not checked)
-            det_unify_lists(Ctx, What, Args, ArgTypes, GotInputTypes, !Varset)
+            det_unify_lists(Ctx, What, Args, ArgTypes, GotInputTypes, Rigids,
+                            !Varset)
         ;
             type_error_arity(Ctx, !.Varset, What, Func, FuncType, Arity,
                 NumArgs)
@@ -286,13 +293,13 @@
 % Applies expr_types to each element of the list, updating the list and
 % returning a list of types.
 :- pred expr_types(context::in, progtable::in, localtable::in,
-                   varset::in, varset::out,
+                   varset::in, varset::out, list(term.var)::in,
                    list(expr)::in, list(expr)::out, list(typeval)::out)
                    is det.
-expr_types(_Ctx, _PT, _LT, !Varset, [], [], []).
-expr_types(Ctx, PT, LT, !Varset, [E0|Es0], [E|Es], [T|Ts]) :-
-    expr_type(Ctx, PT, LT, !Varset, E0, E, T),
-    expr_types(Ctx, PT, LT, !Varset, Es0, Es, Ts).
+expr_types(_Ctx, _PT, _LT, !Varset, _Rigids, [], [], []).
+expr_types(Ctx, PT, LT, !Varset, Rigids, [E0|Es0], [E|Es], [T|Ts]) :-
+    expr_type(Ctx, PT, LT, !Varset, Rigids, E0, E, T),
+    expr_types(Ctx, PT, LT, !Varset, Rigids, Es0, Es, Ts).
 
 type_kind(Ctx, PT, Varset, Type0, Kind) :-
     types.deref(Varset, Type0, Type),
@@ -351,41 +358,51 @@
         kind_error(Ctx, Varset, Type, Type, Kind, kind_star)
     ).
 
-% check_pattern(Context, ProgTable, !LocalTable, !Varset,
+% check_pattern(Context, ProgTable, LocalTable, !Varset,
 %               What, SwitchType, !PatVars, !Pattern).
 % Checks to see if a pattern is type-correct, with respect to its parent
 % switch type.
-% Updates the varset and localtable with the extra type and term variables
-% created by the pattern.
 % Updates pattern by embedding the switch type.
 % !PatVars is the variables bound by this pattern so far.
 % A top-level call to check_pattern should pass set.init, and ignore result.
 % What: The entire top-level pattern, for error purposes.
-:- pred check_pattern(context::in, progtable::in,
-                    localtable::in, localtable::out,
-                    varset::in, varset::out,
+:- pred check_pattern(context::in, progtable::in, localtable::in,
+                    varset::in, varset::out, list(term.var)::in,
                     pattern::in, typeval::in,
                     set(varname)::in, set(varname)::out,
                     pattern::in, pattern::out)
                     is det.
-check_pattern(Ctx, PT, !LT, !Varset, What, SwitchType, !PatVars,
+check_pattern(Ctx, PT, LT, !Varset, Rigids, What, SwitchType, !PatVars,
     pattern(Pattern0, _), pattern(Pattern, yes(SwitchType))) :-
-    check_pattern_(Ctx, PT, !LT, !Varset, What, SwitchType, !PatVars,
+    check_pattern_(Ctx, PT, LT, !Varset, Rigids, What, SwitchType, !PatVars,
         Pattern0, Pattern).
 
-:- pred check_pattern_(context::in, progtable::in,
-                    localtable::in, localtable::out,
-                    varset::in, varset::out,
+:- pred check_pattern_(context::in, progtable::in, localtable::in,
+                    varset::in, varset::out, list(term.var)::in,
                     pattern::in, typeval::in,
                     set(varname)::in, set(varname)::out,
                     pattern_::in, pattern_::out)
                     is det.
-check_pattern_(_Ctx, _PT, !LT, !Varset, _What, _SwitchType, !PatVars,
+check_pattern_(_Ctx, _PT, _LT, !Varset, _Rigids, _What, _SwitchType, !PatVars,
                pat_any, pat_any).
-check_pattern_(Ctx, _PT, !LT, !Varset, _What, SwitchType, !PatVars,
+check_pattern_(Ctx, _PT, LT, !Varset, Rigids, What, SwitchType, !PatVars,
         P@pat_var(Name), P) :-
-    % Create a new variable in the localtable
-    tables.update_localtable(Name, SwitchType, !LT),
+    % Unify the SwitchType with the type of the bound variable
+    % Name is guaranteed to be a declared local variable by the implicit
+    % declaration pass applied before typechecking
+    ( tables.lookup_local(LT, Name, Type_) ->
+        TargetType = Type_
+    ;
+        error(string.format("Pattern variable \"%s\" not in local table",
+              [s(varname_to_string_noescape(Name))]))
+    ),
+    ( types.unify(TargetType, SwitchType, Rigids, !Varset) ->
+        true
+    ;
+        type_error_pattern(Ctx, !.Varset, What, pattern(P,no), TargetType,
+                           SwitchType)
+    ),
+
     % Check that this variable has not been bound previously in this same
     % pattern, and record the binding
     ( set.contains(!.PatVars, Name) ->
@@ -394,7 +411,7 @@
     ;
         svset.insert(Name, !PatVars)
     ).
-check_pattern_(Ctx, PT, !LT, !Varset, What, SwitchType, !PatVars,
+check_pattern_(Ctx, PT, LT, !Varset, Rigids, What, SwitchType, !PatVars,
         P@pat_ctor(VarName, Args0), pat_ctor(VarName, Args)) :-
     ( tables.lookup_ctor(PT, VarName, TypeDef, _) ->
         % Found in global ctor table
@@ -418,6 +435,13 @@
             ;
                 error("check_pattern: varset_merge returned bad output")
             ),
+            % Check that the constructor matches the given switch type.
+            ( types.unify(OutputType, SwitchType, Rigids, !Varset) ->
+                true
+            ;
+                type_error_pattern(Ctx, !.Varset, What, pattern(P,no),
+                                   OutputType, SwitchType)
+            ),
             % Make sure the pattern also has arguments
             ( list.length(CtorArgTypes) = 1 ->
                 Arguments = " argument"
@@ -454,8 +478,8 @@
                     Ctx)
             ),
             % Make sure each argument matches the ctor argument type
-            check_patterns(Ctx, PT, !LT, !Varset, What, CtorArgTypes,
-                !PatVars, YesArgs0, YesArgs),
+            check_patterns(Ctx, PT, LT, !Varset, Rigids, What, CtorArgTypes,
+                           !PatVars, YesArgs0, YesArgs),
             Args = yes(YesArgs)
         ;
             CtorArgTypes0 = no,
@@ -467,6 +491,13 @@
             ;
                 error("check_pattern: varset_merge returned bad output")
             ),
+            % Check that the constructor matches the given switch type.
+            ( types.unify(OutputType, SwitchType, Rigids, !Varset) ->
+                true
+            ;
+                type_error_pattern(Ctx, !.Varset, What, pattern(P,no),
+                                   OutputType, SwitchType)
+            ),
             % Make sure the pattern is also parameter-less
             (
                 Args0 = yes(_),
@@ -481,21 +512,14 @@
                 Args0 = no
             ),
             Args = no
-        ),
-        % Finally, check that the constructor matches the given switch type.
-        ( types.unify(OutputType, SwitchType, !Varset) ->
-            true
-        ;
-            type_error_pattern(Ctx, !.Varset, What, pattern(P,no), OutputType,
-                               SwitchType)
         )
     ;
         context.throw_error("Undefined constructor: " ++ VarName, Ctx)
     ).
-check_pattern_(Ctx, _PT, !LT, !Varset, What, SwitchType0, !PatVars,
+check_pattern_(Ctx, _PT, _LT, !Varset, Rigids, What, SwitchType0, !PatVars,
         P@pat_intlit(_), P) :-
     deref(!.Varset, SwitchType0, SwitchType),
-    ( types.unify(types.const("Int"), SwitchType, !Varset) ->
+    ( types.unify(types.const("Int"), SwitchType, Rigids, !Varset) ->
         true
     ;
         type_error_pattern(Ctx, !.Varset, What, pattern(P,no),
@@ -505,123 +529,111 @@
 % Check a list of patterns against a list of switch types.
 % Note it stops when either list reaches empty. Should check lengths
 % separately.
-:- pred check_patterns(context::in, progtable::in,
-                    localtable::in, localtable::out,
-                    varset::in, varset::out,
+:- pred check_patterns(context::in, progtable::in, localtable::in,
+                    varset::in, varset::out, list(term.var)::in,
                     pattern::in, list(typeval)::in,
                     set(varname)::in, set(varname)::out,
                     list(pattern)::in, list(pattern)::out)
                     is det.
-check_patterns(_Ctx, _PT, !LT, !Varset, _What, [], !PV, Ps, Ps).
-check_patterns(_Ctx, _PT, !LT, !Varset, _What, [_|_], !PV, [], []).
-check_patterns(Ctx, PT, !LT, !Varset, What, [S|Ss], !PV, [P0|Ps0], [P|Ps]) :-
-    check_pattern(Ctx, PT, !LT, !Varset, What, S, !PV, P0, P),
-    check_patterns(Ctx, PT, !LT, !Varset, What, Ss, !PV, Ps0, Ps).
+check_patterns(_Ctx, _PT, _LT, !Varset, _Rigids, _What, [], !PV, Ps, Ps).
+check_patterns(_Ctx, _PT, _LT, !Varset, _Rigids, _What, [_|_], !PV, [], []).
+check_patterns(Ctx, PT, LT, !Varset, Rigids, What, [S|Ss], !PV, [P0|Ps0],
+               [P|Ps]) :-
+    check_pattern(Ctx, PT, LT, !Varset, Rigids, What, S, !PV, P0, P),
+    check_patterns(Ctx, PT, LT, !Varset, Rigids, What, Ss, !PV, Ps0, Ps).
 
 :- func ctor_arg_types(ctor) = maybe(list(typeval)).
 ctor_arg_types(ctor(_,no,_)) = no.
 ctor_arg_types(ctor(_,yes(Args),_)) = yes(map(pair.snd, Args)).
 
-check_stmt(PT, LT, _RetType, !Varset,
+check_stmt(PT, LT, _RetType, !Varset, Rigids,
     basic_stmt(Stmt0, Ctx), basic_stmt(Stmt, Ctx)) :-
-    check_basic_stmt(Ctx, PT, LT, !Varset, Stmt0, Stmt).
-check_stmt(PT, LT, RetType, !Varset,
+    check_basic_stmt(Ctx, PT, LT, !Varset, Rigids, Stmt0, Stmt).
+check_stmt(PT, LT, RetType, !Varset, Rigids,
     compound_stmt(Stmt0, Ctx), compound_stmt(Stmt, Ctx)) :-
-    check_compound_stmt(Ctx, PT, LT, RetType, !Varset, Stmt0, Stmt).
+    check_compound_stmt(Ctx, PT, LT, RetType, !Varset, Rigids, Stmt0, Stmt).
 
-check_basic_stmt(_Ctx, _PT, _LT, !Varset, pass, pass).
-check_basic_stmt(Ctx, PT, LT, !Varset,
+check_basic_stmt(_Ctx, _PT, _LT, !Varset, _Rigids, pass, pass).
+check_basic_stmt(Ctx, PT, LT, !Varset, Rigids,
         assign(VarName, Expr0), assign(VarName, Expr)) :-
     % Get the type of both sides
-    get_local_var(Ctx, PT, LT, VarName, TargetType),  % Throws any errors
-    expr_type(Ctx, PT, LT, !Varset, Expr0, Expr, ExprType),
+    % VarName is guaranteed to be a declared local variable by the implicit
+    % declaration pass applied before typechecking
+    ( tables.lookup_local(LT, VarName, Type_) ->
+        TargetType = Type_
+    ;
+        error(string.format("Assignment target \"%s\" not in local table",
+              [s(varname_to_string_noescape(VarName))]))
+    ),
+    expr_type(Ctx, PT, LT, !Varset, Rigids, Expr0, Expr, ExprType),
     What = "statement '" ++ ir.varname_to_string_noescape(VarName)
         ++ " = " ++ pretty.string_expr(Expr) ++ "'",
     % Unify: TargetType = ExprType
-    det_unify(Ctx, What, Expr, ExprType, TargetType, !Varset).
-check_basic_stmt(Ctx, _PT, _LT, !Varset,
+    det_unify(Ctx, What, Expr, ExprType, TargetType, Rigids, !Varset).
+check_basic_stmt(Ctx, _PT, _LT, !Varset, _Rigids,
             fieldset(Target0, FieldName, Expr0),
             fieldset(Target0, FieldName, Expr0)) :-
     context.throw_error("Sorry: Type checker can't handle fieldset", Ctx).
-check_basic_stmt(Ctx, _PT, _LT, !Varset,
+check_basic_stmt(Ctx, _PT, _LT, !Varset, _Rigids,
             fieldreplace(Target0, FieldName, Expr0),
             fieldreplace(Target0, FieldName, Expr0)) :-
     context.throw_error("Sorry: Type checker can't handle fieldreplace", Ctx).
-check_basic_stmt(Ctx, PT, LT, !Varset, eval(Expr0), eval(Expr)) :-
-    expr_type(Ctx, PT, LT, !Varset, Expr0, Expr, _).
+check_basic_stmt(Ctx, PT, LT, !Varset, Rigids, eval(Expr0), eval(Expr)) :-
+    expr_type(Ctx, PT, LT, !Varset, Rigids, Expr0, Expr, _).
 
 :- pred check_compound_stmt(context::in, progtable::in, localtable::in,
-            typeval::in, varset::in, varset::out,
+            typeval::in, varset::in, varset::out, list(term.var)::in,
             compound_stmt::in, compound_stmt::out) is det.
-check_compound_stmt(Ctx, PT, LT, Ret, !Varset, return(Expr0), return(Expr)) :-
-    expr_type(Ctx, PT, LT, !Varset, Expr0, Expr, ExprType),
+check_compound_stmt(Ctx, PT, LT, Ret, !Varset, Rigids,
+            return(Expr0), return(Expr)) :-
+    expr_type(Ctx, PT, LT, !Varset, Rigids, Expr0, Expr, ExprType),
     What = "statement 'return " ++ pretty.string_expr(Expr) ++ "'",
     % Unify with function return type
-    det_unify(Ctx, What, Expr, ExprType, Ret, !Varset).
-check_compound_stmt(Ctx, PT, LT, Ret, !Varset, switch(Expr0, Cases0),
+    det_unify(Ctx, What, Expr, ExprType, Ret, Rigids, !Varset).
+check_compound_stmt(Ctx, PT, LT, Ret, !Varset, Rigids, switch(Expr0, Cases0),
             switch(Expr, Cases)) :-
-    expr_type(Ctx, PT, LT, !Varset, Expr0, Expr, SwitchType),
-    check_cases(PT, LT, Ret, SwitchType, !Varset, Cases0, Cases).
-check_compound_stmt(Ctx, PT, LT, Ret, !Varset,
+    expr_type(Ctx, PT, LT, !Varset, Rigids, Expr0, Expr, SwitchType),
+    check_cases(PT, LT, Ret, SwitchType, !Varset, Rigids, Cases0, Cases).
+check_compound_stmt(Ctx, PT, LT, Ret, !Varset, Rigids,
             if_then_else(Cond0, ThenPart0, ElsePart0),
             if_then_else(Cond, ThenPart, ElsePart)) :-
-    expr_type(Ctx, PT, LT, !Varset, Cond0, Cond, CondType),
+    expr_type(Ctx, PT, LT, !Varset, Rigids, Cond0, Cond, CondType),
     What = "statement 'if " ++ pretty.string_expr(Cond) ++ ":'",
     % Unify with Int type (all conditions must be Int).
-    det_unify(Ctx, What, Cond, CondType, types.const("Int"), !Varset),
-    check_stmts(PT, LT, Ret, !Varset, ThenPart0, ThenPart),
-    check_stmts(PT, LT, Ret, !Varset, ElsePart0, ElsePart).
-check_compound_stmt(Ctx, PT, LT, Ret, !Varset, while(Cond0, Stmts0),
+    det_unify(Ctx, What, Cond, CondType, types.const("Int"), Rigids, !Varset),
+    check_stmts(PT, LT, Ret, !Varset, Rigids, ThenPart0, ThenPart),
+    check_stmts(PT, LT, Ret, !Varset, Rigids, ElsePart0, ElsePart).
+check_compound_stmt(Ctx, PT, LT, Ret, !Varset, Rigids, while(Cond0, Stmts0),
             while(Cond, Stmts)) :-
-    expr_type(Ctx, PT, LT, !Varset, Cond0, Cond, CondType),
+    expr_type(Ctx, PT, LT, !Varset, Rigids, Cond0, Cond, CondType),
     What = "statement 'while " ++ pretty.string_expr(Cond) ++ ":'",
     % Unify with Int type (all conditions must be Int).
-    det_unify(Ctx, What, Cond, CondType, types.const("Int"), !Varset),
-    check_stmts(PT, LT, Ret, !Varset, Stmts0, Stmts).
+    det_unify(Ctx, What, Cond, CondType, types.const("Int"), Rigids, !Varset),
+    check_stmts(PT, LT, Ret, !Varset, Rigids, Stmts0, Stmts).
 
 % check_stmts(PT, LT, RetType, !Varset, !Stmts).
 :- pred check_stmts(progtable::in, localtable::in, typeval::in,
-    varset::in, varset::out, list(stmt)::in, list(stmt)::out) is det.
-check_stmts(_,_,_,!Varset,[],[]).
-check_stmts(PT, LT, RetType, !Varset, [Stmt0|Stmts0],[Stmt|Stmts]) :-
-    check_stmt(PT, LT, RetType, !Varset, Stmt0, Stmt),
-    check_stmts(PT, LT, RetType, !Varset, Stmts0, Stmts).
+    varset::in, varset::out, list(term.var)::in,
+    list(stmt)::in, list(stmt)::out) is det.
+check_stmts(_,_,_,!Varset,_,[],[]).
+check_stmts(PT, LT, RetType, !Varset, Rigids, [Stmt0|Stmts0],[Stmt|Stmts]) :-
+    check_stmt(PT, LT, RetType, !Varset, Rigids, Stmt0, Stmt),
+    check_stmts(PT, LT, RetType, !Varset, Rigids, Stmts0, Stmts).
 
 % check_cases(PT, LT, RetType, SwitchType, !Varset, !Stmts).
 :- pred check_cases(progtable::in, localtable::in,
-    typeval::in, typeval::in, varset::in, varset::out,
+    typeval::in, typeval::in, varset::in, varset::out, list(term.var)::in,
     list(case_stmt)::in,list(case_stmt)::out) is det.
-check_cases(_,_,_,_,!Varset,[],[]).
-check_cases(PT, LT, RetType, SwitchType, !Varset,
+check_cases(_,_,_,_,!Varset,_,[],[]).
+check_cases(PT, LT, RetType, SwitchType, !Varset, Rigids,
         [case_stmt(Pattern0, Stmts0, Ctx)|Cases0],
         [case_stmt(Pattern, Stmts, Ctx)|Cases]) :-
-    check_pattern(Ctx, PT, LT, LT_Inside, !Varset,
-                  Pattern0, SwitchType, set.init, _, Pattern0, Pattern),
+    check_pattern(Ctx, PT, LT, !Varset, Rigids, Pattern0, SwitchType,
+                  set.init, _, Pattern0, Pattern),
     % Note: Checking the statements uses the new LT which contains the
     % newly-bound variables by this pattern.
-    check_stmts(PT, LT_Inside, RetType, !Varset, Stmts0, Stmts),
-    check_cases(PT, LT, RetType, SwitchType, !Varset, Cases0, Cases).
-
-% Gets the name of a local variable, giving an appropriate error if not found.
-% (Note: Takes a progtable so it gives a different error if it's found
-% globally than not at all).
-:- pred get_local_var(context::in, progtable::in, localtable::in,
-    varname::in, typeval::out) is det.
-get_local_var(Ctx, PT, LT, VarName, Type) :-
-    ( tables.lookup_local(LT, VarName, Type_) ->
-        % Found in local table
-        Type = Type_
-    ;
-        VarName = svname(UnqualVarName),
-        tables.lookup_function(PT, UnqualVarName, _)
-    ->
-        % Found in global function table - cannot assign
-        context.throw_error("Cannot assign global variable: "
-            ++ UnqualVarName, Ctx)
-    ;
-        context.throw_error("Undefined variable: "
-            ++ ir.varname_to_string_noescape(VarName), Ctx)
-    ).
+    check_stmts(PT, LT, RetType, !Varset, Rigids, Stmts0, Stmts),
+    check_cases(PT, LT, RetType, SwitchType, !Varset, Rigids, Cases0, Cases).
 
 check_function(_PT, _LT, !Func) :-
     !.Func^func_body = func_builtin.
@@ -638,22 +650,11 @@
     ),
     check_type_star(Ctx, PT, !.Func^func_varset, !.Func^func_ret_type),
     check_types_star(Ctx, PT, !.Func^func_varset, list.map(pair.snd, Decls)),
-    % Universally-quantify all the variables in Params, by binding them to
-    % constants of the same name. (Note: It is important to ensure no name
-    % conflict with actual type names, but this is already ensured by having
-    % type vars in a different namespace).
-    some [!Varset] (
-        !:Varset = !.Func^func_varset,
-        (
-            !.Func^func_params = no
-        ;
-            !.Func^func_params = yes(Params2),
-            foldl(bind_type, list.map(func({_,B,_})=B, Params2), !Varset)
-        ),
-        bind_type(!.Func^func_ret_type, !Varset),
-        check_stmts(PT, LT, !.Func^func_ret_type, !Varset, Stmts0, Stmts),
-        !Func ^ func_varset := !.Varset
-    ),
+    % Check the function body and update the varset as a result
+    % (Checking may create or unify type variables.)
+    check_stmts(PT, LT, !.Func^func_ret_type, !.Func^func_varset, NewVarset,
+                !.Func^func_rigids, Stmts0, Stmts),
+    !Func ^ func_varset := NewVarset,
     !Func ^ func_body := func_body_ast(Decls, Stmts).
 % TODO: Type-check CFG-bodied functions.
 % This is difficult due to existential type. For now, does not do any checking
@@ -662,20 +663,6 @@
     !.Func^func_body = func_body_cfg(_,_),
     error("Not Implemented: Type checking on a function in CFG form").
 
-% bind_type(Type, !Varset).
-% Bind all variables in the Type to a const type of the same name.
-:- pred bind_type(typeval::in, varset::in, varset::out) is det.
-bind_type(Type, !Varset) :-
-    ( Type = variable(V) ->
-        Term = types.const(types.varset_lookup_name(!.Varset, V)),
-        types.varset_bind_var(V, Term, !Varset)
-    ; Type = app(T1, T2) ->
-        bind_type(T1, !Varset),
-        foldl(bind_type, T2, !Varset)
-    ;
-        true
-    ).
-
 check_typedef(PT, Typedef) :-
     check_ctors(PT, Typedef ^ typedef_varset, Typedef ^ typedef_ctors).
 
@@ -702,8 +689,9 @@
 check_program_(PT, [Node0|Nodes0], [Node|Nodes]) :-
     (
         Node0 = pfunction(Func0),
-        tables.build_localtable(Func0, LT),
-        check_function(PT, LT, Func0, Func),
+        add_implicit_decls(Func0, Func1),
+        tables.build_localtable(Func1, LT),
+        check_function(PT, LT, Func1, Func),
         Node = pfunction(Func)
     ;
         Node0 = ptypedef(Typedef),
@@ -716,26 +704,104 @@
     ),
     check_program_(PT, Nodes0, Nodes).
 
-det_unify(Ctx, What, Term, T1, T2, !Varset) :-
-    ( types.unify(T1, T2, !Varset) ->
+% --- Implicit variable detection --- %
+
+% Augment a function's Decls with all variables which are bound anywhere in
+% the body of the function, but not explicitly declared.
+% (All variables assigned or appearing in a pattern.)
+% Each of these variables is given, as its type, a fresh type variable. (The
+% true type will be automatically inferred from unifications during checking.)
+:- pred add_implicit_decls(function::in, function::out) is det.
+add_implicit_decls(!Func) :-
+    !.Func^func_body = func_builtin.
+add_implicit_decls(!Func) :-
+    !.Func^func_body = func_body_ast(Decls0, Stmts),
+    Varset0 = !.Func^func_varset,
+    (
+        !.Func^func_params = no,
+        Params = []
+    ;
+        !.Func^func_params = yes(FuncParams),
+        Params = map(func({N,_,_}) = svname(N), FuncParams)
+    ),
+    DeclsSet = set(assoc_list.keys(Decls0) ++ Params),
+    % Get the set of all variables bound in the function's body
+    BoundVars0 = remove_dups(boundvars_stmts(Stmts)),
+    % ... which are not already explicitly declared
+    filter((pred(V::in) is semidet :- \+ member(V, DeclsSet)),
+           BoundVars0, BoundVars),
+    % Construct NewDecls, an assoc list which maps each BoundVar onto a fresh
+    % type variable
+    map_foldl((pred(V::in, V-T::out, VS0::in, VS::out) is det :-
+                types.new_var(T, VS0, VS)),
+        BoundVars, NewDecls, Varset0, Varset),
+    !Func^func_body := func_body_ast(Decls0 ++ NewDecls, Stmts),
+    !Func^func_varset := Varset.
+add_implicit_decls(!Func) :-
+    !.Func^func_body = func_body_cfg(_, _),
+    error("Not Implemented: Implicit decls of a function in CFG form").
+
+% Get the set of all variables bound in the statement block.
+:- func boundvars_stmts(list(stmt)) = list(varname).
+boundvars_stmts(Stmts) = condense(map(boundvars_stmt, Stmts)).
+
+% Get the set of all variables bound in the statement.
+:- func boundvars_stmt(stmt) = list(varname).
+boundvars_stmt(basic_stmt(Stmt, _)) = boundvars_basic_stmt(Stmt).
+boundvars_stmt(compound_stmt(Stmt, _)) = boundvars_compound_stmt(Stmt).
+
+:- func boundvars_basic_stmt(basic_stmt) = list(varname).
+boundvars_basic_stmt(Stmt) = Vars :-
+    % Only assignment statements bind variables
+    ( Stmt = assign(Var, _) ->
+        Vars = [Var]
+    ;
+        Vars = []
+    ).
+
+:- func boundvars_compound_stmt(compound_stmt) = list(varname).
+boundvars_compound_stmt(return(_)) = [].
+boundvars_compound_stmt(switch(_, Cases))
+    = condense(map(boundvars_case, Cases)).
+boundvars_compound_stmt(if_then_else(_, ThenPart, ElsePart))
+    = boundvars_stmts(ThenPart) ++ boundvars_stmts(ElsePart).
+boundvars_compound_stmt(while(_, Body)) = boundvars_stmts(Body).
+
+:- func boundvars_case(case_stmt) = list(varname).
+boundvars_case(case_stmt(Pat, Body, _))
+    = boundvars_pattern(Pat^pat_pattern) ++ boundvars_stmts(Body).
+
+:- func boundvars_pattern(pattern_) = list(varname).
+boundvars_pattern(pat_any) = [].
+boundvars_pattern(pat_var(V)) = [V].
+boundvars_pattern(pat_ctor(_, no)) = [].
+boundvars_pattern(pat_ctor(_, yes(Pats)))
+    = condense(map(boundvars_pattern, map(func(P) = P^pat_pattern, Pats))).
+boundvars_pattern(pat_intlit(_)) = [].
+
+det_unify(Ctx, What, Term, T1, T2, BoundVars, !Varset) :-
+    ( types.unify(T1, T2, BoundVars, !Varset) ->
         true
     ;
         type_error(Ctx, !.Varset, What, Term, T1, T2)
     ).
 
+% --- Utility functions and errors --- %
+
 % det_unify_lists(Context, What, Term, Type1, Type2, !Varset).
 % Unify two lists types with respect to a single varset.
 % Zips with det_unify across 3 lists (with Term corresponding to Type1).
 % Precond: All 3 lists are the same size
 :- pred det_unify_lists(context::in, string::in, list(expr)::in,
                   list(typeval)::in, list(typeval)::in,
-                  varset::in, varset::out) is det.
-det_unify_lists(_Ctx, _What, [], _, _, !Varset).
-det_unify_lists(_Ctx, _What, [_|_], [], _, !Varset).
-det_unify_lists(_Ctx, _What, [_|_], [_|_], [], !Varset).
-det_unify_lists(Ctx, What, [Term|Terms], [T1|T1s], [T2|T2s], !Varset) :-
-    det_unify(Ctx, What, Term, T1, T2, !Varset),
-    det_unify_lists(Ctx, What, Terms, T1s, T2s, !Varset).
+                  list(term.var)::in, varset::in, varset::out) is det.
+det_unify_lists(_Ctx, _What, [], _, _, _, !Varset).
+det_unify_lists(_Ctx, _What, [_|_], [], _, _, !Varset).
+det_unify_lists(_Ctx, _What, [_|_], [_|_], [], _, !Varset).
+det_unify_lists(Ctx, What, [Term|Terms], [T1|T1s], [T2|T2s], Rigids,
+                !Varset) :-
+    det_unify(Ctx, What, Term, T1, T2, Rigids, !Varset),
+    det_unify_lists(Ctx, What, Terms, T1s, T2s, Rigids, !Varset).
 
 % type_error(Context, Varset, What, Term, Term_Type, Other_Type).
 % Throws an error resulting from failing to unify Type1 and Type2 with

=== modified file 'src/types.m'
--- src/types.m	2010-05-05 04:05:24 +0000
+++ src/types.m	2010-05-10 05:50:41 +0000
@@ -87,6 +87,10 @@
 % Fails if the types can't unify.
 % Succeeds if they do, and possibly updates varset with new bindings.
 :- pred unify(typeval::in, typeval::in, varset::in, varset::out) is semidet.
+% Like unify, but also takes a list of vars which must not be bound.
+% (The unification fails if these vars get bound.)
+:- pred unify(typeval::in, typeval::in, list(var)::in,
+              varset::in, varset::out) is semidet.
 
 % Get the name of a variable from a varset.
 % Prefix some number with "t_" if not found.
@@ -155,9 +159,11 @@
     term.apply_rec_substitution(Type0, Sub, Type).
 
 unify(T1, T2, !Varset) :-
+    unify(T1, T2, [], !Varset).
+unify(T1, T2, BoundVars, !Varset) :-
     some [!Sub] (
         varset.get_bindings(!.Varset, !:Sub),
-        term.unify_term(T1, T2, !Sub),   % Can fail
+        term.unify_term_dont_bind(T1, T2, BoundVars, !Sub),     % Can fail
         varset.set_bindings(!.Varset, !.Sub, !:Varset)
     ).
 

=== modified file 'src/util.m'
--- src/util.m	2010-05-05 04:06:15 +0000
+++ src/util.m	2010-05-10 05:50:41 +0000
@@ -91,6 +91,10 @@
 % is in the output, then Y-X won't also be in the output set).
 :- func list_all_pairs(list(A)) = list(pair(A,A)).
 
+% list_first_duplicate(L, X). If L contains duplicates, X is the first
+% duplicate. Fails if L does not contain duplicates.
+:- pred list_first_duplicate(list(A)::in, A::out) is semidet.
+
 % set_all_true(Pred, Set) takes a closure with one input argument.
 % Succeeds if Pred succeeds for every member of Set, else fails.
 :- pred set_all_true(pred(X)::in(pred(in) is semidet), set(X)::in)
@@ -234,6 +238,7 @@
 :- import_module dir.
 :- import_module unit.
 :- import_module term_io.
+:- use_module set_tree234.
 
 zipwith(_Pred, [], [], []).
 zipwith(Pred, [X|Xs], [Y|Ys], [A|As]) :-
@@ -287,6 +292,17 @@
     XPairXs = map(func(Y) = X-Y, Xs),
     XsAllPairs = list_all_pairs(Xs).
 
+list_first_duplicate(L, X) :-
+    list_first_duplicate_(L, set_tree234.init, X).
+:- pred list_first_duplicate_(list(A)::in, set_tree234.set_tree234(A)::in,
+                              A::out) is semidet.
+list_first_duplicate_([X|Xs], S, D) :-
+    ( set_tree234.member(S, X) ->
+        D = X
+    ;
+        list_first_duplicate_(Xs, set_tree234.insert(X, S), D)
+    ).
+
 repeat(Pred, Count, !A) :-
     ( Count =< 0 ->
         true

=== added file 'test/cases/compiler/implicitvar.mar'
--- test/cases/compiler/implicitvar.mar	1970-01-01 00:00:00 +0000
+++ test/cases/compiler/implicitvar.mar	2010-05-10 05:50:41 +0000
@@ -0,0 +1,47 @@
+# Assignment to an undeclared variable (should infer the type).
+# Bug #483082 -- Variables should not require declaration
+
+import unittest
+
+def my_id(x :: a) :: a = x
+
+# Test basic ability to assign a variable without declaring it
+def assign_implicit(x :: Int) :: Int:
+    y = x
+    return y
+
+# Test ability to implicitly shadow a global variable by assigning to a local
+# of the same name
+def shadow_global(x :: Int) :: Int:
+    my_id = x
+    return my_id
+
+# Test that the assigned variable has a monomorphic (bindable) type
+def implicit_type(x :: Int) :: Array(Int):
+    # Test using a special construct which creates a monomorphic type variable
+    y = []                  # y :: Array(a)
+    z = array_add(y, x)     # z :: Array(Int)
+    return z
+
+def implicit_type2(x :: Int) :: Int:
+    # Test using a global variable with a type var (all type variables in the
+    # global are converted into new monomorphic type variables)
+    f = my_id       # f :: a -> a
+    y = f(x)        # y :: Int
+    return y
+
+# Unit tests
+def test_assign_implicit() :: Int:
+    begin_case("assign_implicit")
+    assert_eq(assign_implicit(3), 3, "assign_implicit(3) != 3")
+    end_case("assign_implicit")
+    begin_case("shadow_global")
+    assert_eq(shadow_global(3), 3, "shadow_global(3) != 3")
+    end_case("shadow_global")
+    begin_case("implicit_type")
+    assert_eq(implicit_type(3), [3], "implicit_type(3) != [3]")
+    end_case("implicit_type")
+    begin_case("implicit_type")
+    assert_eq(implicit_type2(3), 3, "implicit_type2(3) != 3")
+    end_case("implicit_type")
+    return 0

=== added file 'test/cases/compiler/patterntypeerror.mar'
--- test/cases/compiler/patterntypeerror.mar	1970-01-01 00:00:00 +0000
+++ test/cases/compiler/patterntypeerror.mar	2010-05-10 05:50:41 +0000
@@ -0,0 +1,27 @@
+# A very picky test about the pattern matching type error
+# (Launchpad Bug #574277).
+
+type FooType(a):
+    Foo(a)
+
+type BarType:
+    Bar
+
+type BazType:
+    Baz
+
+# This function contains a type error:
+# Type error in pattern 'Foo(Baz)'
+#        Term:     Baz
+#        Type:     BazType
+#        Expected: BarType.
+# The error is printed at too high a level due to type variable bindings:
+# Type error in pattern 'Foo(Baz)'
+#        Term:     Foo(Baz)
+#        Type:     FooType(BazType)
+#        Expected: FooType(BarType).
+def foo(x :: FooType(BarType)) :: Int:
+    switch x:
+        case Foo(Baz):
+            return 1
+    return 0

=== added file 'test/cases/compiler/patterntypeerror.mtc'
--- test/cases/compiler/patterntypeerror.mtc	1970-01-01 00:00:00 +0000
+++ test/cases/compiler/patterntypeerror.mtc	2010-05-10 05:50:41 +0000
@@ -0,0 +1,8 @@
+# vim: filetype=yaml
+compile:
+    outcome: fail
+    errors: |
+        patterntypeerror.mar:25: (foo) Type error in pattern 'Foo(Baz)'
+                Term:     Baz
+                Type:     BazType
+                Expected: BarType.

=== modified file 'test/cases/compiler/phipred.mtc'
--- test/cases/compiler/phipred.mtc	2010-05-06 12:19:45 +0000
+++ test/cases/compiler/phipred.mtc	2010-05-10 05:50:41 +0000
@@ -3,4 +3,3 @@
 run:
     - call: twoswitch(Nothing, Nothing)
       stdout: "0\n"
-      expect: fail

=== modified file 'test/cases/compiler/switch.mar'
--- test/cases/compiler/switch.mar	2010-05-03 01:50:15 +0000
+++ test/cases/compiler/switch.mar	2010-05-10 05:50:41 +0000
@@ -16,6 +16,10 @@
 type Box(a):
     Box(a)
 
+type OneOrTwo:
+    One(Int)
+    Two(Int)
+
 # Test cases with multiple levels of pattern matching
 def switchtest(x :: Foo) :: Int:
     switch x:
@@ -72,6 +76,18 @@
     # declaration, so calls this an undefined variable).
     return y
 
+# scopes_declare2(4) should be 4.
+# Same test as scopes_declare, but does not contain an explicit assignment
+# (only a pattern binding). Tests that the pattern binding itself is able to
+# escape the scope.
+def scopes_declare2(x :: Int) :: Int:
+    switch x:
+        case y:
+            pass
+    # y must still be bound after the switch statement
+    # (Bug #513638).
+    return y
+
 # Test trivial (unconditional) binding of a variable
 # Although the test suite won't test for this, it should be compiled to code
 # without a switch, because there is no actual condition.
@@ -97,6 +113,14 @@
         case Pair(m, Box(n)):
             return add(m, n)
 
+# Test that it is legal to bind the same variable name twice
+def twobinds(x :: OneOrTwo) :: Int:
+    switch x:
+        case One(y):
+            return y
+        case Two(y):
+            return add(y, 1)
+
 # From fully-worked example in doc/dev/switchfactor.
 # Test that factoring doesn't break the precedence of the cases
 def factor(x :: Pair(Bar, Int)) :: Int:
@@ -185,6 +209,15 @@
     end_case("switch (trickybind)")
     return 0
 
+def test_twobinds() :: Int:
+    begin_case("switch (twobinds)")
+    assert_eq(twobinds(One(7)), 7, "twobinds(One(7)) != 7")
+    end_case("switch (twobinds)")
+    begin_case("switch (twobinds)")
+    assert_eq(twobinds(Two(7)), 8, "twobinds(Two(7)) != 8")
+    end_case("switch (twobinds)")
+    return 0
+
 def test_factor() :: Int:
     begin_case("switch (factoring)")
     assert_eq(factor(Pair(B, 1)), 1, "factor(Pair(B, 1)) != 1")

=== removed file 'test/cases/compiler/switch.mtc'
--- test/cases/compiler/switch.mtc	2010-05-03 02:53:53 +0000
+++ test/cases/compiler/switch.mtc	1970-01-01 00:00:00 +0000
@@ -1,5 +0,0 @@
-# vim: filetype=yaml
-# Temporary: Expect failure due to bug #513578
-compile:
-    outcome: succeed
-    expect: compile_error

=== modified file 'test/cases/semantic/assignglobal.mar'
--- test/cases/semantic/assignglobal.mar	2010-01-28 06:26:27 +0000
+++ test/cases/semantic/assignglobal.mar	2010-05-10 05:50:41 +0000
@@ -1,4 +1,6 @@
-# Expects a "cannot assign global" error.
+# Used to expect a "cannot assign global" error.
+# (Now, due to implicit declarations, myconstant is just a shadowed local
+# variable, so this is no longer an error.)
 
 def myconstant :: Int = 3
 

=== modified file 'test/cases/semantic/assignglobal.mtc'
--- test/cases/semantic/assignglobal.mtc	2010-01-28 06:26:27 +0000
+++ test/cases/semantic/assignglobal.mtc	2010-05-10 05:50:41 +0000
@@ -1,5 +1,3 @@
 # vim: filetype=yaml
 compile:
-    outcome: fail
-    errors: |
-        assignglobal.mar:6: (foo) Cannot assign global variable: myconstant.
+    outcome: succeed

=== modified file 'test/cases/semantic/casetypecheck.mtc'
--- test/cases/semantic/casetypecheck.mtc	2010-01-28 06:47:47 +0000
+++ test/cases/semantic/casetypecheck.mtc	2010-05-10 05:50:41 +0000
@@ -1,7 +1,6 @@
 # vim: filetype=yaml
 compile:
     outcome: fail
-    expect: fail
     errors: |
         casetypecheck.mar:5: (foo) Type error in pattern 'x'
                 Term:     x

=== modified file 'test/cases/semantic/dupfield.mar'
--- test/cases/semantic/dupfield.mar	2010-01-28 04:26:55 +0000
+++ test/cases/semantic/dupfield.mar	2010-05-10 05:50:41 +0000
@@ -1,4 +1,5 @@
-# Expects a "duplicate field name" error.
+# Expects a "duplicate field name" error, in the same constructor, with
+# distinct types.
 
 type Foo:
-    X(v :: Int, v :: Int)
+    X(v :: Int, v :: Array(Int))

=== modified file 'test/cases/semantic/dupfield.mtc'
--- test/cases/semantic/dupfield.mtc	2010-01-28 04:26:55 +0000
+++ test/cases/semantic/dupfield.mtc	2010-05-10 05:50:41 +0000
@@ -1,6 +1,8 @@
 # vim: filetype=yaml
 compile:
     outcome: fail
-    expect: fail
+    # Note: Unacceptable to have the "with differing types" error (from
+    # dupfield3), as it implies that making them the same type will correct
+    # the error. It won't (see dupfield2).
     errors: |
-        dupfield.mar:4: (Foo) Duplicate field name: v.
+        dupfield.mar:5: (Foo) Duplicate field name: v.

=== added file 'test/cases/semantic/dupfield2.mar'
--- test/cases/semantic/dupfield2.mar	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/dupfield2.mar	2010-05-10 05:50:41 +0000
@@ -0,0 +1,5 @@
+# Expects a "duplicate field name" error, in the same constructor, even with
+# the same types.
+
+type Foo:
+    X(v :: Int, v :: Int)

=== added file 'test/cases/semantic/dupfield2.mtc'
--- test/cases/semantic/dupfield2.mtc	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/dupfield2.mtc	2010-05-10 05:50:41 +0000
@@ -0,0 +1,5 @@
+# vim: filetype=yaml
+compile:
+    outcome: fail
+    errors: |
+        dupfield2.mar:5: (Foo) Duplicate field name: v.

=== renamed file 'test/cases/semantic/dupfield2.mar' => 'test/cases/semantic/dupfield3.mar'
=== renamed file 'test/cases/semantic/dupfield2.mtc' => 'test/cases/semantic/dupfield3.mtc'
--- test/cases/semantic/dupfield2.mtc	2010-01-28 06:26:27 +0000
+++ test/cases/semantic/dupfield3.mtc	2010-05-10 05:50:41 +0000
@@ -2,4 +2,4 @@
 compile:
     outcome: fail
     errors: |
-        dupfield2.mar:10: (Bar) Duplicate field name with differing types: v.
+        dupfield3.mar:10: (Bar) Duplicate field name with differing types: v.

=== added file 'test/cases/semantic/dupvarcase.mar'
--- test/cases/semantic/dupvarcase.mar	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/dupvarcase.mar	2010-05-10 05:50:41 +0000
@@ -0,0 +1,16 @@
+# Error if you re-use a name already in-scope in a pattern
+# (Technically a type error, since you're trying to bind an existing variable
+# to a new value with a different type. If it happens to have the same type,
+# then it's not an error.)
+# This used to be a common idiom, until pattern variables were changed so they
+# were scoped to the whole function, making it a type error.
+
+type Box(a):
+    Box(a)
+
+def unbox(x :: Box(a)) :: a:
+    switch x:
+        # Type error: the "x" in the pattern is the same "x" as outside the
+        # pattern, and they have different types
+        case Box(x):
+            return x

=== added file 'test/cases/semantic/dupvarcase.mtc'
--- test/cases/semantic/dupvarcase.mtc	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/dupvarcase.mtc	2010-05-10 05:50:41 +0000
@@ -0,0 +1,8 @@
+# vim: filetype=yaml
+compile:
+    outcome: fail
+    errors: |
+        dupvarcase.mar:15: (unbox) Type error in pattern 'Box(x)'
+                Term:     x
+                Type:     Box(a)
+                Expected: a.

=== added file 'test/cases/semantic/dupvarcase2.mar'
--- test/cases/semantic/dupvarcase2.mar	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/dupvarcase2.mar	2010-05-10 05:50:41 +0000
@@ -0,0 +1,17 @@
+# Error if you bind the same variable name in different patterns, and the
+# types don't unify.
+# (Technically a type error, since you're trying to bind an two variables
+# with different types. If it happens to have the same type, then it's not an
+# error -- this is tested in compiler/switch.twobinds.)
+
+type OneOrTwo:
+    One(Int)
+    Two(Array(Int))
+
+# Test that it is legal to bind the same variable name twice
+def twobinds(x :: OneOrTwo) :: Int:
+    switch x:
+        case One(y):
+            return y
+        case Two(y):
+            return add(array_ref(y, 0), 1)

=== added file 'test/cases/semantic/dupvarcase2.mtc'
--- test/cases/semantic/dupvarcase2.mtc	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/dupvarcase2.mtc	2010-05-10 05:50:41 +0000
@@ -0,0 +1,8 @@
+# vim: filetype=yaml
+compile:
+    outcome: fail
+    errors: |
+        dupvarcase2.mar:16: (twobinds) Type error in pattern 'Two(y)'
+                Term:     y
+                Type:     Int
+                Expected: Array(Int).

=== modified file 'test/cases/semantic/localreadwrite.mtc'
--- test/cases/semantic/localreadwrite.mtc	2010-01-28 07:16:24 +0000
+++ test/cases/semantic/localreadwrite.mtc	2010-05-10 05:50:41 +0000
@@ -1,6 +1,5 @@
 # vim: filetype=yaml
 compile:
     outcome: fail
-    expect: fail
     errors: |
         localreadwrite.mar:8: (foo) Use of uninitialised variable: x.

=== added file 'test/cases/semantic/localreadwrite2.mar'
--- test/cases/semantic/localreadwrite2.mar	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/localreadwrite2.mar	2010-05-10 05:50:41 +0000
@@ -0,0 +1,12 @@
+# Test that reading a local variable before it is defined is a "use of
+# uninitialised variable" error, not an "undefined variable" error.
+
+def foo() :: Int:
+    var y :: Int
+    y = x   # "Use of uninitialised variable: x"
+    # (Bug #513638: Prints "undefined variable" instead.)
+    # Now bind x = 4
+    switch 4:
+        case x:
+            pass
+    return y

=== added file 'test/cases/semantic/localreadwrite2.mtc'
--- test/cases/semantic/localreadwrite2.mtc	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/localreadwrite2.mtc	2010-05-10 05:50:41 +0000
@@ -0,0 +1,5 @@
+# vim: filetype=yaml
+compile:
+    outcome: fail
+    errors: |
+        localreadwrite2.mar:6: (foo) Use of uninitialised variable: x.

=== added file 'test/cases/semantic/localtypevar.mar'
--- test/cases/semantic/localtypevar.mar	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/localtypevar.mar	2010-05-10 05:50:41 +0000
@@ -0,0 +1,14 @@
+# Test that programs are rejected if they name a type variable explicitly in
+# the body, which isn't in the head.
+# (Arguably this should be allowed, but it currently isn't, as per
+# doc/ref/types. See Bug #482947).
+
+# Should be fine
+def foo :: Int:
+    x = error("xxx")
+    return 0
+
+def bar :: Int:
+    var x :: a          # Undefined type variable
+    x = error("xxx")
+    return 0

=== added file 'test/cases/semantic/localtypevar.mtc'
--- test/cases/semantic/localtypevar.mtc	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/localtypevar.mtc	2010-05-10 05:50:41 +0000
@@ -0,0 +1,7 @@
+# vim: filetype=yaml
+
+compile:
+    outcome: fail
+    # For some reason this is reported as a syntax error
+    errors: |
+        localtypevar.mar:12: (bar) Syntax error: Undefined type variable "a".

=== added file 'test/cases/semantic/localtypevar2.mar'
--- test/cases/semantic/localtypevar2.mar	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/localtypevar2.mar	2010-05-10 05:50:41 +0000
@@ -0,0 +1,10 @@
+# Test that programs are rejected if they name a type variable explicitly in
+# the body, which isn't in the head.
+# This example should NOT be allowed even if local type variables may be
+# mentioned. If mentioned, they should be rigid, so this would be a type error
+# (cannot unify rigid variable 'a" with Int).
+
+def foo :: Int:
+    var x :: a          # Undefined type variable
+    x = 4
+    return x

=== added file 'test/cases/semantic/localtypevar2.mtc'
--- test/cases/semantic/localtypevar2.mtc	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/localtypevar2.mtc	2010-05-10 05:50:41 +0000
@@ -0,0 +1,6 @@
+# vim: filetype=yaml
+
+compile:
+    outcome: fail
+    errors: |
+        localtypevar2.mar:8: (foo) Syntax error: Undefined type variable "a".

=== added file 'test/cases/semantic/monomorphism.mar'
--- test/cases/semantic/monomorphism.mar	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/monomorphism.mar	2010-05-10 05:50:41 +0000
@@ -0,0 +1,16 @@
+# Test that local type variables are monomorphic (once bound, they remain
+# bound)
+# From doc/ref/types:
+
+def g :: Array(a) = []
+
+def polymorphic(x :: Int) :: Array(Int):
+    r = array_add(g, x)
+    w = array_add(g, [1])   # Should be fine
+    return r
+
+def monomorphic(x :: Int) :: Array(Int):
+    v = []
+    r = array_add(v, x)
+    w = array_add(v, [1])   # Type error
+    return r

=== added file 'test/cases/semantic/monomorphism.mtc'
--- test/cases/semantic/monomorphism.mtc	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/monomorphism.mtc	2010-05-10 05:50:41 +0000
@@ -0,0 +1,9 @@
+# vim: filetype=yaml
+
+compile:
+    outcome: fail
+    errors: |
+        monomorphism.mar:15: (monomorphic) Type error in expression 'array_add(v, [1])'
+                Term:     [1]
+                Type:     Array(Int)
+                Expected: Int.

=== added file 'test/cases/semantic/monomorphism2.mar'
--- test/cases/semantic/monomorphism2.mar	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/monomorphism2.mar	2010-05-10 05:50:41 +0000
@@ -0,0 +1,23 @@
+# Test that local type variables are monomorphic (once bound, they remain
+# bound).
+# This time, test lifting a global constant into a local variable
+# From doc/ref/types:
+
+type Pair(a, b):
+    Pair(a, b)
+
+def array_map(f :: a -> b, a :: Array(a)) :: Array(b):
+    # Doesn't matter how it's implemented
+    return []
+
+# Should be fine
+def polymorphic(f :: a -> b, g :: a -> c, x :: Array(a)) :: Pair(Array(b), Array(c)):
+    y = array_map(f, x)
+    z = array_map(g, x)     # array_map used polymorphically
+    return Pair(y, z)
+
+def monomorphic(f :: a -> b, g :: a -> c, x :: Array(a)) :: Pair(Array(b), Array(c)):
+    mymap = array_map
+    y = mymap(f, x)
+    z = mymap(g, x)     # Type error
+    return Pair(y, z)

=== added file 'test/cases/semantic/monomorphism2.mtc'
--- test/cases/semantic/monomorphism2.mtc	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/monomorphism2.mtc	2010-05-10 05:50:41 +0000
@@ -0,0 +1,9 @@
+# vim: filetype=yaml
+
+compile:
+    outcome: fail
+    errors: |
+        monomorphism2.mar:22: (monomorphic) Type error in expression 'mymap(g, x)'
+                Term:     g
+                Type:     a -> c
+                Expected: a -> b.

=== added file 'test/cases/semantic/typeerror2.mar'
--- test/cases/semantic/typeerror2.mar	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/typeerror2.mar	2010-05-10 05:50:41 +0000
@@ -0,0 +1,6 @@
+# Expects a type error for unifying an explicit type variable with Int
+
+def badint(x :: a) :: Int:
+    var y :: Int
+    y = x
+    return y

=== added file 'test/cases/semantic/typeerror2.mtc'
--- test/cases/semantic/typeerror2.mtc	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/typeerror2.mtc	2010-05-10 05:50:41 +0000
@@ -0,0 +1,9 @@
+# vim: filetype=yaml
+
+compile:
+    outcome: fail
+    errors: |
+        typeerror2.mar:5: (badint) Type error in statement 'y = x'
+                Term:     x
+                Type:     a
+                Expected: Int.

=== added file 'test/cases/semantic/typeerror3.mar'
--- test/cases/semantic/typeerror3.mar	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/typeerror3.mar	2010-05-10 05:50:41 +0000
@@ -0,0 +1,6 @@
+# Expects a type error for unifying Int with an explicit type variable
+# (This tests the opposite direction of unification than typeerror2)
+
+def badint(x :: a) :: Int:
+    x = 4
+    return 0

=== added file 'test/cases/semantic/typeerror3.mtc'
--- test/cases/semantic/typeerror3.mtc	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/typeerror3.mtc	2010-05-10 05:50:41 +0000
@@ -0,0 +1,9 @@
+# vim: filetype=yaml
+
+compile:
+    outcome: fail
+    errors: |
+        typeerror3.mar:5: (badint) Type error in statement 'x = 4'
+                Term:     4
+                Type:     Int
+                Expected: a.

=== added file 'test/cases/semantic/typeerror4.mar'
--- test/cases/semantic/typeerror4.mar	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/typeerror4.mar	2010-05-10 05:50:41 +0000
@@ -0,0 +1,6 @@
+# The evil cast function
+# Expects a type error for trying to cast one arbitrary type to another
+# (Tests the same as typeerror 1 - 3, but with both sides as a variable)
+
+def cast(x :: a) :: b:
+    return x

=== added file 'test/cases/semantic/typeerror4.mtc'
--- test/cases/semantic/typeerror4.mtc	1970-01-01 00:00:00 +0000
+++ test/cases/semantic/typeerror4.mtc	2010-05-10 05:50:41 +0000
@@ -0,0 +1,9 @@
+# vim: filetype=yaml
+
+compile:
+    outcome: fail
+    errors: |
+        typeerror4.mar:6: (cast) Type error in statement 'return x'
+                Term:     x
+                Type:     a
+                Expected: b.

=== modified file 'test/cases/semantic/undefvar2.mar'
--- test/cases/semantic/undefvar2.mar	2010-01-28 06:26:27 +0000
+++ test/cases/semantic/undefvar2.mar	2010-05-10 05:50:41 +0000
@@ -1,5 +1,7 @@
-# Expects an "undefined variable" error.
+# Used to expect an "undefined variable" error.
+# (Now, due to implicit declarations, y is just assigned as expected,
+# so this is no longer an error.)
 
 def foo(x :: Int) :: Int:
-    y = x           # Undefined variable
+    y = x
     return x

=== modified file 'test/cases/semantic/undefvar2.mtc'
--- test/cases/semantic/undefvar2.mtc	2010-01-28 06:26:27 +0000
+++ test/cases/semantic/undefvar2.mtc	2010-05-10 05:50:41 +0000
@@ -1,5 +1,3 @@
 # vim: filetype=yaml
 compile:
-    outcome: fail
-    errors: |
-        undefvar2.mar:4: (foo) Undefined variable: y.
+    outcome: succeed