raise Data.Function to the type levels

src/Data/Function.hs

@@ -14,26 +14,36 @@
 -- | Defines commonly used functions and combinators
 module Data.Function where
 
--- | Identity Function
+import Data.Singletons.TH
-id ∷ ∀ (a ∷ ★). a → a
+
+singletons [d|
+
+  -- | Identity function
+  id ∷ ∀ a. a → a
   id x = x
 
   -- | Constant function
-const ∷ ∀ (a ∷ ★) (b ∷ ★). a → b → a
+  const ∷ ∀ a b. a → b → a
   const k _ = k
 
+  -- | Flip the arguments of a function
+  flip ∷ ∀ a b c. (a → b → c) → (b → a → c)
+  flip f x y = f y x
+
   -- | Undefined
   (⊥) ∷ ∀ a. a
   (⊥) = (⊥)
 
-infixr 0 $
   infixr 9 ∘
 
--- | Function application operator
-($) ∷ ∀ a b. (a → b) → a → b
-f $ x = f x
-
   -- | Function composition operator
   (∘) :: ∀ a b c. (b → c) → (a → b) → a → c
   f ∘ g = \x → f (g x)
 
+  |]
+
+infixr 0 $
+
+-- | Function application operator
+($) ∷ ∀ a b. (a → b) → a → b
+f $ x = f x