Who needs first class modules when you can set records...

Adam.idr

record Bumpable type where
  constructor B
  bump : type -> type


myIntBumper : Bumpable Int
myIntBumper
  = B (+ 1)


myNatBumper : Bumpable Nat
myNatBumper
  = B (+ 1)


doubleBump : Bumpable a
          -> a
          -> a
doubleBump (B bump) y
  = bump (bump y)


test : Equal
         (doubleBump Adam.myNatBumper (the Nat 1))
         (the Nat 3)
test = Refl