|Version 4 (modified by ross@…, 11 years ago) (diff)|
In Haskell 98,
- an instance head must have the form C (T u1 … uk), where T is a type constructor defined by a data or newtype declaration (see TypeSynonymInstances) and the ui are distinct type variables, and
- each assertion in the context must have the form C' v, where v is one of the ui.
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 v1 … vn, where the vi 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.
instance MArray (STArray s) e (ST s)
With this extension, 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.
- Instance declarations in the Haskell 98 Report
- Type classes: exploring the design space by Simon Peyton Jones, Mark Jones and Erik Meijer, Haskell Workshop 1997.
- Instance declarations in the GHC's User's Guide.
- Such instances often arise with MultiParamTypeClasses.
- The above restrictions rule out some useful instances, e.g. derived instances like:
data Sized s a = N Int (s a) deriving (Show)remain illegal, because the inferred instance has an illegal context:
instance Show (s a) => Show (Sized s a)(see 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 aThe 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
- the variables of the assertion are a sub-multiset of those of the head (though they may be the same), 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 all instances accepted by the GHC rule, plus the Sized example, any instance without a context, and others.