PreviousUpNext

15.4.678  src/lib/compiler/front/typer/types/type-core-language-declaration-g.pkg

## type-core-language-declaration-g.pkg
#
# For a higher-level overview see
#
#     src/lib/compiler/front/typer/main/type-package-language-g.pkg
#
# In this package we accept a deep-syntax Declaration
# and return that declaration rewritten to be fully typed,
# using the unification-based Hindley-Milner type-inference
# algorithm to propagate type information leaf-to-root.
#
# We also resolve overloaded literals and variables.                    # Overloaded literals include for example  1   which might be a byte-length int, a tagged int or a word-length int.
# This process is sort of a bag hung on the side of the
# language design;  it is not well specified and does not
# fit in very well.  Still, it is a real convenience --
# Ocaml lacks it and as a result must have (for example)
# a separate multiply op for every numeric type (ick!).

# Compiled by:
#     src/lib/compiler/front/typer/typer.sublib


# Compiled by:
#     src/lib/compiler/front/typer/typer.sublib




###                   "You get what you give:  Unloved code is ugly code."




stipulate
    package ds  =  deep_syntax;                                         # deep_syntax                   is from   src/lib/compiler/front/typer-stuff/deep-syntax/deep-syntax.pkg
    package err =  error_message;                                       # error_message                 is from   src/lib/compiler/front/basics/errormsg/error-message.pkg
    package lnd =  line_number_db;                                      # line_number_db                is from   src/lib/compiler/front/basics/source/line-number-db.pkg
    package syx =  symbolmapstack;                                      # symbolmapstack                is from   src/lib/compiler/front/typer-stuff/symbolmapstack/symbolmapstack.pkg
herein

    api Type_Core_Language_Declaration {
        #
        type_core_language_declaration                                  # SIDE-EFFECTS:  Sets tdt::TYPEVAR_REF.ref_typevar (in unify_typoids)   and   vac::PLAIN_VARIABLE.vartypoid_ref (in generalize_*).
            :
            { declaration:              ds::Declaration,                # The original declaration -- our primary input.  (?)
              symbolmapstack:           syx::Symbolmapstack,

              outside_all_lets:         Bool,

              error_function:           err::Error_Function,
              source_code_region:       lnd::Source_Code_Region
            }
            -> ds::Declaration                                          # The input declaration rewritten to be fully typed and free of overloaded literals and variables.
            ;

         debugging:  Ref(  Bool );
    };
end;

#  Genericized to factor out dependencies on highcode... 

stipulate
    package cos =  compile_statistics;                                  # compile_statistics                    is from   src/lib/compiler/front/basics/stats/compile-statistics.pkg
    package ctt =  core_type_types;                                     # core_type_types                       is from   src/lib/compiler/front/typer-stuff/types/core-type-types.pkg
    package ds  =  deep_syntax;                                         # deep_syntax                           is from   src/lib/compiler/front/typer-stuff/deep-syntax/deep-syntax.pkg
    package dsj =  deep_syntax_junk;                                    # deep_syntax_junk                      is from   src/lib/compiler/front/typer-stuff/deep-syntax/deep-syntax-junk.pkg
    package err =  error_message;                                       # error_message                         is from   src/lib/compiler/front/basics/errormsg/error-message.pkg
    package id  =  inlining_data;                                       # inlining_data                         is from   src/lib/compiler/front/typer-stuff/basics/inlining-data.pkg
    package ip  =  inverse_path;                                        # inverse_path                          is from   src/lib/compiler/front/typer-stuff/basics/symbol-path.pkg
    package mtt =  more_type_types;                                     # more_type_types                       is from   src/lib/compiler/front/typer/types/more-type-types.pkg
    package pds =  prettyprint_deep_syntax;                             # prettyprint_deep_syntax               is from   src/lib/compiler/front/typer/print/prettyprint-deep-syntax.pkg
    package pp  =  standard_prettyprinter;                              # standard_prettyprinter                is from   src/lib/prettyprint/big/src/standard-prettyprinter.pkg
    package ppt =  prettyprint_type;                                    # prettyprint_type                      is from   src/lib/compiler/front/typer/print/prettyprint-type.pkg
    package rol =  resolve_overloaded_literals;                         # resolve_overloaded_literals           is from   src/lib/compiler/front/typer/types/resolve-overloaded-literals.pkg
    package rov =  resolve_overloaded_variables;                        # resolve_overloaded_variables          is from   src/lib/compiler/front/typer/types/resolve-overloaded-variables.pkg
    package sta =  stamp;                                               # stamp                                 is from   src/lib/compiler/front/typer-stuff/basics/stamp.pkg
    package sy  =  symbol;                                              # symbol                                is from   src/lib/compiler/front/basics/map/symbol.pkg
    package syx =  symbolmapstack;                                      # symbolmapstack                        is from   src/lib/compiler/front/typer-stuff/symbolmapstack/symbolmapstack.pkg
    package tc  =  typer_control;                                       # typer_control                         is from   src/lib/compiler/front/typer/basics/typer-control.pkg
    package td  =  typer_debugging;                                     # typer_debugging                       is from   src/lib/compiler/front/typer/main/typer-debugging.pkg
    package tdt =  type_declaration_types;                              # type_declaration_types                is from   src/lib/compiler/front/typer-stuff/types/type-declaration-types.pkg
    package tyj =  type_junk;                                           # type_junk                             is from   src/lib/compiler/front/typer-stuff/types/type-junk.pkg
    package uds =  unparse_deep_syntax;                                 # unparse_deep_syntax                   is from   src/lib/compiler/front/typer/print/unparse-deep-syntax.pkg
    package uj  =  unparse_junk;                                        # unparse_junk                          is from   src/lib/compiler/front/typer/print/unparse-junk.pkg
    package uty =  unparse_type;                                        # unparse_type                          is from   src/lib/compiler/front/typer/print/unparse-type.pkg
    package uyt =  unify_typoids;                                       # unify_typoids                         is from   src/lib/compiler/front/typer/types/unify-typoids.pkg
    package vac =  variables_and_constructors;                          # variables_and_constructors            is from   src/lib/compiler/front/typer-stuff/deep-syntax/variables-and-constructors.pkg

    Pp = pp::Pp;
herein

    # This generic is invoked (only) from:
    #
    #     src/lib/compiler/front/semantic/types/type-core-language-declaration.pkg
    #
    generic package   type_core_language_declaration_g   (
        #             ================================

                 inlining_data_says_it_is_pure:  id::Inlining_Data -> Bool;                                                     # pure_info                             from   src/lib/compiler/front/semantic/basics/inlining-junk.pkg
                 inlining_data_to_my_type:       id::Inlining_Data -> Null_Or( tdt::Typoid );                                   # inlining_data_to_my_type              from   src/lib/compiler/front/semantic/modules/generics-expansion-junk-parameter.pkg
            )

    : (weak) Type_Core_Language_Declaration                                                                                     # Type_Core_Language_Declaration        is from   src/lib/compiler/front/typer/types/type-core-language-declaration-g.pkg
    {
        stipulate
            #
            Symbolmapstack =  syx::Symbolmapstack;
            Error_Function =  err::Error_Function;

            -->  =   mtt::(-->);

                                                                                                                                # The following is support for tracking the
                                                                                                                                # lexical context in which type variables
                                                                                                                                # appear.  We are interested in whether
                                                                                                                                # type variables are free or bound and also
                                                                                                                                # whether we are inside some let/stipulate
                                                                                                                                # construct or at top level.
                                                                                                                                #
                                                                                                                                # The two critical things we track are:
                                                                                                                                #
                                                                                                                                #
                                                                                                                                # outside_all_lets:
                                                                                                                                #
                                                                                                                                #     TRUE iff we are not lexicallly                    # NB: A 'stipulate' statement is a 'let'
                                                                                                                                #     within the scope of any "let"                             # construct, also { ... } code blocks and
                                                                                                                                #     construct.                                                # 'if'-statement 'then' and 'else' clauses.
                                                                                                                                #
                                                                                                                                #     We need this because (for example)
                                                                                                                                #     it is an error not to generalize                  # Generalization is discussed below.
                                                                                                                                #     a type variable a top level but
                                                                                                                                #     it is ok not to generalize one in
                                                                                                                                #     a 'let' due to the "value restriction".
                                                                                                                                #
                                                                                                                                #
                                                                                                                                # fn_nesting:
                                                                                                                                #
                                                                                                                                #     This is the number of fun/fn                              # 'lambdas', in fp jargon.
                                                                                                                                #     definitions lexically enclosing us.
                                                                                                                                #     This numbering starts at 0.
                                                                                                                                #     
                                                                                                                                #     We need this to support type agnosticism -- "polymorphism".
                                                                                                                                #     
                                                                                                                                #     Mythryl (and ML generally) implement
                                                                                                                                #     what is sometimes called "let-polymorphism",
                                                                                                                                #     in which (canonically) functions defined
                                                                                                                                #     in 'let' constructs have their type variables
                                                                                                                                #     'generalized' to allow them to match different
                                                                                                                                #     types in different invocations.  For example
                                                                                                                                #         {
                                                                                                                                #             ...
                                                                                                                                #             fun swap (a, b) = (b, a);
                                                                                                                                #             ...
                                                                                                                                #             p0 = swap ( 1 ,  2 );
                                                                                                                                #             p1 = swap ('1', '2');
                                                                                                                                #             p2 = swap ("1", "2");
                                                                                                                                #             ...
                                                                                                                                #         };
                                                                                                                                #     
                                                                                                                                #     Here swap() is operating indifferently            # "Don't-care polymorphism" and
                                                                                                                                #     upon pairs of ints, chars and strings.            # "parametric polymorphism" are two
                                                                                                                                #                                                       # more names for this kind of
                                                                                                                                #     Making this typecheck requires a special          # typeagnosticism.
                                                                                                                                #     kludge.  Here's how it works:
                                                                                                                                #     
                                                                                                                                #       o Instead of assigning 'swap' a normal          # In fp jargon this is called a "type scheme".
                                                                                                                                #         type, we assign it a "typescheme"             # We represent them using TYPESCHEME records and
                                                                                                                                #         (template) for a type, with holes             # we represent the 'holes' with TYPESCHEME_ARG,
                                                                                                                                #         where all the type variables should be.       # both from    ssrc/lib/compiler/front/typer-stuff/types/type-declaration-types.pkg
                                                                                                                                #     
                                                                                                                                #       o Each time we come to a call to 'swap'         # This copy-and-complete is implemented by
                                                                                                                                #         we generate a fresh type for it by            #     tyj::instantiate_if_typescheme()
                                                                                                                                #         making a copy of the typescheme and           # from
                                                                                                                                #         filling in all the holes with fresh           #     src/lib/compiler/front/typer-stuff/types/type-junk.pkg
                                                                                                                                #         type variables.                               #
                                                                                                                                #     
                                                                                                                                #     This way type inference is free to deduce
                                                                                                                                #     a different type for each call to 'swap'.
                                                                                                                                #     
                                                                                                                                #     We refer to the process of replacing a
                                                                                                                                #     type by such a type template as
                                                                                                                                #     "type generalization".
                                                                                                                                #
                                                                                                                                #     We implement this below, in
                                                                                                                                #
                                                                                                                                #         generalize_pattern()
                                                                                                                                #         generalize_type()
                                                                                                                                #
                                                                                                                                #     However when doing such type variable
                                                                                                                                #     generalization we must NOT generalize
                                                                                                                                #     any type variables inherited from                 # For a more extended discussion
                                                                                                                                #     enclosing scopes because the inherited            # see Benjamin C Pierce's
                                                                                                                                #     type variables encode important type              # "Types and Programming Languages" 
                                                                                                                                #     constraints which will be lost if we              # Chapter 22, in particular  
                                                                                                                                #     generalize them, allowing incorrect               # page 333 rule 3.
                                                                                                                                #     code to typecheck.        
                                                                                                                                #
                                                                                                                                #     We implement this restriction by
                                                                                                                                #
                                                                                                                                #      1) Tracking our current fn nesting level
                                                                                                                                #         as we do syntactic dagwalks.
                                                                                                                                #
                                                                                                                                #      2) Tagging every type variable with
                                                                                                                                #         the outermost fn nesting level
                                                                                                                                #         mentioning it.  (We refine this
                                                                                                                                #         during the type unification pass.)
                                                                                                                                #
                                                                                                                                #      3) Generalizing only those variables
                                                                                                                                #         defined at a deeper nesting level
                                                                                                                                #         than our current dagwalk fn nesting
                                                                                                                                #         level, which is to say variables
                                                                                                                                #         introduced by 'let' constructs
                                                                                                                                #         nested within the current fun/fn
                                                                                                                                #         (if any), rather than inherited from
                                                                                                                                #         scopes outside the 'let'.
                                                                                                                                #
                                                                                                                                #     Free type variables not declared by the user
                                                                                                                                #     are in general given a lexical nesting depth
                                                                                                                                #     of 'infinity', represented by an arbitrary                # E.g.:   tyj::make_meta_typevar_and_type  tdt::infinity;
                                                                                                                                #     integer larger than any expected real lexical
                                                                                                                                #     nesting depth.
                                                                                                                                #
                                                                                                                                #     USER_TYPEVAR typevars
                                                                                                                                #     are created with fn_nesting == infinity;          # By  make_user_typevar()  in  src/lib/compiler/front/typer-stuff/types/type-junk.pkg 
                                                                                                                                #     this nesting depth can be reduced
                                                                                                                                #     via unification.
                                                                                                                                #
                                                                                                                                #     When we instantiate a typeagnostic
                                                                                                                                #     type body we set all the META
                                                                                                                                #     variables to fn_nesting == "infinity".            # "infinity" being a kilomyriad, which
                                                                                                                                #                                                               # is to say 10000000. See types.pkg. :-)
                                                                                                                                #
                                                                                                                                #
                                                                                                                                # 8/18/92:
                                                                                                                                #     Cleaned up syntax_treewalk_lexical_context
                                                                                                                                #     "state machine" some and fixed bug #612.
                                                                                                                                #

            Syntax_Treewalk_Lexical_Context
                =
                {
                  fn_nesting:        Int,
                  outside_all_lets:  Bool
                };


            # When we start a typechecking a dagwalk
            # at the root of a syntax tree, this is
            # our initial type variable context:
            #
            root_syntax_treewalk_lexical_context
                =
                {
                  fn_nesting       => 0,
                  outside_all_lets => TRUE
                };


            # Note that we have entered the lexical scope
            # of a 'let' equivalent construct.
            # These include 'stipulate's, { ... } codeblocks and
            # if-statement 'then' and 'else' clauses:
            #
            fun enter_let_scope { fn_nesting, outside_all_lets }
                =
                { 
                  outside_all_lets => FALSE,
                  fn_nesting
                };


            # Note that we have entered the lexical scope
            # of a fun/fn or equivalent construct:
            #
            fun enter_fn_scope  { fn_nesting, outside_all_lets }
                =
                {
                                                                                                                                if *uty::debugging
                                                                                                                                    printf "enter_fn_scope bumping fn_nesting from %d to %d\n" fn_nesting (fn_nesting + 1);
                                                                                                                                fi;
                    {
                      fn_nesting =>  fn_nesting + 1,
                      outside_all_lets
                    };
                };

        herein 

            #  Debug support: 

            say         =   control_print::say;

#           debugging   =   tc::type_core_language_declaration_g_debugging;             #  REF FALSE 
#           internals   =   REF FALSE;
debugging   =   log::debugging;
internals   =   log::debugging;

            generalize_mutually_recursive_functions
                =
                tc::generalize_mutually_recursive_functions;                    #  REF FALSE
            #
            fun if_debugging_say (msg: String)
                =
                if *debugging
                    say msg;
                    say "\n";
                fi;

            debug_print   =   (\\ x =  td::debug_print debugging x);
            #
            fun bug msg   =   err::impossible("TypeCheck: " + msg);
            #
            fun print_callstack
                (msg:    String)
                (callstack:  List(String))
                =
                {   printf "%s:  callstack(%d) == " msg (list::length callstack);
                    apply  {. printf " -> %s" #string; }  (reverse callstack);
                    printf "\n";
                };

            is_value      =   tyj::is_value { inlining_data_says_it_is_pure };

            infix my 9  sub ;
            infix my    --> ;

            print_depth = control_print::print_depth;
            #
            fun ref_new_valcon (tdt::VALCON { name, is_constant, form, typoid, signature, is_lazy } )
                = 
                tdt::VALCON
                  {
                    typoid => mtt::ref_pattern_typoid,
                    name,
                    is_constant,
                    form,
                    signature,
                    is_lazy
                  };

            exception NOT_THERE;
            #
            fun message (   msg,    mode: unify_typoids::Unify_Fail   )
                =
                string::cat [ msg, " [", unify_typoids::fail_message mode, "]" ];




                                                                                                                                # Here is the heart of the compiler's type inference engine.
                                                                                                                                #
                                                                                                                                # This is also where we implement type agnosticism
                                                                                                                                # by generalizing USER_TYPEVAR and META_TYPEVAR
                                                                                                                                # types to TYPESCHEME_ARG types whenever permitted
                                                                                                                                # by the "value restriction" as implemented by is_value() in
                                                                                                                                #
                                                                                                                                #     src/lib/compiler/front/typer-stuff/types/type-junk.pkg
                                                                                                                                #
                                                                                                                                # We are called (only) from type_declaration'() in
                                                                                                                                #
                                                                                                                                #     src/lib/compiler/front/typer/main/type-package-language-g.pkg
                                                                                                                                #
                                                                                                                                # We delegate actual type unification to unify_typoids() in
                                                                                                                                #
                                                                                                                                #     src/lib/compiler/front/typer/types/unify-typoids.pkg
                                                                                                                                #
                                                                                                                                # A light overview of Hindley-Milner type inference may be found here:
                                                                                                                                #     http://en.wikipedia.org/wiki/Type_inference
                                                                                                                                #
                                                                                                                                # A more detailed treatment may be found in the
                                                                                                                                #     Types and Programming Languages
                                                                                                                                # text by Benjamin C Pierce, chapter 22.
                                                                                                                                #
            fun type_core_language_declaration                                                                                  # PUBLIC. (The only one in this file.)
                {                                                                                                               # SIDE-EFFECTS:  Sets tdt::TYPEVAR_REF.ref_typevar (in unify_typoids)   and   vac::PLAIN_VARIABLE.vartypoid_ref (in generalize_*).
                  declaration:         ds::Declaration,
                  symbolmapstack:      Symbolmapstack,                                                                          # symbolmapstack is needed only for debug printouts, not for core algorithmic purposes.
                  #
                  outside_all_lets:    Bool,
                  error_function:      Error_Function,
                  source_code_region:  ds::Source_Code_Region
                }
                : ds::Declaration
                = 
                {
                                                                                                                                if_debugging_unparse_declaration     ("\ntype_core_language_declaration: MID, just before calling do_declaration: declaration unparse     is:    ",  declaration     );
                                                                                                                                if_debugging_prettyprint_declaration ("\ntype_core_language_declaration: MID, just before calling do_declaration: declaration prettyprint is:    ", (declaration,100));
                                                                                                                                if_debugging_say "\ntype_core_language_declaration: NEWCODE is set.\n";
                    if (not (dsj::core_declaration_contains_overloaded_variable  declaration))

                                                                                                                                if_debugging_say "\ntype_core_language_declaration: NEWCODE is set but declaration does NOT contain an overloaded variable.\n";
                        # In the absence of overloaded variables,
                        # the old, simple approach is fine:
                        #
                        declaration
                            =
                            do_declaration (
                                #
                                declaration,
                                outside_all_lets  ??                   root_syntax_treewalk_lexical_context
                                                  ::  enter_let_scope  root_syntax_treewalk_lexical_context,
                                source_code_region,
                                []
                            );
                                                                                                                                if_debugging_unparse_declaration     ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]: XYZZ pre-overload-resolution declaration unparse is:\n",  declaration);
                                                                                                                                if_debugging_prettyprint_declaration ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]: XYZZ pre-overload-resolution declaration pyprint is:\n", (declaration,100));

                                                                                                                                if_debugging_say ("\ntype_core_language_declaration: calling resolve_all_overloaded_literals  ... [type-core-language-declaration-g.pkg]\n");
                        r1 =  resolve_all_overloaded_literals ();                                                               if_debugging_say ("\ntype_core_language_declaration: calling resolve_all_overloaded_variables ... [type-core-language-declaration-g.pkg]\n");
                        r2 =  resolve_all_overloaded_variables  symbolmapstack;

                                                                                                                                if_debugging_unparse_declaration     ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]: BOT PLUXX. pre-hack    declaration unparse     is:\n",  declaration);
                                                                                                                                if_debugging_prettyprint_declaration ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]: BOT PLUXX. pre-hack    declaration prettyprint is:\n", (declaration,100));


                                                                                                                                if_debugging_unparse_declaration     ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]: BOT PLUGH. transformed declaration unparse     is:\n",  declaration);
                                                                                                                                if_debugging_prettyprint_declaration ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]: BOT PLUGH. transformed declaration prettyprint is:\n", (declaration,100));
                                                                                                                                if_debugging_say "\n^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^";
                                                                                                                                if_debugging_say   "============= type_core_language_declaration/BOTTOM =============\n";

                        declaration;
                    else


                                                                                                                                if_debugging_say "\ntype_core_language_declaration: NEWCODE is set and declaration DOES contain an overloaded variable.\n";
                        # When overloaded variables are present, we do a couple of passes
                        # to replace them all with the appropriate variants, then proceed
                        # as though they never existed:


                                                                                                                                if_debugging_unparse_declaration     ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]/NEWCODE/O/AAA: declaration unparse     is:\n",  declaration);
                                                                                                                                if_debugging_prettyprint_declaration ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]/NEWCODE/O/AAA: declaration prettyprint is:\n", (declaration,100));

                        undo_log :=  THE [];                                                                                    # Enable undo-log functionality for first pass:  Purpose of first pass is *only* to resolve overloaded variables, all other changes will be undone.

                                                                                                                                if_debugging_say "\ntype_core_language_declaration/NEWCODE calling do_declaration(declaration) (1st)...\n";

                        do_declaration (                                                                                        # Now, we do type deduction on it to select the type-appropriate variant for each overloaded variable.
                            #
                            declaration,
                            outside_all_lets  ??                   root_syntax_treewalk_lexical_context
                                              ::  enter_let_scope  root_syntax_treewalk_lexical_context,
                            source_code_region,
                            []
                        );
                                                                                                                                if_debugging_say "\ntype_core_language_declaration/NEWCODE back from do_declaration(declaration) (1st)...\n";

                                                                                                                                if_debugging_unparse_declaration     ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]/NEWCODE/O/BBB: declaration unparse     is:\n",  declaration);
                                                                                                                                if_debugging_prettyprint_declaration ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]/NEWCODE/O/BBB: declaration prettyprint is:\n", (declaration,100));

                                                                                                                                if_debugging_say "\ntype_core_language_declaration/NEWCODE calling resolve_all_overloaded_variables...\n";
                        resolved_overloaded_variables
                            =
                            resolve_all_overloaded_variables  symbolmapstack                                                    # symbolmapstack is needed only for debug printout etc.
                            :
                            List(vac::Variable);
                                                                                                                                if_debugging_say "\ntype_core_language_declaration/NEWCODE back from resolve_all_overloaded_variables...\n";
                                                                                                                                if_debugging_unparse_declaration     ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]/NEWCODE/O/CCC: declaration unparse     is:\n",  declaration);
                                                                                                                                if_debugging_prettyprint_declaration ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]/NEWCODE/O/CCC: declaration prettyprint is:\n", (declaration,100));

                                                                                                                                if_debugging_say "\ntype_core_language_declaration/NEWCODE running undo_log...\n";
                        apply  (\\ f = f())  (the *undo_log);                                                                   # Execute undo thunks in last-in first-out order to restore 'declaration' to original state.
                                                                                                                                if_debugging_say "\ntype_core_language_declaration/NEWCODE done running undo_log...\n";

                                                                                                                                if_debugging_unparse_declaration     ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]/NEWCODE/O/DDD: declaration unparse     is:\n",  declaration);
                                                                                                                                if_debugging_prettyprint_declaration ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]/NEWCODE/O/DDD: declaration prettyprint is:\n", (declaration,100));


                        undo_log := NULL;                                                                                       # Disable undo-log functionality for second pass.




                                                                                                                                if_debugging_say "\ntype_core_language_declaration/NEWCODE calling replace_overloaded_variables_in_core_declaration...\n";

                        declaration                                                                                             # Now we plug in the appropriate overloaded-variable variants for each overloaded variable in the original declaration tree.
                            =
                            dsj::replace_overloaded_variables_in_core_declaration
                                declaration
                                resolved_overloaded_variables;

                                                                                                                                if_debugging_say "\ntype_core_language_declaration/NEWCODE back from replace_overloaded_variables_in_core_declaration...\n";

                                                                                                                                if_debugging_unparse_declaration     ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]/NEWCODE/O/EEE: declaration unparse     is:\n",  declaration);
                                                                                                                                if_debugging_prettyprint_declaration ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]/NEWCODE/O/EEE: declaration prettyprint is:\n", (declaration,100));


                                                                                                                                if_debugging_say "\ntype_core_language_declaration/NEWCODE calling do_declaration(declaration) (2nd)...\n";

                        declaration                                                                                             # Now we process the patched original declaration tree just as though it had never contained any overloaded variables.
                            =
                            do_declaration (
                                #
                                declaration,
                                outside_all_lets  ??                   root_syntax_treewalk_lexical_context
                                                  ::  enter_let_scope  root_syntax_treewalk_lexical_context,
                                source_code_region,
                                []
                            );
                                                                                                                                if_debugging_say "\ntype_core_language_declaration/NEWCODE back from do_declaration(declaration) (2nd)...\n";

                                                                                                                                if_debugging_unparse_declaration     ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]/NEWCODE/O/FFF: declaration unparse     is:\n",  declaration);
                                                                                                                                if_debugging_prettyprint_declaration ("\ntype_core_language_declaration [type-core-language-declaration-g.pkg]/NEWCODE/O/FFF: declaration prettyprint is:\n", (declaration,100));

                                                                                                                                if_debugging_say "\ntype_core_language_declaration/NEWCODE calling resolve_all_overloaded_literals ... [type-core-language-declaration-g.pkg]\n";
                        r1 =  resolve_all_overloaded_literals ();
                                                                                                                                if_debugging_say "\ntype_core_language_declaration/NEWCODE back from resolve_all_overloaded_literals ... [type-core-language-declaration-g.pkg]\n";

                        declaration;
                    fi;
                }
                where
                    undo_log =  REF (NULL: Null_Or(List(Void -> Void)));                                                        # When non-NULL, undo_log accumulates a list of thunks which will undo everything done by do_declaration() call.
                    #
                    fun maybe_note_ref_in_undo_log                                                                              #
                          (                                                                                                     # We make undo_log an explicit argument for consistency with usage in (e.g.) src/lib/compiler/front/typer/types/unify-typoids.pkg
                             undo_log:  Ref (Null_Or(List(Void -> Void))),                                                      # When non-NULL, *undo_log accumulates a list of thunks which will undo everything done by do_declaration() call.
                             ref:       Ref(X)                                                                                  # If we're maintaining the undo_log, add an entry to undo uncoming assignment to ref.
                          )
                        =
                        case *undo_log
                            #
                            THE log =>  {   oldval    =  *ref;
                                            #
                                            undo_log :=  THE ((\\ () = ref := oldval) ! log);
                                        };
                            NULL    =>  ();
                        esac;

                    (rol::make_overloaded_literal_resolver  ()                                  ) ->   { note_overloaded_literal,  resolve_all_overloaded_literals   };
                    (rov::make_overloaded_variable_resolver (inlining_data_to_my_type, undo_log)) ->   { note_overloaded_variable, resolve_all_overloaded_variables  };

                    prettyprint_named_recursive_value   = pds::prettyprint_named_recursive_value (syx::empty, NULL);
                    prettyprint_declaration             = pds::prettyprint_declaration           (syx::empty, NULL);
                    prettyprint_expression              = pds::prettyprint_expression            (syx::empty, NULL);
                    prettyprint_pattern                 = pds::prettyprint_pattern                syx::empty;

                    prettyprint_typoid                  = ppt::prettyprint_typoid               symbolmapstack;

                    unparse_typoid                      = uty::unparse_typoid                   symbolmapstack;
                    unparse_typevar_ref                 = uty::unparse_typevar_ref              symbolmapstack;
                    unparse_pattern                     = uds::unparse_pattern                  symbolmapstack;
                    unparse_expression                  = uds::unparse_expression              (symbolmapstack, NULL);
                    unparse_rule                        = uds::unparse_rule                    (symbolmapstack, NULL);
                    unparse_named_value                 = uds::unparse_named_value             (symbolmapstack, NULL);
                    unparse_recursively_named_value     = uds::unparse_recursively_named_value (symbolmapstack, NULL);

                    unparse_declaration
                        = 
                        (\\ stream
                            =
                            \\ d =  uds::unparse_declaration
                                            (symbolmapstack, NULL)
                                            stream
                                            (d, *print_depth)
                        );
                    #
