content: module TypeAbstractions where
  
  import Data.Kind
  import Data.Proxy
  import Data.Proxy.Singletons
  import Data.Singletons.Base.TH
  import Data.Singletons.TH.Options
  import Prelude.Singletons
  
  $(withOptions defaultOptions{genSingKindInsts = False} $
    singletons [d|
    type D1 :: forall j k. j -> k -> Type
    data D1 @j @k (a :: j) (b :: k) = MkD1 (Proxy a) (Proxy b)
  
    type D2 :: forall j k. j -> k -> Type
    data D2 @x @y (a :: x) (b :: y) = MkD2 (Proxy a) (Proxy b)
  
    type D3 :: forall j. j -> forall k. k -> Type
    data D3 @j (a :: j) @k (b :: k) = MkD3 (Proxy a) (Proxy b)
  
    type D4 :: forall (a :: Type). Type
    data D4 @a = MkD4 a
  
    type C1 :: forall j k. j -> k -> Constraint
    class C1 @j @k (a :: j) (b :: k) where
      meth1 :: Proxy a -> Proxy b
  
    type C2 :: forall j k. j -> k -> Constraint
    class C2 @x @y (a :: x) (b :: y) where
      meth2 :: Proxy a -> Proxy b
  
    type C3 :: forall j. j -> forall k. k -> Constraint
    class C3 @j (a :: j) @k (b :: k) where
      meth3 :: Proxy a -> Proxy b
  
    type C4 :: forall (a :: Type). Constraint
    class C4 @a where
      meth4 :: a
  
    type TF :: forall j. j -> forall k. k -> Type
    type family TF @j (a :: j) @k (b :: k) where
      TF @j _ @k _ = (j, k)
  
    type TS :: forall j. j -> forall k. k -> Type
    type TS @j (a :: j) @k (b :: k) = (j, k)
    |])
  