Changes between Version 8 and Version 9 of FlexibleInstances

Timestamp:

02/28/06 16:11:16 (7 years ago)

Author:

ross@…

Comment:

re=organize, adding non-local conditions

FlexibleInstances

@@ -4 +4 @@
 == Brief Explanation ==
 
-In Haskell 98,
- * an instance head must have the form C (T u,,1,, ... u,,k,,), where T is a type constructor defined by a `data` or `newtype` declaration (see TypeSynonymInstances) and the u,,i,, are distinct type variables, and
- * each assertion in the context must have the form C' v, where v is one of the u,,i,,.
-
-
-Without restrictions on the form of instances, constraint checking is undecidable (see UndecidableInstances).
-A conservative rule (used by GHC with `-fglasgow-exts`) that ensures termination is:
- * at least one of the type arguments of the instance head must be a non-variable type, and
- * each assertion in the context must have the form C v,,1,, ... v,,n,,, where the v,,i,, are distinct type variables.
-The distinctness requirement prohibits non-terminating instances like
-{{{
-instance C b b => C (Maybe a) b
-}}}
-Note that repeated type variables are permitted in the instance head, e.g.
+Especially with MultiParamTypeClasses, we would like to write instances like
 {{{
 instance MArray (STArray s) e (ST s)
 }}}
+However without some restrictions constraint checking is undecidable.
 
-With this extension, one can write instances like
+This page lists alternative proposals for liberalizing the form of instances while retaining sufficient restrictions to guarantee termination.
+Such restrictions are necessarily conservative: there will always be programs that are clearly safe but still rejected.
+Restrictions on the form of instances also restrict the forms of datatype declarations that can use `deriving` clause (see [http://www.haskell.org/onlinereport/decls.html#sect4.5.3 Context reduction errors] in the Haskell 98 Report).
+
+Note that if FunctionalDependencies are present, additional restrictions are required.
+
+See UndecidableInstances for an alternative strategy using dynamic constraints on context reduction.
+
+If one can write instances like
 {{{
 instance C [Bool] where ...
 instance C [Char] where ...
 }}}
-and assertions like `C [a]` can be neither reduced nor rejected, so FlexibleContexts are also needed.
+then assertions like `C [a]` can be neither reduced nor rejected, so FlexibleContexts are also needed.
 
 == References ==
@@ -37 +33 @@
 [[TicketQuery(description~=FlexibleInstances)]]
 
-== Pros ==
- * Such instances often arise with MultiParamTypeClasses.
+== Local termination conditions ==
 
-== Cons ==
- * The above restrictions rule out some useful instances, e.g. derived instances like:
-   {{{
-data Sized s a = N Int (s a)
-        deriving (Show)
+The idea here is to impose restrictions on the form of each instance in isolation, such that context reduction will be guaranteed to terminate.
+
+=== Haskell 98 ===
+ * an instance head must have the form C (T u,,1,, ... u,,k,,), where T is a type constructor defined by a `data` or `newtype` declaration (see TypeSynonymInstances) and the u,,i,, are distinct type variables, and
+ * each assertion in the context must have the form C' v, where v is one of the u,,i,,.
+
+=== GHC 6.4 and earlier ===
+ * at least one of the type arguments of the instance head must be a non-variable type, and
+ * each assertion in the context must have the form C v,,1,, ... v,,n,,, where the v,,i,, are distinct type variables.
+The distinctness requirement prohibits non-terminating instances like
+{{{
+instance C b b => C (Maybe a) b
 }}}
-   remain illegal, because the inferred instance has an illegal context:
-   {{{
-instance Show (s a) => Show (Sized s a)
-}}}
-   (see [http://www.haskell.org/onlinereport/decls.html#sect4.5.3 Context reduction errors] in the Haskell 98 Report). The following examples from the GHC User's Guide are also forbidden:
-   {{{
-instance C a
-instance (C1 a, C2 a, C3 a) => C a
-}}}
-   The second of these cannot be shown to terminate without considering other instances in the program.
 
-== Relaxed termination condition ==
-An alternative rule would be that each assertion in the context must satisfy
+=== GHC 6.5 ===
+Each assertion in the context must satisfy
  * no variable has more occurrences in the assertion than in the head, and
  * the assertion has fewer constructors and variables (taken together and counting repetitions) than the head.
 (These conditions ensure that under any ground substitution, the assertion contains fewer constructors than the head.)
 
-This rule would allow instances accepted by the GHC rule and more, including
+This rule allows instances accepted by the previous rule and more, including
 {{{
 instance C a
@@ -72 +64 @@
 instance C a a => C [a] [a]
 }}}
+It also allows derived instances like
+{{{
+instance Show (s a) => Show (Sized s a)
+    deriving (Show)
+}}}
+because the derived instance (above) has the required form.
+
+== Non-local termination conditions ==
+
+No local criterion can accept a definition like
+{{{
+instance (C1 a, C2 a, C3 a) => C a
+}}}
+because termination depends on other instances in the program.
+However this is clearly safe if none of the instances for `C1`, `C2` or `C3` contain a direct or indirect constraint using `C`.
+
+The proposal is that one of the above local restrictions be used, but only on cycles of instances.
+
+This is more complex than a local criterion: the instance the compiler complains about might not be the one the programmer just added (creating a cycle), or even in the same module.