{-# LANGUAGE ViewPatterns #-}

-- |
-- Module: Covenant.Data
-- Copyright: (C) MLabs 2025
-- License: Apache 2.0
-- Maintainer: koz@mlabs.city, sean@mlabs.city
--
-- Information about datatype definitions, and various ways to interact with
-- them. Most of the useful functionality is in 'DatatypeInfo' and its optics.
--
-- = Note
--
-- Some of the low-level functions in the module make use of @ScopeBoundary@.
-- This is mostly an artifact of needing this for tests; if you ever need their
-- functionality, assume that the only sensible value is @0@, which will work
-- via its overloaded number syntax.
--
-- @since 1.1.0
module Covenant.Data
  ( -- * Types
    BBFError (..),
    DatatypeInfo (..),

    -- * Functions

    -- ** Datatype-related
    mkDatatypeInfo,
    allComponentTypes,
    mkBBF,
    noPhantomTyVars,

    -- ** Lower-level
    mkBaseFunctor,
    isRecursiveChildOf,
    hasRecursive,
    everythingOf,
  )
where

import Control.Monad.Except (MonadError (throwError))
import Control.Monad.Reader (MonadReader (ask, local), MonadTrans (lift), Reader, runReader)
import Control.Monad.Trans.Except (ExceptT, runExceptT)
import Covenant.DeBruijn (DeBruijn (S, Z), asInt)
import Covenant.Index (Count, Index, count0, intCount, intIndex)
import Covenant.Internal.PrettyPrint (ScopeBoundary (ScopeBoundary))
import Covenant.Internal.Type
  ( AbstractTy (BoundAt),
    CompT (CompT),
    CompTBody (CompTBody),
    Constructor (Constructor),
    ConstructorName (ConstructorName),
    DataDeclaration (DataDeclaration, OpaqueData),
    TyName (TyName),
    ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),
  )
import Data.Bitraversable (bisequence)
import Data.Kind (Type)
import Data.Maybe (fromJust)
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Vector qualified as V
import Data.Vector.NonEmpty qualified as NEV
import Optics.Core (A_Lens, LabelOptic (labelOptic), folded, lens, preview, review, toListOf, view, (%), _2)
import Optics.Indexed.Core (A_Fold)

-- | All possible errors that could arise when constructing a Boehm-Berrarducci
-- form.
--
-- @since 1.1.0
data BBFError
  = -- | The type is recursive in a prohibited way. Typically, this means
    -- contravariant recursion. This gives the type name and the invalid
    -- recursive constructor argument.
    --
    -- @since 1.1.0
    InvalidRecursion TyName (ValT AbstractTy)
  deriving stock
    ( -- | @since 1.1.0
      Int -> BBFError -> ShowS
[BBFError] -> ShowS
BBFError -> String
(Int -> BBFError -> ShowS)
-> (BBFError -> String) -> ([BBFError] -> ShowS) -> Show BBFError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BBFError -> ShowS
showsPrec :: Int -> BBFError -> ShowS
$cshow :: BBFError -> String
show :: BBFError -> String
$cshowList :: [BBFError] -> ShowS
showList :: [BBFError] -> ShowS
Show,
      -- | @since 1.1.0
      BBFError -> BBFError -> Bool
(BBFError -> BBFError -> Bool)
-> (BBFError -> BBFError -> Bool) -> Eq BBFError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BBFError -> BBFError -> Bool
== :: BBFError -> BBFError -> Bool
$c/= :: BBFError -> BBFError -> Bool
/= :: BBFError -> BBFError -> Bool
Eq
    )

-- | Contains essential information about datatype definitions. Most of the
-- time, you want to use this type via its optics, rather than directly.
--
-- In pretty much any case imaginable, the @var@ type variable will be one of
-- 'AbstractTy' or 'Renamed'.
--
-- @since 1.1.0
data DatatypeInfo (var :: Type)
  = DatatypeInfo
  { forall var. DatatypeInfo var -> DataDeclaration var
_originalDecl :: DataDeclaration var,
    forall var.
DatatypeInfo var -> Maybe (DataDeclaration var, ValT var)
_baseFunctorStuff :: Maybe (DataDeclaration var, ValT var),
    -- NOTE: The ONLY type that won't have a BB form is `Void` (or something isomorphic to it)
    forall var. DatatypeInfo var -> Maybe (ValT var)
_bbForm :: Maybe (ValT var)
  }
  deriving stock
    ( -- | @since 1.1.0
      DatatypeInfo var -> DatatypeInfo var -> Bool
(DatatypeInfo var -> DatatypeInfo var -> Bool)
-> (DatatypeInfo var -> DatatypeInfo var -> Bool)
-> Eq (DatatypeInfo var)
forall var. Eq var => DatatypeInfo var -> DatatypeInfo var -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall var. Eq var => DatatypeInfo var -> DatatypeInfo var -> Bool
== :: DatatypeInfo var -> DatatypeInfo var -> Bool
$c/= :: forall var. Eq var => DatatypeInfo var -> DatatypeInfo var -> Bool
/= :: DatatypeInfo var -> DatatypeInfo var -> Bool
Eq,
      -- | @since 1.1.0
      Int -> DatatypeInfo var -> ShowS
[DatatypeInfo var] -> ShowS
DatatypeInfo var -> String
(Int -> DatatypeInfo var -> ShowS)
-> (DatatypeInfo var -> String)
-> ([DatatypeInfo var] -> ShowS)
-> Show (DatatypeInfo var)
forall var. Show var => Int -> DatatypeInfo var -> ShowS
forall var. Show var => [DatatypeInfo var] -> ShowS
forall var. Show var => DatatypeInfo var -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall var. Show var => Int -> DatatypeInfo var -> ShowS
showsPrec :: Int -> DatatypeInfo var -> ShowS
$cshow :: forall var. Show var => DatatypeInfo var -> String
show :: DatatypeInfo var -> String
$cshowList :: forall var. Show var => [DatatypeInfo var] -> ShowS
showList :: [DatatypeInfo var] -> ShowS
Show
    )

-- | The original declaration of the data type.
--
-- @since 1.1.0
instance
  (k ~ A_Lens, a ~ DataDeclaration var, b ~ DataDeclaration var) =>
  LabelOptic "originalDecl" k (DatatypeInfo var) (DatatypeInfo var) a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx (DatatypeInfo var) (DatatypeInfo var) a b
labelOptic =
    (DatatypeInfo var -> a)
-> (DatatypeInfo var -> b -> DatatypeInfo var)
-> Lens (DatatypeInfo var) (DatatypeInfo var) a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(DatatypeInfo DataDeclaration var
ogDecl Maybe (DataDeclaration var, ValT var)
_ Maybe (ValT var)
_) -> a
DataDeclaration var
ogDecl)
      (\(DatatypeInfo DataDeclaration var
_ Maybe (DataDeclaration var, ValT var)
b Maybe (ValT var)
c) b
ogDecl -> DataDeclaration var
-> Maybe (DataDeclaration var, ValT var)
-> Maybe (ValT var)
-> DatatypeInfo var
forall var.
DataDeclaration var
-> Maybe (DataDeclaration var, ValT var)
-> Maybe (ValT var)
-> DatatypeInfo var
DatatypeInfo b
DataDeclaration var
ogDecl Maybe (DataDeclaration var, ValT var)
b Maybe (ValT var)
c)

-- | The base functor for this data type, if it exists. Types which are not
-- self-recursive lack base functors.
--
-- @since 1.1.0
instance
  (k ~ A_Lens, a ~ Maybe (DataDeclaration var, ValT var), b ~ Maybe (DataDeclaration var, ValT var)) =>
  LabelOptic "baseFunctor" k (DatatypeInfo var) (DatatypeInfo var) a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx (DatatypeInfo var) (DatatypeInfo var) a b
labelOptic =
    (DatatypeInfo var -> a)
