Someone asked whether you can model SystemF(omega) in Haskell. I think you can.

SysF.hs

{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeInType             #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# OPTIONS_GHC -Wall #-}

{-# LANGUAGE TypeApplications #-}

import           Data.Kind  (Type)
import           Data.Proxy (Proxy (..))
import           GHC.Exts   (Any)

-------------------------------------------------------------------------------
-- Elem
-------------------------------------------------------------------------------

data Elem (x :: k) (xs :: [k]) where
    Here  :: Elem x (x ': xs)
    There :: Elem x xs -> Elem x (y ':  xs)

data SElem (x :: k) (xs :: [k]) (e :: Elem x xs) where
    SHere  :: SElem x (x ': xs) 'Here
    SThere :: SElem x xs e -> SElem x (y ': xs) ('There e)

weakenElem
    :: SList ctx1
    -> Proxy ctx2
    -> Proxy ki
    -> Elem a (Append ctx1 ctx2)
    -> Elem a (Append ctx1 (ki : ctx2))
weakenElem SNil         _    _  i         = There i
weakenElem (SCons _)    _    _  Here      = Here
weakenElem (SCons ctx1) ctx2 ki (There i) = There (weakenElem ctx1 ctx2 ki i)

-------------------------------------------------------------------------------
-- Sigma
-------------------------------------------------------------------------------

data Sigma (f :: k -> Type) (g :: k -> Type) where
    Exists  :: f k -> g k -> Sigma f g

-------------------------------------------------------------------------------
-- List
-------------------------------------------------------------------------------

type family Append (xs :: [k]) (ys :: [k]) :: [k] where
    Append '[]       ys = ys
    Append (x ': xs) ys = x ': Append xs ys

data SList :: [k] -> Type where
    SNil   :: SList '[]
    SCons  :: SList xs -> SList (x ': xs)

-------------------------------------------------------------------------------
-- Kinds
-------------------------------------------------------------------------------

-- kinds
data Ki
    = KiStar
    | KiArrow Ki Ki

-- kind singletons
data SKi :: Ki -> Type where
    SKiStar  :: SKi 'KiStar
    SKiArrow :: SKi a -> SKi b -> SKi ('KiArrow a b)

-- kind singleton singletons
data SSKi (ki :: Ki) (ski :: SKi ki) :: Type where
    SSKiStar  :: SSKi 'KiStar 'SKiStar
    SSKiArrow :: SSKi a sa
              -> SSKi b sb
              -> SSKi ('KiArrow a b) ('SKiArrow sa sb)

-------------------------------------------------------------------------------
-- Types
-------------------------------------------------------------------------------

type KiCtx = [Ki]

-- | Types are in a normal form, even we have TyLam.
data Ty (kictx :: KiCtx) (ki :: Ki) :: Type where
    TyNeutral :: TyNeutral kictx ki -> Ty kictx ki
    TyLam     :: Ty (ka ': kictx) kb -> Ty kictx ('KiArrow ka kb)
    TyArr     :: Ty kictx 'KiStar -> Ty kictx 'KiStar -> Ty kictx 'KiStar

data TyNeutral (kictx :: KiCtx) (ki :: Ki) :: Type where
    TyVar :: Elem ki kictx -> TyNeutral kictx ki
    TyApp :: TyNeutral kictx ('KiArrow ka kb)
          -> Ty kictx ka
          -> TyNeutral kictx kb

-- example
ex1 :: Sigma SKi (Ty '[ 'KiStar  ])
ex1 = Exists SKiStar (TyNeutral (TyVar Here))

-------------------------------------------------------------------------------
-- Types singleton
-------------------------------------------------------------------------------

data STy (kictx :: KiCtx) (ki :: Ki) (ty :: Ty kictx ki) :: Type where
    STyNeutral :: STyNeutral kictx ki x
               -> STy kictx ki ('TyNeutral x)

    STyLam :: STy (ka ': kictx) kb x
           -> STy kictx ('KiArrow ka kb) ('TyLam x)

    STyArr :: STy kictx 'KiStar a
           -> STy kictx 'KiStar b
           -> STy kictx 'KiStar ('TyArr a b)

data STyNeutral (kictx :: KiCtx) (ki :: Ki) (ty :: TyNeutral kictx ki) :: Type  where
    STyVar :: SElem ki kictx x
           -> STyNeutral kictx ki ('TyVar x)

    STyApp :: STyNeutral kictx ('KiArrow ka kb) f
           -> STy kictx ka x
           -> STyNeutral kictx kb ('TyApp f x)

-------------------------------------------------------------------------------
-- Weakening
-------------------------------------------------------------------------------

weakenKindN :: SList ctx1
            -> Proxy ctx2
            -> Proxy ki
            -> TyNeutral (Append ctx1 ctx2) a
            -> TyNeutral (Append ctx1 (ki ': ctx2)) a
weakenKindN ctx1 ctx2 ki (TyVar e)   = TyVar (weakenElem ctx1 ctx2 ki e)
weakenKindN ctx1 ctx2 ki (TyApp f x) = TyApp (weakenKindN ctx1 ctx2 ki f) (weakenKind ctx1 ctx2 ki x)

weakenKind :: SList ctx1
           -> Proxy ctx2
           -> Proxy ki
           -> Ty (Append ctx1 ctx2) a
           -> Ty (Append ctx1 (ki ': ctx2)) a
weakenKind ctx1 ctx2 ki (TyNeutral n) = TyNeutral (weakenKindN ctx1 ctx2 ki n)
weakenKind ctx1 ctx2 ki (TyLam ty)    = TyLam (weakenKind (SCons ctx1) ctx2 ki ty)
weakenKind ctx1 ctx2 ki (TyArr a b)   = TyArr (weakenKind ctx1 ctx2 ki a) (weakenKind ctx1 ctx2 ki b)

-------------------------------------------------------------------------------
-- Type applications
-------------------------------------------------------------------------------

tySubstV :: SList ctx1
         -> Ty ctx2 a
         -> Elem b (Append ctx1 (a ': ctx2))
         -> Ty (Append ctx1 ctx2) b
tySubstV SNil      s Here      = s
tySubstV SNil      _ (There i) = TyNeutral (TyVar i)
tySubstV (SCons _) _ Here      = TyNeutral (TyVar Here)
tySubstV (SCons c) s (There i) = weakenKind SNil Proxy Proxy $ tySubstV c s i

tySubstN :: SList ctx1
         -> Ty ctx2 a
         -> TyNeutral (Append ctx1 (a ': ctx2)) b
         -> Ty (Append ctx1 ctx2) b
tySubstN p s (TyVar v)   = tySubstV p s v
tySubstN p s (TyApp f x) = tyApp (tySubstN p s f) (tySubst p s x)

tySubst :: SList ctx1
        -> Ty ctx2 a
        -> Ty (Append ctx1 (a ': ctx2)) b
        -> Ty (Append ctx1 ctx2) b
tySubst p s (TyNeutral n) = tySubstN p s n
tySubst p s (TyLam body)  = TyLam $ tySubst (SCons p) s body
tySubst p s (TyArr a b)   = TyArr (tySubst p s a) (tySubst p s b)

-- we'll need a version of this (and tySubst) on type level,
-- i.e. working with singleton of Ty. "fun".
tyApp :: Ty kictx ('KiArrow ka kb) -> Ty kictx ka -> Ty kictx kb
tyApp (TyNeutral f) x = TyNeutral (TyApp f x)
tyApp (TyLam body)  x = tySubst SNil x body

-------------------------------------------------------------------------------
-- tyApp family: TyAppF
-------------------------------------------------------------------------------

type family TyAppF (a :: Ty ictx ('KiArrow ka kb)) (b :: Ty kictx ka) :: Ty kictx kb where
    TyAppF ('TyNeutral f) x = 'TyNeutral ('TyApp f x)
    TyAppF ('TyLam body)  x = Any -- TODO

{- TODO: following doesn't work

8.6.5

    • Illegal type synonym family application in instance: 'TyArr aa bb
    • In the equations for closed type family ‘TySubstF’
      In the type family declaration for ‘TySubstF’

8.8.1

    • Illegal type synonym family application ‘Append
                                                 @Ki ctx1 ((':) @Ki a ctx2)’ in instance:
        TySubstF
          @ctx2
          @a
          @'KiStar
          ctx1
          s
          ('TyArr @(Append @Ki ctx1 ((':) @Ki a ctx2)) aa bb)
    • In the equations for closed type family ‘TySubstF’
      In the type family declaration for ‘TySubstF’

-}
type family TySubstF (ctx1 :: [Ki]) (s :: Ty ctx2 a) (x :: Ty (Append ctx1 (a ': ctx2)) b) :: Ty (Append ctx1 ctx2) b where
    TySubstF ctx1 s ('TyArr aa bb) = 'TyArr (TySubstF ctx1 s aa) (TySubstF ctx1 s bb)

-------------------------------------------------------------------------------
-- Terms / Expressions
-------------------------------------------------------------------------------

type TyCtx (kictx :: KiCtx) = [Sigma SKi (Ty kictx)]

data Expr (kictx :: KiCtx) (tyctx :: TyCtx kictx) (ki :: Ki) (ty :: Ty kictx ki) :: Type where
    Var :: SSKi ki ski -> Elem ('Exists ski ty) tyctx -> Expr kictx tyctx ki ty