/* */               fun if_debugging_unparse_declaration (msg, declaration)
                        =
                        if *debugging
                            if *internals  td::with_internals (\\ () =  td::debug_print debugging (msg, unparse_declaration, declaration));
                            else                                        td::debug_print debugging (msg, unparse_declaration, declaration) ;
                            fi;
                        fi;
                    #
/* */               fun if_debugging_unparse_typoid (msg, type)
                        =
                        if *debugging
                            if *internals   td::with_internals (\\ () =  td::debug_print debugging (msg, unparse_typoid, type));
                            else                                         td::debug_print debugging (msg, unparse_typoid, type) ;
                            fi;
                        fi;
                    #
/* */               fun if_debugging_prprint_typoid (msg, type)
                        =
                        if *debugging
                            if *internals   td::with_internals (\\ () =  td::debug_print debugging (msg, prettyprint_typoid, type));
                            else                                         td::debug_print debugging (msg, prettyprint_typoid, type) ;
                            fi;
                        fi;
                    #
/* */               fun if_debugging_unparse_typevar_ref  (msg, typevar_ref)
                        = 
                        if *debugging           # Without this 'if' (and the matching one in unify_typoids), compiling the compiler takes 5X as long! :-)
                            if *internals    td::with_internals (\\ () =  td::debug_print debugging (msg, unparse_typevar_ref, typevar_ref));
                            else                                          td::debug_print debugging (msg, unparse_typevar_ref, typevar_ref) ;
                            fi;
                        fi;
                    #
/* */               fun if_debugging_unparse_pattern (msg, pattern)
                        =
                        if *debugging
                            if *internals   td::with_internals (\\ () =  td::debug_print debugging (msg, unparse_pattern, pattern));
                            else                                         td::debug_print debugging (msg, unparse_pattern, pattern) ;
                            fi;
                        fi;
                    #
/* */               fun if_debugging_unparse_expression (msg, expression)
                        =
                        if *debugging   
                            if *internals   td::with_internals (\\ () =  td::debug_print debugging (msg, unparse_expression, expression));
                            else                                         td::debug_print debugging (msg, unparse_expression, expression) ;
                            fi;
                        fi;

                    #
/* */               fun if_debugging_prettyprint_expression (msg, expression)
                        =
                        if *debugging   
                            if *internals   td::with_internals (\\ () =    td::debug_print debugging (msg, prettyprint_expression, expression));
                            else                                           td::debug_print debugging (msg, prettyprint_expression, expression) ;
                            fi;
                        fi;
                    #
/* */               fun if_debugging_prettyprint_pattern (msg, pattern)
                        =
                        if *debugging   
                            if *internals   td::with_internals  (\\ () =        td::debug_print debugging (msg, prettyprint_pattern, pattern));
                            else                                                td::debug_print debugging (msg, prettyprint_pattern, pattern) ;
                            fi;
                        fi;
                    #
/* */               fun if_debugging_prettyprint_declaration (msg, declaration)
                        =
                        if *debugging   
                            if *internals   td::with_internals   (\\ () =  td::debug_print debugging (msg, prettyprint_declaration, declaration));
                            else                                           td::debug_print debugging (msg, prettyprint_declaration, declaration) ;
                            fi;
                        fi;
                    #