-> (DatatypeInfo var -> b -> DatatypeInfo var)
-> Lens (DatatypeInfo var) (DatatypeInfo var) a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(DatatypeInfo DataDeclaration var
_ Maybe (DataDeclaration var, ValT var)
baseF Maybe (ValT var)
_) -> a
Maybe (DataDeclaration var, ValT var)
baseF)
      (\(DatatypeInfo DataDeclaration var
a Maybe (DataDeclaration var, ValT var)
_ Maybe (ValT var)
c) b
baseF -> DataDeclaration var
-> Maybe (DataDeclaration var, ValT var)
-> Maybe (ValT var)
-> DatatypeInfo var
forall var.
DataDeclaration var
-> Maybe (DataDeclaration var, ValT var)
-> Maybe (ValT var)
-> DatatypeInfo var
DatatypeInfo DataDeclaration var
a b
Maybe (DataDeclaration var, ValT var)
baseF Maybe (ValT var)
c)

-- | The Boehm-Berrarducci form of this type, if it exists. Types with no
-- constructors (that is, types without inhabitants) lack Boehm-Berrarducci
-- forms.
--
-- @since 1.1.0
instance
  (k ~ A_Lens, a ~ Maybe (ValT var), b ~ Maybe (ValT var)) =>
  LabelOptic "bbForm" k (DatatypeInfo var) (DatatypeInfo var) a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx (DatatypeInfo var) (DatatypeInfo var) a b
labelOptic =
    (DatatypeInfo var -> a)
-> (DatatypeInfo var -> b -> DatatypeInfo var)
-> Lens (DatatypeInfo var) (DatatypeInfo var) a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(DatatypeInfo DataDeclaration var
_ Maybe (DataDeclaration var, ValT var)
_ Maybe (ValT var)
bb) -> a
Maybe (ValT var)
bb)
      (\(DatatypeInfo DataDeclaration var
a Maybe (DataDeclaration var, ValT var)
b Maybe (ValT var)
_) b
bb -> DataDeclaration var
-> Maybe (DataDeclaration var, ValT var)
-> Maybe (ValT var)
-> DatatypeInfo var
forall var.
DataDeclaration var
-> Maybe (DataDeclaration var, ValT var)
-> Maybe (ValT var)
-> DatatypeInfo var
DatatypeInfo DataDeclaration var
a Maybe (DataDeclaration var, ValT var)
b b
Maybe (ValT var)
bb)

-- | The base functor Boehm-Berrarducci form of this type, if it exists. A type
-- must have both a base functor and a Boehm-Berrarducci form to have a base
-- functor Boehm-Berrarducci form. In other words, they must have at least one
-- constructor and be self-recursive.
--
-- @since 1.1.0
instance
  (k ~ A_Fold, a ~ ValT var, b ~ ValT var) =>
  LabelOptic "bbBaseF" k (DatatypeInfo var) (DatatypeInfo var) a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx (DatatypeInfo var) (DatatypeInfo var) a b
labelOptic = Optic
  A_Lens
  NoIx
  (DatatypeInfo var)
  (DatatypeInfo var)
  (Maybe (DataDeclaration var, ValT var))
  (Maybe (DataDeclaration var, ValT var))
#baseFunctor Optic
  A_Lens
  NoIx
  (DatatypeInfo var)
  (DatatypeInfo var)
  (Maybe (DataDeclaration var, ValT var))
  (Maybe (DataDeclaration var, ValT var))
-> Optic
     A_Fold
     NoIx
     (Maybe (DataDeclaration var, ValT var))
     (Maybe (DataDeclaration var, ValT var))
     (DataDeclaration var, ValT var)
     (DataDeclaration var, ValT var)
-> Optic
     A_Fold
     NoIx
     (DatatypeInfo var)
     (DatatypeInfo var)
     (DataDeclaration var, ValT var)
     (DataDeclaration var, ValT var)
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Fold
  NoIx
  (Maybe (DataDeclaration var, ValT var))
  (Maybe (DataDeclaration var, ValT var))
  (DataDeclaration var, ValT var)
  (DataDeclaration var, ValT var)
forall (f :: Type -> Type) a. Foldable f => Fold (f a) a
folded Optic
  A_Fold
  NoIx
  (DatatypeInfo var)
  (DatatypeInfo var)
  (DataDeclaration var, ValT var)
  (DataDeclaration var, ValT var)
-> Optic
     A_Lens
     NoIx
     (DataDeclaration var, ValT var)
     (DataDeclaration var, ValT var)
     a
     b
-> Optic k NoIx (DatatypeInfo var) (DatatypeInfo var) a b
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  (DataDeclaration var, ValT var)
  (DataDeclaration var, ValT var)
  a
  b
forall s t a b. Field2 s t a b => Lens s t a b
_2

-- | Given a declaration of a datatype, either produce its datatype info, or
-- fail.
--
-- @since 1.1.0
mkDatatypeInfo :: DataDeclaration AbstractTy -> Either BBFError (DatatypeInfo AbstractTy)
mkDatatypeInfo :: DataDeclaration AbstractTy
-> Either BBFError (DatatypeInfo AbstractTy)
mkDatatypeInfo DataDeclaration AbstractTy
decl = DataDeclaration AbstractTy
-> Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
-> Maybe (ValT AbstractTy)
-> DatatypeInfo AbstractTy
forall var.
DataDeclaration var
-> Maybe (DataDeclaration var, ValT var)
-> Maybe (ValT var)
-> DatatypeInfo var
DatatypeInfo DataDeclaration AbstractTy
decl (Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
 -> Maybe (ValT AbstractTy) -> DatatypeInfo AbstractTy)
