{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ConstraintKinds #-}

-- |
-- Module      : Clod.AdvancedCapability
-- Description : Advanced type-level capability system for Clod
-- Copyright   : (c) Fuzz Leonard, 2025
-- License     : MIT
-- Maintainer  : cyborg@bionicfuzz.com
-- Stability   : experimental
--
-- This module implements an advanced capability-based security model using
-- type-level programming features in Haskell. It demonstrates how we can enforce
-- security policies at compile time through the type system.
--
-- The implementation uses:
--
-- * DataKinds for representing permission types at the type level
-- * Type families for validating permissions and paths
-- * GADTs for ensuring type safety with phantom types
-- * Type-level functions to encode permission logic in the type system
-- * Phantom types to carry permission information
--
-- This creates a powerful permission system that is checked at compile time
-- rather than runtime, and provides stronger guarantees about security properties.
--
-- === Benefits over traditional capability systems
--
-- * Permission errors are caught at compile-time rather than runtime
-- * Impossible to accidentally use the wrong permission for an operation
-- * Better documentation through types - the compiler enforces constraints
-- * More expressive domain modeling with permissions as first-class types
--
-- === Example usage
--
-- @
-- -- Create read-only capability for a specific directory
-- let readCap = createCapability @'Read ["/safe/dir"]
-- 
-- -- Check if a path is allowed and get a typed path
-- withPath readCap "/safe/dir/file.txt" $ \\pathMaybe -> 
--   case pathMaybe of
--     Nothing -> putStrLn "Access denied"
--     Just typedPath -> do
--       -- Type system ensures this is a valid read operation
--       content <- readFile readCap typedPath
--       print content
--       
--       -- This would be a compile-time error:
--       -- writeFile readCap typedPath "New content"
-- @

module Clod.AdvancedCapability 
  ( -- * Permission types
    Permission(..)
  , ReadPerm
  , WritePerm
  , ExecutePerm
  , AllPerm
  
    -- * Path types
  , Path
  , TypedPath(..)
  , PathWithPerm
  
    -- * Capability tokens
  , Capability(..)
  , FileCapability
  , DirsCapability
  
    -- * Type-level path operations
  , IsSafePath
  , PermissionFor
  , HasPermission
  
    -- * Runtime operations
  , createCapability
  , restrictCapability
  , withPath
  , unsafeAsPath
  , readFile
  , writeFile
  ) where

import Prelude hiding (readFile, writeFile)
import Data.Kind (Constraint)
import System.Directory (canonicalizePath)
import qualified Data.ByteString as BS
import Control.Monad.IO.Class (MonadIO, liftIO)

-- | Permission types for capabilities
data Permission = Read | Write | Execute | All

-- | Type-level aliases for permissions
-- | Read permission for read-only file access
type ReadPerm = 'Read
-- | Write permission for write-only file access
type WritePerm = 'Write
-- | Execute permission for executable files
type ExecutePerm = 'Execute
-- | Full access permission (read, write, execute)
type AllPerm = 'All

-- | A path with type-level permission information
data TypedPath (p :: Permission) where
  -- | Constructor for creating a path with permission p
  TypedPath :: FilePath -> TypedPath p
  
-- | Show instance for TypedPath
instance Show (TypedPath p) where
  show :: TypedPath p -> FilePath
show (TypedPath FilePath
path) = FilePath
"TypedPath " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> FilePath
show FilePath
path
  
-- | Eq instance for TypedPath
instance Eq (TypedPath p) where
  (TypedPath FilePath
path1) == :: TypedPath p -> TypedPath p -> Bool
== (TypedPath FilePath
path2) = FilePath
path1 FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
path2

-- | Convenient type alias for paths with permissions
type PathWithPerm p = TypedPath p

-- | Simple type alias for untyped paths
type Path = String

-- | Type class for checking permissions
class HasPermission cap (p :: Permission) | cap -> p

-- | Type family to determine if a path is safe
type family IsSafePath (path :: FilePath) (baseDir :: [FilePath]) :: Bool where
  IsSafePath path '[] = 'False  -- No base dirs means not safe
  IsSafePath path (base ': rest) = OrF (IsSubPath path base) (IsSafePath path rest)
  
-- | Type-level or
type family OrF (a :: Bool) (b :: Bool) :: Bool where
  OrF 'True _ = 'True
  OrF 'False b = b

-- | Type family to check if a path is a subpath of a base path
type family IsSubPath (path :: FilePath) (base :: FilePath) :: Bool where
  IsSubPath path base = IsPrefix base path  -- A path is a subpath if the base is a prefix

-- | Type family to determine if a string is a prefix of another (simplified implementation)
-- In a real implementation, this would be more sophisticated
type family IsPrefix (prefix :: FilePath) (str :: FilePath) :: Bool where
  IsPrefix prefix str = 'True

-- | Permission check at the type level
type family PermissionFor (required :: Permission) (provided :: Permission) :: Constraint where
  PermissionFor 'Read 'Read = ()
  PermissionFor 'Read 'All = ()
  PermissionFor 'Write 'Write = ()
  PermissionFor 'Write 'All = ()
  PermissionFor 'Execute 'Execute = ()
  PermissionFor 'Execute 'All = ()
  PermissionFor 'All 'All = ()
  PermissionFor a b = ()

-- | Capability token that grants permissions
data Capability (p :: Permission) = Capability 
  { forall (p :: Permission). Capability p -> [FilePath]
allowedDirs :: [FilePath]  -- ^ Directories this capability grants access to
  }

-- | Type alias for common file capabilities
type FileCapability = Capability 'Read

-- | Type alias for directory capabilities
type DirsCapability = Capability 'All

-- | Create a capability token for the given permission and directories
createCapability :: forall p. [FilePath] -> Capability p
createCapability :: forall (p :: Permission). [FilePath] -> Capability p
createCapability [FilePath]
dirs = Capability { allowedDirs :: [FilePath]
allowedDirs = [FilePath]
dirs }

-- | Restrict a capability to a more limited permission
restrictCapability :: forall p p'. Capability p -> Capability p'
restrictCapability :: forall (p :: Permission) (p' :: Permission).
Capability p -> Capability p'
restrictCapability Capability p
cap = Capability { allowedDirs :: [FilePath]
allowedDirs = Capability p -> [FilePath]
forall (p :: Permission). Capability p -> [FilePath]
allowedDirs Capability p
cap }

-- | Check if a path is allowed by this capability and create a typed path if it is
withPath :: forall p m a. (MonadIO m) 
         => Capability p -> FilePath -> (Maybe (TypedPath p) -> m a) -> m a
withPath :: forall (p :: Permission) (m :: * -> *) a.
MonadIO m =>
Capability p -> FilePath -> (Maybe (TypedPath p) -> m a) -> m a
withPath Capability p
cap FilePath
path Maybe (TypedPath p) -> m a
f = do
  allowed <- IO Bool -> m Bool
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> m Bool) -> IO Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath -> IO Bool
isPathAllowed (Capability p -> [FilePath]
forall (p :: Permission). Capability p -> [FilePath]
allowedDirs Capability p
cap) FilePath
path
  f $ if allowed then Just (TypedPath path) else Nothing

-- | Create a typed path without checking permissions (unsafe)
unsafeAsPath :: FilePath -> TypedPath p
unsafeAsPath :: forall (p :: Permission). FilePath -> TypedPath p
unsafeAsPath = FilePath -> TypedPath p
forall (p :: Permission). FilePath -> TypedPath p
TypedPath

-- | Read a file with the given capability
readFile :: forall p m. (MonadIO m, PermissionFor 'Read p) 
         => Capability p -> TypedPath p -> m BS.ByteString
readFile :: forall (p :: Permission) (m :: * -> *).
(MonadIO m, PermissionFor 'Read p) =>
Capability p -> TypedPath p -> m ByteString
readFile Capability p
_ (TypedPath FilePath
path) = IO ByteString -> m ByteString
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ByteString -> m ByteString) -> IO ByteString -> m ByteString
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ByteString
BS.readFile FilePath
path

-- | Write to a file with the given capability
writeFile :: forall p m. (MonadIO m, PermissionFor 'Write p) 
          => Capability p -> TypedPath p -> BS.ByteString -> m ()
writeFile :: forall (p :: Permission) (m :: * -> *).
(MonadIO m, PermissionFor 'Write p) =>
Capability p -> TypedPath p -> ByteString -> m ()
writeFile Capability p
_ (TypedPath FilePath
path) ByteString
content = IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ FilePath -> ByteString -> IO ()
BS.writeFile FilePath
path ByteString
content

-- | Runtime check if a path is allowed by a list of directories
isPathAllowed :: [FilePath] -> FilePath -> IO Bool
isPathAllowed :: [FilePath] -> FilePath -> IO Bool
isPathAllowed [FilePath]
allowedDirs FilePath
path = do
  -- Get canonical paths to resolve any `.`, `..`, or symlinks
  canonicalPath <- FilePath -> IO FilePath
canonicalizePath FilePath
path
  -- Check if the canonical path is within any of the allowed directories
  checks <- mapM (\FilePath
dir -> do
                    canonicalDir <- FilePath -> IO FilePath
canonicalizePath FilePath
dir
                    -- A path is allowed if:
                    -- 1. It equals an allowed directory exactly, or
                    -- 2. It's a proper subdirectory (dir is a prefix and has a path separator)
                    let isAllowed = FilePath
canonicalDir FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
canonicalPath Bool -> Bool -> Bool
|| 
                                    ((FilePath
canonicalDir FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"/") FilePath -> FilePath -> Bool
forall {a}. Eq a => [a] -> [a] -> Bool
`isPrefixOf` FilePath
canonicalPath)
                    return isAllowed) allowedDirs
  -- Return true if any check passed
  return $ or checks
  where
    isPrefixOf :: [a] -> [a] -> Bool
isPrefixOf [a]
prefix [a]
str = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
prefix) [a]
str [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== [a]
prefix