Never substitute bound type variables; defer rigid fundep improvements

doc/BH_ref_guide/BH_lang.tex

@@ -1192,7 +1192,7 @@ \subsection{{\te{class}} declarations}
 were introduced in section {\ref{sec-overloading}}.  A new class is
 declared using the following:
 
-\gram{topDefn}{\term{class} \opt{\nterm{context} \term{=>}} \nterm{classId} \many{\nterm{tyVarId}} \opt{\term{|} \nterm{funDep}}
+\gram{topDefn}{\term{class} \opt{\term{coherent} {\alt} \term{incoherent}} \opt{\nterm{context} \term{=>}} \nterm{classId} \many{\nterm{tyVarId}} \opt{\term{|} \nterm{funDep}}
         \term{where} \term{\{}} \\
 \grammore{ \many{\nterm{varId} \term{::} \nterm{ctxType} \term{;}} } \\
 \grammore{ \term{\}} }
@@ -1263,9 +1263,45 @@ \subsection{{\te{class}} declarations}
 See section {\ref{sec-primitives-size-types}} for more detailed
 insights into the use of functional dependencies.
 
-\begin{NOTE}
-Functional dependencies are not currently checked by the compiler.
-\end{NOTE}
+Functional dependencies are enforced by the compiler.  At a use of an
+overloaded identifier, instances are ordered from more specific to
+less specific and selection is driven by the determining (left-hand
+side) parameters of the dependency alone: the compiler selects the
+most specific instance whose determining parameters match, and that
+instance then fixes the dependent parameters, as the dependency
+promises.  If the context demands dependent types that conflict with
+the selected instance, the program is rejected; the compiler does not
+fall through to a less specific instance, since the demanded result
+would then be choosing the instance ({\emph{incoherence}}).
+
+The compiler also checks that each instance declaration honors the
+class's dependencies: within an instance, the dependent parameters
+should be determined by the determining parameters, directly or
+through the instance's context, and the compiler warns otherwise,
+since an uncovered instance lets the same inputs be satisfied with
+many different results, contradicting what the dependency promises.
+
+\index{coherent@\te{coherent} (keyword)}
+\index{incoherent@\te{incoherent} (keyword)}
+The optional coherence annotation ({\te{coherent}} or
+{\te{incoherent}}, immediately after the {\te{class}} keyword) opts a
+class out of this discipline.  For an {\te{incoherent}} class, an
+instance whose dependent parameters conflict is skipped and a less
+specific instance may be selected instead, so resolution may be
+driven by the demanded result type and may differ from context to
+context; the coverage warning is suppressed for its instances.  This
+is appropriate for classes whose dependency is declared to guide type
+inference even though resolution is intentionally structural (the
+Prelude's tuple-selection classes are an example).  {\te{coherent}}
+states the default explicitly.  The compiler flag
+{\te{-legacy-defer-instances}} restores the older, output-driven
+resolution behavior globally, as a temporary migration aid.
+
+Example:
+\begin{verbatim}
+ class incoherent Pick a b | a -> b where
+     pick :: a -> b
+\end{verbatim}
 
 % ----------------------------------------------------------------
 

doc/BSV_ref_guide/BSV_lang.tex

@@ -4472,14 +4472,17 @@ \subsection{Type class declarations}
 
 A new class is declared using the following syntax:
 
-\gram{typeclassDef}{ \term{typeclass} \nterm{typeclassIde}
+\gram{typeclassDef}{ \term{typeclass} \opt{\nterm{coherenceAnno}}
+                                      \nterm{typeclassIde}
                                       \nterm{typeFormals}
                                       \opt{ \nterm{provisos}}} \\
 \grammore                  { \opt {\nterm{typedepends}} \term{;} } \\
 %                                      \term{;} } \\
 \grammore          { \hmm \many{ \nterm{overloadedDef} } } \\
 \grammore          { \term{endtypeclass} \opt{: \nterm{typeclassIde} } }
 
+\gram{coherenceAnno}{ \term{coherent} {\alt} \term{incoherent} }
+
 \gram{typeclassIde}{ \nterm{Identifier} }
 
 \gram{typeFormals}{\term{\#} \term{(} \nterm{typeFormal} \many{ \term{,} \nterm{typeFormal}}\term{)} }
@@ -4513,6 +4516,25 @@ \subsection{Type class declarations}
 {\nterm{overloadedDef}s} declare the overloaded variables or function
 names,  and their types.
 
+\index{coherent@\te{coherent} (typeclass annotation)}
+\index{incoherent@\te{incoherent} (typeclass annotation)}
+The optional coherence annotation (\texttt{coherent} or
+\texttt{incoherent}, before the typeclass name) declares whether
+instance selection for this class is expected to be a function of the
+use's types alone.  Declaring a typeclass \texttt{incoherent} states
+that its resolution is intentionally relational---the same
+constraint may legitimately be resolvable by more than one
+instance---and permits the compiler to select an instance even when
+the choice is not forced, regardless of the global
+\texttt{-incoherent-instance-matches} flag; \texttt{coherent}
+forbids such selection, likewise regardless of the flag.  An
+unannotated typeclass follows the flag.  Like \texttt{dependencies}
+and \texttt{determines}, the words are recognized only in this
+position and remain usable as ordinary identifiers elsewhere.
+(The same annotation has long been available in the Bluespec Classic
+syntax.)  Section \ref{sec-instance-coherence} specifies the
+selection rules and exactly what the annotation changes.
+
 Example (from the Standard Prelude package):
 \index{Standard Prelude}
 \begin{verbatim}
@@ -4705,6 +4727,116 @@ \subsection{Instance declarations}
 typedef enum { Red, Blue, Green } Color deriving (Eq);
 \end{verbatim}
 
+\index{type classes!dependency coverage}
+Each instance of a typeclass with dependencies (Section
+\ref{sec-typeclass-def}) should itself honor the dependency: within
+the instance declaration, the dependent type parameters should be
+determined by the determining parameters, either directly or through
+the instance's provisos.  The compiler warns about an instance whose
+dependent parameter is not covered in this way, since the same inputs
+could then be satisfied with many different results, contradicting
+what the dependency promises.  If the class's resolution is
+intentionally not a function of its inputs, declare the typeclass
+\texttt{incoherent} (Section \ref{sec-typeclass-def}); the warning is
+suppressed for instances of \texttt{incoherent} classes.
+
+
+% ----------------------------------------------------------------
+
+\subsection{Instance selection and coherence}
+
+\label{sec-instance-coherence}
+
+\index{type classes!instance selection}
+\index{type classes!coherence}
+\index{coherent@\te{coherent} (typeclass annotation)}
+\index{incoherent@\te{incoherent} (typeclass annotation)}
+
+When an overloaded identifier is used, the compiler must select the
+instance declaration that supplies its implementation.  Instances of
+a class may overlap, that is, a use may be matched by the type
+parameters of more than one instance declaration.  The compiler
+orders overlapping instances from more specific to less specific: an
+instance is more specific than another if its parameter types are an
+instantiation of the other's.  Two instances neither of which is more
+specific than the other have no specified relative order.
+
+For a class whose parameters are related by dependencies (Section
+\ref{sec-typeclass-def}), the parameters on the left-hand side of
+\texttt{determines} are the \emph{inputs} of the dependency; instance
+selection is driven by the inputs alone.  The compiler selects the
+most specific instance whose input parameters match the use, and that
+instance's declaration then determines the remaining (dependent)
+parameters, as the dependency promises.  If the types demanded by the
+context conflict with what the selected instance determines, the
+program is rejected; the compiler does \emph{not} skip the selected
+instance and try a less specific one.  Falling through on such a
+conflict would mean that the demanded result type, rather than the
+inputs, chooses the instance, so the same expression could resolve to
+different instances in different contexts.  The property that
+selection is a function of the inputs is called \emph{coherence}.
+
+Example:
+\begin{verbatim}
+typeclass Content#(type c, type e)
+    dependencies (c determines e);
+      function e first(c container);
+endtypeclass
+
+instance Content#(List#(a), a);    // more specific
+   ...
+endinstance
+
+instance Content#(t, Bool);        // less specific (matches any t)
+   ...
+endinstance
+\end{verbatim}
+A use of \texttt{first} at a \texttt{List\#(Bit\#(8))} selects the
+first instance, so its result has type \texttt{Bit\#(8)}.  A context
+that instead demands a \texttt{Bool} result from
+\texttt{first} applied to a \texttt{List\#(Bit\#(8))} is a type error:
+the input (the container type) selects the \texttt{List} instance,
+which determines the element type, and the compiler reports the
+conflict rather than falling through to the catch-all instance.
+
+The compiler commits to an instance only when the use's input types
+are refined enough that no more specific instance could still match,
+and only when no proviso in scope could supply the constraint
+instead.  Inside a polymorphic definition, a constraint whose inputs
+mention the definition's type variables is deferred---to the
+definition's own provisos or to its callers---rather than resolved
+prematurely against a less specific instance.
+
+A typeclass may be declared \texttt{incoherent} to opt out of this
+discipline:
+\begin{verbatim}
+typeclass incoherent Pick#(type a, type b)
+    dependencies (a determines b);
+      function b pick(a x);
+endtypeclass
+\end{verbatim}
+For an \texttt{incoherent} class, an instance whose dependent
+parameters conflict with the context is skipped, and a less specific
+instance may be selected in its place; resolution may therefore be
+driven by the demanded result type as well as by the inputs, and the
+same constraint may resolve to different instances in different
+contexts.  This is appropriate for classes whose dependency is
+declared to guide type inference even though resolution is
+intentionally structural.  Declaring a typeclass \texttt{coherent}
+states the default behavior explicitly.
+
+Separately, each instance is expected to cover the class's
+dependencies within its own declaration (an uncovered instance
+behaves incoherently even in a coherent class); see the coverage
+warning described in Section \ref{sec-instance-def}.
+
+The compiler flag \texttt{-legacy-defer-instances} restores the
+resolution behavior of earlier compiler versions, in which every
+instance whose dependent parameters conflicted was skipped.  It is
+intended as a temporary migration aid for code that relied on
+output-driven selection, and it may be removed in a future release;
+such code should instead declare the affected typeclasses
+\texttt{incoherent}.
 
 % ----------------------------------------------------------------
 

doc/user_guide/user_guide.tex

@@ -2017,6 +2017,20 @@ \subsection{Miscellaneous flags }
 have not otherwise changed between versions.  The \te{-no-show-version}
 flag directs BSC to not include the compiler version.
 
+Two flags are recognized as temporary migration aids for changes to
+typeclass instance resolution; they do not appear in the compiler's
+standard help output and may be removed in a future release.
+\index{-legacy-defer-instances@\te{-legacy-defer-instances} (compiler flag)}
+\index{-legacy-inst-index@\te{-legacy-inst-index} (compiler flag)}
+The \te{-legacy-defer-instances} flag restores the older overloading
+resolution behavior, in which an instance whose dependent (determined)
+type parameters conflicted with the use was skipped in favor of a less
+specific instance, allowing resolution to be driven by the demanded
+result type.  Code that relies on this behavior should instead declare
+the affected typeclasses \te{incoherent} (see the language reference
+guides).  The \te{-legacy-inst-index} flag restores the compiler's
+older internal ordering and indexing of instance declarations.
+
 % -------------------------
 
 \subsection{Run-time system}

src/Libraries/Base2/StmtFSM.bs

@@ -129,7 +129,12 @@ data StmtT a
         | SContinue PosInfo
         | SExprS PosInfo (RStmt a)
 
-class StmtTifiable t a | t -> a where stmtify :: PosInfo -> t -> (StmtT a)
+-- Declared incoherent because the Action instance does not cover the
+-- fundep: an Action statement fits into an FSM of any result type, so
+-- the "determined" type is chosen by the use site, not the input.
+-- XXX Whether the class could instead be given a covering formulation
+-- deserves investigation.
+class incoherent StmtTifiable t a | t -> a where stmtify :: PosInfo -> t -> (StmtT a)
 
 instance StmtTifiable Action t where
     stmtify p a = SAction p a Nothing