-> Either
     BBFError (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> Either
     BBFError (Maybe (ValT AbstractTy) -> DatatypeInfo AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Either
  BBFError (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
baseFStuff Either
  BBFError (Maybe (ValT AbstractTy) -> DatatypeInfo AbstractTy)
-> Either BBFError (Maybe (ValT AbstractTy))
-> Either BBFError (DatatypeInfo AbstractTy)
forall a b.
Either BBFError (a -> b) -> Either BBFError a -> Either BBFError b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> DataDeclaration AbstractTy
-> Either BBFError (Maybe (ValT AbstractTy))
mkBBF DataDeclaration AbstractTy
decl
  where
    baseFStuff :: Either BBFError (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
    baseFStuff :: Either
  BBFError (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
baseFStuff =
      let baseFDecl :: Maybe (DataDeclaration AbstractTy)
baseFDecl = Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy))
-> ScopeBoundary -> Maybe (DataDeclaration AbstractTy)
forall r a. Reader r a -> r -> a
runReader (DataDeclaration AbstractTy
-> Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy))
mkBaseFunctor DataDeclaration AbstractTy
decl) ScopeBoundary
0
          baseBBF :: Either BBFError (Maybe (ValT AbstractTy))
baseBBF = case Maybe (DataDeclaration AbstractTy)
baseFDecl of
            Maybe (DataDeclaration AbstractTy)
Nothing -> Maybe (ValT AbstractTy)
-> Either BBFError (Maybe (ValT AbstractTy))
forall a b. b -> Either a b
Right Maybe (ValT AbstractTy)
forall a. Maybe a
Nothing
            Just DataDeclaration AbstractTy
d -> DataDeclaration AbstractTy
-> Either BBFError (Maybe (ValT AbstractTy))
mkBBF DataDeclaration AbstractTy
d
       in ((Maybe (DataDeclaration AbstractTy), Maybe (ValT AbstractTy))
-> Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
forall (t :: Type -> Type -> Type) (f :: Type -> Type) a b.
(Bitraversable t, Applicative f) =>
t (f a) (f b) -> f (t a b)
bisequence ((Maybe (DataDeclaration AbstractTy), Maybe (ValT AbstractTy))
 -> Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> (Maybe (ValT AbstractTy)
    -> (Maybe (DataDeclaration AbstractTy), Maybe (ValT AbstractTy)))
-> Maybe (ValT AbstractTy)
-> Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe (DataDeclaration AbstractTy)
baseFDecl,) (Maybe (ValT AbstractTy)
 -> Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> Either BBFError (Maybe (ValT AbstractTy))
-> Either
     BBFError (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Either BBFError (Maybe (ValT AbstractTy))
baseBBF)

-- | Returns all datatype constructors used as any argument to the datatype
-- defined by the first argument.
--
-- @since 1.1.0
allComponentTypes :: DataDeclaration AbstractTy -> [ValT AbstractTy]
allComponentTypes :: DataDeclaration AbstractTy -> [ValT AbstractTy]
allComponentTypes = Optic' A_Fold NoIx (DataDeclaration AbstractTy) (ValT AbstractTy)
-> DataDeclaration AbstractTy -> [ValT AbstractTy]
forall k (is :: IxList) s a.
Is k A_Fold =>
Optic' k is s a -> s -> [a]
toListOf (Optic
  A_Fold
  NoIx
  (DataDeclaration AbstractTy)
  (DataDeclaration AbstractTy)
  (Vector (Constructor AbstractTy))
  (Vector (Constructor AbstractTy))
#datatypeConstructors Optic
  A_Fold
  NoIx
  (DataDeclaration AbstractTy)
  (DataDeclaration AbstractTy)
  (Vector (Constructor AbstractTy))
  (Vector (Constructor AbstractTy))
-> Optic
     A_Fold
     NoIx
     (Vector (Constructor AbstractTy))
     (Vector (Constructor AbstractTy))
     (Constructor AbstractTy)
     (Constructor AbstractTy)
-> Optic
     A_Fold
     NoIx
     (DataDeclaration AbstractTy)
     (DataDeclaration AbstractTy)
     (Constructor AbstractTy)
     (Constructor AbstractTy)
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Fold
  NoIx
  (Vector (Constructor AbstractTy))
  (Vector (Constructor AbstractTy))
  (Constructor AbstractTy)
  (Constructor AbstractTy)
forall (f :: Type -> Type) a. Foldable f => Fold (f a) a
folded Optic
  A_Fold
  NoIx
  (DataDeclaration AbstractTy)
  (DataDeclaration AbstractTy)
  (Constructor AbstractTy)
  (Constructor AbstractTy)
-> Optic'
     A_Lens NoIx (Constructor AbstractTy) (Vector (ValT AbstractTy))
-> Optic
     A_Fold
     NoIx
     (DataDeclaration AbstractTy)
     (DataDeclaration AbstractTy)
     (Vector (ValT AbstractTy))
     (Vector (ValT AbstractTy))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic'
  A_Lens NoIx (Constructor AbstractTy) (Vector (ValT AbstractTy))
#constructorArgs Optic
  A_Fold
  NoIx
  (DataDeclaration AbstractTy)
  (DataDeclaration AbstractTy)
  (Vector (ValT AbstractTy))
  (Vector (ValT AbstractTy))
-> Optic
     A_Fold
     NoIx
     (Vector (ValT AbstractTy))
     (Vector (ValT AbstractTy))
     (ValT AbstractTy)
     (ValT AbstractTy)
-> Optic'
     A_Fold NoIx (DataDeclaration AbstractTy) (ValT AbstractTy)
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Fold
  NoIx
  (Vector (ValT AbstractTy))
  (Vector (ValT AbstractTy))
  (ValT AbstractTy)
  (ValT AbstractTy)
forall (f :: Type -> Type) a. Foldable f => Fold (f a) a
folded)

-- | Constructs a base functor from a suitable data declaration, returning
-- 'Nothing' if the input is not a recursive type.
--
-- @since 1.1.0
mkBaseFunctor :: DataDeclaration AbstractTy -> Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy))
mkBaseFunctor :: DataDeclaration AbstractTy
-> Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy))
mkBaseFunctor OpaqueData {} = Maybe (DataDeclaration AbstractTy)
-> Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy))
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (DataDeclaration AbstractTy)
forall a. Maybe a
Nothing
mkBaseFunctor (DataDeclaration TyName
tn Count "tyvar"
numVars Vector (Constructor AbstractTy)
ctors DataEncoding
strat) = do
  Bool
anyRecComponents <- [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
or ([Bool] -> Bool)
-> ReaderT ScopeBoundary Identity [Bool]
-> ReaderT ScopeBoundary Identity Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool)
-> [ValT AbstractTy] -> ReaderT ScopeBoundary Identity [Bool]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (TyName -> ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool
hasRecursive TyName
tn) [ValT AbstractTy]
allCtorArgs
  if Vector (Constructor AbstractTy) -> Bool
forall a. Vector a -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null Vector (Constructor AbstractTy)
ctors Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
anyRecComponents
    then Maybe (DataDeclaration AbstractTy)
-> Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy))
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (DataDeclaration AbstractTy)
forall a. Maybe a
Nothing
    else do
      Vector (Constructor AbstractTy)
baseCtors <- (Constructor AbstractTy
 -> ReaderT ScopeBoundary Identity (Constructor AbstractTy))
-> Vector (Constructor AbstractTy)
-> ReaderT ScopeBoundary Identity (Vector (Constructor AbstractTy))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse Constructor AbstractTy
-> ReaderT ScopeBoundary Identity (Constructor AbstractTy)
mkBaseCtor Vector (Constructor AbstractTy)
ctors
      Maybe (DataDeclaration AbstractTy)
-> Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy))
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe (DataDeclaration AbstractTy)
 -> Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy)))
-> (DataDeclaration AbstractTy
    -> Maybe (DataDeclaration AbstractTy))
-> DataDeclaration AbstractTy
-> Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDeclaration AbstractTy -> Maybe (DataDeclaration AbstractTy)
forall a. a -> Maybe a
Just (DataDeclaration AbstractTy
 -> Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy)))
-> DataDeclaration AbstractTy
-> Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy))
forall a b. (a -> b) -> a -> b
$ TyName
-> Count "tyvar"
-> Vector (Constructor AbstractTy)
-> DataEncoding
-> DataDeclaration AbstractTy
forall a.
TyName
-> Count "tyvar"
-> Vector (Constructor a)
-> DataEncoding
-> DataDeclaration a
DataDeclaration TyName
baseFName Count "tyvar"
baseFNumVars Vector (Constructor AbstractTy)
baseCtors DataEncoding
strat
  where
    baseFName :: TyName
    baseFName :: TyName
baseFName = case TyName
tn of
      TyName Text
tyNameInner -> Text -> TyName
TyName (Text
tyNameInner Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_F")
    baseFNumVars :: Count "tyvar"
    baseFNumVars :: Count "tyvar"
baseFNumVars = Maybe (Count "tyvar") -> Count "tyvar"
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Count "tyvar") -> Count "tyvar")
-> (Int -> Maybe (Count "tyvar")) -> Int -> Count "tyvar"
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int (Count "tyvar")
-> Int -> Maybe (Count "tyvar")
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount (Int -> Count "tyvar") -> Int -> Count "tyvar"
forall a b. (a -> b) -> a -> b
$ Optic' A_Prism NoIx Int (Count "tyvar") -> Count "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount Count "tyvar"
numVars Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    -- The argument position of the new type variable parameter (typically `r`).
    -- A count represents the number of variables, but indices for those variables start at 0,
    -- so an additional tyvar will always have an index == the old count
    rIndex :: Index "tyvar"
    rIndex :: Index "tyvar"
rIndex = Maybe (Index "tyvar") -> Index "tyvar"
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Index "tyvar") -> Index "tyvar")
-> (Int -> Maybe (Index "tyvar")) -> Int -> Index "tyvar"
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int (Index "tyvar")
-> Int -> Maybe (Index "tyvar")
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex (Int -> Index "tyvar") -> Int -> Index "tyvar"
forall a b. (a -> b) -> a -> b
$ Optic' A_Prism NoIx Int (Count "tyvar") -> Count "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount Count "tyvar"
numVars
    -- Replace recursive children with a DeBruijn index & position index that points at the top-level binding context
    -- (technically the top level binding context is the ONLY admissable binding context if we forbid higher-rank types,
    -- but we still have to regard a computation type that binds 0 variables as having a scope boundary)
    replaceWithR :: ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)
    replaceWithR :: ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)
replaceWithR ValT AbstractTy
vt =
      ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool
isRecursive ValT AbstractTy
vt ReaderT ScopeBoundary Identity Bool
-> (Bool -> Reader ScopeBoundary (ValT AbstractTy))
-> Reader ScopeBoundary (ValT AbstractTy)
forall a b.
ReaderT ScopeBoundary Identity a
-> (a -> ReaderT ScopeBoundary Identity b)
-> ReaderT ScopeBoundary Identity b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Bool
True -> do
          ScopeBoundary Int
