foo.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE TypeApplications   #-}
module ApplyLast where

data Nat = Z | S Nat

data NumArgs :: Nat -> * -> * where
  NAZ :: NumArgs Z a
  NAS :: NumArgs n b -> NumArgs (S n) (a -> b)

type family CountArgs (f :: *) :: Nat where
  CountArgs (a -> b) = S (CountArgs b)
  CountArgs result = Z

class CNumArgs (numArgs :: Nat) (arrows :: *) where
  getNA :: NumArgs numArgs arrows
instance CNumArgs Z a where
  getNA = NAZ
instance CNumArgs n b => CNumArgs (S n) (a -> b) where
  getNA = NAS getNA

type family Apply (f :: * -> *) (n :: Nat) (arrows :: *) :: * where
  Apply f (S n) (a -> b) = a -> Apply f n b
  Apply f Z a = f a

applyLast :: forall f fun .
             (Applicative f, CNumArgs (CountArgs fun) fun)
          => fun -> Apply f (CountArgs fun) fun
applyLast = applyLast' @f (getNA :: NumArgs (CountArgs fun) fun)

applyLast' :: forall f n fun .
              Applicative f
           => NumArgs n fun -> fun -> Apply f n fun
applyLast' NAZ x = pure x
applyLast' (NAS n) f = \a -> applyLast' @f n (f a)

-- well

data T = T Int Bool

f' :: Int -> Bool -> Maybe T
f' = applyLast T

f'' = applyLast @Maybe T