Version 8 (modified by ross@…, 10 years ago) (diff) |
---|

# Flexible Instances

## 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.

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.

## References

- 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.

## Tickets

- #32
- add FlexibleInstances

## Pros

- Such instances often arise with MultiParamTypeClasses.

## Cons

- 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 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

- 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

instance C a instance Show (s a) => Show (Sized s a) instance (C1 a, C2 b) => C a b instance C1 Int a => C2 Bool [a] instance C1 Int a => C2 [a] b instance C a a => C [a] [a]