content: ;;;; File containing codes using `DataKinds' language extension
  
  %p(LANGUAGE DataKinds
              GADTs
              KindSignatures
              MultiParamTypeClasses
              RankNTypes
              TypeFamilies
              TypeOperators)
  
  ;;; Ghc <= 8.4 need `FlexibleInstances' language extension for instance
  ;;; declarations of `Has' type class.
  %p(LANGUAGE FlexibleInstances)
  
  (module Main)
  
  ;; base
  (import Data.Proxy ((Proxy ..)))
  (import Data.Kind ((Type)))
  
  ;;; XXX: Need "ExplicitNamespace" extension.
  ;; (import GHC.TypeLits ((Symbol) natVal (type +))
  (import GHC.TypeLits)
  
  ;; finkel-kernel
  (import Language.Finkel)
  
  ;;; Value-level quoted symbols
  
  (:: quoted-1 (IO ()))
  (= quoted-1
    (do (print 'foo)
        (print 'bar)))
  
  (:: quoted-2 (IO ()))
  (= quoted-2
    (do (print '[])
        (print '(, a b c))))
  
  ;;; Overview
  
  (data Na
    Ze
    (Su Na))
  
  (data (Vec (:: a Type) (:: n Na))
    (:: Nil  (Vec a 'Ze))
    (:: Cons (-> a (Vec a n) (Vec a ('Su n)))))
  
  ;;; Alternative syntax
  
  (data (:: Vec2 (-> Type Na Type))
    (:: Nil2 (Vec2 a 'Ze))
    (:: Cons2 (-> a (Vec2 a n) (Vec2 a ('Su n)))))
  
  ;;; Another alternative syntax
  
  (data (:: (Vec3 (:: a Type)) (-> Na Type))
    (:: Nil3 (Vec3 a 'Ze))
    (:: Cons3 (-> a (Vec3 a n) (Vec3 a ('Su n)))))
  
  ;;; Promoted list and tuple types
  
  ;; HList
  
  (data (:: HList (-> [Type] Type))
    (:: HNil (HList '[]))
    (:: HCons (-> a (HList as) (HList (': a as)))))
  
  (:: foo0 (HList '[]))
  (= foo0 HNil)
  
  (:: foo1 (HList '[Int]))
  (= foo1 (HCons (:: 3 Int) foo0))
  
  ;; Explicit quote is required for promoted list.
  (:: foo2 (HList '[Bool Int]))
  (= foo2 (HCons True foo1))
  
  (:: print-foo2 (IO ()))
  (= print-foo2
    (case foo2
      (HCons a (HCons b HNil))
      (putStrLn (++ "foo2: [" (show a) " " (show b) "]"))))
  
  ;; Tuple
  
  (data (:: Tuple (-> (, Type Type) Type))
    (:: Tuple (-> a b (Tuple '(, a b)))))
  
  ;;; Promoting existential data constructors
  
  (data (:: Ex Type)
    (:: MkEx (forall a (-> a Ex))))
  
  (type family (UnEx (:: ex Ex)))
  (type instance (UnEx ('MkEx ex)) ex)
  
  (:: print-ex (IO ()))
  (= print-ex
    (let ((:: ex (UnEx ('MkEx Bool)))
          (= ex True))
      (print ex)))
  
  ;;; Type-Level literals
  
  (data (Label (:: l Symbol)) Get)
  
  (class (Has a l)
    (type (Res a l))
    (:: from (-> a (Label l) (Res a l))))
  
  (data Point
    (Point Int Int)
    (deriving (Show)))
  
  (instance (Has Point "x")
    (type (Res Point "x") Int)
    (= from (Point x _) _ x))
  
  (instance (Has Point "y")
    (type (Res Point "y") Int)
    (= from (Point _ y) _ y))
  
  (:: tylit-syms (IO ()))
  (= tylit-syms
    (do (let ((= p (Point 12 34))))
        (print (from p (:: Get (Label "x"))))
        (print (from p (:: Get (Label "y"))))))
  
  (:: tylit-nats-simple (IO ()))
  (= tylit-nats-simple
    (do (print (natVal (:: Proxy (Proxy 1))))
        (print (natVal (:: Proxy (Proxy 2))))))
  
  (:: tylit-nats-with-op (IO ()))
  (= tylit-nats-with-op
    (do (print (natVal (:: Proxy (Proxy (+ 1 2)))))
        (print (natVal (:: Proxy (Proxy (+ 3 4)))))))
  
  
  ;;; Using same names in type constructor and data constructor
  
  (data Bar Bar)
  
  (type family (:: (Buzz (:: a Bool)) Bar)
    (= (Buzz 'True) 'Bar))
  
  
  ;;; The main function
  
  (:: main (IO ()))
  (= main
    (do (putStrLn ";;; datakinds ;;;")
        quoted-1
        quoted-2
        print-foo2
        print-ex
        tylit-syms
        tylit-nats-simple))
  