idris-lang/Idris-dev — pull request #720 by puffnfresh (2013-12-11 03:49:24+00:00)
Title: Default superclass intances

This allows code like:

data Identity i = Id i

class Functor (f : Type -> Type) where
map : (a -> b) -> f a -> f b

class Functor f => Applicative (f : Type -> Type) where
instance Functor f where
map f fa = ap (pure f) fa
pure : a -> f a
ap : f (a -> b) -> f a -> f b

instance Applicative Identity where
pure = Id
ap (Id f) (Id a) = Id (f a)

data Nat = Z
| S Nat

x : Identity Nat
x = map S (Id Z)

Note the default Functor instance defined as part of the Applicative
class. This allows the Identity data type to omit an explicit Functor
instance and one gets defined from the Applicative instance.

This feature is largely copied from the approach done in She:

https://personal.cis.strath.ac.uk/conor.mcbride/pub/she/superclass.html

It basically does macro expansion of each default superclass instance
(e.g. Functor) when the containing class (e.g. Applicative) gets an
instance defined. Currently, default superclass instance definitions
are not type-checked, only their macro expansions are.

Default superclass instances are limited to being defined for types
which are syntactically equal to one of the superclass constraints.