{-# LANGUAGE DataKinds, TypeFamilies, AllowAmbiguousTypes, UndecidableInstances #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# OPTIONS -dsuppress-all #-}

module Main where

import Data.Kind
import Data.Typeable

main :: IO ()
main = do
  print (check @[Bool, Int])
  -- print (check @[Float, Bool, Int])

-- just check that invariant holds

check :: forall xs. Extendss Proxy xs => ()
check = ()

-- vulkan code itself, see optimisations

data SomeStruct (a :: [Type] -> Type) where
  SomeStruct
    :: forall a es
     . (Extendss a es)
    => a es
    -> SomeStruct a

extendSomeStruct
  :: (Extensible a, Extends a e)
  => e
  -> SomeStruct a
  -> SomeStruct a
extendSomeStruct e (SomeStruct a) = SomeStruct (setNext a (e, getNext a))

class Extensible (a :: [Type] -> Type) where
  extensibleTypeName :: String
  -- ^ For error reporting an invalid extension
  getNext :: a es -> Chain es
  setNext :: a ds -> Chain es -> a es
  extends :: forall e b proxy. Typeable e => proxy e -> (Extends a e => b) -> Maybe b

type family Chain (xs :: [Type]) = (r :: Type) | r -> xs where
  Chain '[]    = ()
  Chain (x:xs) = (x, Chain xs)

-- New

type ReportUnsolved :: () -> Constraint -> Constraint
type family ReportUnsolved a b where
  ReportUnsolved '() x = x

type Extendss :: ([Type] -> Type) -> [Type] -> Constraint 
type family Extendss p xs where
  Extendss p '[] = ()
  Extendss p (x : xs) = (ExtendsWith p x `ReportUnsolved` Extendss p xs)
  
type Extends p x = ExtendsWith p x ~ '()

type ExtendsWith :: ([Type] -> Type) -> Type -> ()
type family ExtendsWith p x where
  ExtendsWith Proxy Bool = '()
  ExtendsWith Proxy Int = '()

-- Old

-- type Extendss :: ([Type] -> Type) -> [Type] -> Constraint 
-- type family Extendss p xs where
--   Extendss p '[] = ()
--   Extendss p (x : xs) = (Extends p x, Extendss p xs)
  

-- type Extends :: ([Type] -> Type) -> Type -> Constraint
-- type family Extends p x where
--   Extends Proxy Bool = ()
--   Extends Proxy Int = ()