Curry / uncurry in generics-sop

CurryNP4.hs

{-# LANGUAGE DataKinds, PolyKinds, MultiParamTypeClasses, TypeFamilies, TypeOperators #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances, ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UndecidableSuperClasses, TypeApplications  #-}
{-# LANGUAGE ConstraintKinds #-}
module CurryNP4 where

import Data.Kind
import Generics.SOP
import GHC.Exts

curryNP :: forall xs a f r . (C a f xs r) => a -> (NP f xs -> r)
curryNP k =
  case sList :: SList xs of
    SNil  -> \ Nil -> k
    SCons -> \ (x :* xs) -> curryNP (k x) xs

uncurryNP :: forall xs a f r . C a f xs r => (NP f xs -> r) -> a
uncurryNP k =
  case sList :: SList xs of
    SNil  -> k Nil
    SCons -> \ x -> uncurryNP (\ xs -> k (x :* xs))

curryNPI :: forall xs a r . CI a xs r => a -> (NP I xs -> r)
curryNPI k =
  case sList :: SList xs of
    SNil  -> \ Nil -> k
    SCons -> \ (I x :* xs) -> curryNPI (k x) xs

uncurryNPI :: forall xs a r . CI a xs r => (NP I xs -> r) -> a
uncurryNPI k =
  case sList :: SList xs of
    SNil  -> k Nil
    SCons -> \ x -> uncurryNPI (\ xs -> k (I x :* xs))

type C a f xs r = (Curry a f xs r, Uncurry a f xs r, SListI xs)
type CI a xs r = (CurryI a xs r, UncurryI a xs r, SListI xs)

type family Uncurry (a :: Type) (f :: k -> Type) (xs :: [k]) (r :: Type) :: Constraint where
  Uncurry a f '[]      r = (r ~ a)
  Uncurry a f (x : xs) r = (a ~ (Arg a -> Res a), Arg a ~ f x, Uncurry (Res a) f xs r)

type family Curry (a :: Type) (f :: k -> Type) (xs :: [k]) (r :: Type) :: Constraint where
  Curry (g x -> a) f xs r = (f ~ g, xs ~ (Head xs : Tail xs), Head xs ~ x, Curry a f (Tail xs) r)
  Curry a          f xs r = (r ~ a, xs ~ '[])

type family UncurryI (a :: Type) (xs :: [k]) (r :: Type) :: Constraint where
  UncurryI a '[]      r = (r ~ a)
  UncurryI a (x : xs) r = (a ~ (Arg a -> Res a), Arg a ~ x, UncurryI (Res a) xs r)

type family CurryI (a :: Type) (xs :: [k]) (r :: Type) :: Constraint where
  CurryI (x -> a) xs r = (xs ~ (Head xs : Tail xs), Head xs ~ x, CurryI a (Tail xs) r)
  CurryI a        xs r = (r ~ a, xs ~ '[])

type family Arg (x :: Type) :: Type where
  Arg (a -> r) = a

type family Res (x :: Type) :: Type where
  Res (a -> r) = r

type family Head (xs :: [k]) :: k where
  Head (x : xs) = x

type family Tail (xs :: [k]) :: [k] where
  Tail (x : xs) = xs

test3 :: String
test3 = uncurryNP showNP (I True) (I 5) (I 'x')
test3I :: String
test3I = uncurryNPI showNP True 'x' 5

test3' = uncurryNP showNP'
test3I' = uncurryNPI showNP'

showNP :: All Show xs => NP I xs -> String
showNP = concat . hcollapse . hcmap (Proxy @Show) (mapIK show)

showNP' :: NP I '[Int, Char, Bool] -> String
showNP' = showNP

test4 = curryNP (\ (I x) (I y) (I z) -> (x + y + z :: Int))
test4I = curryNPI (\ x y z -> x + y + z :: Int)