[m-rev.] diff: fundeps, polymorphic instances

Mark Brown mark at csse.unimelb.edu.au
Sun Oct 29 14:16:07 AEDT 2006


Estimated hours taken: 16
Branches: main

Support polymorphic instances of typeclasses with functional dependencies.
We do this by allowing type variables in the range arguments, which must be
distinct according to existing typeclass restrictions, to be determined
from type variables in the domain arguments by the functional dependencies
on the instance constraints.

compiler/check_typeclass.m:
	Remove the range-restrictedness check and replace it with a coverage
	check, which makes use of the instance constraints when determining
	if a type variable is bound.

	Explicitly pass the range tvars to get_unbound_tvars, so that it
	can be used by the coverage pass as well as the
	check_typeclass_constraints pass.

	Rearrange the structure of the module, since multiple passes now
	make use of the get_unbound_tvars predicate.  Separate out the
	error reporting code from the main logic.

	Clarify the description at the top of this module.  It now corresponds
	more closely with the structure of the module.

	Fix a bug in check_instance_pred_procs/12 whereby the wrong context
	was being used in the new instance definition, leading to incorrect
	error messages; use field update syntax to avoid this problem.

doc/reference_manual.texi:
	Add an example to illustrate the relaxed restrictions.

tests/valid/Mmakefile:
tests/valid/fundeps_poly_instance.m:
	Test the new feature.

tests/invalid/Mmakefile:
tests/invalid/fundeps_coverage.err_exp:
tests/invalid/fundeps_coverage.m:
	Test the new error reporting.

tests/invalid/range_restrict.err_exp:
	Update for the changed error message.

tests/invalid/typeclass_bogus_method.err_exp:
tests/invalid/typeclass_test_10.err_exp:
	Update these expected outputs for the bugfix.

Index: compiler/check_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/check_typeclass.m,v
retrieving revision 1.105
diff -u -r1.105 check_typeclass.m
--- compiler/check_typeclass.m	25 Oct 2006 14:08:58 -0000	1.105
+++ compiler/check_typeclass.m	29 Oct 2006 02:05:37 -0000
@@ -7,15 +7,15 @@
 %---------------------------------------------------------------------------%
 %
 % File: check_typeclass.m.
-% Author: dgj.
+% Author: dgj, mark
 %
 % This module checks conformance of instance declarations to the typeclass
 % declaration. It takes various steps to do this.
 %
-% First, for every method of every instance it generates a new pred
-% whose types and modes are as expected by the typeclass declaration and
-% whose body just calls the implementation provided by the instance
-% declaration.
+% First, in check_instance_decls/6, for every method of every instance we
+% generate a new pred whose types and modes are as expected by the typeclass
+% declaration and whose body just calls the implementation provided by the
+% instance declaration.
 %
 % eg. given the declarations:
 %
@@ -37,30 +37,41 @@
 %
 % By generating the new pred, we check the instance method for type, mode,
 % determinism and uniqueness correctness since the generated pred is checked
-% in each of those passes too.
+% in each of those passes too.  At this point we add instance method pred/proc
+% ids to the instance table of the HLDS.  We also check that there are no
+% missing, duplicate or bogus methods.
 %
-% Second, this pass checks that all superclass constraints are satisfied
-% by the instance declaration.  To do this it attempts to perform context
-% reduction on the typeclass constraints, using the instance constraints
-% as assumptions.
+% In this pass we also call check_superclass_conformance/9, which checks that
+% all superclass constraints are satisfied by the instance declaration.  To do
+% this it attempts to perform context reduction on the typeclass constraints,
+% using the instance constraints as assumptions.  At this point we fill in
+% the super class proofs.
 %
-% Third, typeclass constraints on predicate and function declarations are
-% checked for ambiguity, taking into consideration the information
-% provided by functional dependencies.
+% Second, in check_for_cyclic_classes/4, we check for cycles in the typeclass
+% hierarchy.  A cycle occurs if we can start from any given typeclass
+% declaration and follow the superclass constraints on classes to reach the
+% same class that we started from.  Only the class_id needs to be repeated;
+% it doesn't need to have the parameters.  Note that we follow the constraints
+% on class declarations only, not those on instance declarations.  While doing
+% this, we fill in the fundeps_ancestors field in the class table.
 %
-% Fourth, all visible instances are checked for range-restrictedness and
-% mutual consistency, with respect to any functional dependencies.  This
-% doesn't necessarily catch all cases of inconsistent instances, however,
-% since in general that cannot be done until link time.  We try to catch
-% as many cases as possible here, though, since we can give better error
-% messages.
+% Third, in check_for_missing_concrete_instances/4, we check that each
+% abstract instance has a corresponding concrete instance.
 %
-% This module also checks for cycles in the typeclass hierarchy, and checks
-% that each abstract instance has a corresponding concrete instance.
+% Fourth, in check_functional_dependencies/4, all visible instances are
+% checked for coverage and mutual consistency with respect to any functional
+% dependencies.  This doesn't necessarily catch all cases of inconsistent
+% instances, however, since in general that cannot be done until link time.
+% We try to catch as many cases as possible here, though, since we can give
+% better error messages.
 %
-% This pass fills in the super class proofs and instance method pred/proc ids
-% in the instance table of the HLDS, and fills in the fundeps_ancestors in
-% the class table.
+% Last, in check_typeclass_constraints/4, we check typeclass constraints on
+% predicate and function declarations and on existentially typed data
+% constructors for ambiguity, taking into consideration the information
+% provided by functional dependencies.  We also call check_constraint_quant/5
+% to check that all type variables in constraints are universally quantified,
+% or that they are all existentially quantified.  We don't support constraints
+% where some of the type variables are universal and some are existential.
 %
 %---------------------------------------------------------------------------%
 
@@ -338,31 +349,10 @@
         BogusInstanceMethods = []
     ;
         BogusInstanceMethods = [_ | _],