here <- ReaderT ScopeBoundary Identity ScopeBoundary
forall r (m :: Type -> Type). MonadReader r m => m r
ask -- this should be the distance from the initial binding context (which is what we want)
          let db :: DeBruijn
db = Maybe DeBruijn -> DeBruijn
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe DeBruijn -> DeBruijn) -> Maybe DeBruijn -> DeBruijn
forall a b. (a -> b) -> a -> b
$ Optic' A_Prism NoIx Int DeBruijn -> Int -> Maybe DeBruijn
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int DeBruijn
asInt Int
here
          ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy))
-> ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ AbstractTy -> ValT AbstractTy
forall a. a -> ValT a
Abstraction (DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
db Index "tyvar"
rIndex)
        Bool
False -> ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT AbstractTy
vt
    -- TODO: This should be refactored with `mapMValT`, which I will do after I write it :P
    replaceAllRecursive :: ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)
    replaceAllRecursive :: ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)
replaceAllRecursive = \case
      abst :: ValT AbstractTy
abst@Abstraction {} -> ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT AbstractTy
abst
      bif :: ValT AbstractTy
bif@BuiltinFlat {} -> ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT AbstractTy
bif
      ThunkT (CompT Count "tyvar"
cnt (CompTBody NonEmptyVector (ValT AbstractTy)
compTargs)) ->
        (ScopeBoundary -> ScopeBoundary)
-> Reader ScopeBoundary (ValT AbstractTy)
-> Reader ScopeBoundary (ValT AbstractTy)
forall a.
(ScopeBoundary -> ScopeBoundary)
-> ReaderT ScopeBoundary Identity a
-> ReaderT ScopeBoundary Identity a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (ScopeBoundary -> ScopeBoundary -> ScopeBoundary
forall a. Num a => a -> a -> a
+ ScopeBoundary
1) (Reader ScopeBoundary (ValT AbstractTy)
 -> Reader ScopeBoundary (ValT AbstractTy))
-> Reader ScopeBoundary (ValT AbstractTy)
-> Reader ScopeBoundary (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy -> ValT AbstractTy
forall a. CompT a -> ValT a
ThunkT (CompT AbstractTy -> ValT AbstractTy)
-> (NonEmptyVector (ValT AbstractTy) -> CompT AbstractTy)
-> NonEmptyVector (ValT AbstractTy)
-> ValT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Count "tyvar" -> CompTBody AbstractTy -> CompT AbstractTy
forall a. Count "tyvar" -> CompTBody a -> CompT a
CompT Count "tyvar"
cnt (CompTBody AbstractTy -> CompT AbstractTy)
-> (NonEmptyVector (ValT AbstractTy) -> CompTBody AbstractTy)
-> NonEmptyVector (ValT AbstractTy)
-> CompT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyVector (ValT AbstractTy) -> CompTBody AbstractTy
forall a. NonEmptyVector (ValT a) -> CompTBody a
CompTBody (NonEmptyVector (ValT AbstractTy) -> ValT AbstractTy)
-> ReaderT
     ScopeBoundary Identity (NonEmptyVector (ValT AbstractTy))
-> Reader ScopeBoundary (ValT AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy))
-> NonEmptyVector (ValT AbstractTy)
-> ReaderT
     ScopeBoundary Identity (NonEmptyVector (ValT AbstractTy))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> NonEmptyVector a -> f (NonEmptyVector b)
traverse ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)
replaceAllRecursive NonEmptyVector (ValT AbstractTy)
compTargs
      Datatype TyName
tx Vector (ValT AbstractTy)
args -> (ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)
replaceWithR (ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy))
-> (Vector (ValT AbstractTy) -> ValT AbstractTy)
-> Vector (ValT AbstractTy)
-> Reader ScopeBoundary (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
tx (Vector (ValT AbstractTy)
 -> Reader ScopeBoundary (ValT AbstractTy))
-> ReaderT ScopeBoundary Identity (Vector (ValT AbstractTy))
-> Reader ScopeBoundary (ValT AbstractTy)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< (ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy))
-> Vector (ValT AbstractTy)
-> ReaderT ScopeBoundary Identity (Vector (ValT AbstractTy))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)
replaceAllRecursive Vector (ValT AbstractTy)
args)
    mkBaseCtor :: Constructor AbstractTy -> Reader ScopeBoundary (Constructor AbstractTy)
    mkBaseCtor :: Constructor AbstractTy
-> ReaderT ScopeBoundary Identity (Constructor AbstractTy)
mkBaseCtor (Constructor ConstructorName
ctorNm Vector (ValT AbstractTy)
ctorArgs) = ConstructorName
-> Vector (ValT AbstractTy) -> Constructor AbstractTy
forall a. ConstructorName -> Vector (ValT a) -> Constructor a
Constructor (ConstructorName -> ConstructorName
baseFCtorName ConstructorName
ctorNm) (Vector (ValT AbstractTy) -> Constructor AbstractTy)
-> ReaderT ScopeBoundary Identity (Vector (ValT AbstractTy))
-> ReaderT ScopeBoundary Identity (Constructor AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy))
-> Vector (ValT AbstractTy)
-> ReaderT ScopeBoundary Identity (Vector (ValT AbstractTy))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)
replaceAllRecursive Vector (ValT AbstractTy)
ctorArgs
      where
        baseFCtorName :: ConstructorName -> ConstructorName
        baseFCtorName :: ConstructorName -> ConstructorName