/* */               fun if_debugging_prettyprint_named_recursive_value (msg, val)
                        =
                        if *debugging   
                            if *internals   td::with_internals   (\\ () =  td::debug_print debugging (msg, prettyprint_named_recursive_value, val));
                            else                                           td::debug_print debugging (msg, prettyprint_named_recursive_value, val) ;
                            fi;
                        fi;


                    # This is a simple wrapper for unify_typoids(),
                    # used all through this file.
                    #
                    # 'typoid1' and 'typoid2' are the only
                    # arguments of consequence;  the rest
                    # are just diagnostic printing support:
                    #
                    fun unify_typoids_and_handle_errors                                                                         # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                          {
                            typoid1, name1,                     # typoid1: tdt::Typoid,   name1:  String
                            typoid2, name2,                     # typoid2: tdt::Typoid,   name2:  String

                            message => m,
                            source_code_region,

                            unparse_phrase,                     # prettyprint::String -> (X, Int) -> Void
                            phrase_name,                        # String
                            phrase,                             # X; X here and above is one of deep syntax Case_Pattern, Expression, ...
                            callstack,
                            undo_log
                          }
                        =
                        {
                                                                                                                                # More annoying than helpful:
                                                                                                                                #                       if *debugging
                                                                                                                                #                            printf "type-core-language-declaration-g.pkg:\
                                                                                                                                #                                   \ unify_typoids_and_handle_errors: calling unify_typoids name1 %s name2 %s message %s\n" name1 name2 m;
                                                                                                                                #                        fi;

                            uyt::unify_typoids                                                                                  # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                              (
                                name1, name2,
                                typoid1, typoid2,
                                "unify_typoids_and_handle_errors" ! callstack,
                                undo_log
                              );

                            TRUE;
                        }
                        except
                            uyt::UNIFY_TYPOIDS mode
                                =
                                {   error_function source_code_region
                                        err::ERROR
                                        (message (m, mode))
                                        (\\ pp
                                            =
                                            {   uty::reset_unparse_type();

                                                len1   = size name1;
                                                len2   = size name2;

                                                blanks = "                                   ";

                                                pad1   = substring (blanks, 0, int::max (0, len2-len1));
                                                pad2   = substring (blanks, 0, int::max (0, len2-len1));

                                                m = if (m=="")
                                                         name1 + " and " + name2 + " don't agree";
                                                    else m;
                                                    fi;

                                                if (name1 != "")
                                                    pp.newline(); 
                                                    pp.lit (name1 + ": " + pad1);
                                                    unparse_typoid  pp  typoid1;
                                                fi; 

                                                if (name2 != "")
                                                    pp.newline(); 
                                                    pp.lit (name2 + ": " + pad2);
                                                    unparse_typoid pp typoid2;
                                                fi;

                                                if (phrase_name != "")
                                                    pp.newline();
                                                    pp.lit ("in " + phrase_name + ":");
                                                    pp::break pp { blanks=>1, indent_on_wrap=>2 };
                                                    unparse_phrase pp (phrase,*print_depth);
                                                fi;
                                            }
                                        );
                                    FALSE;
                                };

                                                                                                                                if_debugging_say "\n============= type_core_language_declaration/TOP ============= [type-core-language-declaration-g.pkg]";
                                                                                                                                if_debugging_say   "vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv\n";
                                                                                                                                if_debugging_say ("type_core_language_declaration: outside_all_lets = " + bool::to_string  outside_all_lets);
                                                                                                                                if_debugging_unparse_declaration     ("\ntype_core_language_declaration/TOP: declaration unparse     =    [type-core-language-declaration-g.pkg]", declaration);
                                                                                                                                if_debugging_prettyprint_declaration ("\ntype_core_language_declaration/TOP: declaration prettyprint =    [type-core-language-declaration-g.pkg]", (declaration,100));


                                                                                                                                # This is the core routine responsible for marking
                                                                                                                                # a pattern variable as typeagnostic ("polymorphic").
                                                                                                                                #
                                                                                                                                # Our first argument below is the most important;
                                                                                                                                # it is from a ds::VARIABLE_IN_PATTERN.
                                                                                                                                # The critical part of it is the 'vartypoid_ref' ref:
                                                                                                                                # we will overwrite it with a generalized
                                                                                                                                # version of itself -- a
                                                                                                                                #     tdt::TYPESCHEME_TYPOID { ... }
                                                                                                                                # record wrapping a type scheme -- and then return
                                                                                                                                # the list of generalized type variables as our result.
                                                                                                                                #
                                                                                                                                # We get called frome exactly one place,
                                                                                                                                # in generalize_pattern'() in generalize_pattern(). 
                                                                                                                                #
                    fun generalize_type                                                                                         # SIDE-EFFECT:  Sets vac::PLAIN_VARIABLE.vartypoid_ref
                            (
                              vac::PLAIN_VARIABLE { vartypoid_ref, path, ... }: vac::Variable,
                              user_typevar_refs:                                List( tdt::Typevar_Ref ),                       # *NAMED_VALUE.typevars -- X, Y, Z ... from a function clause pattern or such.

                              syntax_treewalk_lexical_context:                  Syntax_Treewalk_Lexical_Context,
                              generalize:                                       Bool,                                           # Result of tyj::is_value() -- TRUE iff the "value restriction" permits generalizing this type.
                              source_code_region:                               ds::Source_Code_Region,
                              callstack:                                        List(String)                                    # Debug support.
                            )
                            : List( tdt::Typevar_Ref )                                                                          # These will actually always be tdt::META_TYPEVAR or tdt::USER_TYPEVAR.
                            =>
                            {
                                                                                                                                if *debugging
                                                                                                                                    print_callstack "\n=============  generalize_type/TOP =============" callstack;
                                                                                                                                    say (  "vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv  [type-core-language-declaration-g.pkg]\n\n");
                                                                                                                                    say ("generalize_type: " + symbol_path::to_string path);
                                                                                                                                    say "\nuser_typevar_refs: ";
                                                                                                                                    apply  unparse_typevar_ref  user_typevar_refs
                                                                                                                                    where
/* */                                                                                                                                   fun unparse_typevar_ref  typevar_ref
                                                                                                                                            =
                                                                                                                                            if_debugging_unparse_typevar_ref ("", typevar_ref);
                                                                                                                                    end;
                                                                                                                                    printf "\ngeneralize is %s\n" (generalize ?? "TRUE" :: "FALSE");
                                                                                                                                    printf "lexical context: fn_nesting d= %d  outside_all_lets b= %s\n" syntax_treewalk_lexical_context.fn_nesting (syntax_treewalk_lexical_context.outside_all_lets ?? "TRUE" :: "FALSE");
                                                                                                                                fi;

                                failure =   REF FALSE;


                                # Function to create dummy-type generators
                                # used to resolve ungeneralizable free
                                # type variables in typechecking::generalize_type:
                                #
                                make_dummy =    {   syntax_treewalk_lexical_context.outside_all_lets  
                                                        ??
                                                        make_dummytype_generator()
                                                        ::
                                                        make_dummy';            # Shouldn't be called.
                                                }
                                                where
                                                    #
                                                    fun make_dummy' ()
                                                        =
                                                        mtt::void_typoid;

                                                                                                                                                # stamp                         is from   src/lib/compiler/front/typer-stuff/basics/stamp.pkg
                                                    fun make_dummytype_generator ()   :   Void -> tdt::Typoid
                                                        =
                                                        {   count = REF 0;
                                                            #
                                                            fun next ()
                                                                =
                                                                {   count := *count + 1;
                                                                    *count;
                                                                };
                                                            #
                                                            fun next_type ()
                                                                =
                                                                {   name = "X" + int::to_string (next ());
                                                                    #
                                                                    tdt::TYPCON_TYPOID (
                                                                        #       
                                                                        tdt::SUM_TYPE
                                                                          {
                                                                            stamp       =>  sta::make_static_stamp  name,
                                                                            namepath    =>  ip::INVERSE_PATH [sy::make_type_symbol name],
                                                                            arity       =>  0,
                                                                            is_eqtype   =>  REF tdt::e::NO,
                                                                            kind        =>  tdt::ABSTRACT  ctt::bool_type,
                                                                            stub        =>  NULL
                                                                          },

                                                                        []
                                                                    );
                                                                };

                                                            next_type;
                                                        };
                                                end;


                                typescheme_arg_slots_allocated                                                                  # Tracks number of type variables bound. This will wind up being the typescheme arity.
                                    =
                                    REF 0;

                                #
                                fun allot_typescheme_arg_slot ()
                                    =
                                    {   slot =  *typescheme_arg_slots_allocated;
                                        #
                                        typescheme_arg_slots_allocated
                                            :=
                                            slot+1;

                                        slot;
                                    };

                                #
                                fun is_local_function_typevar_ref  ref_typevar                                                  # Check a typevar_ref for membership in our 'user_typevar_refs' parameter.
                                    =
                                    is_member  user_typevar_refs
                                    where
                                        fun is_member (user_typevar_ref ! rest)
                                                =>
                                                tyj::same_typevar_ref (ref_typevar, user_typevar_ref)                           # NB: This compares the refcells, NOT their contents!
                                                or
                                                is_member rest;

                                           is_member [] =>   FALSE;
                                        end;
                                    end;

                                typescheme_eqflags                                                                              # Track which of the below type variables need to be of equality type.
                                    =                                                                                           # This list will always be the same length as the next.
                                    REF ([]: tdt::Typescheme_Eqflags);                                                          # Possibly they should be combined.


                                                                                                                                # In this association list we track the
                                                                                                                                # tdt::TYPESCHEME_ARG slots of variables
                                                                                                                                # we've already generalized, to avoid assigning
                                                                                                                                # two slots to one variable.
                                                                                                                                # 
                                                                                                                                # The keys in this list are USER_TYPEVAR
                                                                                                                                # and META_TYPEVAR type variables;  the
                                                                                                                                # corresponding values are the
                                                                                                                                # tdt::TYPESCHEME_ARG types (slot numbers)
                                                                                                                                # we create for them.
                                                                                                                                #
                                                                                                                                # ASSERTION: There are no duplicate typevars
                                                                                                                                #            in domain of generalized_typevars.
                                                                                                                                #
                                generalized_typevar_ref_types
                                    =
                                    REF ([]:   List( ( tdt::Typevar_Ref,                                                        # This will be REF( tdt::META_TYPEVAR | tdt::USER_TYPEVAR )
                                                       tdt::Typoid                                                              # This will actually always be a tdt::TYPESCHEME_ARG. 
                                        )          ) );

                                #       
                                fun note_generalized_typevar_ref_type                                                           # Add an entry to above list.
                                    (
                                      typevar_ref:      tdt::Typevar_Ref,                                                       # This will reference a tdt::META_TYPEVAR or tdt::USER_TYPEVAR
                                      sometype:         tdt::Typoid                                                             # This will actually always be a tdt::TYPESCHEME_ARG. 
                                    )
                                    =
                                    {
                                                                                                                                if *debugging
                                                                                                                                if_debugging_unparse_typevar_ref  ("\nnote_generalized_typevar_ref_type adding typevar_ref [type-core-language-declaration-g.pkg]: ", typevar_ref);
                                                                                                                                if_debugging_unparse_typoid       (" with type (unparse)", sometype);
                                                                                                                                if_debugging_prprint_typoid       (" with type (prprint)", sometype);
                                                                                                                                fi;
                                        generalized_typevar_ref_types
                                            :=
                                            (typevar_ref, sometype)
                                            !
                                            *generalized_typevar_ref_types;
                                    };

                                #
                                fun find_generalized_typevar_ref_type  typevar_ref                                              # Search above list. Return key's value if found, otherwise raise NOT_THERE.
                                    =
                                    search  *generalized_typevar_ref_types
                                    where
                                        fun search ((typevar_ref', typescheme_arg) ! rest)
                                                =>
                                                tyj::same_typevar_ref (typevar_ref, typevar_ref')
                                                    ?? 
                                                    typescheme_arg
                                                    ::
                                                    search rest;

                                            search [] =>   raise exception NOT_THERE;
                                        end;
                                    end;


                                                                                                                                # Make a type typeagnostic.
                                                                                                                                # This mainly means replacing both of
                                                                                                                                #     META_TYPEVAR
                                                                                                                                #     USER_TYPEVAR
                                                                                                                                # by
                                                                                                                                #     tdt::TYPESCHEME_ARG 
                                                                                                                                # wherever permitted by the "value restriction"
                                                                                                                                # as implemented by tyj::is_value() and passed
                                                                                                                                # to us via the 'generalize' parameter.
                                                                                                                                #       
                                                                                                                                # We construct and return a Type result
                                                                                                                                # to replace our Type argument, but along
                                                                                                                                # the way we also side-effect various
                                                                                                                                # typevars etc in the expression, so
                                                                                                                                # this code is far from pure:
                                #
                                fun generalize_type'                                                                            # SIDE-EFFECT: SETS vac::PLAIN_VARIABLE.vartypoid_ref
                                    (typoid: tdt::Typoid)
                                    :        tdt::Typoid
                                    =     
                                    case typoid
                                        #
                                        tdt::TYPEVAR_REF (typevar_ref                                                           # This is the focal case for this function.
                                                          as  { id,                                                             # The remaining cases are mostly corner cases
                                                                ref_typevar as REF (tdt::META_TYPEVAR { fn_nesting, eq }) }     # and recursive descent to reach this case.
                                                         )
                                            =>
                                            {                                                                                   if *debugging
                                                                                                                                    printf "generalize_type'/META fn_nesting d=%d eq b=%s generalize b=%s\n"
                                                                                                                                           fn_nesting (eq ?? "TRUE" :: "FALSE")  (generalize ?? "TRUE" :: "FALSE");
                                                                                                                                fi;
                                                result
                                                    =
                                                    if (fn_nesting  >  syntax_treewalk_lexical_context.fn_nesting)              # If type variable is not constrained by contexts outside this 'let'.
                                                        #
                                                        if generalize                                                           # If 'value restriction' permits generalization of this type variable.
                                                            #   
                                                                                                                                if_debugging_say ("\ngeneralize_type'/META_TYPEVAR:  converting META to TYPESCHEME_ARG  [type-core-language-declaration-g.pkg]\n");

                                                            find_generalized_typevar_ref_type  typevar_ref                      # If we've already assigned this META variable a TYPESCHEME_ARG slot, return that as our replacement for it.
                                                            except
                                                                NOT_THERE
                                                                    =
                                                                    {   new_typescheme_slot_arg                                 # Assign a new type scheme slot for this META type variable,
                                                                            =
                                                                            tdt::TYPESCHEME_ARG( allot_typescheme_arg_slot() );

                                                                                                                                if_debugging_say ("\ngeneralize_type'/META_TYPEVAR: converting META to TYPESCHEME_ARG by allocating new TYPESCHEME_ARG  [type-core-language-declaration-g.pkg]\n");
                                                                        #
                                                                        typescheme_eqflags                                      # Remember whether this TYPESCHEME_ARG typevar must resolve to an equality type.
                                                                            :=
                                                                            eq ! *typescheme_eqflags;

                                                                        note_generalized_typevar_ref_type                       # Note new typescheme slot for future reference.
                                                                            (typevar_ref, new_typescheme_slot_arg); 

                                                                        new_typescheme_slot_arg;                                # Return new typescheme slot as our replacement for the META type variable.
                                                                    };
                                                        else                                                                    # !generalize
                                                            if syntax_treewalk_lexical_context.outside_all_lets
                                                                #
                                                                typevar = make_dummy ();

                                                                maybe_note_ref_in_undo_log  (undo_log, ref_typevar);

                                                                ref_typevar :=  tdt::RESOLVED_TYPEVAR  typevar;                 if_debugging_say ("\ngeneralize_type'/META_TYPEVAR: generalize FALSE so converting META to RESOLVED_TYPEVAR dummy  [type-core-language-declaration-g.pkg]\n");
                                                                failure     :=  TRUE;

                                                                typevar;
                                                            else
                                                                if *tc::value_restriction_local_warn
                                                                    #
                                                                    error_function  source_code_region  err::WARNING
                                                                          ( "type variable not generalized in local declaration due to 'value restriction': "
                                                                            +
                                                                            (uty::typevar_ref_printname  typevar_ref)
                                                                          )
                                                                          err::null_error_body;
                                                                fi;

                                                                maybe_note_ref_in_undo_log  (undo_log, ref_typevar);

                                                                ref_typevar                                                     # Reset fn_nesting to prevent later incorrect generalization inside a fun/fn expression.  See typechecking test.pkg
                                                                    :=
                                                                    tdt::META_TYPEVAR
                                                                      { eq,
                                                                        fn_nesting => syntax_treewalk_lexical_context.fn_nesting
                                                                      };
                                                                                                                                if_debugging_say ("\ngeneralize_type'/META_TYPEVAR:  generalize FALSE, resetting fn_nesting to prevent incorrect generalization  [type-core-language-declaration-g.pkg]\n");

                                                                typoid;                                                         # Return our (modified) input argument as our result.
                                                            fi;
                                                        fi;

                                                    elif (fn_nesting == 0  and  syntax_treewalk_lexical_context.outside_all_lets)

                                                        # ASSERT: failed generalization at fn_nesting 0.
                                                        # see bug 1066.
                                                                                                                                if_debugging_say ("\ngeneralize_type'/META_TYPEVAR: generalize FALSE, fn_nesting==0, changing to RESOLVED_TYPEVAR dummy  [type-core-language-declaration-g.pkg]\n");

                                                        find_generalized_typevar_ref_type  typevar_ref
                                                        except
                                                            NOT_THERE
                                                                =
                                                                {   new          =  make_dummy ();
                                                                    failure     :=  TRUE;

                                                                    maybe_note_ref_in_undo_log  (undo_log, ref_typevar);

                                                                    ref_typevar :=  tdt::RESOLVED_TYPEVAR  new;

                                                                    new;
                                                                };
                                                    else
                                                        typoid;
                                                    fi;

                                               result;
                                           };

                                        tdt::TYPEVAR_REF (typevar_ref  as  { id,  ref_typevar => REF (tdt::INCOMPLETE_RECORD_TYPEVAR { fn_nesting, eq, known_fields => [ (lab, _) ] } ) })
                                             =>
                                             if ( (       fn_nesting  >  syntax_treewalk_lexical_context.fn_nesting
                                                  and   (generalize  or  syntax_treewalk_lexical_context.outside_all_lets)
                                                  )
                                                  or
                                                  ( fn_nesting == 0
                                                    and
                                                    syntax_treewalk_lexical_context.outside_all_lets  
                                                  )
                                             )
                                                 error_function source_code_region err::ERROR
                                                     (string::cat
                                                         [ "unresolved record type\n\
                                                           \   (Don't know what fields it has beyond .",                        # Originally said 'flex record'.
                                                           sy::name lab,
                                                           ")"
                                                         ]
                                                     )
                                                     err::null_error_body;

                                                                                                                                if_debugging_say ("\ngeneralize_type': converting INCOMPLETE_RECORD_TYPEVAR to WILDCARD  [type-core-language-declaration-g.pkg]\n");
                                                 tdt::WILDCARD_TYPOID;

                                             else
                                                                                                                                if_debugging_say ("\ngeneralize_type': leaving INCOMPLETE_RECORD_TYPEVAR as-is  [type-core-language-declaration-g.pkg]\n");
                                                 typoid;
                                             fi;

                                        tdt::TYPEVAR_REF (typevar_ref as { id, ref_typevar => REF (tdt::INCOMPLETE_RECORD_TYPEVAR { fn_nesting, eq, known_fields } ) } )
                                             =>
                                             if ( (     fn_nesting > syntax_treewalk_lexical_context.fn_nesting  
                                                  and (generalize or syntax_treewalk_lexical_context.outside_all_lets)
                                                  )
                                                or ( fn_nesting == 0
                                                     and
                                                     syntax_treewalk_lexical_context.outside_all_lets
                                                   )
                                                )

                                                known_fields' =  string::cat  (list::map  (\\ (label, _) = sy::name label + " ")  known_fields);

                                                error_function source_code_region err::ERROR                                    # Originally said "flex record".
                                                   ( "unresolved record type:  Know only fields   "
                                                   + known_fields'
                                                   +  "  but need to know the names of ALL the fields in this context."
                                                   )
                                                   (\\ pp
                                                       =
                                                       {   uty::reset_unparse_type();
                                                           pp.newline();
                                                           pp.lit "type: ";
                                                           unparse_typoid pp typoid;
                                                       }
                                                   );

                                                tdt::WILDCARD_TYPOID;

                                            else
                                                typoid;
                                            fi;


                                        tdt::TYPEVAR_REF { id, ref_typevar => REF (tdt::RESOLVED_TYPEVAR typoid) }
                                            =>
                                            {
                                                                                                                                if_debugging_unparse_typoid ("\ngeneralize_type'/RESOLVED_TYPEVAR: generalizing resolved type variable of type (unparse):  [type-core-language-declaration-g.pkg]\n", typoid);
                                                                                                                                if_debugging_prprint_typoid ("\ngeneralize_type'/RESOLVED_TYPEVAR: generalizing resolved type variable of type (prprint):  [type-core-language-declaration-g.pkg]\n", typoid);
                                                # Drop from the type the now-useless prefix
                                                #     tdt::TYPEVAR_REF (REF (tdt::RESOLVED_TYPEVAR
                                                # Process and return the remainder of the type:
                                                #       
                                                generalize_type' typoid;
                                            };

                                        tdt::TYPEVAR_REF (typevar_ref as { id, ref_typevar as REF (tdt::USER_TYPEVAR { name, fn_nesting, eq } ) } )
                                            =>
                                            {                                                                                   if *debugging  printf "generalize_type'/USER_TYPEVAR [type-core-language-declaration-g.pkg]: %s fn_nesting==%d eq==%s\n" (sy::name name) fn_nesting (eq ?? "TRUE" :: "FALSE");  fi;

                                                                                                                                # We're looking at a type variable X or Y in an
                                                                                                                                # expression like  fun foo (x: X) = ... and
                                                                                                                                # wondering if it is ok to generalize.

                                                                                                                                # If it isn't on the list of type variables
                                                                                                                                # used in the current function's pattern
                                                                                                                                # clause(s) (parameter expressions), we have
                                                                                                                                # no business messing with it:
                                                                                                                                #       
                                                if (not (is_local_function_typevar_ref  typevar_ref))                           if_debugging_say "is not local";
                                                    #
                                                    typoid;                                                                     # This USER_TYPEVAR does not belong to us, so we should not generalize it.

                                                else                                                                            if_debugging_say " is local";

                                                                                                                                # This USER_TYPEVAR -does- belong
                                                                                                                                # to us, so we can (maybe) generalize it:

                                                                                                                                # If this type variable is mentioned in an
                                                                                                                                # enclosing lexical context (fun/fn), it
                                                                                                                                # encodes type constraints that would be
                                                                                                                                # lost if we generalized it, allowing
                                                                                                                                # incorrect code to typecheck.

                                                    if ( fn_nesting > syntax_treewalk_lexical_context.fn_nesting                # if external scope references do not forbid generalization...
                                                         and
                                                         generalize                                                             # ... and if "value restriction" does not forbid generalization...
                                                       )
                                                                                                                                # ... then we are GO to generalize this type variable.

                                                                                                                                if_debugging_say " is generalizable, replacing USER_TYPEVAR by TYPESCHEME_ARG  [type-core-language-declaration-g.pkg]";

                                                        find_generalized_typevar_ref_type  typevar_ref                          # If we've already generalized it, use assigned typescheme slot.
                                                        except
                                                            NOT_THERE
                                                                =
                                                                {                                                               # Need to assign a fresh typescheme slot, then note and return it.
                                                                    new_typescheme_slot_arg
                                                                        =
                                                                        tdt::TYPESCHEME_ARG (allot_typescheme_arg_slot());

                                                                    typescheme_eqflags                                          # Remember whether this new type variable resolve to an equality type.
                                                                        :=
                                                                        eq ! *typescheme_eqflags;

                                                                    note_generalized_typevar_ref_type
                                                                        ( typevar_ref,
                                                                          new_typescheme_slot_arg
                                                                        );

                                                                    new_typescheme_slot_arg;
                                                                };
                                                    else
                                                        printf  "generalize_type'/USER_TYPEVAR: %s fn_nesting==%d syntax_treewalk_lexical_context.fn_nesting==%d\n"
                                                                (sy::name name) fn_nesting   syntax_treewalk_lexical_context.fn_nesting;

                                                        error_function source_code_region err::ERROR
                                                            (  "Explicit type variable cannot be generalized at its declaration point: "
                                                               +
                                                               (uty::typevar_ref_printname  typevar_ref)
                                                            )
                                                            err::null_error_body;

                                                        maybe_note_ref_in_undo_log  (undo_log, ref_typevar);

                                                        ref_typevar :=  tdt::RESOLVED_TYPEVAR  tdt::WILDCARD_TYPOID;

                                                        tdt::WILDCARD_TYPOID;
                                                    fi;

                                                fi;
                                            };

                                        ( tdt::TYPEVAR_REF { id, ref_typevar as REF (tdt::LITERAL_TYPEVAR     _) }
                                        | tdt::TYPEVAR_REF { id, ref_typevar as REF (tdt::OVERLOADED_TYPEVAR  _) }
                                        )
                                            =>
                                            typoid;

                                        tdt::TYPCON_TYPOID (typ, args)
                                            =>
                                            {                                                                                   if_debugging_unparse_typoid ("\ngeneralize_type'/TYPCON_TYPE: generalizing constructor type (unparse):   [type-core-language-declaration-g.pkg]\n", typoid);
                                                                                                                                if_debugging_prprint_typoid ("\ngeneralize_type'/TYPCON_TYPE: generalizing constructor type (prprint):   [type-core-language-declaration-g.pkg]\n", typoid);
                                                #
                                                tdt::TYPCON_TYPOID (typ, map generalize_type' args);
                                            };

                                        tdt::WILDCARD_TYPOID
                                            =>
                                            tdt::WILDCARD_TYPOID;

                                        _ => {
                                                yes = REF TRUE;
                                                td::with_internals (\\ () =  td::debug_print yes ("unparsing bad arg to generalize_type:", unparse_typoid,     typoid));
                                                td::with_internals (\\ () =  td::debug_print yes ("pprinting bad arg to generalize_type:", prettyprint_typoid, typoid));
#                                               typoid;
                                                bug "generalize_type -- bad arg";
                                             };
                                    esac;                                                                                       # fun generalize_type'


                                                                                                                                if_debugging_unparse_typoid ("\ngeneralize_type:  vartypoid_ref as given to generalize_type' (unparse):      [type-core-language-declaration-g.pkg]", *vartypoid_ref);
                                                                                                                                if_debugging_prprint_typoid ("\ngeneralize_type:  vartypoid_ref as given to generalize_type' (prprint):      [type-core-language-declaration-g.pkg]", *vartypoid_ref);

                                typescheme_body =  generalize_type'  *vartypoid_ref;

                                                                                                                                if_debugging_unparse_typoid ("\ngeneralize_type: vartypoid_ref as converted by generalize_type' (unparse):    [type-core-language-declaration-g.pkg]", typescheme_body);
                                                                                                                                if_debugging_prprint_typoid ("\ngeneralize_type: vartypoid_ref as converted by generalize_type' (prprint):    [type-core-language-declaration-g.pkg]", typescheme_body);

                                generalized_typevar_refs
                                    =
                                    map #1 (reverse *generalized_typevar_ref_types);

                                                                                                                                if_debugging_say ("\ngeneralize_type: running hack to eliminate user_bound variables.   [type-core-language-declaration-g.pkg]\n");

                                apply  eliminate_user_bound_typevars                                                            # Turn user bound typevars (USER_TYPEVAR) into ordinary META_TYPEVARs.
                                       generalized_typevar_refs
                                where                                                                                           # A hack to eliminate all user bound type variables --zsh 
                                                                                                                                # ZHONG?: is this still necessary? -- David B MacQueen
                                                                                                                                # 2014-01-15 CrT: Apparently it is -- commenting out this block and doing a compile cycle produces:
                                                                                                                                #     Error: Compiler bug: translate_deep_syntax_to_lambdacode: unexpected typevar MACRO_EXPANDED in translate_pattern_expression
                                    fun eliminate_user_bound_typevars
                                          {
                                            id,
                                            ref_typevar as REF (tdt::USER_TYPEVAR { fn_nesting, eq, ... } )
                                          }
                                            => 
                                            {                                                                                   if *debugging   printf "generalize_type: eliminate_user_bound_typevars: converting USER_TYPEVAR id%d to META_TYPEVAR.   [type-core-language-declaration-g.pkg]\n" id;   fi;
                                                maybe_note_ref_in_undo_log  (undo_log, ref_typevar);
                                                #
                                                ref_typevar :=  tdt::META_TYPEVAR { fn_nesting, eq };
                                            };


                                        eliminate_user_bound_typevars _ 
                                            =>
                                            ();
                                    end;
                                end;

                                if *failure
                                    #                                                                                           if_debugging_say ("\ngeneralize_type: type vars left ungeneralized because of value restriction.   [type-core-language-declaration-g.pkg]\n");
                                    if *tc::value_restriction_top_warn
                                        #
                                        error_function  source_code_region  err::WARNING
                                            "type vars not generalized because of\n\
                                             \   value restriction are macro expanded to dummy types (X1, X2, ...)"
                                            err::null_error_body;
                                    fi;
                                fi;

                                                                                                                                if_debugging_say "\ngeneralize_type:  returning   [type-core-language-declaration-g.pkg]";

                                # Set the type variable we're generalizing
                                # to the type scheme we've constructed:

                                maybe_note_ref_in_undo_log  (undo_log, vartypoid_ref);

                                vartypoid_ref := tdt::TYPESCHEME_TYPOID
                                              {
                                                typescheme
                                                    =>
                                                    tdt::TYPESCHEME   { arity => *typescheme_arg_slots_allocated,
                                                                        body  =>  typescheme_body
                                                                      },

                                                typescheme_eqflags
                                                    =>
                                                    reverse  *typescheme_eqflags
                                              };

                                                                                                                                if_debugging_unparse_typoid ("\ngeneralize_type: final value for *vartypoid_ref (unparse):    [type-core-language-declaration-g.pkg]", *vartypoid_ref);
                                                                                                                                if_debugging_prprint_typoid ("\ngeneralize_type: final value for *vartypoid_ref (prprint):    [type-core-language-declaration-g.pkg]", *vartypoid_ref);

                                                                                                                                if *debugging
                                                                                                                                    printf "\ngeneralize_type returning %d type variables:           [type-core-language-declaration-g.pkg] \n" (list::length generalized_typevar_refs);
                                                                                                                                    apply  unparse_typevar_ref  generalized_typevar_refs
                                                                                                                                    where
/* */                                                                                                                                   fun unparse_typevar_ref  typevar_ref
                                                                                                                                            =
                                                                                                                                            if_debugging_unparse_typevar_ref ("", typevar_ref);
                                                                                                                                    end;
                                                                                                                                    say ("\n^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n");
                                                                                                                                    print_callstack "=============  generalize_type/BOTTOM ==========" callstack;
                                                                                                                                    say (  "\n");
                                                                                                                                fi; 

                                generalized_typevar_refs;                                                                       # Return generalized typevars.
                            };

                        generalize_type _ => bug "generalize_type - bad arg";
                    end;                                                                                                        # fun generalize_type


                                                                                                                                # Make 'given_pattern' as typeagnostistic ("polymorphic")
                                                                                                                                # as possible by changing META_TYPEVAR and USER_TYPEVAR
                                                                                                                                # to tdt::TYPESCHEME_ARG wherever permitted
                                                                                                                                # by the "value restriction" as implemented
                                                                                                                                # by tyj::is_value() and passed to us
                                                                                                                                # via the 'generalize' parameter.
                                                                                                                                # 
                                                                                                                                # The 'pattern' argument is updated by
                                                                                                                                # side effects;  we return the list of
                                                                                                                                # generalized type variables.
                                                                                                                                # 
                                                                                                                                # We are called from do_named_value()
                                                                                                                                # in do_declaration/VALUE_DECLARATIONS:
                                                                                                                                #
                    fun generalize_pattern                                                                                      # SIDE-EFFECT: SETS vac::PLAIN_VARIABLE.vartypoid_ref
                        (
                          given_pattern:                    ds::Case_Pattern,                                                   # Left-hand-side of a "fun foo ... = ..." or "my ... = ..." statement or such.
                          userbound:                        List( tdt::Typevar_Ref ),                                           # List of type variables from 'given_pattern'.

                          syntax_treewalk_lexical_context:  Syntax_Treewalk_Lexical_Context, 
                          generalize:                       Bool,
                          source_code_region:               ds::Source_Code_Region,
                          callstack:                        List(String)                                                        # Debug support.
                        )
                        : List( tdt::Typevar_Ref )                                                                              # These will actually always be tdt::META_TYPEVAR or tdt::USER_TYPEVAR
                        =
                        {
                                                                                                                                if *debugging print_callstack "\n============= generalize_pattern/TOP ============= " callstack; fi;
                                                                                                                                if_debugging_say   "vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv   [type-core-language-declaration-g.pkg]\n";
                                                                                                                                if *debugging
                                                                                                                                    printf "lexical context: lex.fn_nesting d= %d  outside_all_lets b= %s\n"
                                                                                                                                            syntax_treewalk_lexical_context.fn_nesting  (syntax_treewalk_lexical_context.outside_all_lets ?? "TRUE" :: "FALSE");
                                                                                                                                fi;
                                                                                                                                if_debugging_unparse_pattern ("\ndo_declaration/VALUE_DECLARATIONS/typecheck_named_value: pattern before generalization ==    [type-core-language-declaration-g.pkg]\n", (given_pattern,100));
                            generalized_typevars
                                =
                                REF( []:  List( tdt::Typevar_Ref ) );


                            generalize_pattern'  given_pattern
                            where
                                fun generalize_pattern' (ds::VARIABLE_IN_PATTERN variable)
                                        => 
                                        {   # This is the core case for this function;
                                            # the others are just recursive descent
                                            # to get here:
                                            # 
                                            added_bound_typevar_refs
                                                =
                                                generalize_type                                                                 # This is the only call to generalize_type().   SIDE-EFFECT: SETS vac::PLAIN_VARIABLE.vartypoid_ref
                                                    ( variable,
                                                      userbound,
                                                      syntax_treewalk_lexical_context,
                                                      generalize,
                                                      source_code_region,
                                                      "generalize_pattern" ! callstack
                                                    );

                                                                                                                                if *debugging
/* */                                                                                                                               fun unparse_typevar_ref  typevar_ref
                                                                                                                                        =
                                                                                                                                        if_debugging_unparse_typevar_ref ("", typevar_ref);

                                                                                                                                    say ("\ngeneralize_pattern' [type-core-language-declaration-g.pkg]: added_bound_typevar_refs: ");
                                                                                                                                    apply  unparse_typevar_ref   added_bound_typevar_refs;

                                                                                                                                    say ("\ngeneralize_pattern' [type-core-language-declaration-g.pkg]: *generalized_typevars: ");
                                                                                                                                    apply  unparse_typevar_ref   *generalized_typevars;
                                                                                                                                fi;
                                            case (added_bound_typevar_refs, *generalized_typevars) 
                                                #
                                                (_ ! _, _ ! _) => bug "generalize_pattern' 1234";                               # ???
                                                _ => ();
                                            esac;

                                            generalized_typevars
                                                :=
                                                added_bound_typevar_refs
                                                @
                                               *generalized_typevars;
                                                                                                                                if *debugging
                                                                                                                                    say ("\ngeneralize_pattern' [type-core-language-declaration-g.pkg]: resulting type variables list: ");
                                                                                                                                    apply  unparse_typevar_ref  *generalized_typevars
                                                                                                                                    where
/* */                                                                                                                                   fun unparse_typevar_ref  typevar_ref
                                                                                                                                            =
                                                                                                                                            if_debugging_unparse_typevar_ref ("", typevar_ref);
                                                                                                                                    end;
                                                                                                                                    say ("\n");
                                                                                                                                fi;
                                        };

                                   generalize_pattern' (ds::RECORD_PATTERN { fields, ... } )          =>   apply (generalize_pattern' o #2) fields;
                                   generalize_pattern' (ds::APPLY_PATTERN(_, _, arg)       )          =>   generalize_pattern' arg;
                                   generalize_pattern' (ds::TYPE_CONSTRAINT_PATTERN (pattern, _)  )   =>   generalize_pattern' pattern;
                                   generalize_pattern' (ds::AS_PATTERN (var_pattern, pattern))        =>   {   generalize_pattern' var_pattern;
                                                                                                               generalize_pattern' pattern;
                                                                                                           };
                                   generalize_pattern' _ => ();
                                end;
                            end;


                                                                                                                                if_debugging_unparse_pattern  ("do_declaration/VALUE_DECLARATIONS/typecheck_named_value: pattern after generalization ==     [type-core-language-declaration-g.pkg]\n", (given_pattern,100));
                                                                                                                                if_debugging_say "\n^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^";
                                                                                                                                if *debugging print_callstack "\n============= generalize_pattern/BOTTOM ==========    [type-core-language-declaration-g.pkg]" callstack; fi;
                                                                                                                                if_debugging_say   "\n";
                            *generalized_typevars;
                        };                                                                                                      # fun generalize_pattern


                    # Compute type of f(x)
                    # given types for f and x:
                    #
                    fun compute_fn_application_type
                          ( operator_type:      tdt::Typoid,
                            operand_type:       tdt::Typoid,
                            callstack:          List(String)
                          ):                    tdt::Typoid
                        =
                        {   result_type
                                =
                                tyj::make_meta_typevar_and_type
                                  ( tdt::infinity,
                                    ["compute_fn_application_type  from  type-core-language-declaration-g.pkg"]
                                  );

                                                                                                                                if_debugging_say "\ncompute_fn_application_type calling unify_typoids   [type-core-language-declaration-g.pkg]\n";

                            uyt::unify_typoids                                                                                  # SIDE-EFFECT:  Sets tdt::TYPEVAR_REF.ref_typevar
                              (
                                "operator_type",   "operand_type --> result_type",
                                 operator_type,    (operand_type --> result_type),
                                "compute_fn_application_type" ! callstack,
                                undo_log
                              );
                                                                                                                                if_debugging_say "\ncompute_fn_application_type back from unify_typoids   [type-core-language-declaration-g.pkg]\n";

                            result_type;
                        };


                    # Use unification to compute the most
                    # general non-typeagnostic type for
                    # a pattern.  This includes checking
                    # that all values in a vector pattern
                    # are of compatible type etc.
                    #
                    # Generalizing to typeagnostic type is
                    # done later if permitted by
                    # tyj::is_value():
                    #
                    fun compute_pattern_type                                                                                    # Not exported.
                        (
                          given_pattern:       ds::Case_Pattern,                                                                # Compute a type for this pattern.
                          fn_nesting:          Int,                                                                             # Lexical nesting of fun/fn constructs at this point in deep syntax dagwalk.
                          source_code_region:  ds::Source_Code_Region,
                          callstack:           List(String)                                                                     # Debug support.
                        )
                        :
                        ( ds::Case_Pattern,                                                                                     # Possibly (probably) updated version of given_pattern deep syntax tree.
                          tdt::Typoid                                                                                           # Computed type of given_pattern.
                        )
                        =
                        {
                                                                                                                                if *debugging print_callstack "\ncompute_pattern_type/TOP [type-core-language-declaration-g.pkg]" callstack; fi;
                                                                                                                                if_debugging_unparse_pattern ("\ncompute_pattern_type/TOP [type-core-language-declaration-g.pkg] given_pattern == ", (given_pattern,100));
                            result
                                =
                                case given_pattern
                                    #
                                    ds::WILDCARD_PATTERN
                                        =>
                                        ( given_pattern,
                                          tyj::make_meta_typevar_and_type  (fn_nesting, ["compute_pattern_type/WILDCARD_PATTERN  from  type-core-language-declaration-g.pkg"])
                                        );

                                    ds::VARIABLE_IN_PATTERN (vac::PLAIN_VARIABLE { vartypoid_ref as REF tdt::UNDEFINED_TYPOID, ... } )
                                        => 
                                        {   
                                            maybe_note_ref_in_undo_log  (undo_log, vartypoid_ref);

                                            vartypoid_ref :=  tyj::make_meta_typevar_and_type
                                                           ( fn_nesting,
                                                             ["compute_pattern_type/VARIABLE_IN_PATTERN  from  type-core-language-declaration-g.pkg"]
                                                           );

                                            (given_pattern, *vartypoid_ref);
                                        };

                                    # Multiple occurrence due to or-pattern 
                                    #
                                    ds::VARIABLE_IN_PATTERN (vac::PLAIN_VARIABLE { vartypoid_ref, ... } )       =>  (given_pattern, *vartypoid_ref); 

                                    ds::FLOAT_CONSTANT_IN_PATTERN _                                     =>  (given_pattern, mtt::float64_typoid);
                                    ds::STRING_CONSTANT_IN_PATTERN _                                    =>  (given_pattern, mtt::string_typoid);
                                    ds::CHAR_CONSTANT_IN_PATTERN _                                      =>  (given_pattern, mtt::char_typoid);

                                    ds::INT_CONSTANT_IN_PATTERN (_, type)                               =>  {   note_overloaded_literal type;   (given_pattern, type); };
                                    ds::UNT_CONSTANT_IN_PATTERN (_, type)                               =>  {   note_overloaded_literal type;   (given_pattern, type); };

                                    ds::RECORD_PATTERN { fields, is_incomplete, type_ref }
                                        =>
                                        # The record fields are already sorted by label,
                                        # typically by make_record_pattern() in
                                        #
                                        #     src/lib/compiler/front/typer/main/typer-junk.pkg
                                        #
                                        {   my (fields, field_types)
                                                =
                                                tyj::map_unzip  do_field  fields
                                                where
                                                    fun do_field (label, pattern)
                                                        = 
                                                        {   my (field_pattern, field_type)
                                                                =
                                                                compute_pattern_type
                                                                  ( pattern,
                                                                    fn_nesting,
                                                                    source_code_region,
                                                                    "compute_pattern_type/RECORD_PATTERN" ! callstack
                                                                  );

                                                            ( (label, field_pattern),
                                                              (label, field_type)
                                                            );
                                                        };
                                                end; 

                                            new_record_pattern
                                                =
                                                ds::RECORD_PATTERN { fields, is_incomplete, type_ref };

                                            if (not is_incomplete)
                                                #
                                                ( new_record_pattern,
                                                  mtt::record_typoid  field_types
                                                );
                                            else
                                                # We need to recover the rest of the fields
                                                # in this record before we can compute a
                                                # full type for it.  In   src/lib/compiler/front/typer-stuff/types/type-declaration-types.api
                                                # we define a special INCOMPLETE_RECORD_TYPEVAR
                                                # just to handle this situation:
                                                #
                                                record_typoid
                                                    =
                                                    tdt::TYPEVAR_REF
                                                      (
                                                        tdt::make_typevar_ref
                                                          (
                                                            tyj::make_incomplete_record_typevar
                                                              (field_types,  fn_nesting),

                                                            ["compute_pattern_type/RECORD_PATTERN  from  type-core-language-declaration-g.pkg"]
                                                      )   );

                                                maybe_note_ref_in_undo_log  (undo_log, type_ref);

                                                type_ref := record_typoid;

                                                (new_record_pattern, record_typoid);
                                            fi;
                                        };

                                    ds::VECTOR_PATTERN (patterns, _)
                                        => 
                                        {   
                                            stipulate
                                                fun do_pattern  pattern
                                                    =
                                                    compute_pattern_type
                                                      ( pattern,
                                                        fn_nesting,
                                                        source_code_region,
                                                        "compute_pattern_type/VECTOR_PATTERN" ! callstack
                                                      );
                                            herein
                                                (tyj::map_unzip  do_pattern  patterns)
                                                    ->
                                                    (patterns, pattern_types);
                                            end;

                                                                                                                                if_debugging_say "\ncompute_pattern_type/VECTOR_PATTERN folding calls to unify_typoids  [type-core-language-declaration-g.pkg]\n";
                                            # Force all vector elements
                                            # to have the same type:
                                            #
                                            vector_element_type                                                                 # SIDE-EFFECT:   unify_typoids  sets tdt::TYPEVAR_REF.ref_typevar
                                                =
                                                fold_backward
                                                      (\\ (a, b) =  { uyt::unify_typoids ("vector a", "vector b", a, b, "compute_pattern_type/VECTOR_PATTERN(2)" ! callstack, undo_log); b;})
                                                      (tyj::make_meta_typevar_and_type  (fn_nesting, "compute_pattern_type/VECTOR_PATTERN(3)" ! callstack))
                                                      pattern_types;
                                                                                                                                if_debugging_say "\ncompute_pattern_type/VECTOR_PATTERN done folding calls to unify_typoids  [type-core-language-declaration-g.pkg]\n";

                                            ( ds::VECTOR_PATTERN (patterns, vector_element_type),
                                              tdt::TYPCON_TYPOID (mtt::ro_vector_type, [ vector_element_type ] )
                                            );
                                        }
                                        except
                                            uyt::UNIFY_TYPOIDS mode
                                                =
                                                {  error_function
                                                       source_code_region
                                                       err::ERROR 
                                                       (message("vector pattern type failure", mode))
                                                       err::null_error_body;

                                                   (given_pattern, tdt::WILDCARD_TYPOID);
                                                };


                                    ds::OR_PATTERN (pattern1, pattern2)
                                        => 
                                          {
                                                                                                                                if *debugging print_callstack "\ncompute_pattern_type/ds::OR_PATTERN/TOP  [type-core-language-declaration-g.pkg]" callstack; fi;

                                              my (pattern1, typoid1) = compute_pattern_type (pattern1, fn_nesting, source_code_region, "compute_pattern_type/ds::OR_PATTERN"    ! callstack);
                                              my (pattern2, typoid2) = compute_pattern_type (pattern2, fn_nesting, source_code_region, "compute_pattern_type/ds::OR_PATTERN(2)" ! callstack);

                                                                                                                                if_debugging_say "\ncompute_pattern_type/ds::OR_PATTERN calling unify_typoids_and_handle_errors  [type-core-language-declaration-g.pkg]\n";
                                              # Force both sides of the '|'
                                              # pattern to have the same type:
                                              #
                                              unify_typoids_and_handle_errors                                                   # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                  {
                                                    typoid1,  name1 => "expected",
                                                    typoid2,  name2 => "found",

                                                    message => "or-patterns don't agree",
                                                    source_code_region,

                                                    unparse_phrase =>  unparse_pattern,
                                                    phrase_name    => "pattern",
                                                    phrase         =>  given_pattern,

                                                    callstack      => "compute_pattern_type/ds::OR_PATTERN(3)" ! callstack,

                                                    undo_log
                                                  };
                                                                                                                                if_debugging_say "\ncompute_pattern_type/ds::OR_PATTERN done calling unify_typoids_and_handle_errors  [type-core-language-declaration-g.pkg]\n";

                                              ( ds::OR_PATTERN (pattern1, pattern2),
                                                typoid1
                                              );
                                          };

                                    ds::CONSTRUCTOR_PATTERN (valcon as tdt::VALCON { typoid, ... }, _)
                                        => 
                                        {   (tyj::instantiate_if_typescheme  (typoid, symbolmapstack, "compute_pattern_type/ds::CONSTRUCTOR_PATTERN" ! callstack))              # symbolmapstack is used only for debugging.
                                                ->
                                                (type, fresh_meta_typevars);
                                                  

                                              # The following is to set the correct fn_nesting information
                                              # on the type variables in type. (ZHONG)
                                              #
                                                                                                                                if_debugging_say "\ncompute_pattern_type/ds::CONSTRUCTOR_PATTERN calling unify_typoids  [type-core-language-declaration-g.pkg]\n";

                                              uyt::unify_typoids                                                                # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                (
                                                  "type", "temp_type",
                                                   type,   temp_type,
                                                  ["compute_pattern_type/ds::CONSTRUCTOR_PATTERN  from  type-core-language-declaration-g.pkg"],
                                                   undo_log
                                                )
                                              where
                                                  temp_type = tyj::make_meta_typevar_and_type
                                                                ( fn_nesting,
                                                                  ["compute_pattern_type/ds::CONSTRUCTOR_PATTERN  from  type-core-language-declaration-g.pkg"]
                                                                );
                                              end;
                                                                                                                                if_debugging_say "\ncompute_pattern_type/ds::CONSTRUCTOR_PATTERN done calling unify_typoids  [type-core-language-declaration-g.pkg]\n";

                                              ( ds::CONSTRUCTOR_PATTERN (valcon, fresh_meta_typevars),
                                                type
                                              );
                                         };

                                    ds::APPLY_PATTERN (valcon as tdt::VALCON { typoid, form, ... }, _, arg)
                                        =>
                                        {   (compute_pattern_type ( arg,
                                                                    fn_nesting,
                                                                    source_code_region,
                                                                    "compute_pattern_type/ds::APPLY_PATTERN" ! callstack
                                                                  ))
                                                ->
                                                (arg_pattern, arg_type);

                                            my (constructor, type)
                                                =
                                                case form   varhome::REFCELL_REP =>  (ref_new_valcon valcon,  mtt::ref_pattern_typoid);
                                                            _                    =>  (valcon,                 typoid    );
                                                esac;

                                            (tyj::instantiate_if_typescheme (type, symbolmapstack, "compute_pattern_type/ds::APPLY_PATTERN" ! callstack))
                                                ->
                                                (type, fresh_meta_typevars);

                                            result_pattern
                                               =
                                               ds::APPLY_PATTERN (constructor, fresh_meta_typevars, arg_pattern);

                                                                                                                                if_debugging_say "\ncompute_pattern_type/ds::APPLY_PATTERN calling compute_fn_application_type  [type-core-language-declaration-g.pkg]\n";
                                            ( result_pattern,
                                              compute_fn_application_type (type, arg_type, callstack)
                                            )
                                            except
                                                uyt::UNIFY_TYPOIDS  mode
                                                    =
                                                    {   error_function source_code_region err::ERROR
                                                            (message("constructor and argument don't agree in pattern", mode))
                                                            (\\ pp
                                                                =
                                                                {   uty::reset_unparse_type();                  pp.newline();
                                                                    pp.lit "constructor: ";
                                                                    unparse_typoid  pp  type;                   pp.newline();
                                                                    pp.lit "argument:    ";
                                                                    unparse_typoid pp arg_type;                 pp.newline();
                                                                    pp.lit "in pattern:";
                                                                    pp::break pp { blanks=>1, indent_on_wrap=>2 };
                                                                    unparse_pattern pp (given_pattern, *print_depth);
                                                                }
                                                            );

                                                        ( given_pattern,
                                                          tdt::WILDCARD_TYPOID
                                                        );
                                                    };
                                        };

                                    ds::TYPE_CONSTRAINT_PATTERN (pattern, type)
                                        => 
                                        {
                                                                                                                                if_debugging_say "\ncompute_pattern_type/ds::TYPE_CONSTRAINT_PATTERN calling compute_pattern_type  [type-core-language-declaration-g.pkg]\n";
                                            my (npat, pat_type)
                                                =
                                                compute_pattern_type
                                                  ( pattern,
                                                    fn_nesting,
                                                    source_code_region,
                                                    "compute_pattern_type/ds::TYPE_CONSTRAINT_PATTERN" ! callstack
                                                  );
                                                                                                                                if_debugging_say "\ncompute_pattern_type/ds::TYPE_CONSTRAINT_PATTERN done calling compute_pattern_type  [type-core-language-declaration-g.pkg]\n";

                                                                                                                                if_debugging_say "\ncompute_pattern_type/ds::TYPE_CONSTRAINT_PATTERN calling unify_typoids_and_handle_errors  [type-core-language-declaration-g.pkg]\n";

                                            if (unify_typoids_and_handle_errors                                                 # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                     {
                                                       typoid1 => pat_type,  name1 => "pattern",
                                                       typoid2 => type,      name2 => "constraint",

                                                       message=>"pattern and constraint don't agree",
                                                       source_code_region,

                                                       unparse_phrase => unparse_pattern,
                                                       phrase_name    => "pattern",
                                                       phrase         => given_pattern,

                                                       callstack      => "compute_pattern_type/ds::TYPE_CONSTRAINT_PATTERN(2)" ! callstack,

                                                       undo_log
                                                     }
                                               ) 

                                                                                                                              if_debugging_say "\ncompute_pattern_type/ds::TYPE_CONSTRAINT_PATTERN done calling unify_typoids_and_handle_errors (succeeded)  [type-core-language-declaration-g.pkg]\n";
                                                ( ds::TYPE_CONSTRAINT_PATTERN (npat, type),
                                                  type
                                                );
                                            else
                                                                                                                               if_debugging_say "\ncompute_pattern_type/ds::TYPE_CONSTRAINT_PATTERN done calling unify_typoids_and_handle_errors (failed)  [type-core-language-declaration-g.pkg]\n";
                                                ( given_pattern,
                                                  tdt::WILDCARD_TYPOID
                                                );
                                            fi;
                                        };

                                    ds::AS_PATTERN (var_pattern as ds::VARIABLE_IN_PATTERN (vac::PLAIN_VARIABLE { vartypoid_ref, ... } ), main_pattern)
                                        =>
                                        {
                                                                                                                                if_debugging_say "\ncompute_pattern_type/AS_PATTERN calling compute_pattern_type  [type-core-language-declaration-g.pkg]\n";
                                            my  (main_pattern, main_pattern_type)
                                                =
                                                compute_pattern_type
                                                  ( main_pattern,
                                                    fn_nesting,
                                                    source_code_region,
                                                    "compute_pattern_type/AS_PATTERN" ! callstack
                                                  );

                                                                                                                                if_debugging_say "\ncompute_pattern_type/AS_PATTERN done calling compute_pattern_type  [type-core-language-declaration-g.pkg]\n";
                                            maybe_note_ref_in_undo_log  (undo_log, vartypoid_ref);

                                            vartypoid_ref :=  main_pattern_type;

                                            ( ds::AS_PATTERN (var_pattern, main_pattern),
                                              main_pattern_type
                                            );
                                        };

                                    ds::AS_PATTERN (constraint_pattern as ds::TYPE_CONSTRAINT_PATTERN (ds::VARIABLE_IN_PATTERN (vac::PLAIN_VARIABLE { vartypoid_ref, ... } ), constraining_type), main_pattern)
                                        =>
                                        {
                                                                                                                                if_debugging_say "\ncompute_pattern_type/AS_PATTERN II calling compute_pattern_type  [type-core-language-declaration-g.pkg]\n";
                                            my  (main_pattern, main_pattern_type)
                                                =
                                                compute_pattern_type
                                                  ( main_pattern,
                                                    fn_nesting,
                                                    source_code_region,
                                                    "compute_pattern_type/AS_PATTERN(2)" ! callstack
                                                  );
                                                                                                                                if_debugging_say "\ncompute_pattern_type/AS_PATTERN II done calling compute_pattern_type  [type-core-language-declaration-g.pkg]\n";

                                                                                                                                if_debugging_say "\ncompute_pattern_type/AS_PATTERN II calling unify_typoids_and_handle_errors  [type-core-language-declaration-g.pkg]\n";

                                            if (unify_typoids_and_handle_errors                                                 # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                  {
                                                    typoid1        => main_pattern_type,    name1 => "pattern",
                                                    typoid2        => constraining_type,    name2 => "constraint",

                                                    message        => "pattern and constraint don't agree",
                                                    source_code_region,

                                                    unparse_phrase =>  unparse_pattern,
                                                    phrase_name    => "pattern",
                                                    phrase         =>  given_pattern,

                                                    callstack      => "compute_pattern_type/AS_PATTERN(3)" ! callstack,

                                                    undo_log
                                                  }
                                               )

                                                                                                                                if_debugging_say "\ncompute_pattern_type/AS_PATTERN II done calling unify_typoids_and_handle_errors (succeeded)  [type-core-language-declaration-g.pkg]\n";
                                                maybe_note_ref_in_undo_log  (undo_log, vartypoid_ref);

                                                vartypoid_ref :=  constraining_type;

                                                ( ds::AS_PATTERN (constraint_pattern, main_pattern),
                                                  constraining_type
                                                );
                                            else
                                                                                                                                if_debugging_say "\ncompute_pattern_type/AS_PATTERN II done calling unify_typoids_and_handle_errors (failed)  [type-core-language-declaration-g.pkg]\n";
                                                ( given_pattern,
                                                  tdt::WILDCARD_TYPOID
                                                );
                                            fi;
                                        };

                                    p => bug "compute_pattern_type -- unexpected pattern";
                                esac;                                                                                           # fun compute_pattern_type

                                                                                                                                if *debugging print_callstack "\ncompute_pattern_type/BOTTOM [type-core-language-declaration-g.pkg] " callstack; fi;

                            result;
                        };

                    # Use unification to compute the most
                    # general non-typeagnostic type for
                    # an expression.  This includes checking
                    # that all values in a vector are of
                    # compatible type etc.
                    #
                    # Generalizing to typeagnostic type
                    # is done later if permitted by
                    # is tyj::is_value():
                    #
                    fun compute_expression_type                                                                                 # Not exported.
                        (
                          given_expression:                 ds::Deep_Expression,                                                # Our primary input.  We do not modify it.
                          syntax_treewalk_lexical_context:  Syntax_Treewalk_Lexical_Context,
                          source_code_region:               ds::Source_Code_Region,                                             # Debug support.
                          callstack:                        List(String)                                                        # Debug support.
                        )
                        :
                        (ds::Deep_Expression, tdt::Typoid)                                                                      # Rewritten (fully typed) version of given_expression, plus its type.
                        =
                        {
                                                                                                                                if *debugging print_callstack        "\ncompute_expression_type/TOP [type-core-language-declaration-g.pkg]" callstack; fi;
                                                                                                                                if_debugging_unparse_expression     ("\ncompute_expression_type/TOP [type-core-language-declaration-g.pkg]: expression unparse == ", (given_expression,100));
                                                                                                                                if_debugging_prettyprint_expression ("\ncompute_expression_type/TOP [type-core-language-declaration-g.pkg]: expression prettyprint == ", (given_expression,100));
                            fun bool_unify_err { type, name, message }
                                =
                                {
                                                                                                                                if_debugging_say "\ncompute_expression_type: bool_unify_err: calling unify_and-handle_errors  [type-core-language-declaration-g.pkg]\n";
                                                                                                                                result =
                                    unify_typoids_and_handle_errors                                                             # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                      {
                                        typoid1    => type,               name1 => name,
                                        typoid2    => mtt::bool_typoid,   name2 => "",

                                        message,
                                        source_code_region,

                                        unparse_phrase =>  unparse_expression,
                                        phrase_name    => "expression",
                                        phrase         =>  given_expression,

                                        callstack      => "compute_expression_type()/bool_unify_error()" ! callstack,

                                        undo_log
                                      };
                                                                                                                                if_debugging_say "\ncompute_expression_type: bool_unify_err: done calling unify_and-handle_errors  [type-core-language-declaration-g.pkg]\n";
                                                                                                                                result;
                                };      

                            # Typing of boolean short-circuit
                            # operators 'and' and 'or':
                            #
                            fun short_circuit_and_or
                                  (
                                    con,                                                                                        # ds::AND_EXPRESSION or ds::OR_EXPRESSION
                                    what,                                                                                       # "an" or "or"
                                    expression1,
                                    expression2
                                  )
                                =
                                {                                                                                               if_debugging_say "\ncompute_expression_type/short_circuit_and_or calling compute_expression_type.   [type-core-language-declaration-g.pkg]";

                                    my (expression1', type1) =   compute_expression_type (expression1, syntax_treewalk_lexical_context, source_code_region, "compute_expression_type/short_circuit_and_or"    ! callstack);
                                    my (expression2', type2) =   compute_expression_type (expression2, syntax_treewalk_lexical_context, source_code_region, "compute_expression_type/short_circuit_and_or(2)" ! callstack);

                                                                                                                                if_debugging_say "\ncompute_expression_type/short_circuit_and_or done calling compute_expression_type.  [type-core-language-declaration-g.pkg]";
                                    m =   string::cat ["operand of ", what, " is not of type bool"];

                                    if (    bool_unify_err {   type => type1,   name => "operand",   message => m   }
                                       and  bool_unify_err {   type => type2,   name => "operand",   message => m   }
                                       )

                                        ( con (expression1', expression2'),                                                                     #
                                          mtt::bool_typoid
                                        );
                                    else
                                        ( given_expression,                                                                     # Continue after error.
                                          tdt::WILDCARD_TYPOID
                                        );
                                    fi;
                                };

                                                                                                                                if *debugging print_callstack "\ncompute_expression_type/TOP.z [type-core-language-declaration-g.pkg] " callstack; fi;
                            case given_expression
                                #
                                ds::VARIABLE_IN_EXPRESSION { var             =>  var_ref  as  REF (vac::PLAIN_VARIABLE { vartypoid_ref, inlining_data, ... } ),
                                                             typescheme_args =>  _
                                                           }
                                    =>
                                    {   
                                                                                                                                 if_debugging_say "\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE/TOP.   [type-core-language-declaration-g.pkg]";
                                                                                                                                 if_debugging_unparse_typoid("\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE unparse [type-core-language-declaration-g.pkg]: *vartypoid_ref == ", *vartypoid_ref);
                                                                                                                                 if_debugging_prprint_typoid("\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE prprint [type-core-language-declaration-g.pkg]: *vartypoid_ref == ", *vartypoid_ref);
                                        case (inlining_data_to_my_type  inlining_data)                                          # For builtins like string::get_byte_as_char, inlining_data was set up from   all_primops   in   src/lib/compiler/front/semantic/symbolmapstack/base-types-and-ops.pkg
                                            #
                                            THE inl_typoid
                                                =>
                                                {   (tyj::instantiate_if_typescheme  (inl_typoid, symbolmapstack, "compute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE/THE st" ! callstack)) ->  (inl_typoid', fresh_meta_typevars);
                                                    (tyj::instantiate_if_typescheme  (*vartypoid_ref,  symbolmapstack, "compute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE/THE st" ! callstack)) ->  (var_typoid', _);

/* */                                                                                                                           fun prettyprint_typoid typoid =   if_debugging_prprint_typoid ("", typoid);
                                                                                                                                len =  list::length  fresh_meta_typevars;
                                                                                                                                if_debugging_say "\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE/THE t.   [type-core-language-declaration-g.pkg]";

                                                                                                                                if_debugging_unparse_typoid("\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE/THE [type-core-language-declaration-g.pkg] unparse_typoid inl_typoid ==",inl_typoid);
                                                                                                                                if_debugging_prprint_typoid("\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE/THE [type-core-language-declaration-g.pkg] prprint_typoid inl_typoid ==",inl_typoid);

                                                                                                                                if_debugging_unparse_typoid("\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE/THE [type-core-language-declaration-g.pkg] unparse_typoid inl_typoid'==",inl_typoid');
                                                                                                                                if_debugging_prprint_typoid("\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE/THE [type-core-language-declaration-g.pkg] prprint_typoid inl_typoid'==",inl_typoid');

                                                                                                                                if_debugging_unparse_typoid("\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE/THE [type-core-language-declaration-g.pkg] unparse_typoid var_typoid'==",var_typoid');
                                                                                                                                if_debugging_prprint_typoid("\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE/THE [type-core-language-declaration-g.pkg] prprint_typoid var_typoid'==",var_typoid');

                                                                                                                                if_debugging_say (sprintf "\nprprinting %d fresh_meta_typevars:  compute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE [type-core-language-declaration-g.pkg]"  len);
                                                                                                                                apply prettyprint_typoid  fresh_meta_typevars;
                                                                                                                                if_debugging_say (sprintf "\nprprinted %d fresh_meta_typevars.   compute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE [type-core-language-declaration-g.pkg]"  len);

                                                                                                                                if_debugging_say "\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE II calling unify_typoids.  [type-core-language-declaration-g.pkg]";

                                                                                                                                

                                                    uyt::unify_typoids                                                          # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                      ( "inl_typoid'", "var_typoid'", inl_typoid', var_typoid',
                                                        ["compute_expression_type/ds::VARIABLE_IN_EXPRESSION"],
                                                        undo_log
                                                      )
                                                    except
                                                        _ = ();   #  ??? XXX BUGGO FIXME 
                                                                                                                                len =  list::length  fresh_meta_typevars;
                                                                                                                                if_debugging_say (sprintf "\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE II done calling unify_typoids%s. [type-core-language-declaration-g.pkg]"
                                                                                                                                                  (len > 0 ?? " -- NOW SETTING VARIABLE_IN_EXPRESSION.typescheme_args" :: ""));
                                                                                                                                if_debugging_say (sprintf "\nprprinting %d fresh_meta_typevars: compute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE.z [type-core-language-declaration-g.pkg]" len);
                                                                                                                                apply prettyprint_typoid  fresh_meta_typevars;
                                                                                                                                if_debugging_say (sprintf "\nprprinted %d fresh_meta_typevars.  compute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE.z [type-core-language-declaration-g.pkg]" len);

                                                    ( ds::VARIABLE_IN_EXPRESSION
                                                        { var             =>  var_ref,
                                                          typescheme_args =>  fresh_meta_typevars
                                                        },
                                                      inl_typoid'
                                                    );
                                                };

                                            NULL =>
                                                {
                                                                                                                                if_debugging_say "\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE I: calling tyj::instantiate_if_typescheme.  [type-core-language-declaration-g.pkg]";

                                                    (tyj::instantiate_if_typescheme  (*vartypoid_ref, symbolmapstack, "compute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE I" ! callstack))
                                                        ->
                                                        (fresh_type, fresh_meta_typevars);
                                                                                                                                if_debugging_say "\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE I: done calling tyj::instantiate_if_typescheme.  [type-core-language-declaration-g.pkg]";
                                                                                                                                if_debugging_unparse_typoid ("\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE I: type unparse ==    [type-core-language-declaration-g.pkg]", fresh_type);
                                                                                                                                if_debugging_prprint_typoid ("\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE I: type prprint ==    [type-core-language-declaration-g.pkg]", fresh_type);
                                                                                                                                if_debugging_unparse_expression ("\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE I: result expression (unparse)==    [type-core-language-declaration-g.pkg]",
                                                                                                                                        (ds::VARIABLE_IN_EXPRESSION { var => var_ref, typescheme_args => fresh_meta_typevars },100));
                                                                                                                                if_debugging_prettyprint_expression ("\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::PLAIN_VARIABLE I: result expression (prprint) ==    [type-core-language-declaration-g.pkg]",
                                                                                                                                        (ds::VARIABLE_IN_EXPRESSION { var => var_ref, typescheme_args => fresh_meta_typevars },100));

                                                    ( ds::VARIABLE_IN_EXPRESSION
                                                        { var             =>  var_ref,
                                                          typescheme_args =>  fresh_meta_typevars
                                                        },
                                                      fresh_type
                                                    );
                                                };
                                        esac;
                                     };

                                ds::VARIABLE_IN_EXPRESSION { var =>  var_ref  as  REF (vac::OVERLOADED_VARIABLE _),  typescheme_args }
                                    =>
                                    {
                                                                                                                                 if_debugging_say (sprintf "\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION/vac::OVERLOADED_VARIABLE. |typescheme_args|=%d  [type-core-language-declaration-g.pkg] "
                                                                                                                                                           (list::length typescheme_args));
                                        ( given_expression,
                                          note_overloaded_variable (var_ref, typescheme_args, error_function source_code_region)
                                        );
                                    };

                                ds::VARIABLE_IN_EXPRESSION { var => REF _, ... }
                                    =>
                                    {
                                                                                                                                 if_debugging_say "\ncompute_expression_type/ds::VARIABLE_IN_EXPRESSION III.   [type-core-language-declaration-g.pkg]";
                                        ( given_expression,
                                          tdt::WILDCARD_TYPOID
                                        );
                                    };

                                ds::VALCON_IN_EXPRESSION { valcon as tdt::VALCON { typoid, ... },  ... }
                                    => 
                                    {
                                                                                                                                 if_debugging_say "\ncompute_expression_type/VALCON_IN_EXPRESSION.   [type-core-language-declaration-g.pkg]";
                                        (tyj::instantiate_if_typescheme  (typoid, symbolmapstack, "compute_expression_type/VALCON_IN_EXPRESSION" ! callstack))
                                            ->
                                            (type, fresh_meta_typevars);


                                                                                                                                len =  list::length  fresh_meta_typevars;
                                                                                                                                if (len > 0)
                                                                                                                                    if_debugging_say (sprintf "\ncompute_expression_type/ds::VALCON_IN_EXPRESSION -- NOW SETTING %d VALCON_IN_EXPRESSION.typescheme_args. [type-core-language-declaration-g.pkg]" len);
                                                                                                                                fi;
                                        ( ds::VALCON_IN_EXPRESSION  { valcon,  typescheme_args => fresh_meta_typevars },
                                          type
                                        );
                                    };

                                ds::INT_CONSTANT_IN_EXPRESSION (_, type) =>  { note_overloaded_literal type;  (given_expression, type);};
                                ds::UNT_CONSTANT_IN_EXPRESSION (_, type) =>  { note_overloaded_literal type;  (given_expression, type);};

                                ds::FLOAT_CONSTANT_IN_EXPRESSION  _ =>  (given_expression, mtt::float64_typoid);
                                ds::STRING_CONSTANT_IN_EXPRESSION _ =>  (given_expression, mtt::string_typoid);
                                ds::CHAR_CONSTANT_IN_EXPRESSION   _ =>  (given_expression, mtt::char_typoid);

                                ds::RECORD_IN_EXPRESSION fields
                                    =>
                                    {                                                                                           if_debugging_say "\ncompute_expression_type/RECORD_IN_EXPRESSION.   [type-core-language-declaration-g.pkg]";
                                        my (fields, field_types)
                                            =
                                            tyj::map_unzip  do_field  fields                                                    # Apply do_field to each field, return resulting value pairs in two lists.
                                            where
                                                fun do_field
                                                    ( label as ds::NUMBERED_LABEL _,
                                                      expression'
                                                    )
                                                    = 
                                                    {   my  (expression, expression_type)
                                                            =
                                                            compute_expression_type
                                                              ( expression',
                                                                syntax_treewalk_lexical_context,
                                                                source_code_region,
                                                                "compute_expression_type/RECORD_IN_EXPRESSION" ! callstack
                                                              );

                                                        ( (label, expression),
                                                          (label, expression_type)
                                                        );
                                                    };
                                            end;

                                        record_typoid
                                            =
                                            map  extract_field_name_and_type  (tyj::sort_fields field_types)
                                            where
                                                fun extract_field_name_and_type  (ds::NUMBERED_LABEL { name, ... }, field_type)
                                                    =
                                                    (name, field_type);
                                            end;

                                        ( ds::RECORD_IN_EXPRESSION fields,
                                          mtt::record_typoid   record_typoid
                                        );
                                    };

                                ds::RECORD_SELECTOR_EXPRESSION (label, record_expression)
                                    =>
                                    {
                                                                                                                                 if_debugging_say "\ncompute_expression_type/RECORD_SELECTOR_EXPRESSION   [type-core-language-declaration-g.pkg]";
                                                                                                                                 if_debugging_say "calling compute_expression_type:  compute_expression_type/RECORD_SELECTOR_EXPRESSION   [type-core-language-declaration-g.pkg]";
                                        my  (record_expression, record_expression_type)
                                            =
                                            compute_expression_type
                                              ( record_expression,
                                                syntax_treewalk_lexical_context,
                                                source_code_region,
                                                "compute_expression_type/RECORD_SELECTOR_EXPRESSION" ! callstack
                                              );
                                                                                                                                 if_debugging_say "\ncompute_expression_type() call done:  compute_expression_type/RECORD_SELECTOR_EXPRESSION   [type-core-language-declaration-g.pkg]";
                                        result_type
                                            =
                                            tyj::make_meta_typevar_and_type
                                              ( tdt::infinity,
                                                ["result_type in compute_expression_type/RECORD_SELECTOR_EXPRESSION  from  type-core-language-declaration-g.pkg"]
                                              );

                                        # Remember that we need to infer the
                                        # the rest of the fields in the record:
                                        #
                                        incomplete_record_type
                                            =
                                            tdt::TYPEVAR_REF
                                              (
                                                tdt::make_typevar_ref
                                                  (
                                                    tyj::make_incomplete_record_typevar
                                                      (label_types, tdt::infinity),

                                                    ["incomplete_record_type in compute_expression_type/RECORD_SELECTOR_EXPRESSION  from  type-core-language-declaration-g.pkg"]
                                              )   )
                                            where
                                                label_types =   [ (typer_junk::symbol_naming_label  label,  result_type) ];
                                            end;


                                        {                                                                                       if_debugging_say "\ncompute_expression_type/RECORD_SELECTOR_EXPRESSION: calling unify_typoids.   [type-core-language-declaration-g.pkg]";
                                            uyt::unify_typoids                                                                  # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                              ( "incomplete_record_type", "record_expression_type",
                                                 incomplete_record_type,   record_expression_type,
                                                ["compute_expression_type/RECORD_SELECTOR_EXPRESSION"],
                                                undo_log
                                              );
                                                                                                                                 if_debugging_say "\ncompute_expression_type/RECORD_SELECTOR_EXPRESSION: done calling unify_typoids.   [type-core-language-declaration-g.pkg]";
                                            (ds::RECORD_SELECTOR_EXPRESSION (label, record_expression), result_type);
                                        }
                                        except
                                            uyt::UNIFY_TYPOIDS  mode
                                               =
                                               {   error_function
                                                       source_code_region
                                                       err::ERROR
                                                       (   message("selecting a non-existing field from a record", mode))
                                                       (\\ pp
                                                           =
                                                           {  uty::reset_unparse_type ();
                                                              pp.newline();
                                                              pp.lit "the field name: ";

                                                              case label
                                                                  ds::NUMBERED_LABEL { name, ... } =>  uj::unparse_symbol pp name;
                                                              esac;

                                                              pp.newline();
                                                              pp.lit "the record type:    ";
                                                              unparse_typoid  pp  record_expression_type;                       pp.newline();
                                                              pp.lit "in expression:"; 
                                                              pp::break pp { blanks=>1, indent_on_wrap=>2 };
                                                              unparse_expression pp (given_expression, *print_depth);
                                                           }
                                                       );

                                                   ( given_expression,
                                                     tdt::WILDCARD_TYPOID
                                                   );
                                             };
                                    };

                                ds::VECTOR_IN_EXPRESSION (expressions, _)
                                    =>
                                    {                                                                                            if_debugging_say "\ncompute_expression_type/VECTOR_IN_EXPRESSION.   [type-core-language-declaration-g.pkg]";
                                        my  (expressions, expression_types)
                                            =
                                            tyj::map_unzip
                                                (\\ e =   compute_expression_type ( e,
                                                                                    syntax_treewalk_lexical_context,
                                                                                    source_code_region,
                                                                                    "compute_expression_type/VECTOR_IN_EXPRESSION" ! callstack
                                                                                  )
                                                )
                                                expressions;
                                                                                                                                 if_debugging_say "\ncompute_expression_type/VECTOR_IN_EXPRESSION: folding unify_typoids calls.   [type-core-language-declaration-g.pkg]";
                                        # Check that all expressions in vector have
                                        # compatible types, and combine them all to
                                        # yield the final vector element type:
                                        #
                                        vector_element_type
                                            =
                                            fold_backward
                                                (\\ (a, b) =    {   uyt::unify_typoids( "vector a",                             # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                                                        "vector b",
                                                                                        a, b,
                                                                                        ["compute_expression_type/VECTOR_IN_EXPRESSION  from  type-core-language-declaration-g.pkg"],
                                                                                        undo_log
                                                                                      );
                                                                    b;
                                                                }
                                                )
                                                (tyj::make_meta_typevar_and_type  (tdt::infinity, ["compute_expression_type/VECTOR_IN_EXPRESSION  from  type-core-language-declaration-g.pkg"]))
                                                expression_types;
                                                                                                                                 if_debugging_say "\ncompute_expression_type/VECTOR_IN_EXPRESSION: done folding unify_typoids calls.   [type-core-language-declaration-g.pkg]";

                                        ( ds::VECTOR_IN_EXPRESSION (expressions, vector_element_type),
                                          tdt::TYPCON_TYPOID (mtt::ro_vector_type, [vector_element_type])
                                        );
                                    }
                                    except
                                        uyt::UNIFY_TYPOIDS mode
                                            =
                                            {   error_function source_code_region err::ERROR
                                                  (message("vector expression type failure", mode))
                                                  err::null_error_body;

                                                (given_expression, tdt::WILDCARD_TYPOID);
                                            };


                                ds::SEQUENTIAL_EXPRESSIONS expressions
                                    => 
                                    {   (scan expressions) ->   (expressions, sequence_type);
                                        #
                                        ( ds::SEQUENTIAL_EXPRESSIONS expressions,
                                          sequence_type
                                        );
                                    }
                                    where                                                                                        if_debugging_say "\ncompute_expression_type/SEQUENTIAL_EXPRESSION.   [type-core-language-declaration-g.pkg]";
                                        fun scan NIL
                                                =>
                                                (NIL, mtt::void_typoid);

                                            scan [expression]
                                                => 
                                                {   my  (expression, expression_type)
                                                        =
                                                        compute_expression_type
                                                          ( expression,
                                                            syntax_treewalk_lexical_context,
                                                            source_code_region,
                                                            "compute_expression_type/SEQUENTIAL_EXPRESSIONS" ! callstack
                                                          );

                                                    ([expression], expression_type);
                                                };

                                            scan (expression ! rest)
                                                => 
                                                {   # The type of a sequence of expressions is
                                                    # the type of the final expression.  We
                                                    # do type-checking on all of them, but we
                                                    # only keep the result of last one:

                                                    my  (expression, _)                                                         # Discard type of non-final expression.
                                                        =
                                                        compute_expression_type
                                                          ( expression,
                                                            syntax_treewalk_lexical_context,
                                                            source_code_region,
                                                            "compute_expression_type/SEQUENTIAL_EXPRESSIONS(2)" ! callstack
                                                          );

                                                    (scan rest) ->   (expressions, expression_type);

                                                    (expression ! expressions, expression_type);                                # Type of final expression is type of sequence.
                                                };
                                        end;
                                    end;
        
                                ds::APPLY_EXPRESSION { operator, operand } 
                                    =>
                                    {
                                                                                                                                 if_debugging_say                     "\ncompute_expression_type/APPLY_EXPRESSION.1 [type-core-language-declaration-g.pkg]";
                                                                                                                                 if_debugging_unparse_expression     ("\ncompute_expression_type/APPLY_EXPRESSION.1 [type-core-language-declaration-g.pkg]: operator unparse == qqq ", (operator,100));
                                                                                                                                 if_debugging_prettyprint_expression ("\ncompute_expression_type/APPLY_EXPRESSION.1 [type-core-language-declaration-g.pkg]: operator prprint == qqq ", (operator,100));
                                                                                                                                 if_debugging_say                     "\ncompute_expression_type/APPLY_EXPRESSION.1 operator pprint done.  [type-core-language-declaration-g.pkg]";
                                                                                                                                 if_debugging_unparse_expression     ("\ncompute_expression_type/APPLY_EXPRESSION.1 [type-core-language-declaration-g.pkg]: operand  unparse == ", (operand, 100));
                                                                                                                                 if_debugging_prettyprint_expression ("\ncompute_expression_type/APPLY_EXPRESSION.1 [type-core-language-declaration-g.pkg]: operand  prprint == ", (operand, 100));
                                                                                                                                 if_debugging_say "\ncompute_expression_type/APPLY_EXPRESSION.1: calling compute_expression_type on operator. [type-core-language-declaration-g.pkg]";
                                        my  (operator, operator_type)
                                            =
                                            compute_expression_type
                                                (operator, syntax_treewalk_lexical_context, source_code_region, "compute_expression_type/APPLY_EXPRESSION" ! callstack);
                                                                                                                                 if_debugging_say                     "\ncompute_expression_type/APPLY_EXPRESSION.2: done calling compute_expression_type on operator.   [type-core-language-declaration-g.pkg]";
                                                                                                                                 if_debugging_unparse_expression     ("\ncompute_expression_type/APPLY_EXPRESSION.2 [type-core-language-declaration-g.pkg]: operator unparse == ", (operator,100));
                                                                                                                                 if_debugging_prettyprint_expression ("\ncompute_expression_type/APPLY_EXPRESSION.2 [type-core-language-declaration-g.pkg]: operator prprint == ", (operator,100));
                                                                                                                                 if_debugging_say                     "\ncompute_expression_type/APPLY_EXPRESSION.2 operator pprint done.  [type-core-language-declaration-g.pkg]";
                                                                                                                                 if_debugging_unparse_typoid         ("\ncompute_expression_type/APPLY_EXPRESSION.2 [type-core-language-declaration-g.pkg]: operator_type unparse == ", operator_type);
                                                                                                                                 if_debugging_prprint_typoid         ("\ncompute_expression_type/APPLY_EXPRESSION.2 [type-core-language-declaration-g.pkg]: operator_type prprint == ", operator_type);

                                                                                                                                 if_debugging_say "\ncompute_expression_type/APPLY_EXPRESSION [type-core-language-declaration-g.pkg]: calling compute_expression_type on operand.";
                                        my  (operand, operand_type)
                                            =
                                            compute_expression_type
                                              ( operand,
                                                syntax_treewalk_lexical_context,
                                                source_code_region,
                                                "compute_expression_type/APPLY_EXPRESSION(2)" ! callstack
                                              );
                                                                                                                                 if_debugging_say                     "\ncompute_expression_type/APPLY_EXPRESSION.3 [type-core-language-declaration-g.pkg]: done calling compute_expression_type on operand.";
                                                                                                                                 if_debugging_unparse_expression     ("\ncompute_expression_type/APPLY_EXPRESSION.3 [type-core-language-declaration-g.pkg]: operand unparse == ", (operand,100));
                                                                                                                                 if_debugging_prettyprint_expression ("\ncompute_expression_type/APPLY_EXPRESSION.3 [type-core-language-declaration-g.pkg]: operand prprint == ", (operand,100));
                                                                                                                                 if_debugging_unparse_typoid         ("\ncompute_expression_type/APPLY_EXPRESSION.3 [type-core-language-declaration-g.pkg]: operand_type unparse == ", operand_type);
                                                                                                                                 if_debugging_prprint_typoid         ("\ncompute_expression_type/APPLY_EXPRESSION.3 [type-core-language-declaration-g.pkg]: operand_type prprint == ", operand_type);
                                        expression
                                            =
                                            ds::APPLY_EXPRESSION { operator, operand };
                                                                                                                                 if_debugging_unparse_expression ("\ncompute_expression_type/APPLY_EXPRESSION [type-core-language-declaration-g.pkg]: expression == ", (expression,100));

                                        {
                                                                                                                                 if_debugging_say "\ncompute_expression_type/APPLY_EXPRESSION: calling compute_fn_application_type.   [type-core-language-declaration-g.pkg]";
                                            expression_type =  compute_fn_application_type (operator_type, operand_type, callstack);
                                                                                                                                 if_debugging_say "\ncompute_expression_type/APPLY_EXPRESSION: done calling compute_fn_application_type I.   [type-core-language-declaration-g.pkg]";
                                                                                                                                 if_debugging_prprint_typoid         ("\ncompute_expression_type/APPLY_EXPRESSION.4 [type-core-language-declaration-g.pkg]: operator_type   prprint == ", operator_type);
                                                                                                                                 if_debugging_prprint_typoid         ("\ncompute_expression_type/APPLY_EXPRESSION.4 [type-core-language-declaration-g.pkg]: operand_type    prprint == ", operand_type);
                                                                                                                                 if_debugging_prprint_typoid         ("\ncompute_expression_type/APPLY_EXPRESSION.4 [type-core-language-declaration-g.pkg]: expression_type prprint == ", expression_type);

                                            ( expression,
                                              expression_type
                                            );
                                        }
                                        except
                                            uyt::UNIFY_TYPOIDS  mode
                                            =
                                            {
                                                                                                                                 if_debugging_say "\ncompute_expression_type/APPLY_EXPRESSION: done calling compute_fn_application_type II.   [type-core-language-declaration-g.pkg]";
                                                operator_type   = tyj::drop_resolved_typevars  operator_type;

                                                reduced_operator_type =   tyj::head_reduce_typoid  operator_type;

                                                uty::reset_unparse_type ();

                                                if (mtt::is_arrow_type (reduced_operator_type))
                                                   #
                                                   error_function source_code_region err::ERROR
                                                       (message("Operator and operand do not agree", mode))
                                                       (\\ pp
                                                            =
                                                            {
#                                                               pp.newline();
                                                                pp::break pp { blanks=>1, indent_on_wrap=>2 };
                                                                pp.box' 0 0 {.
                                                                    pp.lit "operator domain: ";
                                                                    unparse_typoid pp  (mtt::domain reduced_operator_type);
                                                                };
                                                                pp::break pp { blanks=>1, indent_on_wrap=>2 };
#                                                               pp.newline();

                                                                pp.box' 0 0 {.
                                                                    pp.lit "operand:         ";
                                                                    unparse_typoid pp  operand_type;
                                                                };
                                                                pp::break pp { blanks=>1, indent_on_wrap=>2 };
#                                                               pp.newline();

                                                                pp.box' 0 0 {.
                                                                    pp.lit "in expression:";
                                                                    pp::break pp { blanks=>1, indent_on_wrap=>2 };
                                                                    unparse_expression pp (given_expression, *print_depth);
                                                                };
                                                                pp::break pp { blanks=>1, indent_on_wrap=>2 };
                                                            }
                                                       );

                                                    (given_expression, tdt::WILDCARD_TYPOID);

                                                else
                                                    error_function source_code_region err::ERROR
                                                        (message("operator is not a function", mode))
                                                        (\\ pp
                                                            =
                                                            { pp.newline();
                                                              pp.lit "operator: ";
                                                              unparse_typoid pp (operator_type);                        pp.newline();
                                                              pp.lit "in expression:";
                                                              pp::break pp { blanks=>1, indent_on_wrap=>2 };
                                                              unparse_expression pp (given_expression,*print_depth);
                                                            }
                                                        );

                                                    (given_expression, tdt::WILDCARD_TYPOID);
                                                fi;
                                            };
                                    };

                                ds::TYPE_CONSTRAINT_EXPRESSION (expression, constraining_type)
                                    =>
                                    {
                                                                                                                                if_debugging_say "\ncompute_expression_type/ds::TYPE_CONSTRAINT_EXPRESSION.   [type-core-language-declaration-g.pkg]";
                                        my  (expression, expression_type)
                                            =
                                            compute_expression_type
                                              ( expression,
                                                syntax_treewalk_lexical_context,
                                                source_code_region,
                                                "compute_expression_type/ds::TYPE_CONSTRAINT_EXPRESSION" ! callstack
                                              );

                                                                                                                                if_debugging_say "\ncompute_expression_type/TYPE_CONSTRAINT_EXPRESSION: calling unify_typoids_and_handle_errors.   [type-core-language-declaration-g.pkg]";

                                        if (unify_typoids_and_handle_errors                                                     # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                {
                                                  typoid1 => expression_type,    name1 => "expression",
                                                  typoid2 => constraining_type,  name2 => "constraint",

                                                  message => "expression doesn't match constraint",
                                                  source_code_region,

                                                  unparse_phrase =>  unparse_expression,
                                                  phrase_name    => "expression",
                                                  phrase         =>  given_expression,

                                                  callstack      => "compute_expression_type/ds::TYPE_CONSTRAINT_EXPRESSION(2)" ! callstack,

                                                  undo_log
                                                }
                                           )

                                                                                                                                 if_debugging_say "\ncompute_expression_type/TYPE_CONSTRAINT_EXPRESSION: done calling unify_typoids_and_handle_errors (succeeded).   [type-core-language-declaration-g.pkg]";
                                            (ds::TYPE_CONSTRAINT_EXPRESSION (expression, constraining_type), constraining_type);
                                        else
                                                                                                                                 if_debugging_say "\ncompute_expression_type/TYPE_CONSTRAINT_EXPRESSION: done calling unify_typoids_and_handle_errors (failed).   [type-core-language-declaration-g.pkg]";
                                            (given_expression, tdt::WILDCARD_TYPOID);
                                        fi;
                                    };

                                ds::EXCEPT_EXPRESSION (expression, (rules, _))
                                    =>
                                    {
                                                                                                                                 if_debugging_say "\ncompute_expression_type/EXCEPT_EXPRESSION.   [type-core-language-declaration-g.pkg]";
                                        my (expression, expression_type)
                                            =
                                            compute_expression_type
                                              ( expression,
                                                syntax_treewalk_lexical_context,
                                                source_code_region,
                                                "compute_expression_type/EXCEPT_EXPRESSION" ! callstack
                                              );

                                        my (rules, rule_pattern_type, exception_handler_type)
                                            =
                                            compute_match_type
                                              ( rules,
                                                syntax_treewalk_lexical_context,
                                                source_code_region,
                                                "compute_expression_type/EXCEPT_EXPRESSION(2)" ! callstack
                                              );

                                        expression =  ds::EXCEPT_EXPRESSION (expression, (rules, rule_pattern_type));

                                                                                                                                 if_debugging_say "\ncompute_expression_type/EXCEPT_EXPRESSION: above call to unify_typoids   [type-core-language-declaration-g.pkg]";

                                        {   uyt::unify_typoids                                                                  # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                              ( "exception_handler_type",    "exception_typoid --> expression_type",            
                                                 exception_handler_type,  mtt::exception_typoid --> expression_type,
                                                 ["compute_expression_type/EXCEPT_EXPRESSION"],
                                                 undo_log
                                              );

                                            (expression, expression_type);
                                        }
                                        except uyt::UNIFY_TYPOIDS  mode
                                            =
                                            {
                                                                                                                                if_debugging_say "\ncompute_expression_type/EXCEPT_EXPRESSION: above second call to unify_typoids   [type-core-language-declaration-g.pkg]";

                                                if (unify_typoids_and_handle_errors                                             # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                        {
                                                          typoid1 => mtt::domain (tyj::drop_resolved_typevars  exception_handler_type),   name1 => "handler domain",
                                                          typoid2 => mtt::exception_typoid,                                               name2 => "",

                                                          message => "handler domain is not exception",
                                                          source_code_region,

                                                          unparse_phrase =>  unparse_expression,
                                                          phrase_name    => "expression",
                                                          phrase         =>  given_expression,

                                                          callstack      => "compute_expression_type/EXCEPT_EXPRESSION(3)" ! callstack,

                                                          undo_log
                                                        }
                                                   )

                                                                                                                                if_debugging_say "\ncompute_expression_type/EXCEPT_EXPRESSION: above third call to unify_typoids   [type-core-language-declaration-g.pkg]";

                                                    unify_typoids_and_handle_errors                                             # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                      {
                                                        typoid1 => expression_type,                                                  name1 => "body",
                                                        typoid2 => mtt::range (tyj::drop_resolved_typevars exception_handler_type),  name2 => "handler range",

                                                        message => "expression and handler don't agree",
                                                        source_code_region,

                                                        unparse_phrase =>  unparse_expression,
                                                        phrase_name    => "expression",
                                                        phrase         =>  given_expression,

                                                        callstack      => "compute_expression_type/EXCEPT_EXPRESSION(4)" ! callstack,

                                                        undo_log
                                                      };
                                                else
                                                    FALSE;
                                                fi;

                                                ( given_expression,
                                                  tdt::WILDCARD_TYPOID
                                                );
                                            };
                                    };

                                ds::RAISE_EXPRESSION (expression, _)
                                    =>
                                    {
                                                                                                                                 if_debugging_say "\ncompute_expression_type/RAISE_EXPRESSION:  TOP: calling compute_expression_type.   [type-core-language-declaration-g.pkg]";
                                        my (expression, expression_type)
                                            =
                                            compute_expression_type
                                              ( expression,
                                                syntax_treewalk_lexical_context,
                                                source_code_region,
                                                "compute_expression_type/RAISE_EXPRESSION" ! callstack
                                              );

                                                                                                                                if_debugging_say "\ncompute_expression_type/RAISE_EXPRESSION:  BBB: back from compute_expression_type.   [type-core-language-declaration-g.pkg]";

                                                                                                                                if_debugging_say "\ncompute_expression_type/RAISE_EXPRESSION:  CCC: calling unify_typoids_and_handle_errors.   [type-core-language-declaration-g.pkg]";
                                        # Verify that 'expression' has an exception type:
                                        #
                                        unify_typoids_and_handle_errors                                                         # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                            {
                                              typoid1 => expression_type,     name1 => "raised",
                                              typoid2 => mtt::exception_typoid,  name2 => "",

                                              message => "argument of raise is not an exception",
                                              source_code_region,

                                              unparse_phrase =>  unparse_expression,
                                              phrase_name    => "expression",
                                              phrase         =>  given_expression,

                                              callstack      => "compute_expression_type/RAISE_EXPRESSION(2)" ! callstack,

                                              undo_log
                                            };

                                        # Now we discard all available type information
                                        # and return a totally unrestricted type
                                        # because the environment is free to consider
                                        # a 'raise' as returning whatever type it likes
                                        # -- since in fact 'raise' does not return at all:
                                        #
                                        fantasy_return_type
                                            =
                                            tyj::make_meta_typevar_and_type  (tdt::infinity, ["compute_expression_type/RAISE_EXPRESSION   from   type-core-language-declaration-g.pkg"]);


                                                                                                                                 if_debugging_say "\ncompute_expression_type/RAISE_EXPRESSION   [type-core-language-declaration-g.pkg]:  BOT";
                                        (ds::RAISE_EXPRESSION (expression, fantasy_return_type), fantasy_return_type);
                                    };

                                ds::LET_EXPRESSION (declaration, expression)
                                    => 
                                    {
                                        # The type of a 'let' construct
                                        # depends entirely upon its terminal
                                        # 'expression':

                                                                                                                                if_debugging_say "\ncompute_expression_type/LET_EXPRESSION:  TOP: calling do_declaration on LET_EXPRESSION.d.    [type-core-language-declaration-g.pkg]";
                                        declaration =   do_declaration
                                                          ( declaration,
                                                            enter_let_scope (syntax_treewalk_lexical_context),
                                                            source_code_region,
                                                            "compute_expression_type/LET_EXPRESSION" ! callstack
                                                          );
                                                                                                                                if_debugging_say "\ncompute_expression_type/LET_EXPRESSION:  done calling do_declaration on LET_EXPRESSION.d.    [type-core-language-declaration-g.pkg]";
                                                                                                                                if_debugging_say "\ncompute_expression_type/LET_EXPRESSION:  BBB: calling compute_expression_type on LET_EXPRESSION.e.    [type-core-language-declaration-g.pkg]";
                                        my (expression, expression_type)
                                            =
                                            compute_expression_type
                                              ( expression,
                                                syntax_treewalk_lexical_context,
                                                source_code_region,
                                                "compute_expression_type/LET_EXPRESSION(2)" ! callstack
                                              );
                                                                                                                                if_debugging_say "\ncompute_expression_type/LET_EXPRESSION:  done calling compute_expression_type on LET_EXPRESSION.e.    [type-core-language-declaration-g.pkg]";
                                                                                                                                if_debugging_say "\ncompute_expression_type/LET_EXPRESSION:  BOT.    [type-core-language-declaration-g.pkg]";

                                        ( ds::LET_EXPRESSION (declaration, expression),
                                          expression_type
                                        );
                                    };

                                ds::CASE_EXPRESSION (expression, rules, is_match)
                                    =>
                                    {                                                                                           if_debugging_say "\ncompute_expression_type/CASE_EXPRESSION:  TOP.    [type-core-language-declaration-g.pkg]";

                                        my (expression, expression_type) =  compute_expression_type (expression, syntax_treewalk_lexical_context, source_code_region, "compute_expression_type/CASE_EXPRESSION(2) " ! callstack);
                                        my (rules', _, rule_type)        =  compute_match_type      (rules,      syntax_treewalk_lexical_context, source_code_region, "compute_expression_type/CASE_EXPRESSION(3) " ! callstack);

                                        expression = ds::CASE_EXPRESSION (expression, rules', is_match);

                                                                                                                                if_debugging_say "\ncompute_expression_type/CASE_EXPRESSION:  above call to compute_fn_application_type.   [type-core-language-declaration-g.pkg]";
                                        ( expression,
                                          compute_fn_application_type (rule_type, expression_type, callstack)
                                        )
                                        except
                                            uyt::UNIFY_TYPOIDS  mode
                                                =
                                                {   if is_match
                                                                                                                                if_debugging_say "\ncompute_expression_type/CASE_EXPRESSION:  above call to unify_typoids_and_handle_errors.   [type-core-language-declaration-g.pkg]";

                                                        unify_typoids_and_handle_errors                                         # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                          {
                                                            typoid1 => mtt::domain rule_type,    name1 => "rule domain",
                                                            typoid2 => expression_type,   name2 => "object",

                                                            message=>"case object and rules don't agree",
                                                            source_code_region,

                                                            unparse_phrase =>  unparse_expression,
                                                            phrase_name    => "expression",
                                                            phrase         =>  given_expression,

                                                            callstack      => "compute_expression_type/CASE_EXPRESSION(4)" ! callstack,

                                                            undo_log
                                                          };
                                                    else 
                                                        declaration =   case rules 
                                                                            #   
                                                                            (ds::CASE_RULE (pattern, _)) ! _
                                                                                => 
                                                                                ds::VALUE_NAMING
                                                                                  {
                                                                                    pattern,
                                                                                    expression           =>  given_expression,
                                                                                    raw_typevars         =>  REF [],
                                                                                    generalized_typevars =>  []
                                                                                  };

                                                                            _ => bug "unexpected rule list 456";
                                                                        esac;

                                                                                                                                if_debugging_say "\ncompute_expression_type/CASE_EXPRESSION:  above second call to unify_typoids_and_handle_errors.   [type-core-language-declaration-g.pkg]";

                                                        unify_typoids_and_handle_errors                                         # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                          {
                                                            typoid1 => mtt::domain rule_type,   name1 => "pattern",
                                                            typoid2 => expression_type,        name2 => "expression",

                                                            message => "pattern and expression in my declaration don't agree",
                                                            source_code_region,

                                                            unparse_phrase =>  unparse_named_value,
                                                            phrase_name    => "declaration",
                                                            phrase         =>  declaration,

                                                            callstack      => "compute_expression_type/CASE_EXPRESSION(5)" ! callstack,

                                                            undo_log
                                                          };
                                                    fi;

                                                                                                                                  if_debugging_say "\ncompute_expression_type/CASE_EXPRESSION:  BOT.   [type-core-language-declaration-g.pkg]";
                                                    ( given_expression,
                                                      tdt::WILDCARD_TYPOID
                                                    );
                                                };
                                    };
                                        #######################################################
                                        # This causes 'case' to behave differently from 'let'
                                        #       -- bound variables do not have generic types.
                                        #######################################################

                                ds::IF_EXPRESSION { test_case, then_case, else_case }
                                    =>
                                    {
                                                                                                                                 if_debugging_say "\ncompute_expression_type/IF_EXPRESSION:  TOP.";

                                        my (test_case', tty) = compute_expression_type (test_case, syntax_treewalk_lexical_context, source_code_region, "compute_expression_type/ds::IF_EXPRESSION(1) " ! callstack);
                                        my (then_case', tct) = compute_expression_type (then_case, syntax_treewalk_lexical_context, source_code_region, "compute_expression_type/ds::IF_EXPRESSION(2) " ! callstack);
                                        my (else_case', ect) = compute_expression_type (else_case, syntax_treewalk_lexical_context, source_code_region, "compute_expression_type/ds::IF_EXPRESSION(3) " ! callstack);

                                        if
                                        (  bool_unify_err
                                               { type  => tty,
                                                 name    => "test expression",
                                                 message => "test expression in if is not of type bool"
                                               }
                                        and
                                           unify_typoids_and_handle_errors                                                      # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                               {
                                                 typoid1 => tct,   name1 => "then branch",
                                                 typoid2 => ect,   name2 => "else branch",

                                                 message  => "types of if branches do not agree",
                                                 source_code_region,

                                                 unparse_phrase =>  unparse_expression,
                                                 phrase_name    => "expression",
                                                 phrase         =>  given_expression,

                                                 callstack      => "compute_expression_type/ds::IF_EXPRESSION(4)" ! callstack,

                                                 undo_log
                                               }
                                        )

                                                                                                                                if_debugging_say "\ncompute_expression_type/IF_EXPRESSION:  success.   [type-core-language-declaration-g.pkg]";
                                            ( ds::IF_EXPRESSION { test_case => test_case',
                                                                  then_case => then_case',
                                                                  else_case => else_case'
                                                                },
                                              tct
                                            );
                                        else
                                                                                                                                if_debugging_say "\ncompute_expression_type/IF_EXPRESSION:  failure.   [type-core-language-declaration-g.pkg]";
                                            ( given_expression,
                                              tdt::WILDCARD_TYPOID
                                            );
                                        fi;
                                    };

                                ds::AND_EXPRESSION (expression1, expression2)
                                    =>
                                    {
                                                                                                                                if_debugging_say "\ncompute_expression_type/ds::AND_EXPRESSION.   [type-core-language-declaration-g.pkg]";
                                        short_circuit_and_or (ds::AND_EXPRESSION, "and", expression1, expression2);
                                    };

                                ds::OR_EXPRESSION (expression1, expression2)
                                    =>
                                    {
                                                                                                                                if_debugging_say "\ncompute_expression_type/OR_EXPRESSION.   [type-core-language-declaration-g.pkg]";
                                        short_circuit_and_or (ds::OR_EXPRESSION, "or", expression1, expression2);
                                    };

                                ds::WHILE_EXPRESSION { test, expression }
                                    =>
                                    {
                                                                                                                                 if_debugging_say "\ncompute_expression_type/ds::WHILE_EXPRESSION.   [type-core-language-declaration-g.pkg]";

                                        my (test', testtype) = compute_expression_type (test,       syntax_treewalk_lexical_context, source_code_region, "compute_expression_type/ds::WHILE_EXPRESSION(1) " ! callstack);
                                        my (expression', _)  = compute_expression_type (expression, syntax_treewalk_lexical_context, source_code_region, "compute_expression_type/ds::WHILE_EXPRESSION(2) " ! callstack);

                                        if (bool_unify_err
                                                { type  => testtype,
                                                  name    => "test expression",
                                                  message => "test expression in while is not of type bool"
                                                }
                                           )

                                            (ds::WHILE_EXPRESSION { test => test', expression => expression' }, mtt::void_typoid);
                                        else
                                            (expression, tdt::WILDCARD_TYPOID);
                                        fi;
                                    };

                                ds::FN_EXPRESSION (rules, _)
                                    => 
                                    {
                                                                                                                                 if_debugging_say "\ncompute_expression_type/ds::FN_EXPRESSION.   [type-core-language-declaration-g.pkg]";
                                        my (rules, rule_pattern_type, rule_type)
                                            =
                                            compute_match_type
                                              ( rules,
                                                syntax_treewalk_lexical_context,
                                                source_code_region,
                                                "compute_expression_type/ds::FN_EXPRESSION" ! callstack
                                              );

                                        ( ds::FN_EXPRESSION (rules, rule_pattern_type),
                                          rule_type
                                        );
                                    };

                                ds::SOURCE_CODE_REGION_FOR_EXPRESSION (expression, source_code_region)
                                    => 
                                    {
                                                                                                                                 if_debugging_say "\ncompute_expression_type/ds::SOURCE_CODE_REGION_FOR_EXPRESSION.   [type-core-language-declaration-g.pkg]";
                                        my (expression, expression_type)
                                            =
                                            compute_expression_type
                                              ( expression,
                                                syntax_treewalk_lexical_context,
                                                source_code_region,
                                                callstack
                                              );

                                        ( ds::SOURCE_CODE_REGION_FOR_EXPRESSION (expression, source_code_region),
                                          expression_type
                                        );
                                    };

                                _ => bug "exptype -- bad expression";
                            esac;
                        }                                                                                                       # fun compute_expression_type

                    also
                    fun compute_rule_type                                                                                       # Not exported.
                          (
                            ds::CASE_RULE (pattern, expression),
                            syntax_treewalk_lexical_context,
                            source_code_region, callstack                                                                       # Debug support.
                          )
                        =  
                        {
                                                                                                                                if *debugging print_callstack "\ncompute_rule_type/TOP [type-core-language-declaration-g.pkg]" callstack; fi;
                                                                                                                                if *debugging printf "compute_rule_type/TOP [type-core-language-declaration-g.pkg]: incrementing lex.fn_nesting from %d to %d\n"
                                                                                                                                                     (syntax_treewalk_lexical_context.fn_nesting) (syntax_treewalk_lexical_context.fn_nesting + 1); fi;
                            syntax_treewalk_lexical_context     =  enter_fn_scope  syntax_treewalk_lexical_context;

                            my   (pattern, pattern_type)        =  compute_pattern_type    (pattern,    syntax_treewalk_lexical_context.fn_nesting,  source_code_region, "compute_rule_type(1)" ! callstack); if_debugging_say "\ncompute_rule_type calling compute_expression_type.   [type-core-language-declaration-g.pkg]";
                            my   (expression, expression_type)  =  compute_expression_type (expression, syntax_treewalk_lexical_context,             source_code_region, "compute_rule_type(2)" ! callstack);

                                                                                                                                if_debugging_say "\ncompute_rule_type done calling compute_expression_type.   [type-core-language-declaration-g.pkg]";

                                                                                                                                if *debugging print_callstack "\ncompute_rule_type/BOTTOM [type-core-language-declaration-g.pkg]" callstack; fi;
                                                                                                                                if *debugging printf "compute_rule_type/BOTTOM [type-core-language-declaration-g.pkg]: returning from lex.fn_nesting %d to %d\n"
                                                                                                                                                        (syntax_treewalk_lexical_context.fn_nesting) (syntax_treewalk_lexical_context.fn_nesting - 1); fi;
                            ( ds::CASE_RULE (pattern, expression),
                              pattern_type,
                              pattern_type --> expression_type
                            );
                        }

                    also
                    fun compute_match_type (rules, syntax_treewalk_lexical_context, source_code_region, callstack)              # Not exported.
                        =
                        case rules
                            #
                            [] => bug "empty rule list in typecheck::compute_match_type";

                            [rule]
                                => 
                                {   my (rule0, argt, rule_type)
                                        =
                                        compute_rule_type
                                          ( rule,
                                            syntax_treewalk_lexical_context,
                                            source_code_region,
                                            "compute_match_type(1)" ! callstack
                                          );

                                    ( [rule0],
                                      argt,
                                      rule_type
                                    );
                                };

                            rule ! rest
                                =>
                                {   my (rule0, argt, rule_type)
                                        =
                                        compute_rule_type
                                          ( rule,
                                            syntax_treewalk_lexical_context,
                                            source_code_region,
                                            "compute_match_type(2)" ! callstack
                                          );
                                    #
                                    fun unify_with_rule0 rule
                                        =
                                        {   my (rule', argt', rule_type')
                                                =
                                                compute_rule_type
                                                  ( rule,
                                                    syntax_treewalk_lexical_context,
                                                    source_code_region,
                                                    "compute_match_type(3)" ! callstack
                                                  );

                                                                                                                                if_debugging_say "\ncompute_match_type: unify_with_rule0: calling unify_typoids_and_handle_errors.   [type-core-language-declaration-g.pkg]";

                                            unify_typoids_and_handle_errors                                                     # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                              {
                                                typoid1 => rule_type,  name1 => "earlier rule (s)",
                                                typoid2 => rule_type', name2 => "this rule",

                                                message => "types of rules don't agree",
                                                source_code_region,

                                                unparse_phrase =>  unparse_rule,
                                                phrase_name    => "rule",
                                                phrase         =>  rule,

                                                callstack      => "compute_match_type(4)" ! callstack,

                                                undo_log
                                              };

                                            rule';
                                        };

                                    ( rule0 ! (map  unify_with_rule0  rest),
                                      argt,
                                      rule_type
                                    );
                                };
                        esac

                    also
                    fun do_declaration
                        ( given_declaration:                    ds::Declaration,
                          syntax_treewalk_lexical_context:      Syntax_Treewalk_Lexical_Context,
                          source_code_region:                   ds::Source_Code_Region,
                          callstack:                            List(String)                                                    # Debug support.
                        )
                        :
                        ds::Declaration
                        =
                        {
                                                                                                                                if *debugging   print_callstack "\ndo_declaration/TOP   [type-core-language-declaration-g.pkg]" callstack; fi;
                                                                                                                                if_debugging_unparse_declaration     ("\ndo_declaration/TOP given_declaration unparse     is:    [type-core-language-declaration-g.pkg]\n",  given_declaration);
                                                                                                                                if_debugging_prettyprint_declaration ("\ndo_declaration/TOP given_declaration prettyprint is:    [type-core-language-declaration-g.pkg]\n", (given_declaration,100));

                            case given_declaration
                                #
                                ds::VALUE_DECLARATIONS named_values
                                    =>
                                    {
                                                                                                                                if_debugging_say "\ndo_declaration/VALUE_DECLARATIONS   [type-core-language-declaration-g.pkg]\n";
                                        declaration
                                            =
                                            ds::VALUE_DECLARATIONS (map  do_named_value  named_values)
                                            where
                                                fun  do_named_value                                                             # Processing something typically like   x = foo(bar);   but potentially    my THIS(that,that,tother) = foo(a,b,bar(y,z));   or worse.
                                                     (  named_value
                                                        as
                                                        ds::VALUE_NAMING
                                                          {
                                                            pattern          =>  given_pattern,                                 #  Left-hand side of our '=' statement.
                                                            expression       =>  given_expression,                              # Right-hand side of our '=' statement.
                                                            raw_typevars,
                                                            generalized_typevars =>  generalized_typevars'                      # Ignored.  Always [] at this point, I think.
                                                          }
                                                     )
                                                    =
                                                    {
                                                                                                                                if_debugging_say "\ndo_declaration/VALUE_DECLARATIONS/do_named_value   [type-core-language-declaration-g.pkg]\n";
                                                                                                                                #
                                                                                                                                if_debugging_unparse_pattern        ("\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  pattern unparse == \n",    (given_pattern,   100));
                                                                                                                                if_debugging_prettyprint_pattern    ("\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  pattern prprint == \n",    (given_pattern,   100));
                                                                                                                                #
                                                                                                                                if_debugging_unparse_expression     ("\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  expression unparse == \n", (given_expression,100));
                                                                                                                                if_debugging_prettyprint_expression ("\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  expression prprint == \n", (given_expression,100));

                                                        my (pattern,    pattern_type   ) =  compute_pattern_type    (given_pattern,        tdt::infinity,                   source_code_region, "do_declaration/VALUE_DECLARATIONS/do_named_value(1) " ! callstack);    # Propagate type data leaf-to-root in pattern.
                                                        my (expression, expression_type) =  compute_expression_type (given_expression,     syntax_treewalk_lexical_context, source_code_region, "do_declaration/VALUE_DECLARATIONS/do_named_value(2) " ! callstack);    # Propagate type data leaf-to-root in expression.

                                                                                                                                if_debugging_say "\ndo_declaration/VALUE_DECLARATIONS/do_named_value done calling compute_expression_type.   [type-core-language-declaration-g.pkg]";
                                                                                                                                #
                                                                                                                                if_debugging_unparse_pattern        ("\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  pattern unparse == \n",     (pattern,100));
                                                                                                                                if_debugging_prettyprint_pattern    ("\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  pattern prettyprint == \n", (pattern,100));
                                                                                                                                #
                                                                                                                                if_debugging_unparse_expression     ("\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  expression unparse == \n",     (expression,100));
                                                                                                                                if_debugging_prettyprint_expression ("\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  expression prettyprint == \n", (expression,100));
                                                                                                                                #
                                                                                                                                if_debugging_unparse_typoid     ("\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  pattern type unparse == \n",    pattern_type);
                                                                                                                                if_debugging_prprint_typoid     ("\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  pattern type prprint == \n",    pattern_type);
                                                                                                                                #
                                                                                                                                if_debugging_unparse_typoid     ("\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  expression type unparse == \n", expression_type);
                                                                                                                                if_debugging_prprint_typoid     ("\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  expression type prprint == \n", expression_type);

                                                        generalize =  is_value  given_expression;                               # (Once had in addition:   "or is_variable_typoid expression_type")
                                                                                                                                #
                                                                                                                                # Decide whether to try generalizing this expression.  For background see:  http://en.wikipedia.org/wiki/Value_restriction
                                                                                                                                #
                                                                                                                                # This is the sole call to   tyj::is_value(),
                                                                                                                                # the fn implementing the "value restriction" test.

                                                                                                                                if *debugging
                                                                                                                                    say "\n=========================== do_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  is_value() reports that:\n";
                                                                                                                                    say (sprintf "Following expression %s a value:\n" (generalize ?? "IS" :: "is NOT"));
                                                                                                                                    if_debugging_unparse_expression ("", (given_expression,100));
                                                                                                                                fi;     

                                                                                                                                if_debugging_say "\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  calling unify_typoids_and_handle_errors on pattern + expression\n";

                                                        unify_typoids_and_handle_errors                                         # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                            {                                                                   # Propagate type information between left- and right-hand side.
                                                              name1 => "pattern",       typoid1 => pattern_type,                # typoid1 and typoid2 are the two args that matter.
                                                              name2 => "expression",    typoid2 => expression_type,

                                                              message => "Pattern and expression in 'my' declaration do not agree",

                                                              source_code_region,

                                                              unparse_phrase =>  unparse_named_value,
                                                              phrase_name    => "declaration",
                                                              phrase         =>  named_value,

                                                              callstack      =>  "do_declaration/VALUE_DECLARATIONS/do_named_value(3)" ! callstack,

                                                              undo_log
                                                            };
                                                                                                                                if_debugging_say "\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  done calling unify_typoids_and_handle_errors on pattern + expression\n";
                                                                                                                                if_debugging_say "\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]:  calling generalize_pattern\n";
                                                        generalized_typevars
                                                            =
                                                            generalize_pattern                                                  # This is the only call to generalize_pattern().
                                                              (
                                                                given_pattern,                                                  # <------------ SHOULD THIS BE pattern INSTEAD? (Empirically, seems to make no difference.)
                                                               *raw_typevars,                                                   # Type variables explicitly specified by user:  X, Y, ... 
                                                                syntax_treewalk_lexical_context,
                                                                generalize,
                                                                source_code_region,
                                                                "do_declaration/VALUE_DECLARATIONS/do_named_value(4)" ! callstack
                                                              );

                                                                                                                                if *debugging
                                                                                                                                    printf "\ndo_declaration/VALUE_DECLARATIONS/do_named_value [type-core-language-declaration-g.pkg]: Creating NAMED_VALUE node with %d (was %d) generalized_typevars: \n"
                                                                                                                                    (list::length generalized_typevars) (list::length generalized_typevars');
                                                                                                                                    printf "\nNAMED_VALUE.generalized_typevars [type-core-language-declaration-g.pkg]: (%d)\n" (list::length generalized_typevars);
                                                                                                                                    apply  unparse_typevar_ref  generalized_typevars
                                                                                                                                        where
/* */                                                                                                                                       fun unparse_typevar_ref  typevar_ref
                                                                                                                                                =
                                                                                                                                                if_debugging_unparse_typevar_ref ("", typevar_ref);
                                                                                                                                        end;
                                                                                                                                    printf "\n";
                                                                                                                                    if_debugging_unparse_pattern        ("\n[type-core-language-declaration-g.pkg]  NAMED_VALUE.pattern == \n",                (pattern,   100));
                                                                                                                                    if_debugging_unparse_expression     ("\n[type-core-language-declaration-g.pkg]  NAMED_VALUE.expression == \n",             (expression,100));
                                                                                                                                    #
                                                                                                                                    if_debugging_prettyprint_pattern    ("\n[type-core-language-declaration-g.pkg]  NAMED_VALUE.pattern    prettyprint == \n", (pattern,   100));
                                                                                                                                    if_debugging_prettyprint_expression ("\n[type-core-language-declaration-g.pkg]  NAMED_VALUE.expression prettyprint == \n", (expression,100));
                                                                                                                                fi;
                                                        ds::VALUE_NAMING
                                                          {
                                                            pattern,
                                                            expression,
                                                            raw_typevars,
                                                            generalized_typevars
                                                          };
                                                    };                                                                          # fun do_named_value
                                            end;                                                                                # where
                                                                                                                                if *debugging       print_callstack   "\ndo_declaration/VALUE_DECLARATIONS/BOTTOM [type-core-language-declaration-g.pkg]" callstack; fi;
                                                                                                                                if_debugging_unparse_declaration     ("\ndo_declaration/VALUE_DECLARATIONS/BOTTOM [type-core-language-declaration-g.pkg]:  final result unparse     is:\n", declaration);
                                                                                                                                if_debugging_prettyprint_declaration ("\ndo_declaration/VALUE_DECLARATIONS/BOTTOM [type-core-language-declaration-g.pkg]:  final result prettyprint is:\n", (declaration,100));

                                        declaration;
                                    };

                                ds::RECURSIVE_VALUE_DECLARATIONS  named_recursive_values_records                                # "rvbs" == "recursive value bindings".
                                    =>
                                    {
                                                                                                                                if *debugging print_callstack "do_declaration/RECURSIVE_VALUE_DECLARATIONS/TOP  [type-core-language-declaration-g.pkg]" callstack; fi;
                                                                                                                                if *debugging printf "do_declaration/RECURSIVE_VALUE_DECLARATIONS/TOP:  incrementing lex.fn_nesting from %d to %d  [type-core-language-declaration-g.pkg]\n"
                                                                                                                                                     (syntax_treewalk_lexical_context.fn_nesting) (syntax_treewalk_lexical_context.fn_nesting + 1);
                                                                                                                                fi;
                                        previous_syntax_treewalk_lexical_context
                                            =
                                            syntax_treewalk_lexical_context;

                                        syntax_treewalk_lexical_context
                                            =
                                            enter_fn_scope   syntax_treewalk_lexical_context;

                                                                                                                                if_debugging_say "\ndo_declaration/RECURSIVE_VALUE_DECLARATIONS: TOP   [type-core-language-declaration-g.pkg]";

                                                                                                                                # A general RECURSIVE_VALUE_DECLARATIONS statement              # NB: Technically, the values don't have to be functions, they can be anything,
                                                                                                                                # represents mutually recursive functions each of               # but in practice it is vanishingly rare for them to be anything but functions. 
                                                                                                                                # which may have multiple rules:
                                                                                                                                #
                                                                                                                                #    fun foo ... => ...;
                                                                                                                                #        foo ... => ...;
                                                                                                                                #    end
                                                                                                                                #    also
                                                                                                                                #    fun bar ... => ...;
                                                                                                                                #        bar ... => ...;
                                                                                                                                #    end;
                                                                                                                                #
                                                                                                                                # Here each function (foo, bar ...) will be
                                                                                                                                # represented by one NAMED_RECURSIVE_VALUE
                                                                                                                                # record, where NAMED_RECURSIVE_VALUE/expression
                                                                                                                                # will be a ds::FN_EXPRESSION (rules, _) with 'rules'
                                                                                                                                # having one CASE_PATTERN (pattern, expression) clause
                                                                                                                                # per pattern => expression rule.  Schematically:
                                                                                                                                #
                                                                                                                                #     RECURSIVE_VALUE_DECLARATIONS [
                                                                                                                                #         NAMED_RECURSIVE_VALUE.expression                      # Represents all of 'foo'.
                                                                                                                                #             =>
                                                                                                                                #             ds::FN_EXPRESSION.rules
                                                                                                                                #                 =>
                                                                                                                                #                 [ CASE_PATTERN( pattern, expression )         # One  foo ... => ... ;   rule.
                                                                                                                                #                   ...
                                                                                                                                #                 ]
                                                                                                                                #         ...
                                                                                                                                #     ]
                                                                                                                                #
                                                                                                                                # We use a two-pass algorithm here in which the first
                                                                                                                                # pass typecheckes the left-hand sides of all the rules
                                                                                                                                # and the second pass typechecks the right-hand sides.


                                                                                                                                # First pass: rule patterns and types.
                                                                                                                                # As we go, we accumulate the second-pass
                                                                                                                                # worklist in "expression_thunks':
                                                                                                                                #       
                                        rvbs_expression_thunk_pairs
                                            =
                                            map  do_one_function  named_recursive_values_records
                                            where
                                                                                                                                # Process one NAMED_RECURSIVE_VALUE record,
                                                                                                                                # which is to say all the rules for one function.
                                                                                                                                #       
                                                                                                                                # We derive a first-pass approximation to the
                                                                                                                                # function's type by unifying together domain
                                                                                                                                # types computed from the rule left hand sides
                                                                                                                                # (the patterns) together with any explicitly
                                                                                                                                # declared type constraints on the rule's range
                                                                                                                                # (result) type.
                                                                                                                                #
                                                                                                                                # We save the result in
                                                                                                                                #     NAMED_RECURSIVE_VALUE /
                                                                                                                                #     ORDINARY_VARIBLE /
                                                                                                                                #     vartypoid_ref.
                                                                                                                                #
                                                                                                                                # During this first pass we do not compute any range
                                                                                                                                # range types from the actual rule right hand sides
                                                                                                                                # (the function bodies) -- we leave that for the
                                                                                                                                # second pass.
                                                                                                                                #
                                                fun do_one_function
                                                      ( named_recursive_values
                                                            as
                                                            ds::NAMED_RECURSIVE_VALUE
                                                              {
                                                                variable =>  variable as  vac::PLAIN_VARIABLE { vartypoid_ref, ... },
                                                                expression,
                                                                raw_typevars,
                                                                generalized_typevars,
                                                                null_or_type
                                                              }
                                                      )
                                                        => 
                                                        {
                                                            result =  ( ds::NAMED_RECURSIVE_VALUE
                                                                          {
                                                                            variable,
                                                                            expression,
                                                                            raw_typevars,
                                                                            generalized_typevars =>  *bound_typevar_refs_accumulator,
                                                                            null_or_type
                                                                          },
                                                                        expression_thunk
                                                                      );

                                                                                                                                if (*debugging and ((list::length *bound_typevar_refs_accumulator) > 0))
                                                                                                                                    if *debugging print_callstack "do_declaration/RECURSIVE_VALUE_DECLARATIONS/do_one_function/TOP [type-core-language-declaration-g.pkg]" callstack; fi;
                                                                                                                                    printf "\nCreating NAMED_RECURSIVE_VALUE with %d-entry generalized_typevars list do_one_function  in do_declaration/RECURSIVE_VALUE_DECLARATIONS in type-core-language-declaration-g.pkg\n"
                                                                                                                                            (list::length *bound_typevar_refs_accumulator);
                                                                                                                                    printf "\n[type-core-language-declaration-g.pkg]  NAMED_RECURSIVE_VALUES.generalized_typevars: (%d) (was %d)\n"
                                                                                                                                            (list::length *bound_typevar_refs_accumulator) (list::length generalized_typevars);
                                                                                                                                    apply  unparse_typevar_ref  *bound_typevar_refs_accumulator
                                                                                                                                    where
                                                                                                                                        fun unparse_typevar_ref  typevar_ref
                                                                                                                                            =
                                                                                                                                            if_debugging_unparse_typevar_ref ("", typevar_ref);
                                                                                                                                    end;
                                                                                                                                    printf "\n";
                                                                                                                                    if_debugging_unparse_expression     ("\n[type-core-language-declaration-g.pkg]  NAMED_RECURSIVE_VALUES.expression unparse == \n", (expression,100));
                                                                                                                                    if_debugging_prettyprint_expression ("\n[type-core-language-declaration-g.pkg]  NAMED_RECURSIVE_VALUES.expression prettyprint == \n", (expression,100));
                                                                                                                                fi;
                                                             result;
                                                        }
                                                        where

                                                                                                                                # We compute the function type by starting with
                                                                                                                                # an initially completely unconstrained arrow
                                                                                                                                # (function) type and then unifying it with all
                                                                                                                                # available type information.  The eventual result
                                                                                                                                # is a type which is as general as possible while
                                                                                                                                # still being consistent with all known type
                                                                                                                                # constraints/information.
                                                                                                                                #
                                                                                                                                # We use 'function_type_so_far' as our type result
                                                                                                                                # accumulator:
                                                                                                                                #

                                                            domain_type =   tyj::make_meta_typevar_and_type  (syntax_treewalk_lexical_context.fn_nesting, ["domain_type in do_one_function  in do_declaration/RECURSIVE_VALUE_DECLARATIONS  from  type-core-language-declaration-g.pkg"]);
                                                            result_type =   tyj::make_meta_typevar_and_type  (syntax_treewalk_lexical_context.fn_nesting, ["result_type in do_one_function  in do_declaration/RECURSIVE_VALUE_DECLARATIONS  from  type-core-language-declaration-g.pkg"]);
                                                            #
                                                            function_type_so_far =   domain_type --> result_type;


                                                                                                                                # If the user explicitly declared a type for the
                                                                                                                                # function, fold that type information into our
                                                                                                                                # 'function_type_so_far' accumulator:
                                                                                                                                #
                                                            case null_or_type 
                                                                #
                                                                NULL => TRUE;

                                                                THE declared_function_type
                                                                    =>
                                                                    {
                                                                                                                                if_debugging_say "\ndo_one_function: calling unify_typoids_and_handle_errors in do_declaration/RECURSIVE_VALUE_DECLARATIONS  from  type-core-language-declaration-g.pkg\n";

                                                                        unify_typoids_and_handle_errors                         # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                                            {
                                                                              typoid1 => function_type_so_far,    name1 => "",
                                                                              typoid2 => declared_function_type,  name2 => "constraint",

                                                                              message => "type constraint of my rec declaration\
                                                                                     \ is not a function type",
                                                                              source_code_region,

                                                                              unparse_phrase =>  unparse_recursively_named_value,
                                                                              phrase_name    => "declaration",
                                                                              phrase         =>  named_recursive_values,

                                                                              callstack      => "do_declaration/RECURSIVE_VALUE_DECLARATIONS/do_one_function(1)" ! callstack,

                                                                              undo_log
                                                                            };
                                                                    };
                                                            esac;

                                                                                                                                # As we generalize rule patterns we
                                                                                                                                # generate additional bound type variables,
                                                                                                                                # which we will accumulate here:
                                                                                                                                #
                                                            bound_typevar_refs_accumulator
                                                                =
                                                                REF generalized_typevars;                                       # Always [] at this point.

                                                            my (expression, expression_thunk)
                                                                =
                                                                f (expression, source_code_region, function_type_so_far)
                                                                where
                                                                    fun f (ds::FN_EXPRESSION (rules, fn_type), source_code_region, function_type_so_far)
                                                                            =>
                                                                            {
                                                                                stipulate

                                                                                    pattern_type_expression_triples
                                                                                        =
                                                                                        map  approximate_rule_type  rules
                                                                                        where
                                                                                            fun approximate_rule_type (ds::CASE_RULE (pattern, expression))
                                                                                                =
                                                                                                {   my (pattern, pattern_type)
                                                                                                        =
                                                                                                        compute_pattern_type
                                                                                                          (
                                                                                                            pattern,
                                                                                                           *generalize_mutually_recursive_functions                     # See Note[1].
                                                                                                                ??  tdt::infinity
                                                                                                                ::  syntax_treewalk_lexical_context.fn_nesting,
                                                                                                            source_code_region,
                                                                                                            "do_declaration/RECURSIVE_VALUE_DECLARATIONS/do_one_function(2)" ! callstack
                                                                                                          );

                                                                                                    case expression
                                                                                                        #
                                                                                                        ds::TYPE_CONSTRAINT_EXPRESSION (expression, result_type_constraint)
                                                                                                            =>
                                                                                                            ( pattern,
                                                                                                              pattern_type --> result_type_constraint,
                                                                                                              (expression, source_code_region)
                                                                                                            );

                                                                                                        expression
                                                                                                            =>
                                                                                                            ( pattern,
                                                                                                              pattern_type --> result_type,
                                                                                                              (expression, source_code_region)
                                                                                                            );
                                                                                                    esac;
                                                                                                };
                                                                                        end; 

                                                                                herein

                                                                                    rule_patterns    =  map  #1  pattern_type_expression_triples;
                                                                                    rule_types       =  map  #2  pattern_type_expression_triples;
                                                                                    rule_expressions =  map  #3  pattern_type_expression_triples;

                                                                                end;

                                                                                apply   unify_rule_type_with_function_type_so_far  rule_types
                                                                                where
                                                                                    fun unify_rule_type_with_function_type_so_far  rule_type
                                                                                        =
                                                                                        {
                                                                                                                                if_debugging_say "\ndo_declaration/RECURSIVE_VALUE_DECLARATIONS [type-core-language-declaration-g.pkg]: \
                                                                                                                                                        \do_one_function: unify_rule_type_with_function_type_so_far:  calling unify_typoids_and_handle_errors\n";

                                                                                            unify_typoids_and_handle_errors     # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                                                              {
                                                                                                typoid1 => rule_type,              name1 => "this clause",
                                                                                                typoid2 => function_type_so_far,   name2 => "previous clauses",

                                                                                                message => "parameter or result constraints\
                                                                                                           \ of clauses don't agree",

                                                                                                source_code_region,

                                                                                                unparse_phrase =>  unparse_recursively_named_value,
                                                                                                phrase_name    =>  "declaration",
                                                                                                phrase         =>  named_recursive_values,

                                                                                                callstack      =>  "do_declaration/RECURSIVE_VALUE_DECLARATIONS/do_one_function(3)" ! callstack,

                                                                                                undo_log
                                                                                              };

                                                                                            ();
                                                                                        };
                                                                                end;

                                                                                maybe_note_ref_in_undo_log  (undo_log, vartypoid_ref);

                                                                                vartypoid_ref := function_type_so_far;

                                                                                # Added 2009-04-25 CrT: See Note[1] at bottom of tile -- this stuff is unused and usable and should probably be deleted soon unless we can work out a special case sufficient for OOP or something like that.
                                                                                #               
# src/lib/compiler/front/typer/types/type-core-language-declaration-g.pkg: generalize_type'/USER_TYPEVAR: X fn_nesting 1 syntax_treewalk_lexical_context.fn_nesting  1
# src/lib/thread-kit/src/core-thread-kit/event.pkg:151.9-172.3 Error: Explicit type variable cannot be generalized at its declaration point: X
# src/lib/compiler/front/typer/types/type-core-language-declaration-g.pkg: generalize_type'/USER_TYPEVAR: X fn_nesting 1 syntax_treewalk_lexical_context.fn_nesting  1
# src/lib/thread-kit/src/core-thread-kit/event.pkg:357.9-374.3 Error: Explicit type variable cannot be generalized at its declaration point: X
                                                                                #
                                                                                if *generalize_mutually_recursive_functions
                                                                                    #   
                                                                                    apply  generalize_rule_pattern  rule_patterns
                                                                                    where
                                                                                        fun generalize_rule_pattern  pattern                            # SIDE-EFFECT: SETS vac::PLAIN_VARIABLE.vartypoid_ref
                                                                                            =
                                                                                            {
                                                                                                                                if *debugging
                                                                                                                                printf "\n========== do_one_function CALLING generalize_pattern ==========  in do_declaration/RECURSIVE_VALUE_DECLARATIONS because *generalize_mutually_recursive_functions is TRUE.\n";
                                                                                                                                printf   "vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv\n";
                                                                                                                                fi;
                                                                                                added_typevars
                                                                                                    =
                                                                                                    generalize_pattern                                  # SIDE-EFFECT: SETS vac::PLAIN_VARIABLE.vartypoid_ref
                                                                                                      (
                                                                                                        pattern,
                                                                                                       *raw_typevars,                                   # Type variables explicitly specified by user:  X, Y, ... 
                                                                                                        previous_syntax_treewalk_lexical_context,
                                                                                                        TRUE,                                           # "generalize"
                                                                                                        source_code_region,
                                                                                                       "do_declaration/RECURSIVE_VALUE_DECLARATIONS/do_one_function(4)" ! callstack
                                                                                                      );

                                                                                                                                if *debugging
                                                                                                                                    printf "\n^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n";
                                                                                                                                    printf   "========== do_one_function CALLED  generalize_pattern ==========  in do_declaration/RECURSIVE_VALUE_DECLARATIONS   [type-core-language-declaration-g.pkg]\n";
                                                                                                                                    say ("\ndo_declaration/RECURSIVE_VALUE_DECLARATIONS: do_one_function: added_typevars:   [type-core-language-declaration-g.pkg]\n");
                                                                                                                                    apply  unparse_typevar_ref  added_typevars
                                                                                                                                    where
/* */                                                                                                                                   fun unparse_typevar_ref  typevar_ref
                                                                                                                                            =
                                                                                                                                            if_debugging_unparse_typevar_ref ("", typevar_ref);
                                                                                                                                    end;
                                                                                                                                fi;
                                                                                                bound_typevar_refs_accumulator
                                                                                                    :=
                                                                                                    added_typevars
                                                                                                    @
                                                                                                  *bound_typevar_refs_accumulator;
                                                                                            };
                                                                                    end;
                                                                                                                                if *debugging
                                                                                                                                    say ("\ndo_declaration/RECURSIVE_VALUE_DECLARATIONS [type-core-language-declaration-g.pkg]: do_one_function: FINAL bound_typevar_refs_accumulator: \n");
                                                                                                                                    apply  unparse_typevar_ref  *bound_typevar_refs_accumulator
                                                                                                                                    where
/* */                                                                                                                                   fun unparse_typevar_ref  typevar_ref
                                                                                                                                            =
                                                                                                                                            if_debugging_unparse_typevar_ref ("", typevar_ref);
                                                                                                                                    end;
                                                                                                                                fi;
                                                                                fi;                                             # end of bogus generalization of mutually recursive fns

                                                                                expression_thunk
                                                                                    =
                                                                                    \\ ()
                                                                                        =
                                                                                        ds::FN_EXPRESSION
                                                                                            ( paired_lists::map
                                                                                                  ds::CASE_RULE
                                                                                                  ( rule_patterns,
                                                                                                    map  unify_expression_with_result_type  rule_expressions
                                                                                                  ),

                                                                                              mtt::domain  (tyj::drop_resolved_typevars  function_type_so_far)
                                                                                            )
                                                                                        where
                                                                                            fun unify_expression_with_result_type  (expression,  source_code_region)
                                                                                                =
                                                                                                {
                                                                                                                                if_debugging_say "\ncalling compute_expression_type [type-core-language-declaration-g.pkg]: unify_expression_with_result_type() in \
                                                                                                                                        \f() in do_one_function() in RECURSIVE_VALUE_DECLARATIONS in do_declaration() \
                                                                                                                                        \in type-core-language-declaration-g.pkg";
                                                                                                    my (expression, expression_type)
                                                                                                        =
                                                                                                        compute_expression_type
                                                                                                          (
                                                                                                            expression,
                                                                                                            syntax_treewalk_lexical_context,
                                                                                                            source_code_region,
                                                                                                            "do_declaration/RECURSIVE_VALUE_DECLARATIONS/do_one_function(5)" ! callstack
                                                                                                          );
                                                                                                                                if_debugging_say "\nback from compute_expression_type [type-core-language-declaration-g.pkg]:  unify_expression_with_result_type() in f() in do_one_function() in \
                                                                                                                                                    \RECURSIVE_VALUE_DECLARATIONS in do_declaration() in type-core-language-declaration-g.pkg";

                                                                                                                                if_debugging_say "\ncalling unify_typoids_and_handle_errors:   unify_expression_with_result_type() in f() in \
                                                                                                                                                    \do_one_function() in RECURSIVE_VALUE_DECLARATIONS in do_declaration() in type-core-language-declaration-g.pkg";
                                                                                                    unify_typoids_and_handle_errors {                                           # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                                                                        #
                                                                                                        typoid1 => expression_type,   name1 => "expression",
                                                                                                        typoid2 =>     result_type,   name2 => "result type",

                                                                                                        message=>"right-hand-side of clause\
                                                                                                                 \ doesn't agree with function result type",

                                                                                                        source_code_region,

                                                                                                        unparse_phrase =>  unparse_recursively_named_value,
                                                                                                        phrase_name    => "declaration",
                                                                                                        phrase         =>  named_recursive_values,

                                                                                                        callstack      => "do_declaration/RECURSIVE_VALUE_DECLARATIONS/do_one_function(6)" ! callstack,

                                                                                                        undo_log
                                                                                                      };
                                                                                                                                if_debugging_say "\nback from unify_typoids_and_handle_errors:   unify_expression_with_result_type() in \
                                                                                                                                                        \f() in do_one_function() in RECURSIVE_VALUE_DECLARATIONS in do_declaration() in type-core-language-declaration-g.pkg";

                                                                                                    expression;
                                                                                                };

                                                                                        end; 

                                                                               ( ds::FN_EXPRESSION (rules, fn_type),
                                                                                 expression_thunk
                                                                               );
                                                                            };

                                                                        f (ds::SOURCE_CODE_REGION_FOR_EXPRESSION (expression, source_code_region), _, function_type_so_far)
                                                                            => 
                                                                            {   (f (expression, source_code_region, function_type_so_far))
                                                                                    ->
                                                                                    (expression, subthunk);

                                                                                expression_thunk
                                                                                    =
                                                                                    \\ () =  ds::SOURCE_CODE_REGION_FOR_EXPRESSION (subthunk(), source_code_region);

                                                                                ( ds::SOURCE_CODE_REGION_FOR_EXPRESSION (expression, source_code_region),
                                                                                  expression_thunk
                                                                                );
                                                                            };

                                                                        f (ds::TYPE_CONSTRAINT_EXPRESSION (expression, constraining_type), source_code_region, function_type_so_far)
                                                                            =>
                                                                            {
                                                                                                                                if_debugging_say "\ndo_declaration/RECURSIVE_VALUE_DECLARATIONS [type-core-language-declaration-g.pkg]: do_one_function: f:  calling unify_typoids_and_handle_errors\n";

                                                                                unify_typoids_and_handle_errors                 # SIDE-EFFECT:   Sets tdt::TYPEVAR_REF.ref_typevar
                                                                                    {
                                                                                      typoid1 => constraining_type,      name1 => "this constraint",
                                                                                      typoid2 => function_type_so_far,   name2 => "outer constraints",

                                                                                       message=>"type constraints on my rec\
                                                                                                 \ declaraction disagree",
                                                                                       source_code_region,

                                                                                       unparse_phrase =>  unparse_recursively_named_value,
                                                                                       phrase_name    => "declaration",
                                                                                       phrase         =>  named_recursive_values,

                                                                                       callstack      => "do_declaration/RECURSIVE_VALUE_DECLARATIONS/do_one_function/f/ds::TYPE_CONSTRAINT_EXPRESSION" ! callstack,

                                                                                       undo_log
                                                                                    };
                                                                                                                                if_debugging_say "\ndo_declaration/RECURSIVE_VALUE_DECLARATIONS [type-core-language-declaration-g.pkg]: do_one_function: f:  done calling unify_typoids_and_handle_errors\n";

                                                                                (f (expression, source_code_region, function_type_so_far))
                                                                                    ->
                                                                                    (expression, subthunk);

                                                                                expression_thunk
                                                                                    =
                                                                                    \\()  = ds::TYPE_CONSTRAINT_EXPRESSION (subthunk(), constraining_type);

                                                                                ( ds::TYPE_CONSTRAINT_EXPRESSION (expression, constraining_type),
                                                                                  expression_thunk
                                                                                );
                                                                            };

                                                                       f _ => bug "typecheck.823";
                                                                   end;                                                 # fun f
                                                               end;                                                     # where
                                                       end;                                                             # where

                                                    do_one_function _ => bug "do_one_function";
                                                end;                                                                    # fun do_one_function
                                            end;                                                                        # where (rvbs_expression_thunk_pairs)

                                                                                                                        # paired_lists          is from   src/lib/std/src/paired-lists.pkg
                                        named_recursive_values_records  =  map  #1  rvbs_expression_thunk_pairs;
                                        expression_thunks               =  map  #2  rvbs_expression_thunk_pairs;

                                        # Second pass: type-check and update
                                        # the right-hand-side expressions
                                        # (function bodies):
                                        #
                                        named_recursive_values_records                                                  # "rvb" == "recursive value binding"
                                            =
                                            paired_lists::map
                                                do_rvb_expression
                                                (named_recursive_values_records,  expression_thunks)
                                            where
                                                fun do_rvb_expression
                                                    (  ds::NAMED_RECURSIVE_VALUE { variable, null_or_type, raw_typevars, generalized_typevars, expression => _ },
                                                       expression_thunk
                                                    )
                                                    =
                                                    {   expression  =  expression_thunk();
                                                                                                                                if_debugging_prettyprint_expression ("\ndo_declaration/RECURSIVE_VALUE_DECLARATIONS/do_rvb_expression: expression_thunk() yielded", (expression,100));
                                                        #
                                                                                                                                result =
                                                        ds::NAMED_RECURSIVE_VALUE
                                                          {
                                                            expression,
                                                            variable,
                                                            raw_typevars,
                                                            generalized_typevars,
                                                            null_or_type
                                                          };
                                                                                                                                if_debugging_prettyprint_named_recursive_value ("\ndo_declaration/RECURSIVE_VALUE_DECLARATIONS/do_rvb_expression: returning", (result,100));
                                                                                                                                result;
                                                    };
                                            end;

                                        # 2009-05-14 CrT:       
                                        # The SML/NJ codebase has a comment here:
                                        #       
                                        #    "No need to generalize here, because every RECURSIVE_VALUE_DECLARATIONS is
                                        #     wrapped in a VALUE_DECLARATIONS, and the generalization occurs at the
                                        #     outer level.  Previously had:
                                        #       
                                        #         named_recursive_values_records
                                        #             =
                                        #             map  generalize_type
                                        #                  named_recursive_values_records
                                        #       
                                        # The above code does not actually typecheck, but something similar
                                        # seems needed if mutually recursive functions are to be
                                        # typeagnostic ("polymorphic"), which I need to make OOP work decently,
                                        # so I've added a
                                        #       
                                        #     if *generalize_mutually_recursive_functions
                                        #              apply  generalize_rule_pattern  rule_patterns
                                        #       
                                        # call above in:
                                        #       
                                        #     do_declaration()/RECURSIVE_VALUE_DECLARATIONS/do_one_function()
                                        #       
                                        # [ LATER: This CANNOT WORK -- see Note[1] ]

                                                                                                                                if_debugging_say "\ndo_declaration/RECURSIVE_VALUE_DECLARATIONS: calling \
                                                                                                                                                \typer_junk::convert_deep_syntax_named_recursive_values_list_to_deep_syntax_value_declarations_or_recursive_value_declarations [type-core-language-declaration-g.pkg]\n";
                                        declaration
                                            =
                                            typer_junk::convert_deep_syntax_named_recursive_values_list_to_deep_syntax_value_declarations_or_recursive_value_declarations
                                                named_recursive_values_records;
                                                                                                                                if *debugging       print_callstack "\ndo_declaration/RECURSIVE_VALUE_DECLARATIONS/BOTTOM [type-core-language-declaration-g.pkg] " callstack; fi;
                                                                                                                                if *debugging       printf "\ndo_declaration/RECURSIVE_VALUE_DECLARATIONS/BOTTOM [type-core-language-declaration-g.pkg]:  returning from lex.fn_nesting %d to %d\n"
                                                                                                                                                            syntax_treewalk_lexical_context.fn_nesting (syntax_treewalk_lexical_context.fn_nesting - 1);
                                                                                                                                fi;
                                                                                                                                if_debugging_unparse_declaration     ("\ndo_declaration/RECURSIVE_VALUE_DECLARATIONS/BOTTOM [type-core-language-declaration-g.pkg]:  final result unparse     is:\n", declaration);
                                                                                                                                if_debugging_prettyprint_declaration ("\ndo_declaration/RECURSIVE_VALUE_DECLARATIONS/BOTTOM [type-core-language-declaration-g.pkg]:  final result prettyprint is:\n", (declaration,100));

                                        declaration;
                                    };                          # RECURSIVE_VALUE_DECLARATIONS

                                ds::EXCEPTION_DECLARATIONS  ebs
                                    =>
                                    {
                                                                                                                                if_debugging_say "\ndo_declaration/EXCEPTION_DECLARATIONS/TOP   [type-core-language-declaration-g.pkg]\n";
                                        if_debugging_say "\ndo_declaration: EXCEPTION_DECLARATIONS";

                                        if (syntax_treewalk_lexical_context.fn_nesting  < 1)
                                            #
                                            apply eb_type ebs
                                            where
                                                fun check (tdt::TYPEVAR_REF { id, ref_typevar as REF (tdt::USER_TYPEVAR _) } )
                                                        => 
                                                        error_function source_code_region err::ERROR
                                                            "type variable in top level exception type"
                                                            err::null_error_body;

                                                    check (tdt::TYPCON_TYPOID(_, args))
                                                        =>
                                                        apply check args;

                                                    check _ => ();
                                                end;
                                                #
                                                fun eb_type (ds::NAMED_EXCEPTION { exception_typoid => THE type, ... } ) =>   check type;
                                                    eb_type _ => ();
                                                end;
                                            end;
                                        fi;

                                                                                                                                if_debugging_say "\ndo_declaration/EXCEPTION_DECLARATIONS/BOT   [type-core-language-declaration-g.pkg]\n";
                                        given_declaration;
                                    };

                                ds::LOCAL_DECLARATIONS (dec_in, dec_out)
                                    =>
                                    {
                                                                                                                                if_debugging_say "\ndo_declaration/LOCAL_DECLARATIONS/TOP   [type-core-language-declaration-g.pkg]\n";

                                        dec_in'  = do_declaration (dec_in,  enter_let_scope syntax_treewalk_lexical_context, source_code_region, "\ndo_declaration/LOCAL_DECLARATIONS(1) " ! callstack);
                                        dec_out' = do_declaration (dec_out,                 syntax_treewalk_lexical_context, source_code_region, "\ndo_declaration/LOCAL_DECLARATIONS(2) " ! callstack);

                                                                                                                                if_debugging_say "\ndo_declaration: LOCAL_DECLARATION   [type-core-language-declaration-g.pkg] ";
                                                                                                                                if_debugging_say "\ndo_declaration/LOCAL_DECLARATIONS/BOT   [type-core-language-declaration-g.pkg]\n";
                                        ds::LOCAL_DECLARATIONS (dec_in', dec_out');
                                    };

                                ds::SEQUENTIAL_DECLARATIONS (decls)
                                    => 
                                    {
                                                                                                                                if_debugging_say "\ndo_declaration/SEQUENTIAL_DECLARATIONS/TOP   [type-core-language-declaration-g.pkg]\n";

                                        result =    ds::SEQUENTIAL_DECLARATIONS
                                                        (map (\\ decl = do_declaration  ( decl,
                                                                                          syntax_treewalk_lexical_context,
                                                                                          source_code_region,
                                                                                          "do_declaration/SEQUENTIAL_DECLARATIONS" ! callstack
                                                                                        )
                                                             )
                                                             decls
                                                        );

                                                                                                                                if_debugging_say "\ndo_declaration/SEQUENTIAL_DECLARATIONS/BOT   [type-core-language-declaration-g.pkg]\n";
                                        result;
                                    };

                                ds::SOURCE_CODE_REGION_FOR_DECLARATION (declaration, source_code_region)
                                    =>
                                    {
                                                                                                                                if_debugging_say "\ndo_declaration/ds::SOURCE_CODE_REGION_FOR_DECLARATION   [type-core-language-declaration-g.pkg]\n";
                                        ds::SOURCE_CODE_REGION_FOR_DECLARATION (
                                            do_declaration (declaration, syntax_treewalk_lexical_context, source_code_region, callstack),
                                            source_code_region
                                        );
                                    }; 


                                # The next several declarations will never be seen ordinarily;
                                # they are for re-typechecking after the instrumentation phase
                                # of debugger or profiler. 
                                #
                                ds::PACKAGE_DECLARATIONS  named_packages
                                    =>
                                    ds::PACKAGE_DECLARATIONS          (map (named_package_type  (syntax_treewalk_lexical_context, source_code_region, "do_declaration/PACKAGE_DECLARATIONS " ! callstack)) named_packages);

                                ds::GENERIC_DECLARATIONS  named_generics
                                    =>
                                    ds::GENERIC_DECLARATIONS          (map (generic_naming_type (syntax_treewalk_lexical_context, source_code_region, "do_declaration/ds::GENERIC_DECLARATIONS " ! callstack)) named_generics);

                                _ => given_declaration;
                            esac;
                        }

                    also
                    fun generic_naming_type
                        ( syntax_treewalk_lexical_context, 
                          source_code_region,
                          callstack
                        )
                        (ds::NAMED_GENERIC { definition,
                                             name_symbol,
                                             a_generic
                                           }
                        )
                        =
                        ds::NAMED_GENERIC { definition  => generic_expression_type  definition,
                                            name_symbol,
                                            a_generic
                                          }
                        where
                            fun generic_expression_type ( ds::GENERIC_DEFINITION { parameter, parameter_types, definition } )
                                    =>
                                    ds::GENERIC_DEFINITION { parameter,
                                                             parameter_types,
                                                             definition
                                                                 =>
                                                                 package_expression_type
                                                                     (syntax_treewalk_lexical_context, source_code_region, "generic_naming_type/generic_expression_type/ds::GENERIC_DEFINITION " ! callstack)
                                                                     definition
                                                         };

                                generic_expression_type (ds::GENERIC_LET (declaration, expression))
                                    =>
                                    ds::GENERIC_LET
                                      ( do_declaration
                                          ( declaration,
                                            enter_let_scope  syntax_treewalk_lexical_context,
                                            source_code_region,
                                            "generic_naming_type/generic_expression_type/ds::GENERIC_LET" ! callstack
                                      ),
                                      generic_expression_type expression
                                    );

                                generic_expression_type (ds::SOURCE_CODE_REGION_FOR_GENERIC (generic_expression, source_code_region))
                                    =>
                                    ds::SOURCE_CODE_REGION_FOR_GENERIC (generic_expression_type generic_expression, source_code_region);

                                generic_expression_type  other
                                    =>
                                    other;
                            end;
                        end

                    also
                    fun package_expression_type
                            (syntax_treewalk_lexical_context, source_code_region, callstack)
                            (se as (ds::COMPUTED_PACKAGE { a_generic, generic_argument, parameter_types } ))
                            =>
                            se;

                        package_expression_type (syntax_treewalk_lexical_context, source_code_region, callstack) (ds::PACKAGE_LET { declaration, expression })
                            =>
                            ds::PACKAGE_LET { declaration =>  do_declaration (declaration, enter_let_scope syntax_treewalk_lexical_context, source_code_region, "package_expression_type/ds::PACKAGE_LET "    ! callstack),
                                              expression  =>  package_expression_type                     (syntax_treewalk_lexical_context, source_code_region, "package_expression_type/ds::PACKAGE_LET(2) " ! callstack) expression
                                            };


                        package_expression_type (syntax_treewalk_lexical_context, _, callstack) (ds::SOURCE_CODE_REGION_FOR_PACKAGE (expression, source_code_region))
                            => 
                            ds::SOURCE_CODE_REGION_FOR_PACKAGE (package_expression_type (syntax_treewalk_lexical_context, source_code_region, callstack) expression, source_code_region);

                        package_expression_type _ other
                            =>
                            other;
                    end 

                    also
                    fun named_package_type
                            (syntax_treewalk_lexical_context, source_code_region, callstack)
                            (ds::NAMED_PACKAGE { a_package, definition, name_symbol } )
                        =
                        ds::NAMED_PACKAGE { a_package,
                                            definition => package_expression_type (syntax_treewalk_lexical_context, source_code_region, "named_package_type/ds::NAMED_PACKAGE" ! callstack) definition,
                                            name_symbol
                                          };



                end;                                                                                                            # function type_core_language_declaration 

            type_core_language_declaration
                =
                cos::do_compiler_phase  (cos::make_compiler_phase "Compiler 035  typecheck")  type_core_language_declaration;

        end;    # stipulate
    };          # generic package type_core_language_declaration_g 
