6 | | In Haskell 98, |
7 | | * 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 |
8 | | * each assertion in the context must have the form C' v, where v is one of the u,,i,,. |
9 | | |
10 | | |
11 | | Without restrictions on the form of instances, constraint checking is undecidable (see UndecidableInstances). |
12 | | A conservative rule (used by GHC with `-fglasgow-exts`) that ensures termination is: |
13 | | * at least one of the type arguments of the instance head must be a non-variable type, and |
14 | | * each assertion in the context must have the form C v,,1,, ... v,,n,,, where the v,,i,, are distinct type variables. |
15 | | The distinctness requirement prohibits non-terminating instances like |
16 | | {{{ |
17 | | instance C b b => C (Maybe a) b |
18 | | }}} |
19 | | Note that repeated type variables are permitted in the instance head, e.g. |
| 6 | Especially with MultiParamTypeClasses, we would like to write instances like |
24 | | With this extension, one can write instances like |
| 12 | This page lists alternative proposals for liberalizing the form of instances while retaining sufficient restrictions to guarantee termination. |
| 13 | Such restrictions are necessarily conservative: there will always be programs that are clearly safe but still rejected. |
| 14 | 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). |
| 15 | |
| 16 | Note that if FunctionalDependencies are present, additional restrictions are required. |
| 17 | |
| 18 | See UndecidableInstances for an alternative strategy using dynamic constraints on context reduction. |
| 19 | |
| 20 | If one can write instances like |
42 | | == Cons == |
43 | | * The above restrictions rule out some useful instances, e.g. derived instances like: |
44 | | {{{ |
45 | | data Sized s a = N Int (s a) |
46 | | deriving (Show) |
| 37 | The idea here is to impose restrictions on the form of each instance in isolation, such that context reduction will be guaranteed to terminate. |
| 38 | |
| 39 | === Haskell 98 === |
| 40 | * 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 |
| 41 | * each assertion in the context must have the form C' v, where v is one of the u,,i,,. |
| 42 | |
| 43 | === GHC 6.4 and earlier === |
| 44 | * at least one of the type arguments of the instance head must be a non-variable type, and |
| 45 | * each assertion in the context must have the form C v,,1,, ... v,,n,,, where the v,,i,, are distinct type variables. |
| 46 | The distinctness requirement prohibits non-terminating instances like |
| 47 | {{{ |
| 48 | instance C b b => C (Maybe a) b |
| 66 | It also allows derived instances like |
| 67 | {{{ |
| 68 | instance Show (s a) => Show (Sized s a) |
| 69 | deriving (Show) |
| 70 | }}} |
| 71 | because the derived instance (above) has the required form. |
| 72 | |
| 73 | == Non-local termination conditions == |
| 74 | |
| 75 | No local criterion can accept a definition like |
| 76 | {{{ |
| 77 | instance (C1 a, C2 a, C3 a) => C a |
| 78 | }}} |
| 79 | because termination depends on other instances in the program. |
| 80 | However this is clearly safe if none of the instances for `C1`, `C2` or `C3` contain a direct or indirect constraint using `C`. |
| 81 | |
| 82 | The proposal is that one of the above local restrictions be used, but only on cycles of instances. |
| 83 | |
| 84 | 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. |