baseFCtorName (ConstructorName Text
nm) = Text -> ConstructorName
ConstructorName (Text
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_F")
    allCtorArgs :: [ValT AbstractTy]
    allCtorArgs :: [ValT AbstractTy]
allCtorArgs = (Constructor AbstractTy -> [ValT AbstractTy])
-> Vector (Constructor AbstractTy) -> [ValT AbstractTy]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap (Vector (ValT AbstractTy) -> [ValT AbstractTy]
forall a. Vector a -> [a]
V.toList (Vector (ValT AbstractTy) -> [ValT AbstractTy])
-> (Constructor AbstractTy -> Vector (ValT AbstractTy))
-> Constructor AbstractTy
-> [ValT AbstractTy]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic'
  A_Lens NoIx (Constructor AbstractTy) (Vector (ValT AbstractTy))
-> Constructor AbstractTy -> Vector (ValT AbstractTy)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic'
  A_Lens NoIx (Constructor AbstractTy) (Vector (ValT AbstractTy))
#constructorArgs) Vector (Constructor AbstractTy)
ctors
    -- This tells us whether the ValT *is* a recursive child of the parent type
    isRecursive :: ValT AbstractTy -> Reader ScopeBoundary Bool
    isRecursive :: ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool
isRecursive = TyName -> ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool
isRecursiveChildOf TyName
tn

-- | Returns 'True' if the second argument is a recursive child of the datatype
-- named by the first argument.
--
-- @since 1.1.0
isRecursiveChildOf :: TyName -> ValT AbstractTy -> Reader ScopeBoundary Bool
isRecursiveChildOf :: TyName -> ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool
isRecursiveChildOf TyName
tn = \case
  Datatype TyName
tn' Vector (ValT AbstractTy)
args
    | TyName
tn' TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
tn -> (Bool
 -> Int -> ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool)
-> Bool
-> Vector (ValT AbstractTy)
-> ReaderT ScopeBoundary Identity Bool
forall (m :: Type -> Type) a b.
Monad m =>
(a -> Int -> b -> m a) -> a -> Vector b -> m a
V.ifoldM Bool
-> Int -> ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool
checkArgsIsRec' Bool
True Vector (ValT AbstractTy)
args
    | Bool
otherwise -> Bool -> ReaderT ScopeBoundary Identity Bool
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
  ValT AbstractTy
_ -> Bool -> ReaderT ScopeBoundary Identity Bool
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
  where
    checkArgsIsRec' :: Bool -> Int -> ValT AbstractTy -> Reader ScopeBoundary Bool
    checkArgsIsRec' :: Bool
-> Int -> ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool
checkArgsIsRec' Bool
acc Int
n = \case
      Abstraction (BoundAt DeBruijn
db Index "tyvar"
varIx) -> do
        ScopeBoundary Int
here <- ReaderT ScopeBoundary Identity ScopeBoundary
forall r (m :: Type -> Type). MonadReader r m => m r
ask
        let dbInt :: Int
dbInt = Optic' A_Prism NoIx Int DeBruijn -> DeBruijn -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int DeBruijn
asInt DeBruijn
db
        -- Explanation: A component ValT is only a recursive instance of the parent type if
        --              the DeBruijn index of its type variables points to Z (and the other conditions obtain)
        if Int
dbInt Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
here Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 Bool -> Bool -> Bool
&& Optic' A_Prism NoIx Int (Index "tyvar") -> Index "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex Index "tyvar"
varIx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n
          then Bool -> ReaderT ScopeBoundary Identity Bool
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
acc
          else Bool -> ReaderT ScopeBoundary Identity Bool
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
      ValT AbstractTy
_ -> Bool -> ReaderT ScopeBoundary Identity Bool
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False

-- | Determines whether the type represented by the second argument and named by
-- the first requires a base functor.
--
-- @since 1.1.0
hasRecursive :: TyName -> ValT AbstractTy -> Reader ScopeBoundary Bool
hasRecursive :: TyName -> ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool
hasRecursive TyName
tn = \case
  Abstraction {} -> Bool -> ReaderT ScopeBoundary Identity Bool
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
  BuiltinFlat {} -> Bool -> ReaderT ScopeBoundary Identity Bool
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
  -- NOTE: This assumes that we've forbidden higher rank arguments to constructors (i.e. we can ignore the scope here)
  ThunkT (CompT Count "tyvar"
_ (CompTBody (NonEmptyVector (ValT AbstractTy) -> [ValT AbstractTy]
forall a. NonEmptyVector a -> [a]
NEV.toList -> [ValT AbstractTy]
compTArgs))) -> (ScopeBoundary -> ScopeBoundary)
-> ReaderT ScopeBoundary Identity Bool
-> ReaderT ScopeBoundary Identity Bool
forall a.
(ScopeBoundary -> ScopeBoundary)
-> ReaderT ScopeBoundary Identity a
-> ReaderT ScopeBoundary Identity a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (ScopeBoundary -> ScopeBoundary -> ScopeBoundary
forall a. Num a => a -> a -> a
+ ScopeBoundary
1) (ReaderT ScopeBoundary Identity Bool
 -> ReaderT ScopeBoundary Identity Bool)
-> ReaderT ScopeBoundary Identity Bool
-> ReaderT ScopeBoundary Identity Bool
forall a b. (a -> b) -> a -> b
$ do
    [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
or ([Bool] -> Bool)
-> ReaderT ScopeBoundary Identity [Bool]
-> ReaderT ScopeBoundary Identity Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool)
-> [ValT AbstractTy] -> ReaderT ScopeBoundary Identity [Bool]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (TyName -> ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool
hasRecursive TyName
tn) [ValT AbstractTy]
compTArgs
  dt :: ValT AbstractTy
dt@(Datatype TyName
_ Vector (ValT AbstractTy)
args) -> do
    Bool
thisTypeIsRecursive <- TyName -> ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool
isRecursiveChildOf TyName
tn ValT AbstractTy
dt
    Bool
aComponentIsRecursive <- Vector Bool -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
or (Vector Bool -> Bool)
-> ReaderT ScopeBoundary Identity (Vector Bool)
-> ReaderT ScopeBoundary Identity Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool)
-> Vector (ValT AbstractTy)
-> ReaderT ScopeBoundary Identity (Vector Bool)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse (TyName -> ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool
hasRecursive TyName
tn) Vector (ValT AbstractTy)
args
    Bool -> ReaderT ScopeBoundary Identity Bool
forall a. a -> ReaderT ScopeBoundary Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> ReaderT ScopeBoundary Identity Bool)
-> Bool -> ReaderT ScopeBoundary Identity Bool
forall a b. (a -> b) -> a -> b
$ Bool
thisTypeIsRecursive Bool -> Bool -> Bool
|| Bool
aComponentIsRecursive

-- | Constructs a base functor Boehm-Berrarducci form for the given datatype.
-- Returns 'Nothing' if the type is not self-recursive.
--
-- @since 1.1.0
mkBBF :: DataDeclaration AbstractTy -> Either BBFError (Maybe (ValT AbstractTy))
mkBBF :: DataDeclaration AbstractTy
-> Either BBFError (Maybe (ValT AbstractTy))
mkBBF DataDeclaration AbstractTy
decl = Maybe (Either BBFError (ValT AbstractTy))
-> Either BBFError (Maybe (ValT AbstractTy))
forall (t :: Type -> Type) (m :: Type -> Type) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: Type -> Type) a. Monad m => Maybe (m a) -> m (Maybe a)
sequence (Maybe (Either BBFError (ValT AbstractTy))
 -> Either BBFError (Maybe (ValT AbstractTy)))
-> (ExceptT BBFError Maybe (ValT AbstractTy)
    -> Maybe (Either BBFError (ValT AbstractTy)))
-> ExceptT BBFError Maybe (ValT AbstractTy)
-> Either BBFError (Maybe (ValT AbstractTy))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT BBFError Maybe (ValT AbstractTy)
-> Maybe (Either BBFError (ValT AbstractTy))
forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT BBFError Maybe (ValT AbstractTy)
 -> Either BBFError (Maybe (ValT AbstractTy)))
-> ExceptT BBFError Maybe (ValT AbstractTy)
-> Either BBFError (Maybe (ValT AbstractTy))
forall a b. (a -> b) -> a -> b
$ DataDeclaration AbstractTy
-> ExceptT BBFError Maybe (ValT AbstractTy)
mkBBF' DataDeclaration AbstractTy
decl

-- | Verifies that all type variables declared by the given datatype have a
-- corresponding value in some \'arm\'.
--
-- @since 1.1.0
noPhantomTyVars :: DataDeclaration AbstractTy -> Bool
noPhantomTyVars :: DataDeclaration AbstractTy -> Bool
noPhantomTyVars OpaqueData {} = Bool
True
noPhantomTyVars decl :: DataDeclaration AbstractTy
decl@(DataDeclaration TyName
_ Count "tyvar"
numVars Vector (Constructor AbstractTy)
_ DataEncoding
_) =
  let allChildren :: [ValT AbstractTy]
allChildren = DataDeclaration AbstractTy -> [ValT AbstractTy]
allComponentTypes DataDeclaration AbstractTy
decl
      allResolved :: Set AbstractTy
allResolved = [Set AbstractTy] -> Set AbstractTy
forall (f :: Type -> Type) a.
(Foldable f, Ord a) =>
f (Set a) -> Set a
Set.unions ([Set AbstractTy] -> Set AbstractTy)
-> [Set AbstractTy] -> Set AbstractTy
forall a b. (a -> b) -> a -> b
$ Reader Int [Set AbstractTy] -> Int -> [Set AbstractTy]
forall r a. Reader r a -> r -> a
runReader ((ValT AbstractTy -> ReaderT Int Identity (Set AbstractTy))
-> [ValT AbstractTy] -> Reader Int [Set AbstractTy]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ValT AbstractTy -> ReaderT Int Identity (Set AbstractTy)
allResolvedTyVars' [ValT AbstractTy]
allChildren) Int
0
      indices :: [Index "tyvar"]
      indices :: [Index "tyvar"]
indices = Maybe (Index "tyvar") -> Index "tyvar"
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Index "tyvar") -> Index "tyvar")
-> (Int -> Maybe (Index "tyvar")) -> Int -> Index "tyvar"
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int (Index "tyvar")
-> Int -> Maybe (Index "tyvar")
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex (Int -> Index "tyvar") -> [Int] -> [Index "tyvar"]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0 .. (Optic' A_Prism NoIx Int (Count "tyvar") -> Count "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount Count "tyvar"
numVars Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]
      declaredTyVars :: [AbstractTy]
declaredTyVars = DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
Z (Index "tyvar" -> AbstractTy) -> [Index "tyvar"] -> [AbstractTy]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Index "tyvar"]
indices
   in (AbstractTy -> Bool) -> [AbstractTy] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all (AbstractTy -> Set AbstractTy -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set AbstractTy
allResolved) [AbstractTy]
declaredTyVars

