{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilyDependencies #-}
-- {-# LANGUAGE FunctionalDependencies #-}
-- {-# LANGUAGE AllowAmbiguousTypes #-}
-- {-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GHC2024 #-}
-- {-# LANGUAGE AllowAmbiguousTypes #-}
import Data.Kind (Type)
import Data.Tuple
import Language.Haskell.TH qualified as TH

-- | N-ary product without a type function comparing to its homonym in the "sop" package.
data NP :: (k -> Type) -> [k] -> Type where
  Nil  :: NP f '[]
  (:*) :: f x %1 -> NP f xs %1 -> NP f (x : xs)

infixr 5 :*

newtype I (a :: Type) = I a deriving (Functor, Foldable, Traversable)

type family TupleNtoNP m tpl = r | r -> m tpl where
  TupleNtoNP m () = NP m '[] -- This is not possible
  TupleNtoNP m (m x) = NP m '[x]
  TupleNtoNP m (m x1, m x2) = NP m '[x1, x2]
  TupleNtoNP m (m x1, m x2, m x3) = NP m '[x1, x2, x3]

class HavingFromTupleNPtoNP m tpl where
  fromTupleNtoNP :: tpl %p -> TupleNtoNP m tpl

instance HavingFromTupleNPtoNP m () where
  fromTupleNtoNP () = Nil

instance HavingFromTupleNPtoNP m (m a) where
  fromTupleNtoNP (a) = a :* Nil
  
instance HavingFromTupleNPtoNP m (m a1, m a2) where
  fromTupleNtoNP (a1, a2) = a1 :* a2 :* Nil
  
-- t :: IO [TH.Dec]
-- t = [d|
--   type family TupleNtoNP m tpl = r | r -> m tpl where
--     TupleNtoNP m () = NP m '[] -- This is not possible
--     TupleNtoNP m (m x) = NP m '[x]
--     TupleNtoNP m (m x1, m x2) = NP m '[x1, x2]

--   class HavingFromTupleNPtoNP m tpl where
--     fromTupleNtoNP :: tpl %p -> TupleNtoNP m tpl

--   instance HavingFromTupleNPtoNP m () where
--     fromTupleNtoNP () = Nil

--   instance HavingFromTupleNPtoNP m () where
--     fromTupleNtoNP (MkSolo a) = a :* Nil
--   |]

main :: IO ()
main = do
  -- t >>= mapM (putStrLn . (<> "\n") . show)
  pure ()