-        % There were one or more bogus methods.
-        % Construct an appropriate error message.
-        ClassId = class_id(ClassName, ClassArity),
-        ErrorMsgStart =  [
-            words("In instance declaration for"),
-            sym_name_and_arity(ClassName / ClassArity),
-            suffix(":"),
-            words("incorrect method name(s):")
-        ],
-        ErrorMsgBody0 = list.map(format_method_name, BogusInstanceMethods),
-        ErrorMsgBody1 = list.condense(ErrorMsgBody0),
-        ErrorMsgBody = list.append(ErrorMsgBody1, [suffix(".")]),
-        Pieces = ErrorMsgStart ++ ErrorMsgBody,
-        Msg = simple_msg(Context, [always(Pieces)]),
-        Spec = error_spec(severity_error, phase_type_check, [Msg]),
-        !:Specs = [Spec | !.Specs]
+        report_bogus_instance_methods(ClassId, BogusInstanceMethods, Context,
+            !Specs)
     ).
 
-:- func format_method_name(instance_method) = format_components.
-
-format_method_name(Method) = MethodName :-
-    Method = instance_method(PredOrFunc, Name, _Defn, Arity, _Context),
-    adjust_func_arity(PredOrFunc, Arity, PredArity),
-    MethodName = [p_or_f(PredOrFunc), sym_name_and_arity(Name / PredArity)].
-
 %----------------------------------------------------------------------------%
 
 :- type instance_check_info
@@ -501,9 +491,9 @@
 check_instance_pred_procs(ClassId, ClassVars, MethodName, Markers,
         InstanceDefn0, InstanceDefn, OrderedInstanceMethods0,
         OrderedInstanceMethods, !Info, !Specs) :-
-    InstanceDefn0 = hlds_instance_defn(InstanceModuleName, InstanceStatus,
-        InstanceContext, InstanceConstraints, InstanceTypes,
-        InstanceBody, MaybeInstancePredProcs, InstanceVarSet, InstanceProofs),
+    InstanceDefn0 = hlds_instance_defn(InstanceModuleName, _InstanceStatus,
+        _InstanceContext, InstanceConstraints, InstanceTypes,
+        InstanceBody, MaybeInstancePredProcs, InstanceVarSet, _InstanceProofs),
     !.Info = instance_method_info(_ModuleInfo, _QualInfo, _PredName, Arity,
         _ExistQVars, _ArgTypes, _ClassContext, _ArgModes, _ArgTypeVars,
         _Status, PredOrFunc),
@@ -529,61 +519,20 @@
             MaybeInstancePredProcs = no,
             InstancePredProcs = InstancePredProcs1
         ),
-        InstanceDefn = hlds_instance_defn(InstanceModuleName, InstanceStatus,
-            Context, InstanceConstraints, InstanceTypes,
-            InstanceBody, yes(InstancePredProcs), InstanceVarSet,
-            InstanceProofs)
+        InstanceDefn = InstanceDefn0
+            ^ instance_hlds_interface := yes(InstancePredProcs)
     ;
-        MatchingInstanceMethods = [Instance1, Instance2 | LaterInstances],
-        % Duplicate method definition error.
+        MatchingInstanceMethods = [_, _ | _],
         OrderedInstanceMethods = OrderedInstanceMethods0,
         InstanceDefn = InstanceDefn0,
-        ClassId = class_id(ClassName, _ClassArity),
-        ClassNameString = sym_name_to_string(ClassName),
-        InstanceTypesString = mercury_type_list_to_string(InstanceVarSet,
-            InstanceTypes),
-        HeaderPieces =
-            [words("In instance declaration for"),
-            words("`" ++ ClassNameString ++
-                "(" ++ InstanceTypesString ++ ")':"),
-            words("multiple implementations of type class"),
-            p_or_f(PredOrFunc), words("method"),
-            sym_name_and_arity(MethodName / Arity), suffix("."), nl],
-        HeadingMsg = simple_msg(InstanceContext, [always(HeaderPieces)]),
-        Instance1Context = Instance1 ^ instance_method_decl_context,
-        FirstPieces = [words("First definition appears here."), nl],
-        FirstMsg = simple_msg(Instance1Context, [always(FirstPieces)]),
-        DefnToMsg = (pred(Definition::in, Msg::out) is det :-
-            TheContext = Definition ^ instance_method_decl_context,
-            SubsequentPieces =
-                [words("Subsequent definition appears here."), nl],
-            Msg = simple_msg(TheContext, [always(SubsequentPieces)])
-        ),
-        list.map(DefnToMsg, [Instance2 | LaterInstances], LaterMsgs),
-
-        Spec = error_spec(severity_error, phase_type_check,
-            [HeadingMsg, FirstMsg | LaterMsgs]),
-        !:Specs = [Spec | !.Specs]
+        report_duplicate_method_defn(ClassId, InstanceDefn0, PredOrFunc,
+            MethodName, Arity, MatchingInstanceMethods, !Specs)
     ;
         MatchingInstanceMethods = [],
-        % Undefined method error.
         OrderedInstanceMethods = OrderedInstanceMethods0,
         InstanceDefn = InstanceDefn0,
-        ClassId = class_id(ClassName, _ClassArity),
-        ClassNameString = sym_name_to_string(ClassName),
-        InstanceTypesString = mercury_type_list_to_string(InstanceVarSet,
-            InstanceTypes),
-
-        Pieces = [words("In instance declaration for"),
-            words("`" ++ ClassNameString ++
-                "(" ++ InstanceTypesString ++ ")'"),
-            suffix(":"),
-            words("no implementation for type class"), p_or_f(PredOrFunc),
-            words("method"), sym_name_and_arity(MethodName / Arity),
-            suffix("."), nl],
-        Msg = simple_msg(InstanceContext, [always(Pieces)]),
-        Spec = error_spec(severity_error, phase_type_check, [Msg]),
-        !:Specs = [Spec | !.Specs]
+        report_undefined_method(ClassId, InstanceDefn0, PredOrFunc,
+            MethodName, Arity, !Specs)
     ).
 
     % Get all the instance definitions which match the specified
@@ -1121,35 +1070,6 @@
         find_cycle(ClassId, Tail, Path, Cycle)
     ).
 