-- | Collect all (other) value types a given value type refers to.
--
-- @since 1.1.0
everythingOf :: forall (a :: Type). (Ord a) => ValT a -> Set (ValT a)
everythingOf :: forall a. Ord a => ValT a -> Set (ValT a)
everythingOf = (Set (ValT a) -> ValT a -> Set (ValT a))
-> Set (ValT a) -> ValT a -> Set (ValT a)
forall a b. (b -> ValT a -> b) -> b -> ValT a -> b
foldValT ((ValT a -> Set (ValT a) -> Set (ValT a))
-> Set (ValT a) -> ValT a -> Set (ValT a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ValT a -> Set (ValT a) -> Set (ValT a)
forall a. Ord a => a -> Set a -> Set a
Set.insert) Set (ValT a)
forall a. Set a
Set.empty

-- Helpers

{- NOTE: For the purposes of base functor transformation, we follow the pattern established by Edward Kmett's
         'recursion-schemes' library. That is, we regard a datatype as "recursive" if and only if at least one
         argument to a constructor contains "the exact same thing as we find to the left of the =". Dunno how to
         describe it more precisely, but the general idea is that things like these ARE recursive for us:

           data Foo = End Int | More Foo Int -- contains 'Foo' as a ctor arg

           data Bar a = Beep | Boom a (Bar a) -- contains 'Bar a'

         but things like this are NOT recursive by our reckoning (even though in some sense they might be considered as such):

           data FunL a b = Done b | Go (FunL b a) a -- `FunL b a` isn't `FunL a b` so it's not literally recursive

         Obviously we're working with DeBruijn indices so the letters are more-or-less fictitious, but hopefully
         these examples nonetheless get the point across.
-}

-- TODO: Rewrite this as `mapMValT`. The change to a `Reader` below makes this unusable, but we can
--       write the non-monadic version as a special case of the monadic version and it is *highly* likely
--       we will need both going forward.
mapValT :: forall (a :: Type). (ValT a -> ValT a) -> ValT a -> ValT a
mapValT :: forall a. (ValT a -> ValT a) -> ValT a -> ValT a
mapValT ValT a -> ValT a
f = \case
  -- for terminal nodes we just apply the function
  absr :: ValT a
absr@(Abstraction {}) -> ValT a -> ValT a
f ValT a
absr
  bif :: ValT a
bif@BuiltinFlat {} -> ValT a -> ValT a
f ValT a
bif
  -- For CompT and Datatype we apply the function to the components and then to the top level
  ThunkT (CompT Count "tyvar"
cnt (CompTBody NonEmptyVector (ValT a)
compTargs)) -> ValT a -> ValT a
f (CompT a -> ValT a
forall a. CompT a -> ValT a
ThunkT (CompT a -> ValT a) -> CompT a -> ValT a
forall a b. (a -> b) -> a -> b
$ Count "tyvar" -> CompTBody a -> CompT a
forall a. Count "tyvar" -> CompTBody a -> CompT a
CompT Count "tyvar"
cnt (NonEmptyVector (ValT a) -> CompTBody a
forall a. NonEmptyVector (ValT a) -> CompTBody a
CompTBody ((ValT a -> ValT a) -> ValT a -> ValT a
forall a. (ValT a -> ValT a) -> ValT a -> ValT a
mapValT ValT a -> ValT a
f (ValT a -> ValT a)
-> NonEmptyVector (ValT a) -> NonEmptyVector (ValT a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmptyVector (ValT a)
compTargs)))
  Datatype TyName
tn Vector (ValT a)
args -> ValT a -> ValT a
f (ValT a -> ValT a) -> ValT a -> ValT a
forall a b. (a -> b) -> a -> b
$ TyName -> Vector (ValT a) -> ValT a
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
tn ((ValT a -> ValT a) -> ValT a -> ValT a
forall a. (ValT a -> ValT a) -> ValT a -> ValT a
mapValT ValT a -> ValT a
f (ValT a -> ValT a) -> Vector (ValT a) -> Vector (ValT a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (ValT a)
args)

-- Did in fact need it
foldValT :: forall (a :: Type) (b :: Type). (b -> ValT a -> b) -> b -> ValT a -> b
foldValT :: forall a b. (b -> ValT a -> b) -> b -> ValT a -> b
foldValT b -> ValT a -> b
f b
e = \case
  absr :: ValT a
absr@(Abstraction {}) -> b -> ValT a -> b
f b
e ValT a
absr
  bif :: ValT a
bif@(BuiltinFlat {}) -> b -> ValT a -> b
f b
e ValT a
bif
  thk :: ValT a
thk@(ThunkT (CompT Count "tyvar"
_ (CompTBody NonEmptyVector (ValT a)
compTArgs))) ->
    let e' :: b
e' = (b -> ValT a -> b) -> b -> NonEmptyVector (ValT a) -> b
forall a b. (a -> b -> a) -> a -> NonEmptyVector b -> a
NEV.foldl' b -> ValT a -> b
f b
e NonEmptyVector (ValT a)
compTArgs
     in b -> ValT a -> b
f b
e' ValT a
thk
  dt :: ValT a
dt@(Datatype TyName
_ Vector (ValT a)
args) ->
    let e' :: b
e' = (b -> ValT a -> b) -> b -> Vector (ValT a) -> b
forall a b. (a -> b -> a) -> a -> Vector b -> a
V.foldl' b -> ValT a -> b
f b
e Vector (ValT a)
args
     in b -> ValT a -> b
f b
e' ValT a
dt

allResolvedTyVars' :: ValT AbstractTy -> Reader Int (Set AbstractTy)
allResolvedTyVars' :: ValT AbstractTy -> ReaderT Int Identity (Set AbstractTy)
allResolvedTyVars' = \case
  Abstraction (BoundAt DeBruijn
db Index "tyvar"
argpos) -> do
    Int
here <- ReaderT Int Identity Int
forall r (m :: Type -> Type). MonadReader r m => m r
ask
    let db' :: DeBruijn
db' = Maybe DeBruijn -> DeBruijn
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe DeBruijn -> DeBruijn)
-> (Int -> Maybe DeBruijn) -> Int -> DeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int DeBruijn -> Int -> Maybe DeBruijn
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int DeBruijn
asInt (Int -> DeBruijn) -> Int -> DeBruijn
forall a b. (a -> b) -> a -> b
$ Optic' A_Prism NoIx Int DeBruijn -> DeBruijn -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int DeBruijn
asInt DeBruijn
db Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
here
    Set AbstractTy -> ReaderT Int Identity (Set AbstractTy)
forall a. a -> ReaderT Int Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Set AbstractTy -> ReaderT Int Identity (Set AbstractTy))
-> (AbstractTy -> Set AbstractTy)
-> AbstractTy
-> ReaderT Int Identity (Set AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractTy -> Set AbstractTy
forall a. a -> Set a
Set.singleton (AbstractTy -> ReaderT Int Identity (Set AbstractTy))
-> AbstractTy -> ReaderT Int Identity (Set AbstractTy)
forall a b. (a -> b) -> a -> b
$ DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
db' Index "tyvar"
argpos
  ThunkT (CompT Count "tyvar"
_ (CompTBody NonEmptyVector (ValT AbstractTy)
nev)) -> (Int -> Int)
-> ReaderT Int Identity (Set AbstractTy)
-> ReaderT Int Identity (Set AbstractTy)
forall a.
(Int -> Int) -> ReaderT Int Identity a -> ReaderT Int Identity a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (ReaderT Int Identity (Set AbstractTy)
 -> ReaderT Int Identity (Set AbstractTy))
-> ReaderT Int Identity (Set AbstractTy)
-> ReaderT Int Identity (Set AbstractTy)
forall a b. (a -> b) -> a -> b
$ do
    NonEmptyVector (Set AbstractTy) -> Set AbstractTy
forall (f :: Type -> Type) a.
(Foldable f, Ord a) =>
f (Set a) -> Set a
Set.unions (NonEmptyVector (Set AbstractTy) -> Set AbstractTy)
-> ReaderT Int Identity (NonEmptyVector (Set AbstractTy))
-> ReaderT Int Identity (Set AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (ValT AbstractTy -> ReaderT Int Identity (Set AbstractTy))
-> NonEmptyVector (ValT AbstractTy)
-> ReaderT Int Identity (NonEmptyVector (Set AbstractTy))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> NonEmptyVector a -> f (NonEmptyVector b)
traverse ValT AbstractTy -> ReaderT Int Identity (Set AbstractTy)
allResolvedTyVars' NonEmptyVector (ValT AbstractTy)
nev
  BuiltinFlat {} -> Set AbstractTy -> ReaderT Int Identity (Set AbstractTy)
forall a. a -> ReaderT Int Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Set AbstractTy
forall a. Set a
Set.empty
  Datatype TyName
_ Vector (ValT AbstractTy)
args -> Vector (Set AbstractTy) -> Set AbstractTy
forall (f :: Type -> Type) a.
(Foldable f, Ord a) =>
f (Set a) -> Set a
Set.unions (Vector (Set AbstractTy) -> Set AbstractTy)
-> ReaderT Int Identity (Vector (Set AbstractTy))
-> ReaderT Int Identity (Set AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (ValT AbstractTy -> ReaderT Int Identity (Set AbstractTy))
-> Vector (ValT AbstractTy)
-> ReaderT Int Identity (Vector (Set AbstractTy))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ValT AbstractTy -> ReaderT Int Identity (Set AbstractTy)
allResolvedTyVars' Vector (ValT AbstractTy)
args

incAbstractionDB :: ValT AbstractTy -> ValT AbstractTy
incAbstractionDB :: ValT AbstractTy -> ValT AbstractTy
incAbstractionDB = (ValT AbstractTy -> ValT AbstractTy)
-> ValT AbstractTy -> ValT AbstractTy
forall a. (ValT a -> ValT a) -> ValT a -> ValT a
mapValT ((ValT AbstractTy -> ValT AbstractTy)
 -> ValT AbstractTy -> ValT AbstractTy)
-> (ValT AbstractTy -> ValT AbstractTy)
-> ValT AbstractTy
-> ValT AbstractTy
forall a b. (a -> b) -> a -> b
$ \case
  Abstraction (BoundAt DeBruijn
db Index "tyvar"
indx) ->
    let db' :: DeBruijn
db' = Maybe DeBruijn -> DeBruijn
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe DeBruijn -> DeBruijn)
-> (Int -> Maybe DeBruijn) -> Int -> DeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int DeBruijn -> Int -> Maybe DeBruijn
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int DeBruijn
asInt (Int -> DeBruijn) -> Int -> DeBruijn
forall a b. (a -> b) -> a -> b
$ Optic' A_Prism NoIx Int DeBruijn -> DeBruijn -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int DeBruijn
asInt DeBruijn
db Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
     in AbstractTy -> ValT AbstractTy
forall a. a -> ValT a
Abstraction (DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
db' Index "tyvar"
indx)
  ValT AbstractTy
other -> ValT AbstractTy
other

-- Only returns `Nothing` if there are no Constructors or the type is Opaque
mkBBF' :: DataDeclaration AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
mkBBF' :: DataDeclaration AbstractTy
-> ExceptT BBFError Maybe (ValT AbstractTy)
mkBBF' OpaqueData {} = Maybe (ValT AbstractTy) -> ExceptT BBFError Maybe (ValT AbstractTy)
forall (m :: Type -> Type) a.
Monad m =>
m a -> ExceptT BBFError m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Maybe (ValT AbstractTy)
forall a. Maybe a
Nothing
mkBBF' (DataDeclaration TyName
tn Count "tyvar"
numVars Vector (Constructor AbstractTy)
ctors DataEncoding
_)
  | Vector (Constructor AbstractTy) -> Bool
forall a. Vector a -> Bool
V.null Vector (Constructor AbstractTy)
ctors = Maybe (ValT AbstractTy) -> ExceptT BBFError Maybe (ValT AbstractTy)
forall (m :: Type -> Type) a.
Monad m =>
m a -> ExceptT BBFError m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Maybe (ValT AbstractTy)
forall a. Maybe a
Nothing
  | Bool
otherwise = do
      Vector (ValT AbstractTy)
ctors' <- (Constructor AbstractTy
 -> ExceptT BBFError Maybe (ValT AbstractTy))
-> Vector (Constructor AbstractTy)
-> ExceptT BBFError Maybe (Vector (ValT AbstractTy))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse Constructor AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
mkBBCtor Vector (Constructor AbstractTy)
ctors
      Maybe (ValT AbstractTy) -> ExceptT BBFError Maybe (ValT AbstractTy)
forall (m :: Type -> Type) a.
Monad m =>
m a -> ExceptT BBFError m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (ValT AbstractTy)
 -> ExceptT BBFError Maybe (ValT AbstractTy))
