## unify-types.pkg
# Compiled by:
# src/lib/compiler/front/typer/typer.sublib# The center of the typechecker is
#
# src/lib/compiler/front/typer/main/type-package-language-g.pkg#
# -- see it for a higher-level overview.
#
# We get called from
#
# src/lib/compiler/front/typer/modules/api-match-g.pkg# src/lib/compiler/front/typer/types/unify-and-generalize-types-g.pkg#
# The Hindley-Milner type inference algorithm on which the
# typechecker is based uses Prolog-style logical unification
# to propagate type information to syntax nodes lacking
# explicit programmer-supplied type declarations. (Which is,
# typically, the overwhelming majority of them.)
#
# 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.
#
# In this file we implement the required unification operation.
#
# For unification, our primary analog of a logic variable is
# a type variable set to META_TYPE_VARIABLE;
# this represents a totally unconstrained type about which
# we as yet know nothing at all.
#
# Various other type variable values also admit specialization
# during unification to reflect additional knowledge gained.
# For example INCOMPLETE_RECORD_TYPE_VARIABLE; values represent
# incompletely specified records ("..." used), which can be
# updated to reflect the complete record definition if we find it.
#
# Unification thus mostly consists of propagating type knowledge
# by setting such type variables to something more specific, perhaps
# a compound type containing more META_TYPE_VARIABLE
# type variables to be set in their turn.
#
# The entrypoint into this file is unify_types(). It has a
# Void result type since all its work is done via side-effects,
# setting type variables embedded in its type arguments to
# less general (and thus more informative) values.
api Unify_Types {
# If unification fails we raise
# the exception UNIFY_TYPES with
# a Unify_Fail value to detail
# the exact reason for failure:
#
Unify_Fail
= CIRCULARITY # Cycle in type graph -- type variable loop.
| NEED_EQUALITY_TYPE # Equality type required.
| TYP_MISMATCH (types::Typ, types::Typ) # Type constructor mismatch.
| TYPE_MISMATCH (types::Type, types::Type) # Type mismatch.
| LITERAL_TYPE_MISMATCH types::Type_Variable # Type of literal could not be resolved.
| USER_TYPE_VARIABLE_MISMATCH types::Type_Variable # USER_TYPE_VARIABLE match
| OVERLOADED_TYPE_VARIABLE_MISMATCH # OVERLOADED_TYPE_VARIABLE, equality mismatch
| RECORD_FIELD_LABELS_MISMATCH # Record labels did not match.
;
exception UNIFY_TYPES Unify_Fail;
fail_message: Unify_Fail -> String;
unify_types: (String, String, types::Type, types::Type, List(String)) -> Void;
debugging: Ref( Bool );
};
stipulate
package ty = types; # types is from src/lib/compiler/front/typer-stuff/types/types.pkg package ts = type_junk; # type_junk is from src/lib/compiler/front/typer-stuff/types/type-junk.pkg # resolve_overloaded_literals is from src/lib/compiler/front/typer/types/resolve-overloaded-literals.pkg # typer_debugging is from src/lib/compiler/front/typer/main/typer-debugging.pkg # unparse_type is from src/lib/compiler/front/typer/print/unparse-type.pkgherein
package unify_types
: (weak) Unify_Types # Unify_Types is from src/lib/compiler/front/typer/types/unify-types.pkg {
# Type unification.
debugging = typer_control::unify_types_debugging; # REF FALSE
stipulate
# include types;
# Debugging
say = control_print::say;
fun if_debugging_say (msg: String)
=
if *debugging
say msg;
say "\n";
fi;
fun bug msg
=
error_message::impossible("unify_types: " + msg);
unparse_type
=
unparse_type::unparse_type symbolmapstack::empty;
fun debug_unparse_type (msg, type)
=
typer_debugging::debug_print debugging (msg, unparse_type, type);
fun debug_unparse_typevar_ref typevar_ref
=
if *debugging # Without this 'if' (and the matching one in unify_and_generalize_types_g), compiling the compiler takes 5X as long! :-)
typer_debugging::with_internals
(fn () = if_debugging_say (unparse_type::typevar_ref_printname typevar_ref));
fi;
prettyprint_type
=
prettyprint_type::prettyprint_type symbolmapstack::empty;
fun debug_pptype (msg, type)
=
typer_debugging::debug_print debugging (msg, prettyprint_type, type);
herein
Unify_Fail
= CIRCULARITY # Cycle in type graph -- type variable loop.
| NEED_EQUALITY_TYPE # Equality type required.
| TYP_MISMATCH (types::Typ, types::Typ) # Type constructor mismatch.
| TYPE_MISMATCH (types::Type, types::Type) # Type mismatch.
| LITERAL_TYPE_MISMATCH types::Type_Variable # Type of literal could not be resolved.
| USER_TYPE_VARIABLE_MISMATCH types::Type_Variable # USER_TYPE_VARIABLE match.
| OVERLOADED_TYPE_VARIABLE_MISMATCH # OVERLOADED_TYPE_VARIABLE, equality mismatch.
| RECORD_FIELD_LABELS_MISMATCH # Record labels did not match.
;
fun fail_message failure
=
case failure
CIRCULARITY => "circularity";
NEED_EQUALITY_TYPE => "equality type required";
TYP_MISMATCH _ => "typ mismatch";
TYPE_MISMATCH _ => "type mismatch";
LITERAL_TYPE_MISMATCH _ => "literal";
USER_TYPE_VARIABLE_MISMATCH _ => "USER_TYPE_VARIABLE match";
OVERLOADED_TYPE_VARIABLE_MISMATCH => "OVERLOADED_TYPE_VARIABLE, equality mismatch";
RECORD_FIELD_LABELS_MISMATCH => "record labels";
esac;
exception UNIFY_TYPES Unify_Fail;
########################################################
# Miscellaneous functions:
eq_label = symbol::eq;
fun literal_is_equality_kind (lk: ty::Literal_Kind)
=
case lk
(ty::INT | ty::UNT | ty::CHAR | ty::STRING) => TRUE;
ty::FLOAT => FALSE;
esac;
# equality_property_of_typ typ:
#
# This function returns the equality_property
# of typ for use in determining
# when a TYPCON_TYPE is an equality type.
#
# Note: Calling this function on ERRONEOUS_TYP produces an impossible
# because an ERRONEOUS_TYP should never occur in a TYPCON_TYPE
# and hence an equality_property of one of them should never be needed.
#
# Calling this function on a DEFINED_TYP also produces an impossible because
# the current equality_property scheme is insufficiently expressive to describe
# the possibilities. (Ex: first argument must be an eq type but not
# necessarily the second) Because of this, it is currently necessary to
# expand a DEFINED_TYP before computing its equality type.
#
fun equality_property_of_typ (ty::PLAIN_TYP { eqtype_info, ... } )
=>
case *eqtype_info
#
ty::eq_type::EQ_ABSTRACT => ty::eq_type::NO;
ep => ep;
esac;
equality_property_of_typ (ty::RECORD_TYP _) => ty::eq_type::YES;
equality_property_of_typ (ty::DEFINED_TYP _) => bug "equality_property_of_typ: DEFINED_TYP";
equality_property_of_typ (ty::ERRONEOUS_TYP) => bug "equality_property_of_typ: ERRONEOUS_TYP";
equality_property_of_typ _ => bug "equality_property_of_typ: unexpected typ";
end;
# fieldwise (just1, just2, combine, fields1, fields2):
#
# This function merges two sorted lists of (label, type) pairs
# (sorted by label) into a single sorted list of (label, type) pairs.
# If (l1, t1) occurs in fields1 but l1 doesn't occur in fields2 then
# (l1, just1 t1) occurs in the output. Similarly with just2.
# If (l, t1) occurs in fields1 and (l, t2) in fields2, then
# (l, combine t1 t2) occurs in the output.
#
fun fieldwise (_, just2, _, [], fields2) => map (fn (n, t) = (n, just2 t)) fields2;
fieldwise (just1, _, _, fields1, []) => map (fn (n, t) = (n, just1 t)) fields1;
fieldwise (just1, just2, combine, ((n1, t1) ! r1), ((n2, t2) ! r2))
=>
if (eq_label (n1, n2))
(n1, combine (t1, t2)) ! (fieldwise (just1, just2, combine, r1, r2));
else
if (ts::label_is_greater_than (n2, n1))
(n1, just1 t1) ! (fieldwise (just1, just2, combine, r1, ((n2, t2) ! r2)));
else
(n2, just2 t2) ! (fieldwise (just1, just2, combine, ((n1, t1) ! r1), r2));
fi;
fi;
end;
# ************** adjust function ****************************************
# We are about to do
#
# given_type_var := ty::RESOLVED_TYPE_VARIABLE given_type;
#
# or something very similar, and before doing
# so we want to propagate any relevant type
# information from the current value of *given_type_var
# into 'given_type'.
#
# We also want to incorporate into 'given_type'
# our given_fn_nesting and 'given_eq' values,
# by setting
# given_type_var.fn_nesting to minimum of current and given value;
# given_type_var.eq to 'or' of current value and 'given_eq'.
#
# Raise CIRCULARITY if there is a type variable loop.
#
fun adjust_type
( given_type: types::Type,
given_typevar_ref: types::Typevar_Ref,
given_fn_nesting: Int, # Count of enclosing fun/fn lexical scopes.
given_eq: Bool # TRUE if type variable must resolve to an equality type.
)
: Void
=
adjust_type' given_eq given_type
where
if_debugging_say "\n\nadjust_type: variable ";
debug_unparse_typevar_ref given_typevar_ref;
debug_unparse_type (" ==> ty::RESOLVED_TYPE_VARIABLE ", given_type);
fun adjust_type' this_eq (ty::TYPE_VARIABLE_REF (tv as { id, ref_typevar as REF type_variable } ))
=>
case type_variable
#
ty::USER_TYPE_VARIABLE { fn_nesting, eq, name }
=>
# Check if eq is compatible and propagate fn_nesting:
#
if (this_eq and not eq) raise exception UNIFY_TYPES NEED_EQUALITY_TYPE;
elif (given_fn_nesting < fn_nesting) ref_typevar := ty::USER_TYPE_VARIABLE { fn_nesting => given_fn_nesting, eq, name };
fi;
ty::META_TYPE_VARIABLE { eq, fn_nesting }
=>
# Check for circularity,
# propagate eq and fn_nesting
#
if (ts::typevar_refs_are_equal (given_typevar_ref, tv))
raise exception UNIFY_TYPES CIRCULARITY;
else
ref_typevar := ty::META_TYPE_VARIABLE
{
fn_nesting => int::min (given_fn_nesting, fn_nesting),
eq => this_eq or eq
};
fi;
ty::INCOMPLETE_RECORD_TYPE_VARIABLE { known_fields, eq, fn_nesting }
=>
# Check for circularity,
# propagate eq and fn_nesting
#
if (ts::typevar_refs_are_equal (given_typevar_ref, tv))
raise exception UNIFY_TYPES CIRCULARITY;
else
# Do field types recursively:
#
apply (fn (l, t) = adjust_type (t, given_typevar_ref, given_fn_nesting, eq))
known_fields;
ref_typevar := ty::INCOMPLETE_RECORD_TYPE_VARIABLE
{
fn_nesting => int::min (given_fn_nesting, fn_nesting),
eq => this_eq or eq,
known_fields
};
fi;
ty::RESOLVED_TYPE_VARIABLE type
=>
adjust_type' this_eq type;
ty::LITERAL_TYPE_VARIABLE { kind, ... }
=>
# Check if eq is compatible
#
if (this_eq and not (literal_is_equality_kind kind))
raise exception UNIFY_TYPES NEED_EQUALITY_TYPE;
fi;
ty::OVERLOADED_TYPE_VARIABLE eq'
=>
if (ts::typevar_refs_are_equal (given_typevar_ref, tv)) raise exception UNIFY_TYPES CIRCULARITY;
elif (this_eq and not eq') ref_typevar := ty::OVERLOADED_TYPE_VARIABLE this_eq;
fi;
ty::TYPE_VARIABLE_MARK _
=>
bug "unify: adjust_type: ty::TYPE_VARIABLE_MARK";
esac;
adjust_type' this_eq (type as ty::TYPCON_TYPE (ty::DEFINED_TYP _, args))
=>
adjust_type' this_eq (ts::head_reduce_type type);
adjust_type' this_eq (ty::TYPCON_TYPE (typ, args))
=>
case (equality_property_of_typ typ)
#
ty::eq_type::CHUNK => apply (adjust_type' FALSE ) args;
ty::eq_type::YES => apply (adjust_type' this_eq) args;
_ => if this_eq raise exception UNIFY_TYPES NEED_EQUALITY_TYPE;
else apply (adjust_type' FALSE) args;
fi;
esac;
adjust_type' _ ty::WILDCARD_TYPE
=>
();
# BUG? why don't these cases blow up
# (in equality_property_of_typ)
# when adjust_type' is applied to arguments that
# are unreduced applications of DEFINED_TYP?
# XXX BUGGO FIXME
# (Is this answered by the previous comment that
# a DEFINED_TYP must always be expanded
# before calling equality_property_of_typ?)
adjust_type' _ (ty::TYPE_SCHEME_TYPE _) => bug "adjust_type 1";
adjust_type' _ (ty::TYPE_SCHEME_ARG_I _) => bug "adjust_type 2";
adjust_type' _ _ => bug "adjust_type 3";
end;
end;
# Reorder two type_variables in descending order according to the ordering
# ty::LITERAL_TYPE_VARIABLE > ty::USER_TYPE_VARIABLE > ty::OVERLOADED_TYPE_VARIABLE > ty::INCOMPLETE_RECORD_TYPE_VARIABLE > ty::META_TYPE_VARIABLE
#
fun sort_vars ( typevar_ref1 as { id => id1, ref_typevar => REF typevar1 },
typevar_ref2 as { id => id2, ref_typevar => REF typevar2 }
)
=
case (typevar1, typevar2)
(ty::LITERAL_TYPE_VARIABLE _, _) => (typevar_ref1, typevar_ref2);
(_, ty::LITERAL_TYPE_VARIABLE _) => (typevar_ref2, typevar_ref1);
(ty::USER_TYPE_VARIABLE _, _) => (typevar_ref1, typevar_ref2);
(_, ty::USER_TYPE_VARIABLE _) => (typevar_ref2, typevar_ref1);
(ty::OVERLOADED_TYPE_VARIABLE _, _) => (typevar_ref1, typevar_ref2);
(_, ty::OVERLOADED_TYPE_VARIABLE _) => (typevar_ref2, typevar_ref1);
(ty::INCOMPLETE_RECORD_TYPE_VARIABLE _, _) => (typevar_ref1, typevar_ref2);
(_, ty::INCOMPLETE_RECORD_TYPE_VARIABLE _) => (typevar_ref2, typevar_ref1);
_ => (typevar_ref1, typevar_ref2); # Both ty::META_TYPE_VARIABLE
esac;
# Here is the externally visible entrypoint.
# It is just a wrapper for unify_types':
#
fun unify_types
( name1, name2,
type1, type2,
stack
)
=
{ type1 = ts::prune type1; # Reduce ty::TYPE_VARIABLE_REF (REF (ty::RESOLVED_TYPE_VARIABLE type)) to just type.
type2 = ts::prune type2; # " ".
if (not *debugging)
unify_types' (stack, type1, type2);
else
verbose = case (type1, type2)
#
(ty::TYPE_VARIABLE_REF _, ty::TYPE_VARIABLE_REF _) => FALSE;
_ => TRUE;
esac;
if verbose
if_debugging_say "\n\n============= unify_types/TOP ===============";
if_debugging_say "vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv\n";
if_debugging_say ("\nCalled by: " + (string::join " " (reverse stack)) + "\n");
debug_unparse_type(" " + name1 + ": ", type1);
debug_unparse_type( name2 + ": ", type2);
# if_debugging_say "\n\n----------prettyprinting unify_types args------------\n";
# debug_pptype(">>unify_types: type1: ", type1);
# debug_pptype(">>unify_types: type2: ", type2);
fi;
unify_types' (stack, type1, type2);
if verbose
if_debugging_say "\nRESULTS:\n";
debug_unparse_type(" " + name1 + ": ", type1);
debug_unparse_type( name2 + ": ", type2);
# if_debugging_say "\n\n----------prettyprinting unify_types results------------\n";
# debug_pptype(">>unify_types: type1: ", type1);
# debug_pptype(">>unify_types: type2: ", type2);
if_debugging_say "\n^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^";
if_debugging_say "============= unify_types/BOTTOM ===============\n";
fi;
fi;
}
# The real work is unifying type variables.
# Here we handle interactions at the next
# level up, the various settings in which
# type variables are embedded:
#
also
fun unify_types' (stack, type1, type2)
=
{ case ( ts::head_reduce_type type1, # Mainly evaluates DEFINED_TYP type functions.
ts::head_reduce_type type2 # " ".
)
( ty::TYPE_VARIABLE_REF var1,
ty::TYPE_VARIABLE_REF var2
)
=>
unify_type_variables (var1, var2);
(ty::TYPE_VARIABLE_REF (var1 as { id, ref_typevar }), etype2)
=>
resolve_type_variable (var1, type2, etype2); # E.g. if var1 is ty::META_TYPE_VARIABLE it becomes ty::RESOLVED_TYPE_VARIABLE(type).
(etype1, ty::TYPE_VARIABLE_REF (var2 as { id, ref_typevar }))
=>
resolve_type_variable (var2, type1, etype1); # " ".
( ty::TYPCON_TYPE (typ1, args1),
ty::TYPCON_TYPE (typ2, args2)
)
=>
if (ts::typs_are_equal (typ1, typ2) )
if_debugging_say "--------- unify_types'/CONSTRUCTOR recursive calls TOP\n";
paired_lists::apply unify (args1, args2)
where
fun unify (type1, type2) = unify_types ("1", "2", type1, type2, stack);
end;
if_debugging_say "--------- unify_types'/CONSTRUCTOR recursive calls BOTTOM\n";
else
raise exception UNIFY_TYPES (TYP_MISMATCH (typ1, typ2));
fi;
# If one of the types is ty::WILDCARD_TYPE, propagate it down into the
# other type to eliminate type_variables that might otherwise cause
# generalize_type to complain.
#
(ty::WILDCARD_TYPE, ty::TYPCON_TYPE(_, args2))
=>
{
if_debugging_say "--------- unify_types'/WILD+CONSTRUCTOR recursive calls TOP\n";
apply (fn x = unify_types ("1", "2", x, ty::WILDCARD_TYPE, stack))
args2;
if_debugging_say "--------- unify_types'/WILD+CONSTRUCTOR recursive calls BOTTOM\n";
};
(ty::TYPCON_TYPE(_, args1), ty::WILDCARD_TYPE)
=>
{
if_debugging_say "--------- unify_types'/CONSTRUCTOR+WILD recursive calls TOP\n";
apply (fn x = unify_types ("1", "2", x, ty::WILDCARD_TYPE, stack))
args1;
if_debugging_say "--------- unify_types'/CONSTRUCTOR+WILD recursive calls BOTTOM\n";
};
(ty::WILDCARD_TYPE, _) => ();
(_, ty::WILDCARD_TYPE) => ();
other => raise exception UNIFY_TYPES (TYPE_MISMATCH other);
esac;
}
also
fun unify_type_variables (var1, var2)
=
{ if_debugging_say ">>unify_type_variables";
if (not (ts::typevar_refs_are_equal (var1, var2)))
unify_type_variables' (sort_vars (var1, var2));
fi;
}
where
# Here is the beating heart of the unification logic.
# The essential tranforms are:
#
# ty::LITERAL_TYPE_VARIABLE can resolve to a compatible
# ty::LITERAL_TYPE_VARIABLE or a monotype of its ty::LITERAL_TYPE_VARIABLE ilk.
#
# ty::USER_TYPE_VARIABLE cannot be changed,
# but its fn_nesting can be reduced.
#
# FLEX can merge with another FLEX or resolve to a META.
#
# META can resolve to anything.
#
# Note that our (typevar_ref1, typevar_ref2) arguments are run
# through sort_vars() before we are called. This reduces the
# number of cases we must consider.
# For example, we can have (USER, META)
# but we can never have (META, USER).
#
fun unify_type_variables'
(
typevar_ref1 as { id => id1, ref_typevar => ref_tv1 as REF type1 },
typevar_ref2 as { id => id2, ref_typevar => ref_tv2 as REF type2 }
)
=
# ASSERT: ref_tv1 != ref_tv2
case type1
#
ty::META_TYPE_VARIABLE
{
fn_nesting => fn_nesting1,
eq => eq1
}
=>
case type2
#
ty::META_TYPE_VARIABLE { fn_nesting=>fn_nesting2, eq=>eq2 }
=>
{ fn_nesting = int::min (fn_nesting1, fn_nesting2);
eq = eq1 or eq2;
#
ref_tv1 := ty::META_TYPE_VARIABLE { fn_nesting, eq };
ref_tv2 := ty::RESOLVED_TYPE_VARIABLE (ty::TYPE_VARIABLE_REF typevar_ref1 );
};
_ => bug "unify_Type_variables 3";
esac;
ty::USER_TYPE_VARIABLE { fn_nesting=>fn_nesting1, eq=>eq1, name }
=>
case type2
#
ty::META_TYPE_VARIABLE { eq=>eq2, fn_nesting=>fn_nesting2 }
=>
if (eq1 or (not eq2))
if (fn_nesting2 < fn_nesting1)
ref_tv1 := ty::USER_TYPE_VARIABLE { fn_nesting=>fn_nesting2, eq=>eq1, name };
fi;
ref_tv2 := ty::RESOLVED_TYPE_VARIABLE (ty::TYPE_VARIABLE_REF typevar_ref1);
else
raise exception UNIFY_TYPES (USER_TYPE_VARIABLE_MISMATCH type1);
fi;
_ => {
raise exception UNIFY_TYPES (USER_TYPE_VARIABLE_MISMATCH type1);
};
esac;
ty::INCOMPLETE_RECORD_TYPE_VARIABLE { known_fields => known_fields1, fn_nesting => fn_nesting1, eq => eq1 }
=>
case type2
#
ty::META_TYPE_VARIABLE { eq=>eq2, fn_nesting=>fn_nesting2 }
=>
{ fn_nesting = int::min (fn_nesting1, fn_nesting2);
eq = eq1 or eq2;
apply (fn (l, t) = adjust_type (t, typevar_ref2, fn_nesting, eq))
known_fields1;
ref_tv1 := ty::INCOMPLETE_RECORD_TYPE_VARIABLE { known_fields=>known_fields1, fn_nesting, eq };
ref_tv2 := ty::RESOLVED_TYPE_VARIABLE (ty::TYPE_VARIABLE_REF typevar_ref1);
};
ty::INCOMPLETE_RECORD_TYPE_VARIABLE { known_fields=>known_fields2, eq=>eq2, fn_nesting=>fn_nesting2 }
=>
{ fn_nesting = int::min (fn_nesting1, fn_nesting2);
eq = eq1 or eq2;
apply (fn (l, t) = adjust_type (t, typevar_ref1, fn_nesting, eq)) known_fields2;
apply (fn (l, t) = adjust_type (t, typevar_ref2, fn_nesting, eq)) known_fields1;
ref_tv1 := ty::INCOMPLETE_RECORD_TYPE_VARIABLE
{ fn_nesting,
eq,
known_fields => (merge_fields (TRUE, TRUE, known_fields1, known_fields2))
};
ref_tv2 := ty::RESOLVED_TYPE_VARIABLE (ty::TYPE_VARIABLE_REF typevar_ref1);
};
_ => bug "unify_type_variables 2";
esac;
ty::LITERAL_TYPE_VARIABLE { kind, source_code_region }
=>
case type2
#
ty::LITERAL_TYPE_VARIABLE { kind=>kind', ... }
=>
if (kind == kind')
ref_tv2 := ty::RESOLVED_TYPE_VARIABLE (ty::TYPE_VARIABLE_REF typevar_ref1);
else
raise exception UNIFY_TYPES (LITERAL_TYPE_MISMATCH type1);
fi;
(ty::META_TYPE_VARIABLE { eq=>e2, ... } | ty::OVERLOADED_TYPE_VARIABLE e2)
=>
# Check eq compatibility
if (not e2 or literal_is_equality_kind kind)
ref_tv2 := ty::RESOLVED_TYPE_VARIABLE (ty::TYPE_VARIABLE_REF typevar_ref1);
else
raise exception UNIFY_TYPES (LITERAL_TYPE_MISMATCH type1);
fi;
_ => raise exception UNIFY_TYPES (LITERAL_TYPE_MISMATCH type1);
esac;
ty::OVERLOADED_TYPE_VARIABLE eq1
=>
case type2
#
ty::OVERLOADED_TYPE_VARIABLE eq2
=>
if (eq1 or not eq2) ref_tv2 := ty::RESOLVED_TYPE_VARIABLE (ty::TYPE_VARIABLE_REF typevar_ref1);
else ref_tv1 := ty::RESOLVED_TYPE_VARIABLE (ty::TYPE_VARIABLE_REF typevar_ref2);
fi;
ty::META_TYPE_VARIABLE { eq=>eq2, fn_nesting=>fn_nesting2 }
=>
if (eq1 or (not eq2))
ref_tv2 := ty::RESOLVED_TYPE_VARIABLE (ty::TYPE_VARIABLE_REF typevar_ref1);
else ref_tv1 := ty::OVERLOADED_TYPE_VARIABLE eq2;
ref_tv2 := ty::RESOLVED_TYPE_VARIABLE (ty::TYPE_VARIABLE_REF typevar_ref1);
fi;
_ => raise exception UNIFY_TYPES OVERLOADED_TYPE_VARIABLE_MISMATCH;
esac;
_ => bug "unify_type_variables 4";
esac; # fun unify_type_variables
end # where
also
fun resolve_type_variable
( var as { id, ref_typevar as REF (ty::META_TYPE_VARIABLE { fn_nesting, eq } ) },
type,
ety
)
=>
{ case ety
ty::WILDCARD_TYPE => ();
_ => adjust_type (ety, var, fn_nesting, eq);
esac;
ref_typevar := ty::RESOLVED_TYPE_VARIABLE type;
};
resolve_type_variable (var as { id, ref_typevar as REF (ty::INCOMPLETE_RECORD_TYPE_VARIABLE { known_fields, fn_nesting, eq } ) }, type, ety)
=>
case ety
#
ty::TYPCON_TYPE (ty::RECORD_TYP field_names, field_types)
=>
{ record_fields = paired_lists::zip (field_names, field_types);
#
apply (fn t = adjust_type (t, var, fn_nesting, eq))
field_types;
merge_fields (FALSE, TRUE, known_fields, record_fields);
ref_typevar := ty::RESOLVED_TYPE_VARIABLE type;
};
ty::WILDCARD_TYPE # propagate ty::WILDCARD_TYPE to the fields
=>
apply (fn (lab, type) = unify_types ("1", "2", ty::WILDCARD_TYPE, type, ["resolve_type_variable"]))
known_fields;
_ => raise exception UNIFY_TYPES (TYPE_MISMATCH (ty::TYPE_VARIABLE_REF (var), ety));
esac;
resolve_type_variable (var as { id, ref_typevar as REF (i as ty::OVERLOADED_TYPE_VARIABLE eq) }, type, ety)
=>
{ adjust_type (ety, var, ty::infinity, eq);
ref_typevar := ty::RESOLVED_TYPE_VARIABLE type;
};
resolve_type_variable (var as { id, ref_typevar as REF (i as ty::LITERAL_TYPE_VARIABLE { kind, ... } ) }, type, ety)
=>
case ety
ty::WILDCARD_TYPE => ();
_ => if (resolve_overloaded_literals::is_literal_type (kind, ety))
ref_typevar := ty::RESOLVED_TYPE_VARIABLE type;
else
raise exception UNIFY_TYPES (LITERAL_TYPE_MISMATCH i); # Should return the type for error msg. XXX BUGGO FIXME
fi;
esac;
resolve_type_variable ({ id, ref_typevar as REF (i as ty::USER_TYPE_VARIABLE _) }, _, ety)
=>
case ety
ty::WILDCARD_TYPE => ();
_ => {
raise exception UNIFY_TYPES (USER_TYPE_VARIABLE_MISMATCH i); # Should return the type for error msg. XXX BUGGO FIXME.
};
esac;
resolve_type_variable ({ id, ref_typevar as REF (ty::RESOLVED_TYPE_VARIABLE _) }, _, _) => bug "resolve_type_variable: ty::RESOLVED_TYPE_VARIABLE";
resolve_type_variable ({ id, ref_typevar as REF (ty::TYPE_VARIABLE_MARK _) }, _, _) => bug "resolve_type_variable: ty::TYPE_VARIABLE_MARK";
end
# merge_fields (extra1, extra2, fields1, fields2):
#
# This function merges the 2 sorted field lists. Fields occurring
# in both lists have their types unified. If a field occurs in only
# one list, say fields { i } then if extra { i } is TRUE, a unify_types
# error is raised.
also
fun merge_fields (extra1, extra2, fields1, fields2)
=
{ fun extra allowed t
=
if (not allowed)
raise exception UNIFY_TYPES RECORD_FIELD_LABELS_MISMATCH;
else t;
fi;
fieldwise ( extra extra1,
extra extra2,
(fn (t1, t2) = { unify_types ("1", "2", t1, t2, ["unify_types::merge_fields"]); t1;}),
fields1,
fields2
);
};
end; # local
}; # package unify_types
end;