inject.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits

data NPlus = One | Suc NPlus

class Applicable (n :: NPlus) a f | f n -> a where
  type ApplyAt n a f :: *
  inject :: a -> f -> ApplyAt n a f

instance Applicable One a (a -> b) where
  type ApplyAt One a (a -> b) = b
  inject a f = f a

instance (Applicable n a c) => Applicable (Suc n) a (b -> c) where
  type ApplyAt (Suc n) a (b -> c) = b -> ApplyAt n a c
  inject a f = \x -> inject @n a (f x)

type family ToNPlus (n :: Nat) :: NPlus where
  ToNPlus 0 = TypeError (Text "0 is not a positive integer")
  ToNPlus 1 = One
  ToNPlus n = Suc (ToNPlus (n - 1))

main = do
  putStrLn $ (inject @(ToNPlus 1) "a" (\a b c -> "a: " <> a <> "\nb: " <> b <> "\nc: " <> c <> "\n")) "b" "c"
  putStrLn $ (inject @(ToNPlus 2) "a" (\a b c -> "a: " <> a <> "\nb: " <> b <> "\nc: " <> c <> "\n")) "b" "c"
  putStrLn $ (inject @(ToNPlus 3) "a" (\a b c -> "a: " <> a <> "\nb: " <> b <> "\nc: " <> c <> "\n")) "b" "c"