-> Maybe (ValT AbstractTy)
-> ExceptT BBFError Maybe (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy -> ValT AbstractTy
forall a. CompT a -> ValT a
ThunkT (CompT AbstractTy -> ValT AbstractTy)
-> (NonEmptyVector (ValT AbstractTy) -> CompT AbstractTy)
-> NonEmptyVector (ValT AbstractTy)
-> ValT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Count "tyvar" -> CompTBody AbstractTy -> CompT AbstractTy
forall a. Count "tyvar" -> CompTBody a -> CompT a
CompT Count "tyvar"
bbfCount (CompTBody AbstractTy -> CompT AbstractTy)
-> (NonEmptyVector (ValT AbstractTy) -> CompTBody AbstractTy)
-> NonEmptyVector (ValT AbstractTy)
-> CompT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyVector (ValT AbstractTy) -> CompTBody AbstractTy
forall a. NonEmptyVector (ValT a) -> CompTBody a
CompTBody (NonEmptyVector (ValT AbstractTy) -> CompTBody AbstractTy)
-> (NonEmptyVector (ValT AbstractTy)
    -> NonEmptyVector (ValT AbstractTy))
-> NonEmptyVector (ValT AbstractTy)
-> CompTBody AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmptyVector (ValT AbstractTy)
 -> ValT AbstractTy -> NonEmptyVector (ValT AbstractTy))
-> ValT AbstractTy
-> NonEmptyVector (ValT AbstractTy)
-> NonEmptyVector (ValT AbstractTy)
forall a b c. (a -> b -> c) -> b -> a -> c
flip NonEmptyVector (ValT AbstractTy)
-> ValT AbstractTy -> NonEmptyVector (ValT AbstractTy)
forall a. NonEmptyVector a -> a -> NonEmptyVector a
NEV.snoc ValT AbstractTy
topLevelOut (NonEmptyVector (ValT AbstractTy) -> ValT AbstractTy)
-> Maybe (NonEmptyVector (ValT AbstractTy))
-> Maybe (ValT AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (ValT AbstractTy)
-> Maybe (NonEmptyVector (ValT AbstractTy))
forall a. Vector a -> Maybe (NonEmptyVector a)
NEV.fromVector Vector (ValT AbstractTy)
ctors'
  where
    topLevelOut :: ValT AbstractTy
topLevelOut = AbstractTy -> ValT AbstractTy
forall a. a -> ValT a
Abstraction (AbstractTy -> ValT AbstractTy) -> AbstractTy -> ValT AbstractTy
forall a b. (a -> b) -> a -> b
$ DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
Z Index "tyvar"
outIx

    outIx :: Index "tyvar"
    outIx :: Index "tyvar"
outIx = Maybe (Index "tyvar") -> Index "tyvar"
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Index "tyvar") -> Index "tyvar")
-> (Int -> Maybe (Index "tyvar")) -> Int -> Index "tyvar"
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int (Index "tyvar")
-> Int -> Maybe (Index "tyvar")
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex (Int -> Index "tyvar") -> Int -> Index "tyvar"
forall a b. (a -> b) -> a -> b
$ Optic' A_Prism NoIx Int (Count "tyvar") -> Count "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount Count "tyvar"
numVars

    bbfCount :: Count "tyvar"
bbfCount = Maybe (Count "tyvar") -> Count "tyvar"
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Count "tyvar") -> Count "tyvar")
-> (Int -> Maybe (Count "tyvar")) -> Int -> Count "tyvar"
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int (Count "tyvar")
-> Int -> Maybe (Count "tyvar")
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount (Int -> Count "tyvar") -> Int -> Count "tyvar"
forall a b. (a -> b) -> a -> b
$ Optic' A_Prism NoIx Int (Count "tyvar") -> Count "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount Count "tyvar"
numVars Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

    mkBBCtor :: Constructor AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
    mkBBCtor :: Constructor AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
