content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE ExistentialQuantification #-}
  {-# OPTIONS_GHC -fno-warn-orphans #-}
  
  module Ivory.Language.Area where
  
  import Ivory.Language.Proxy
  import Ivory.Language.Type
  import qualified Ivory.Language.Syntax as I
  
  import GHC.TypeLits (Nat, Symbol)
  
  -- Memory Areas ----------------------------------------------------------------
  
  -- | Type proxies for @Area@s.
  type AProxy a = Proxy (a :: Area *)
  
  -- | The kind of memory-area types.
  data Area k
    = Struct Symbol
    | Array Nat (Area k)
    | CArray (Area k)
    | Stored k
      -- ^ This is lifting for a *-kinded type
  
  -- | Guard the inhabitants of the Area type, as not all *s are Ivory *s.
  class IvoryArea (a :: Area *) where
    ivoryArea :: Proxy a -> I.Type
  
  instance (ANat len, IvoryArea area)
        => IvoryArea ('Array len area) where
    ivoryArea _ = I.TyArr len area
      where
      len  = fromInteger (fromTypeNat (aNat :: NatType len))
      area = ivoryArea (Proxy :: Proxy area)
  
  instance IvoryType a => IvoryArea ('Stored a) where
    ivoryArea _ = ivoryType (Proxy :: Proxy a)
  
  