{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

{- |
The module provides 'Borrows', which is a heterogeneous list of 'Borrow's in the same lifetime.
-}
module Control.Monad.Borrow.Pure.Experimental.Borrows (
  Borrows (..),
) where

import Control.Functor.Linear qualified as Control
import Control.Monad.Borrow.Pure.Affine
import Control.Monad.Borrow.Pure.Affine.Unsafe (unsafeAff)
import Control.Monad.Borrow.Pure.BO
import Control.Monad.Borrow.Pure.Experimental.Reborrowable
import Data.Coerce.Directed.Unsafe
import Data.Kind
import Prelude.Linear hiding (foldMap)
import Unsafe.Linear qualified as Unsafe

type Borrows :: BorrowKind -> Lifetime -> [Type] -> Type
data Borrows bk α xs where
  BNil :: Borrows bk α '[]
  (:-) :: !(Borrow bk α x) %1 -> !(Borrows bk α xs) %1 -> Borrows bk α (x ': xs)

infixr 5 :-

instance Affine (Borrows bk α xs) where
  aff :: Borrows bk α xs %1 -> Aff (Borrows bk α xs)
aff = Borrows bk α xs %1 -> Aff (Borrows bk α xs)
forall a. a %1 -> Aff a
unsafeAff

deriving via AsAffine (Borrows bk α xs) instance Consumable (Borrows bk α xs)

instance (β <= α) => Borrows bk α xs <: Borrows bk' β xs where
  subtype :: SubtypeWitness (Borrows bk α xs) (Borrows bk' β xs)
subtype = SubtypeWitness (Borrows bk α xs) (Borrows bk' β xs)
forall {k} {k1} (a :: k) (b :: k1). SubtypeWitness a b
UnsafeSubtype

instance Reborrowable (Borrows bk) where
  locally' :: forall (α :: Lifetime) (a :: [*]) (α' :: Lifetime) r.
Borrows bk α a
%1 -> (forall (β :: Lifetime).
       Borrows bk (β /\ α) a %1 -> BO (β /\ α') (After β r))
%1 -> BO α' (r, Borrows bk α a)
locally' = (Borrows bk α a
 -> (forall (β :: Lifetime).
     Borrows bk (β /\ α) a %1 -> BO (β /\ α') (After β r))
 %1 -> BO α' (r, Borrows bk α a))
%1 -> Borrows bk α a
%1 -> (forall (β :: Lifetime).
       Borrows bk (β /\ α) a %1 -> BO (β /\ α') (After β r))
%1 -> BO α' (r, Borrows bk α a)
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear \Borrows bk α a
bors forall (β :: Lifetime).
Borrows bk (β /\ α) a %1 -> BO (β /\ α') (After β r)
k -> Control.do
    (,Borrows bk α a
bors) (r %1 -> (r, Borrows bk α a))
%1 -> BO α' r %1 -> BO α' (r, Borrows bk α a)
forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
Control.<$> (forall (α :: Lifetime). BO (α /\ α') (After α r)) %1 -> BO α' r
forall (β :: Lifetime) a.
(forall (α :: Lifetime). BO (α /\ β) (After α a)) %1 -> BO β a
srunBO (Borrows bk (α /\ α) a %1 -> BO (α /\ α') (After α r)
forall (β :: Lifetime).
Borrows bk (β /\ α) a %1 -> BO (β /\ α') (After β r)
k (Borrows bk (α /\ α) a %1 -> BO (α /\ α') (After α r))
%1 -> Borrows bk (α /\ α) a %1 -> BO (α /\ α') (After α r)
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ Borrows bk α a %1 -> Borrows bk (α /\ α) a
forall a b. (a <: b) => a %1 -> b
upcast Borrows bk α a
bors)
  {-# INLINE locally' #-}