mkBBCtor (Constructor ConstructorName
_ Vector (ValT AbstractTy)
args)
      | Vector (ValT AbstractTy) -> Bool
forall a. Vector a -> Bool
V.null Vector (ValT AbstractTy)
args = ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
forall a. a -> ExceptT BBFError Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT AbstractTy
topLevelOut
      | Bool
otherwise = do
          Vector (ValT AbstractTy)
elimArgs <- (ValT AbstractTy -> ValT AbstractTy)
-> Vector (ValT AbstractTy) -> Vector (ValT AbstractTy)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ValT AbstractTy -> ValT AbstractTy
incAbstractionDB (Vector (ValT AbstractTy) -> Vector (ValT AbstractTy))
-> ExceptT BBFError Maybe (Vector (ValT AbstractTy))
-> ExceptT BBFError Maybe (Vector (ValT AbstractTy))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy))
-> Vector (ValT AbstractTy)
-> ExceptT BBFError Maybe (Vector (ValT AbstractTy))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
fixArg Vector (ValT AbstractTy)
args
          NonEmptyVector (ValT AbstractTy)
elimArgs' <- Maybe (NonEmptyVector (ValT AbstractTy))
-> ExceptT BBFError Maybe (NonEmptyVector (ValT AbstractTy))
forall (m :: Type -> Type) a.
Monad m =>
m a -> ExceptT BBFError m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (NonEmptyVector (ValT AbstractTy))
 -> ExceptT BBFError Maybe (NonEmptyVector (ValT AbstractTy)))
-> (Vector (ValT AbstractTy)
    -> Maybe (NonEmptyVector (ValT AbstractTy)))
-> Vector (ValT AbstractTy)
-> ExceptT BBFError Maybe (NonEmptyVector (ValT AbstractTy))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (ValT AbstractTy)
-> Maybe (NonEmptyVector (ValT AbstractTy))
forall a. Vector a -> Maybe (NonEmptyVector a)
NEV.fromVector (Vector (ValT AbstractTy)
 -> ExceptT BBFError Maybe (NonEmptyVector (ValT AbstractTy)))
-> Vector (ValT AbstractTy)
-> ExceptT BBFError Maybe (NonEmptyVector (ValT AbstractTy))
forall a b. (a -> b) -> a -> b
$ Vector (ValT AbstractTy)
elimArgs
          let out :: ValT AbstractTy
out = AbstractTy -> ValT AbstractTy
forall a. a -> ValT a
Abstraction (AbstractTy -> ValT AbstractTy) -> AbstractTy -> ValT AbstractTy
forall a b. (a -> b) -> a -> b
$ DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt (DeBruijn -> DeBruijn
S DeBruijn
Z) Index "tyvar"
outIx
          ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
forall a. a -> ExceptT BBFError Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy))
-> (NonEmptyVector (ValT AbstractTy) -> ValT AbstractTy)
-> NonEmptyVector (ValT AbstractTy)
-> ExceptT BBFError Maybe (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> ValT AbstractTy
forall a. CompT a -> ValT a
ThunkT (CompT AbstractTy -> ValT AbstractTy)
-> (NonEmptyVector (ValT AbstractTy) -> CompT AbstractTy)
-> NonEmptyVector (ValT AbstractTy)
-> ValT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Count "tyvar" -> CompTBody AbstractTy -> CompT AbstractTy
forall a. Count "tyvar" -> CompTBody a -> CompT a
CompT Count "tyvar"
forall (ofWhat :: Symbol). Count ofWhat
count0 (CompTBody AbstractTy -> CompT AbstractTy)
-> (NonEmptyVector (ValT AbstractTy) -> CompTBody AbstractTy)
-> NonEmptyVector (ValT AbstractTy)
-> CompT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyVector (ValT AbstractTy) -> CompTBody AbstractTy
forall a. NonEmptyVector (ValT a) -> CompTBody a
CompTBody (NonEmptyVector (ValT AbstractTy) -> CompTBody AbstractTy)
-> (NonEmptyVector (ValT AbstractTy)
    -> NonEmptyVector (ValT AbstractTy))
-> NonEmptyVector (ValT AbstractTy)
-> CompTBody AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmptyVector (ValT AbstractTy)
 -> ValT AbstractTy -> NonEmptyVector (ValT AbstractTy))
-> ValT AbstractTy
-> NonEmptyVector (ValT AbstractTy)
-> NonEmptyVector (ValT AbstractTy)
forall a b c. (a -> b -> c) -> b -> a -> c
flip NonEmptyVector (ValT AbstractTy)
-> ValT AbstractTy -> NonEmptyVector (ValT AbstractTy)
forall a. NonEmptyVector a -> a -> NonEmptyVector a
NEV.snoc ValT AbstractTy
out (NonEmptyVector (ValT AbstractTy)
 -> ExceptT BBFError Maybe (ValT AbstractTy))
-> NonEmptyVector (ValT AbstractTy)
-> ExceptT BBFError Maybe (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ NonEmptyVector (ValT AbstractTy)
elimArgs'

    fixArg :: ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
    fixArg :: ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
fixArg ValT AbstractTy
arg = do
      let isDirectRecursiveTy :: Bool
isDirectRecursiveTy = ReaderT ScopeBoundary Identity Bool -> ScopeBoundary -> Bool
forall r a. Reader r a -> r -> a
runReader (TyName -> ValT AbstractTy -> ReaderT ScopeBoundary Identity Bool
isRecursiveChildOf TyName
tn ValT AbstractTy
arg) ScopeBoundary
0
      if Bool
isDirectRecursiveTy
        then ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
forall a. a -> ExceptT BBFError Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy))
-> ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ AbstractTy -> ValT AbstractTy
forall a. a -> ValT a
Abstraction (DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
Z Index "tyvar"
outIx)
        else case ValT AbstractTy
arg of
          Datatype TyName
tn' Vector (ValT AbstractTy)
dtArgs
            | TyName
tn TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
tn' -> BBFError -> ExceptT BBFError Maybe (ValT AbstractTy)
forall a. BBFError -> ExceptT BBFError Maybe a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (BBFError -> ExceptT BBFError Maybe (ValT AbstractTy))
-> BBFError -> ExceptT BBFError Maybe (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ TyName -> ValT AbstractTy -> BBFError
InvalidRecursion TyName
tn ValT AbstractTy
arg
            | Bool
otherwise -> do
                Vector (ValT AbstractTy)
dtArgs' <- (ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy))
-> Vector (ValT AbstractTy)
-> ExceptT BBFError Maybe (Vector (ValT AbstractTy))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
fixArg Vector (ValT AbstractTy)
dtArgs
                ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
forall a. a -> ExceptT BBFError Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy))
-> (Vector (ValT AbstractTy) -> ValT AbstractTy)
-> Vector (ValT AbstractTy)
-> ExceptT BBFError Maybe (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
tn' (Vector (ValT AbstractTy)
 -> ExceptT BBFError Maybe (ValT AbstractTy))
-> Vector (ValT AbstractTy)
-> ExceptT BBFError Maybe (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ Vector (ValT AbstractTy)
dtArgs'
          ValT AbstractTy
_ -> ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
forall a. a -> ExceptT BBFError Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT AbstractTy
arg

{- Note (Sean, 14/05/25): Re  DeBruijn indices:

     - None of the existing variable DeBruijn or position indices change at all b/c the binding context of the
       `forall` we're introducing replaces the binding context of the datatype declaration and only extends it.

     - The only special thing we have to keep track of is the (DeBruijn) index of the `out` variable, but this doesn't require
       any fancy scope tracking: It will always be Z for the top-level result and `S Z` wherever it occurs in a
       transformed constructor. It won't ever occur any "deeper" than that (because we don't nest these, and a constructor gets exactly one
       `out`)

     - Actually this is slightly false, we need to "bump" all of the indices inside constructor arms by one (because
       they now occur within a Thunk), but after that bump everything is stable as indicated above.
-}

{- Here for lack of a better place to put it (has to be available to Unification and ASG)
-}