Default superclass instances in Idris.

DefaultSuperclass.idr

module DefaultSuperclass

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' = ap' . pure'
  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)

inc : Int -> Int
inc a = a + 1

x : Identity' Int
x = map' inc (Id' 2)