-    % Report an error using the format
-    %
-    %   module.m:NNN: Error: cyclic superclass relation detected:
-    %   module.m:NNN:   `foo/N' <= `bar/N' <= `baz/N' <= `foo/N'
-    %
-:- func report_cyclic_classes(class_table, class_path) = error_spec.
-
-report_cyclic_classes(ClassTable, ClassPath) = Spec :-
-    (
-        ClassPath = [],
-        unexpected(this_file, "report_cyclic_classes: empty cycle found.")
-    ;
-        ClassPath = [ClassId | Tail],
-        Context = map.lookup(ClassTable, ClassId) ^ class_context,
-        ClassId = class_id(Name, Arity),
-        RevPieces0 = [sym_name_and_arity(Name/Arity),
-            words("Error: cyclic superclass relation detected:")],
-        RevPieces = foldl(add_path_element, Tail, RevPieces0),
-        Pieces = list.reverse(RevPieces),
-        Msg = simple_msg(Context, [always(Pieces)]),
-        Spec = error_spec(severity_error, phase_parse_tree_to_hlds, [Msg])
-    ).
-
-:- func add_path_element(class_id, list(format_component))
-    = list(format_component).
-
-add_path_element(class_id(Name, Arity), RevPieces0) =
-    [sym_name_and_arity(Name/Arity), words("<=") | RevPieces0].
-
 %---------------------------------------------------------------------------%
 
     % Check that all instances are range restricted with respect to the
@@ -1183,79 +1103,44 @@
     module_info_get_instance_table(!.ModuleInfo, InstanceTable),
     map.lookup(InstanceTable, ClassId, InstanceDefns),
     FunDeps = ClassDefn ^ class_fundeps,
-    check_range_restrictedness(ClassId, InstanceDefns, FunDeps,
-        !ModuleInfo, !Specs),
+    check_coverage(ClassId, InstanceDefns, FunDeps, !ModuleInfo, !Specs),
     check_consistency(ClassId, ClassDefn, InstanceDefns, FunDeps,
         !ModuleInfo, !Specs).
 
-:- pred check_range_restrictedness(class_id::in, list(hlds_instance_defn)::in,
+:- pred check_coverage(class_id::in, list(hlds_instance_defn)::in,
     hlds_class_fundeps::in, module_info::in, module_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-check_range_restrictedness(_, [], _, !ModuleInfo, !Specs).
-check_range_restrictedness(ClassId, [InstanceDefn | InstanceDefns], FunDeps,
-        !ModuleInfo, !Specs) :-
-    list.foldl2(check_range_restrictedness_2(ClassId, InstanceDefn),
-        FunDeps, !ModuleInfo, !Specs),
-    check_range_restrictedness(ClassId, InstanceDefns, FunDeps,
-        !ModuleInfo, !Specs).
+check_coverage(_, [], _, !ModuleInfo, !Specs).
+check_coverage(ClassId, [InstanceDefn | InstanceDefns], FunDeps, !ModuleInfo,
+        !Specs) :-
+    list.foldl2(check_coverage_2(ClassId, InstanceDefn), FunDeps, !ModuleInfo,
+        !Specs),
+    check_coverage(ClassId, InstanceDefns, FunDeps, !ModuleInfo, !Specs).
 
-:- pred check_range_restrictedness_2(class_id::in, hlds_instance_defn::in,
+:- pred check_coverage_2(class_id::in, hlds_instance_defn::in,
     hlds_class_fundep::in, module_info::in, module_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-check_range_restrictedness_2(ClassId, InstanceDefn, FunDep, !ModuleInfo,
-        !Specs) :-
+check_coverage_2(ClassId, InstanceDefn, FunDep, !ModuleInfo, !Specs) :-
+    TVarSet = InstanceDefn ^ instance_tvarset,
     Types = InstanceDefn ^ instance_types,
     FunDep = fundep(Domain, Range),
     DomainTypes = restrict_list_elements(Domain, Types),
     type_vars_list(DomainTypes, DomainVars),
     RangeTypes = restrict_list_elements(Range, Types),
     type_vars_list(RangeTypes, RangeVars),
-    solutions.solutions((pred(V::out) is nondet :-
-            list.member(V, RangeVars),
-            \+ list.member(V, DomainVars)
-        ), UnboundVars),
+    Constraints = InstanceDefn ^ instance_constraints,
+    get_unbound_tvars(TVarSet, DomainVars, RangeVars, Constraints,
+        !.ModuleInfo, UnboundVars),
     (
         UnboundVars = []
     ;
         UnboundVars = [_ | _],
-        Spec = report_range_restriction_error(ClassId, InstanceDefn,
-            UnboundVars),
+        Spec = report_coverage_error(ClassId, InstanceDefn, UnboundVars),
         !:Specs = [Spec | !.Specs]
     ).
 
-    % The error message is intended to look like this:
-    %
-    % long_module_name:001: In instance for typeclass `long_class/2':
-    % long_module_name:001:   functional dependency not satisfied: type
-    % long_module_name:001:   variables T1, T2 and T3 occur in the range of a
-    % long_module_name:001:   functional dependency, but are not in the
-    % long_module_name:001:   domain.
-
-:- func report_range_restriction_error(class_id, hlds_instance_defn,
-    list(tvar)) = error_spec.
-
-report_range_restriction_error(ClassId, InstanceDefn, Vars) = Spec :-
-    ClassId = class_id(SymName, Arity),
-    TVarSet = InstanceDefn ^ instance_tvarset,
-    Context = InstanceDefn ^ instance_context,
-
-    VarsStrs = list.map((func(Var) = mercury_var_to_string(Var, TVarSet, no)),
-        Vars),
-
-    Pieces = [words("In instance for typeclass"),
-        sym_name_and_arity(SymName / Arity), suffix(":"), nl,
-        words("functional dependency not satisfied:"),
-        words(choose_number(Vars, "type variable", "type variables"))]
-        ++ list_to_pieces(VarsStrs) ++
-        [words(choose_number(Vars, "occurs", "occur")),
-        words("in the range of the functional dependency, but"),
-        words(choose_number(Vars, "is", "are")),
-        words("not in the domain."), nl],
-    Msg = simple_msg(Context, [always(Pieces)]),
-    Spec = error_spec(severity_error, phase_type_check, [Msg]).
-
     % Check the consistency of each (unordered) pair of instances.
     %
 :- pred check_consistency(class_id::in, hlds_class_defn::in,
@@ -1317,34 +1202,6 @@
         true
     ).
 
