content: {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE TypeAbstractions #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE DataKinds, NoListTuplePuns #-}
  
  module T23501a where
  
  import Prelude.Experimental (List, Unit)
  import Data.Kind (Type, Constraint)
  
  ----------------------------
  --   Class declarations   --
  ----------------------------
  
  class C1 (_ :: k) _   -- no SAKS
    where f1 :: k -> Unit
  
  f1' :: C1 @k a b => k -> Unit
  f1' @_ @a @b = f1 @_ @a @b
  
  type C2 :: k1 -> k2 -> Constraint
  class C2 (_ :: k) _ where
    f2 :: k -> Unit
  
  f2' :: C2 @k1 @k2 a b => k1 -> Unit
  f2' @_ @_ @a @b = f2 @_ @_ @a @b
  
  type C3 :: k1 -> k2 -> Constraint
  class C3 @k @_ _ _ where
    f3 :: k -> Unit
  
  f3' :: C3 @k1 @k2 a b => k1 -> Unit
  f3' @_ @_ @a @b = f3 @_ @_ @a @b
  
  ---------------------------
  --   Data declarations   --
  ---------------------------
  
  data D1 k (_ :: k) _  -- no SAKS
    where MkD1 :: k -> D1 k a b
  
  mkD1 :: k -> D1 k a b
  mkD1 = MkD1
  
  type D2 :: forall (k1 :: Type) -> k1 -> k2 -> Type
  data D2 k (_ :: k) _ where
    MkD2 :: k -> D2 k a b
  
  mkD2 :: k -> D2 k a b
  mkD2 = MkD2
  
  type D3 :: k1 -> k2 -> Type
  data D3 @k @_ _ _ = MkD3 k
  
  data MProxy (_ :: Type) = MPrx
  data CProxy (_ :: k -> Constraint) = CPrx
  
  type Rec :: (k -> Type) -> List k -> Type
  data Rec _ _ where
    RNil :: Rec f []
    (:&) :: f x -> Rec f xs -> Rec f (x:xs)
  
  ------------------
  --   Newtypes   --
  ------------------
  
  newtype N1 k (_ :: k) _   -- no SAKS
    = MkN1 k
  
  mkN1 :: k -> N1 k a b
  mkN1 = MkN1
  
  type N2 :: forall (k1 :: Type) -> k1 -> k2 -> Type
  newtype N2 k (_ :: k) _ = MkN2 k
  
  mkN2 :: k -> N2 k a b
  mkN2 = MkN2
  
  ----------------------------
  --   Open type families   --
  ----------------------------
  
  type family OTF1 (_ :: Type -> Type) _    -- no SAKS
  
  type instance OTF1 f x = f x
  
  otf1 :: OTF1 Maybe Int -> Int
  otf1 Nothing = 0
  otf1 (Just x) = x
  
  type OTF2 :: (Type -> Type) -> Type -> Type
  type family OTF2 (_ :: Type -> Type) _
  
  type instance OTF2 f x = f x
  
  otf2 :: OTF2 Maybe Int -> Int
  otf2 Nothing = 0
  otf2 (Just x) = x
  
  ------------------------------
  --   Closed type families   --
  ------------------------------
  
  type family CTF1 (_ :: Type -> Type) _  -- no SAKS
    where CTF1 f x = f x
  
  ctf1 :: CTF1 Maybe Int -> Int
  ctf1 Nothing = 0
  ctf1 (Just x) = x
  
  type CTF2 :: (Type -> Type) -> Type -> Type
  type family CTF2 (_ :: Type -> Type) _ where
    CTF2 f x = f x
  
  ctf2 :: CTF2 Maybe Int -> Int
  ctf2 Nothing = 0
  ctf2 (Just x) = x
  
  type CTF3 :: k1 -> k2 -> Type
  type family CTF3 @_ @k _ _
    where CTF3 @_ @k _ _ = k
  
  ctf3 :: CTF3 a True -> Bool
  ctf3 = id
  
  -----------------------
  --   Type synonyms   --
  -----------------------
  
  type T1 (_ :: Type -> Type) _ = ()   -- no SAKS
  
  type T2 :: (Type -> Type) -> k -> Type
  type T2 (_ :: Type -> Type) _ = Unit
  
  type T3 :: k1 -> k2 -> Type
  type T3 @_ @k _ _ = k
  
  type FConst _ = ()
  