end;

################################################################
# Note[1]:                                        2009-04-25 CrT
#
# While implementing OOP support and attempting
# to make 'new' and method functions mutually
# recursive, I discovered that
#
#     package test: api { f: X -> Void; } {
#
#          fun f (x: X) = ();
#          fun g () = f 0;
#      };
#
# typechecked ok but
#
#     package test: api { f: X -> Void; } {
#
#          fun f (x: X) = ()
#          also
#          fun g () = f 0;
#      };
#
# did not.  This was a bit of a showstopper,
# since forbidding class methods from creating
# new class instances is a major restriction.
#
# After some digging I discovered that the SML/NJ
# version of do_declaration/RECURSIVE_VALUE_DECLARATIONS
# in this file apparently once generalized its patterns
# but stopped doing so, judging by the comment
#
#                                    # No need to generalize here, because every RECURSIVE_VALUE_DECLARATIONS is
#                                    # wrapped in a VALUE_DECLARATIONS, and the generalization occurs at the
#                                    # outer level.  Previously: named_recursive_values_records = map generalize_type named_recursive_values_records
#
# This omission appeared to be the root cause
# of my above typechecking issue.
#
# Poking around farther, I found in
#     src/lib/compiler/back/top/translate/translate-deep-syntax-to-lambdacode.pkg
#         fun make_named_recursive_values
#             fun g
# the code and comment
#                                   ee = make_expression (expression, d); #  Was make_pattern_expression (expression, d, tvs) 
#                                                                         #  We no longer track type namings at NAMED_RECURSIVE_VALUE anymore ! 
#
# and in fact the NAMED_RECURSIVE_VALUE.generalized_typevars
# field seemed at to be entirely unused by the compiler.
#
# [LATER -- 2011-06-07 CrT:] Robert Harper informs me that finding the
#    most general polymorphic type for mutually recursive functions is
#    a mathematically undecidable problem.
#    =====================================
#
#    (This is probably why SML/NJ doesn't attempt this.
#    The Definition seems notably reticent on this front....  *wrygrin*)
#
#    He says that Haskell requires explicit user-supplied types in
#    such situations, and that SML should follow suit.




Comments and suggestions to: bugs@mythryl.org

PreviousUpNext