-:- func report_consistency_error(class_id, hlds_class_defn,
-    hlds_instance_defn, hlds_instance_defn, hlds_class_fundep) = error_spec.
-
-report_consistency_error(ClassId, ClassDefn, InstanceA, InstanceB, FunDep)
-        = Spec :-
-    ClassId = class_id(SymName, Arity),
-    Params = ClassDefn ^ class_vars,
-    TVarSet = ClassDefn ^ class_tvarset,
-    ContextA = InstanceA ^ instance_context,
-    ContextB = InstanceB ^ instance_context,
-
-    FunDep = fundep(Domain, Range),
-    DomainParams = restrict_list_elements(Domain, Params),
-    RangeParams = restrict_list_elements(Range, Params),
-    DomainList = mercury_vars_to_string(DomainParams, TVarSet, no),
-    RangeList = mercury_vars_to_string(RangeParams, TVarSet, no),
-    FunDepStr = "`(" ++ DomainList ++ " -> " ++ RangeList ++ ")'",
-
-    PiecesA = [words("Inconsistent instance declaration for typeclass"),
-        sym_name_and_arity(SymName / Arity),
-        words("with functional dependency"), fixed(FunDepStr),
-        suffix("."), nl],
-    PiecesB = [words("Here is the conflicting instance.")],
-
-    MsgA = simple_msg(ContextA, [always(PiecesA)]),
-    MsgB = error_msg(yes(ContextB), yes, 0, [always(PiecesB)]),
-    Spec = error_spec(severity_error, phase_parse_tree_to_hlds, [MsgA, MsgB]).
-
 %---------------------------------------------------------------------------%
 
     % Look for pred or func declarations for which the type variables in
@@ -1408,8 +1265,11 @@
     pred_info_get_typevarset(PredInfo, TVarSet),
     pred_info_get_arg_types(PredInfo, ArgTypes),
     pred_info_get_class_context(PredInfo, Constraints),
-    type_vars_list(ArgTypes, TVars),
-    get_unbound_tvars(TVarSet, TVars, Constraints, !.ModuleInfo, UnboundTVars),
+    type_vars_list(ArgTypes, ArgTVars),
+    prog_constraints_get_tvars(Constraints, ConstrainedTVars),
+    Constraints = constraints(UnivCs, ExistCs),
+    get_unbound_tvars(TVarSet, ArgTVars, ConstrainedTVars, UnivCs ++ ExistCs,
+        !.ModuleInfo, UnboundTVars),
     (
         UnboundTVars = []
     ;
@@ -1442,8 +1302,9 @@
     type_vars_list(ArgTypes, ArgTVars),
     list.filter((pred(V::in) is semidet :- list.member(V, ExistQVars)),
         ArgTVars, ExistQArgTVars),
+    constraint_list_get_tvars(Constraints, ConstrainedTVars),
     get_type_defn_tvarset(TypeDefn, TVarSet),
-    get_unbound_tvars(TVarSet, ExistQArgTVars, constraints([], Constraints),
+    get_unbound_tvars(TVarSet, ExistQArgTVars, ConstrainedTVars, Constraints,
         !.ModuleInfo, UnboundTVars),
     (
         UnboundTVars = []
@@ -1454,30 +1315,57 @@
         !:Specs = [Spec | !.Specs]
     ).
 
-:- pred get_unbound_tvars(tvarset::in, list(tvar)::in, prog_constraints::in,
-    module_info::in, list(tvar)::out) is det.
+%---------------------------------------------------------------------------%
 
-get_unbound_tvars(TVarSet, TVars, Constraints, ModuleInfo, UnboundTVars) :-
-    module_info_get_class_table(ModuleInfo, ClassTable),
-    InducedFunDeps = induced_fundeps(ClassTable, TVarSet, Constraints),
-    FunDepsClosure = fundeps_closure(InducedFunDeps, list_to_set(TVars)),
-    solutions.solutions(
-        constrained_var_not_in_closure(Constraints, FunDepsClosure),
-            UnboundTVars).
+    % Check that all types appearing in universal (existential) constraints are
+    % universally (existentially) quantified.
+    %
+:- pred check_constraint_quant(pred_info::in,
+    module_info::in, module_info::out,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+check_constraint_quant(PredInfo, !ModuleInfo, !Specs) :-
+    pred_info_get_exist_quant_tvars(PredInfo, ExistQVars),
+    pred_info_get_class_context(PredInfo, Constraints),
+    Constraints = constraints(UnivCs, ExistCs),
+    prog_type.constraint_list_get_tvars(UnivCs, UnivTVars),
+    solutions.solutions((pred(V::out) is nondet :-
+            list.member(V, UnivTVars),
+            list.member(V, ExistQVars)
+        ), BadUnivTVars),
+    maybe_report_badly_quantified_vars(PredInfo, universal_constraint,
+        BadUnivTVars, !ModuleInfo, !Specs),
+    prog_type.constraint_list_get_tvars(ExistCs, ExistTVars),
+    list.delete_elems(ExistTVars, ExistQVars, BadExistTVars),
+    maybe_report_badly_quantified_vars(PredInfo, existential_constraint,
+        BadExistTVars, !ModuleInfo, !Specs).
 
-:- pred constrained_var_not_in_closure(prog_constraints::in, set(tvar)::in,
-    tvar::out) is nondet.
+:- pred maybe_report_badly_quantified_vars(pred_info::in, quant_error_type::in,
+    list(tvar)::in, module_info::in, module_info::out,
+    list(error_spec)::in, list(error_spec)::out) is det.
 
-constrained_var_not_in_closure(ClassContext, Closure, UnboundTVar) :-
-    ClassContext = constraints(UnivCs, ExistCs),
+maybe_report_badly_quantified_vars(PredInfo, QuantErrorType, TVars,
+        !ModuleInfo, !Specs) :-
     (
-        Constraints = UnivCs
+        TVars = []
     ;
-        Constraints = ExistCs
-    ),
-    prog_type.constraint_list_get_tvars(Constraints, TVars),
-    list.member(UnboundTVar, TVars),
-    \+ set.member(UnboundTVar, Closure).
+        TVars = [_ | _],
+        Spec = report_badly_quantified_vars(PredInfo, QuantErrorType, TVars),
+        !:Specs = [Spec | !.Specs]
+    ).
+
+%---------------------------------------------------------------------------%
+
+:- pred get_unbound_tvars(tvarset::in, list(tvar)::in, list(tvar)::in,
+    list(prog_constraint)::in, module_info::in, list(tvar)::out) is det.
+
+get_unbound_tvars(TVarSet, RootTVars, AllTVars, Constraints, ModuleInfo,
+        UnboundTVars) :-
+    module_info_get_class_table(ModuleInfo, ClassTable),
+    InducedFunDeps = induced_fundeps(ClassTable, TVarSet, Constraints),
+    FunDepsClosure = fundeps_closure(InducedFunDeps, list_to_set(RootTVars)),
+    UnboundTVarsSet = set.difference(list_to_set(AllTVars), FunDepsClosure),
+    UnboundTVars = set.to_sorted_list(UnboundTVarsSet).
 
 :- type induced_fundeps == list(induced_fundep).
 :- type induced_fundep
@@ -1486,12 +1374,11 @@
                 range       :: set(tvar)
             ).
 
-:- func induced_fundeps(class_table, tvarset, prog_constraints)
+:- func induced_fundeps(class_table, tvarset, list(prog_constraint))
     = induced_fundeps.
 
-induced_fundeps(ClassTable, TVarSet, constraints(UnivCs, ExistCs))
-    = foldl(induced_fundeps_2(ClassTable, TVarSet), UnivCs,
-        foldl(induced_fundeps_2(ClassTable, TVarSet), ExistCs, [])).
+induced_fundeps(ClassTable, TVarSet, Constraints)
+    = foldl(induced_fundeps_2(ClassTable, TVarSet), Constraints, []).
 
 :- func induced_fundeps_2(class_table, tvarset, prog_constraint,
     induced_fundeps) = induced_fundeps.
@@ -1585,7 +1472,213 @@
         !:FunDeps = [FunDep | !.FunDeps]
     ).
 
