wiki:FlexibleInstances

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

--

Flexible Instances

Brief Explanation

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.

References

Tickets

#32
add FlexibleInstances

Pros

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]