-    % The error message is intended to look like this:
+%---------------------------------------------------------------------------%
+%---------------------------------------------------------------------------%
+%
+% Error reporting.
+%
+%---------------------------------------------------------------------------%
+
+    % Duplicate method definition error.
+    %
+:- pred report_duplicate_method_defn(class_id::in, hlds_instance_defn::in,
+    pred_or_func::in, sym_name::in, arity::in, instance_methods::in,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+report_duplicate_method_defn(ClassId, InstanceDefn, PredOrFunc, MethodName,
+        Arity, MatchingInstanceMethods, !Specs) :-
+    InstanceVarSet = InstanceDefn ^ instance_tvarset,
+    InstanceTypes = InstanceDefn ^ instance_types,
+    InstanceContext = InstanceDefn ^ instance_context,
+    ClassId = class_id(ClassName, _ClassArity),
+    ClassNameString = sym_name_to_string(ClassName),
+    InstanceTypesString = mercury_type_list_to_string(InstanceVarSet,
+        InstanceTypes),
+    HeaderPieces =
+        [words("In instance declaration for"),
+        words("`" ++ ClassNameString ++
+            "(" ++ InstanceTypesString ++ ")':"),
+        words("multiple implementations of type class"),
+        p_or_f(PredOrFunc), words("method"),
+        sym_name_and_arity(MethodName / Arity), suffix("."), nl],
+    HeadingMsg = simple_msg(InstanceContext, [always(HeaderPieces)]),
+    ( MatchingInstanceMethods = [FirstInstance0 | LaterInstances0] ->
+        FirstInstance = FirstInstance0,
+        LaterInstances = LaterInstances0
+    ;
+        unexpected(this_file, "no matching instances")
+    ),
+    FirstInstanceContext = FirstInstance ^ instance_method_decl_context,
+    FirstPieces = [words("First definition appears here."), nl],
+    FirstMsg = simple_msg(FirstInstanceContext, [always(FirstPieces)]),
+    DefnToMsg = (pred(Definition::in, Msg::out) is det :-
+        TheContext = Definition ^ instance_method_decl_context,
+        SubsequentPieces =
+            [words("Subsequent definition appears here."), nl],
+        Msg = simple_msg(TheContext, [always(SubsequentPieces)])
+    ),
+    list.map(DefnToMsg, LaterInstances, LaterMsgs),
+
+    Spec = error_spec(severity_error, phase_type_check,
+        [HeadingMsg, FirstMsg | LaterMsgs]),
+    !:Specs = [Spec | !.Specs].
+
+%---------------------------------------------------------------------------%
+
+    % Undefined method error.
+    %
+:- pred report_undefined_method(class_id::in, hlds_instance_defn::in,
+    pred_or_func::in, sym_name::in, arity::in,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+report_undefined_method(ClassId, InstanceDefn, PredOrFunc, MethodName, Arity,
+        !Specs) :-
+    InstanceVarSet = InstanceDefn ^ instance_tvarset,
+    InstanceTypes = InstanceDefn ^ instance_types,
+    InstanceContext = InstanceDefn ^ instance_context,
+    ClassId = class_id(ClassName, _ClassArity),
+    ClassNameString = sym_name_to_string(ClassName),
+    InstanceTypesString = mercury_type_list_to_string(InstanceVarSet,
+        InstanceTypes),
+
+    Pieces = [words("In instance declaration for"),
+        words("`" ++ ClassNameString ++
+            "(" ++ InstanceTypesString ++ ")'"),
+        suffix(":"),
+        words("no implementation for type class"), p_or_f(PredOrFunc),
+        words("method"), sym_name_and_arity(MethodName / Arity),
+        suffix("."), nl],
+    Msg = simple_msg(InstanceContext, [always(Pieces)]),
+    Spec = error_spec(severity_error, phase_type_check, [Msg]),
+    !:Specs = [Spec | !.Specs].
+
+%---------------------------------------------------------------------------%
+
+:- pred report_bogus_instance_methods(class_id::in, instance_methods::in,
+    prog_context::in, list(error_spec)::in, list(error_spec)::out) is det.
+
+report_bogus_instance_methods(ClassId, BogusInstanceMethods, Context, !Specs) :-
+    % There were one or more bogus methods.
+    % Construct an appropriate error message.
+    ClassId = class_id(ClassName, ClassArity),
+    ErrorMsgStart =  [
+        words("In instance declaration for"),
+        sym_name_and_arity(ClassName / ClassArity),
+        suffix(":"),
+        words("incorrect method name(s):")
+    ],
+    ErrorMsgBody0 = list.map(format_method_name, BogusInstanceMethods),
+    ErrorMsgBody1 = list.condense(ErrorMsgBody0),
+    ErrorMsgBody = list.append(ErrorMsgBody1, [suffix(".")]),
+    Pieces = ErrorMsgStart ++ ErrorMsgBody,
+    Msg = simple_msg(Context, [always(Pieces)]),
+    Spec = error_spec(severity_error, phase_type_check, [Msg]),
+    !:Specs = [Spec | !.Specs].
+
+:- func format_method_name(instance_method) = format_components.
+
+format_method_name(Method) = MethodName :-
+    Method = instance_method(PredOrFunc, Name, _Defn, Arity, _Context),
+    adjust_func_arity(PredOrFunc, Arity, PredArity),
+    MethodName = [p_or_f(PredOrFunc), sym_name_and_arity(Name / PredArity)].
+
+%---------------------------------------------------------------------------%
+
+    % The error message for cyclic classes is intended to look like this:
+    %
+    %   module.m:NNN: Error: cyclic superclass relation detected:
+    %   module.m:NNN:   `foo/N' <= `bar/N' <= `baz/N' <= `foo/N'
+    %
+:- func report_cyclic_classes(class_table, class_path) = error_spec.
+
+report_cyclic_classes(ClassTable, ClassPath) = Spec :-
+    (
+        ClassPath = [],
+        unexpected(this_file, "report_cyclic_classes: empty cycle found.")
+    ;
+        ClassPath = [ClassId | Tail],
+        Context = map.lookup(ClassTable, ClassId) ^ class_context,
+        ClassId = class_id(Name, Arity),
+        RevPieces0 = [sym_name_and_arity(Name/Arity),
+            words("Error: cyclic superclass relation detected:")],
+        RevPieces = foldl(add_path_element, Tail, RevPieces0),
+        Pieces = list.reverse(RevPieces),
+        Msg = simple_msg(Context, [always(Pieces)]),
+        Spec = error_spec(severity_error, phase_parse_tree_to_hlds, [Msg])
+    ).
+
+:- func add_path_element(class_id, list(format_component))
+    = list(format_component).
+
+add_path_element(class_id(Name, Arity), RevPieces0) =
+    [sym_name_and_arity(Name/Arity), words("<=") | RevPieces0].
+
+%---------------------------------------------------------------------------%
+
+    % The coverage error message is intended to look like this:
+    %
+    % long_module_name:001: In instance for typeclass `long_class/2':
+    % long_module_name:001:   functional dependency not satisfied: type
+    % long_module_name:001:   variables T1, T2 and T3 occur in the range of a
+    % long_module_name:001:   functional dependency, but are not determined
+    % long_module_name:001:   by the domain.
+
+:- func report_coverage_error(class_id, hlds_instance_defn, list(tvar))
+    = error_spec.
+
+report_coverage_error(ClassId, InstanceDefn, Vars) = Spec :-
+    ClassId = class_id(SymName, Arity),
+    TVarSet = InstanceDefn ^ instance_tvarset,
+    Context = InstanceDefn ^ instance_context,
+
+    VarsStrs = list.map((func(Var) = mercury_var_to_string(Var, TVarSet, no)),
+        Vars),
+
+    Pieces = [words("In instance for typeclass"),
+        sym_name_and_arity(SymName / Arity), suffix(":"), nl,
+        words("functional dependency not satisfied:"),
+        words(choose_number(Vars, "type variable", "type variables"))]
+        ++ list_to_pieces(VarsStrs) ++
+        [words(choose_number(Vars, "occurs", "occur")),
+        words("in the range of the functional dependency, but"),
+        words(choose_number(Vars, "is", "are")),
+        words("not determined by the domain."), nl],
+    Msg = simple_msg(Context, [always(Pieces)]),
+    Spec = error_spec(severity_error, phase_type_check, [Msg]).
+
+%---------------------------------------------------------------------------%
+
+:- func report_consistency_error(class_id, hlds_class_defn,
+    hlds_instance_defn, hlds_instance_defn, hlds_class_fundep) = error_spec.
+
+report_consistency_error(ClassId, ClassDefn, InstanceA, InstanceB, FunDep)
+        = Spec :-
+    ClassId = class_id(SymName, Arity),
+    Params = ClassDefn ^ class_vars,
+    TVarSet = ClassDefn ^ class_tvarset,
+    ContextA = InstanceA ^ instance_context,
+    ContextB = InstanceB ^ instance_context,
+
+    FunDep = fundep(Domain, Range),
+    DomainParams = restrict_list_elements(Domain, Params),
+    RangeParams = restrict_list_elements(Range, Params),
+    DomainList = mercury_vars_to_string(DomainParams, TVarSet, no),
+    RangeList = mercury_vars_to_string(RangeParams, TVarSet, no),
+    FunDepStr = "`(" ++ DomainList ++ " -> " ++ RangeList ++ ")'",
+
+    PiecesA = [words("Inconsistent instance declaration for typeclass"),
+        sym_name_and_arity(SymName / Arity),
+        words("with functional dependency"), fixed(FunDepStr),
+        suffix("."), nl],
+    PiecesB = [words("Here is the conflicting instance.")],
+
+    MsgA = simple_msg(ContextA, [always(PiecesA)]),
+    MsgB = error_msg(yes(ContextB), yes, 0, [always(PiecesB)]),
+    Spec = error_spec(severity_error, phase_parse_tree_to_hlds, [MsgA, MsgB]).
+
+%---------------------------------------------------------------------------%
+
+    % The error messages for ambiguous types are intended to look like this:
     %
     % long_module_name:001: In declaration for function `long_function/2':
     % long_module_name:001:   error in type class constraints: type variables
@@ -1698,47 +1791,10 @@
 
 %---------------------------------------------------------------------------%
 
-    % Check that all types appearing in universal (existential) constraints are
-    % universally (existentially) quantified.
-    %
-:- pred check_constraint_quant(pred_info::in,
-    module_info::in, module_info::out,
-    list(error_spec)::in, list(error_spec)::out) is det.
-
-check_constraint_quant(PredInfo, !ModuleInfo, !Specs) :-
-    pred_info_get_exist_quant_tvars(PredInfo, ExistQVars),
-    pred_info_get_class_context(PredInfo, Constraints),
-    Constraints = constraints(UnivCs, ExistCs),
-    prog_type.constraint_list_get_tvars(UnivCs, UnivTVars),
-    solutions.solutions((pred(V::out) is nondet :-
-            list.member(V, UnivTVars),
-            list.member(V, ExistQVars)
-        ), BadUnivTVars),
-    maybe_report_badly_quantified_vars(PredInfo, universal_constraint,
-        BadUnivTVars, !ModuleInfo, !Specs),
-    prog_type.constraint_list_get_tvars(ExistCs, ExistTVars),
-    list.delete_elems(ExistTVars, ExistQVars, BadExistTVars),
-    maybe_report_badly_quantified_vars(PredInfo, existential_constraint,
-        BadExistTVars, !ModuleInfo, !Specs).
-
 :- type quant_error_type
     --->    universal_constraint
     ;       existential_constraint.
 
-:- pred maybe_report_badly_quantified_vars(pred_info::in, quant_error_type::in,
-    list(tvar)::in, module_info::in, module_info::out,
-    list(error_spec)::in, list(error_spec)::out) is det.
-
-maybe_report_badly_quantified_vars(PredInfo, QuantErrorType, TVars,
-        !ModuleInfo, !Specs) :-
-    (
-        TVars = []
-    ;
-        TVars = [_ | _],
-        Spec = report_badly_quantified_vars(PredInfo, QuantErrorType, TVars),
-        !:Specs = [Spec | !.Specs]
-    ).
-
 :- func report_badly_quantified_vars(pred_info, quant_error_type, list(tvar))
     = error_spec.
 
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.371
diff -u -r1.371 reference_manual.texi
--- doc/reference_manual.texi	4 Oct 2006 06:36:56 -0000	1.371
+++ doc/reference_manual.texi	29 Oct 2006 01:48:40 -0000
@@ -5428,6 +5428,15 @@
 
 @noindent
 since the variable @samp{T} may not always be bound to the same type.
+However, the instance
+
+ at example
+	:- instance baz(list(S), list(T)) <= baz(S, T) where @dots{}
+ at end example
+
+is legal because the @samp{baz(S, T)} constraint ensures that whatever
+ at samp{T} is bound to, it is always uniquely determined from the binding
+of @samp{S}.
 
 The extra requirements that result from the use of functional dependencies
 allow the bindings of some variables to be determined from the bindings
Index: tests/invalid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.199
diff -u -r1.199 Mmakefile
--- tests/invalid/Mmakefile	19 Oct 2006 07:29:53 -0000	1.199
+++ tests/invalid/Mmakefile	28 Oct 2006 16:12:00 -0000
@@ -87,6 +87,7 @@
 	freefree \
 	func_errors \
 	funcs_as_preds \
+	fundeps_coverage \
 	fundeps_unbound_in_ctor \
 	fundeps_vars \
 	hawkins_mm_fail_reset \
Index: tests/invalid/fundeps_coverage.err_exp
===================================================================
RCS file: tests/invalid/fundeps_coverage.err_exp
diff -N tests/invalid/fundeps_coverage.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/fundeps_coverage.err_exp	28 Oct 2006 16:16:41 -0000
@@ -0,0 +1,4 @@
+fundeps_coverage.m:011: In instance for typeclass `fundeps_coverage.bar'/3:
+fundeps_coverage.m:011:   functional dependency not satisfied: type variable C
+fundeps_coverage.m:011:   occurs in the range of the functional dependency, but
+fundeps_coverage.m:011:   is not determined by the domain.
Index: tests/invalid/fundeps_coverage.m
===================================================================
RCS file: tests/invalid/fundeps_coverage.m
diff -N tests/invalid/fundeps_coverage.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/fundeps_coverage.m	28 Oct 2006 16:15:54 -0000
@@ -0,0 +1,12 @@
+:- module fundeps_coverage.
+:- interface.
+
+:- typeclass foo(A, B, C) <= (A -> B) where [].
+:- typeclass bar(A, B, C) <= (A -> B, C) where [].
+
+:- implementation.
+
+:- type t(T) ---> t(T).
+
+:- instance bar(t(A), t(B), t(C)) <= foo(A, B, C) where [].
+
Index: tests/invalid/range_restrict.err_exp
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/range_restrict.err_exp,v
retrieving revision 1.4
diff -u -r1.4 range_restrict.err_exp
--- tests/invalid/range_restrict.err_exp	19 Oct 2006 07:29:54 -0000	1.4
+++ tests/invalid/range_restrict.err_exp	29 Oct 2006 03:08:50 -0000
@@ -1,4 +1,4 @@
 range_restrict.m:010: In instance for typeclass `range_restrict.foo'/2:
 range_restrict.m:010:   functional dependency not satisfied: type variables Y
 range_restrict.m:010:   and Z occur in the range of the functional dependency,
-range_restrict.m:010:   but are not in the domain.
+range_restrict.m:010:   but are not determined by the domain.
Index: tests/invalid/typeclass_bogus_method.err_exp
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/typeclass_bogus_method.err_exp,v
retrieving revision 1.4
diff -u -r1.4 typeclass_bogus_method.err_exp
--- tests/invalid/typeclass_bogus_method.err_exp	14 Sep 2005 05:26:52 -0000	1.4
+++ tests/invalid/typeclass_bogus_method.err_exp	28 Oct 2006 15:26:30 -0000
@@ -1,11 +1,11 @@
-typeclass_bogus_method.m:022: In instance declaration for
-typeclass_bogus_method.m:022:   `typeclass_bogus_method.tc1'/1: incorrect
-typeclass_bogus_method.m:022:   method name(s): function
-typeclass_bogus_method.m:022:   `typeclass_bogus_method.bar'/3.
-typeclass_bogus_method.m:026: In instance declaration for
-typeclass_bogus_method.m:026:   `typeclass_bogus_method.tc2'/1: incorrect
-typeclass_bogus_method.m:026:   method name(s): function
-typeclass_bogus_method.m:026:   `typeclass_bogus_method.baz'/2.
+typeclass_bogus_method.m:021: In instance declaration for
+typeclass_bogus_method.m:021:   `typeclass_bogus_method.tc1'/1: incorrect
+typeclass_bogus_method.m:021:   method name(s): function
+typeclass_bogus_method.m:021:   `typeclass_bogus_method.bar'/3.
+typeclass_bogus_method.m:025: In instance declaration for
+typeclass_bogus_method.m:025:   `typeclass_bogus_method.tc2'/1: incorrect
+typeclass_bogus_method.m:025:   method name(s): function
+typeclass_bogus_method.m:025:   `typeclass_bogus_method.baz'/2.
 typeclass_bogus_method.m:029: In instance declaration for
 typeclass_bogus_method.m:029:   `typeclass_bogus_method.tc3(int)': no
 typeclass_bogus_method.m:029:   implementation for type class function method
@@ -14,7 +14,7 @@
 typeclass_bogus_method.m:029:   `typeclass_bogus_method.tc3'/1: incorrect
 typeclass_bogus_method.m:029:   method name(s): function
 typeclass_bogus_method.m:029:   `typeclass_bogus_method.foo5'/2.
-typeclass_bogus_method.m:033: In instance declaration for
-typeclass_bogus_method.m:033:   `typeclass_bogus_method.tc4'/1: incorrect
-typeclass_bogus_method.m:033:   method name(s): function
-typeclass_bogus_method.m:033:   `typeclass_bogus_method.foo5'/2.
+typeclass_bogus_method.m:032: In instance declaration for
+typeclass_bogus_method.m:032:   `typeclass_bogus_method.tc4'/1: incorrect
+typeclass_bogus_method.m:032:   method name(s): function
+typeclass_bogus_method.m:032:   `typeclass_bogus_method.foo5'/2.
Index: tests/invalid/typeclass_test_10.err_exp
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/typeclass_test_10.err_exp,v
retrieving revision 1.4
diff -u -r1.4 typeclass_test_10.err_exp
--- tests/invalid/typeclass_test_10.err_exp	14 Sep 2005 05:26:53 -0000	1.4
+++ tests/invalid/typeclass_test_10.err_exp	28 Oct 2006 15:26:49 -0000
@@ -1,6 +1,6 @@
 typeclass_test_10.m:012: In instance declaration for `typeclass_test_10.bar'/1:
 typeclass_test_10.m:012:   incorrect method name(s): predicate
 typeclass_test_10.m:012:   `typeclass_test_10.p'/0.
-typeclass_test_10.m:017: In instance declaration for `typeclass_test_10.baz'/1:
-typeclass_test_10.m:017:   incorrect method name(s): predicate
-typeclass_test_10.m:017:   `typeclass_test_10.r'/0.
+typeclass_test_10.m:015: In instance declaration for `typeclass_test_10.baz'/1:
+typeclass_test_10.m:015:   incorrect method name(s): predicate
+typeclass_test_10.m:015:   `typeclass_test_10.r'/0.
Index: tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.181
diff -u -r1.181 Mmakefile
--- tests/valid/Mmakefile	22 Oct 2006 09:14:33 -0000	1.181
+++ tests/valid/Mmakefile	28 Oct 2006 15:31:04 -0000
@@ -29,6 +29,7 @@
 	func_class \
 	func_method \
 	fundeps \
+	fundeps_poly_instance \
 	instance_superclass \
 	instance_unconstrained_tvar \
 	mpj2 \
Index: tests/valid/fundeps_poly_instance.m
===================================================================
RCS file: tests/valid/fundeps_poly_instance.m
diff -N tests/valid/fundeps_poly_instance.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/valid/fundeps_poly_instance.m	29 Oct 2006 01:36:06 -0000
@@ -0,0 +1,26 @@
+:- module fundeps_poly_instance.
+:- interface.
+
+:- typeclass foo(A, B) <= (A -> B) where [].
+
+:- typeclass bar(A, B, C) <= foo(A, B) where [].
+
+:- typeclass baz(A, B, C) <= ((A -> B, C), bar(A, B, C)) where [].
+
+:- implementation.
+
+:- type t(T) ---> t(T).
+
+	% B is in the range of the functional dependency we must satisfy,
+	% but it is determined from A by the functional dependencies on the
+	% constraint.
+	%
+:- instance foo(t(A), t(B)) <= foo(A, B) where [].
+
+:- instance bar(t(A), t(B), t(C)) <= foo(A, B) where [].
+
+	% B and C are in the range of the functional dependency we must
+	% satisfy.  B is determined from the foo/2 constraint, and C is
+	% determined by an ancestor of the bar/3 constraint.
+:- instance baz(t(A), t(B), t(C)) <= (foo(A, B), bar(B, C, A)) where [].
+
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------



More information about the reviews mailing list