{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE ScopedTypeVariables #-}
module PlutusIR.Subst
    ( uniquesTerm
    , uniquesType
    , fvTerm
    , ftvTerm
    , fvBinding
    , ftvBinding
    , ftvTy
    ) where

import PlutusCore.Core.Type qualified as PLC
import PlutusCore.Name qualified as PLC
import PlutusCore.Subst (ftvTy, uniquesType)

import PlutusIR.Compiler.Datatype
import PlutusIR.Core

import Control.Lens
import Data.Set as S hiding (foldr)
import Data.Set.Lens (setOf)

uniquesTerm
    :: PLC.HasUniques (Term tyname name uni fun ann)
    => Term tyname name uni fun ann -> Set PLC.Unique
uniquesTerm :: Term tyname name uni fun ann -> Set Unique
uniquesTerm = Getting (Set Unique) (Term tyname name uni fun ann) Unique
-> Term tyname name uni fun ann -> Set Unique
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set Unique) (Term tyname name uni fun ann) Unique
forall tyname name (uni :: * -> *) fun ann.
HasUniques (Term tyname name uni fun ann) =>
Fold (Term tyname name uni fun ann) Unique
termUniquesDeep

-- | Get all the free term variables in a PIR term.
fvTerm :: Ord name => Term tyname name uni fun ann -> Set name
fvTerm :: Term tyname name uni fun ann -> Set name
fvTerm = \case
    Let ann
_ Recursivity
NonRec NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
tIn ->
        let fvLinearScope :: Binding tyname a uni fun a -> Set a -> Set a
fvLinearScope Binding tyname a uni fun a
b Set a
acc = Binding tyname a uni fun a -> Set a
forall name tyname (uni :: * -> *) fun ann.
Ord name =>
Binding tyname name uni fun ann -> Set name
fvBinding Binding tyname a uni fun a
b
                                   Set a -> Set a -> Set a
forall a. Semigroup a => a -> a -> a
<> (Set a
acc Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
\\ Getting (Set a) (Binding tyname a uni fun a) a
-> Binding tyname a uni fun a -> Set a
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set a) (Binding tyname a uni fun a) a
forall tyname name (uni :: * -> *) fun a.
Traversal' (Binding tyname name uni fun a) name
bindingNames Binding tyname a uni fun a
b)
        in (Binding tyname name uni fun ann -> Set name -> Set name)
-> Set name
-> NonEmpty (Binding tyname name uni fun ann)
-> Set name
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding tyname name uni fun ann -> Set name -> Set name
forall a tyname (uni :: * -> *) fun a.
Ord a =>
Binding tyname a uni fun a -> Set a -> Set a
fvLinearScope (Term tyname name uni fun ann -> Set name
forall name tyname (uni :: * -> *) fun ann.
Ord name =>
Term tyname name uni fun ann -> Set name
fvTerm Term tyname name uni fun ann
tIn) NonEmpty (Binding tyname name uni fun ann)
bs

    Let ann
_ Recursivity
Rec NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
tIn ->
        ((Binding tyname name uni fun ann -> Set name)
-> NonEmpty (Binding tyname name uni fun ann) -> Set name
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Binding tyname name uni fun ann -> Set name
forall name tyname (uni :: * -> *) fun ann.
Ord name =>
Binding tyname name uni fun ann -> Set name
fvBinding NonEmpty (Binding tyname name uni fun ann)
bs Set name -> Set name -> Set name
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun ann -> Set name
forall name tyname (uni :: * -> *) fun ann.
Ord name =>
Term tyname name uni fun ann -> Set name
fvTerm Term tyname name uni fun ann
tIn)
        Set name -> Set name -> Set name
forall a. Ord a => Set a -> Set a -> Set a
\\ Getting
  (Set name) (NonEmpty (Binding tyname name uni fun ann)) name
-> NonEmpty (Binding tyname name uni fun ann) -> Set name
forall a s. Getting (Set a) s a -> s -> Set a
setOf ((Binding tyname name uni fun ann
 -> Const (Set name) (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> Const (Set name) (NonEmpty (Binding tyname name uni fun ann))
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
traversed((Binding tyname name uni fun ann
  -> Const (Set name) (Binding tyname name uni fun ann))
 -> NonEmpty (Binding tyname name uni fun ann)
 -> Const (Set name) (NonEmpty (Binding tyname name uni fun ann)))
-> ((name -> Const (Set name) name)
    -> Binding tyname name uni fun ann
    -> Const (Set name) (Binding tyname name uni fun ann))
-> Getting
     (Set name) (NonEmpty (Binding tyname name uni fun ann)) name
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(name -> Const (Set name) name)
-> Binding tyname name uni fun ann
-> Const (Set name) (Binding tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a.
Traversal' (Binding tyname name uni fun a) name
bindingNames) NonEmpty (Binding tyname name uni fun ann)
bs

    LamAbs ann
_ name
n Type tyname uni ann
_ Term tyname name uni fun ann
t -> name -> Set name -> Set name
forall a. Ord a => a -> Set a -> Set a
delete name
n (Set name -> Set name) -> Set name -> Set name
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann -> Set name
forall name tyname (uni :: * -> *) fun ann.
Ord name =>
Term tyname name uni fun ann -> Set name
fvTerm Term tyname name uni fun ann
t
    Apply ann
_ Term tyname name uni fun ann
t1 Term tyname name uni fun ann
t2 -> Term tyname name uni fun ann -> Set name
forall name tyname (uni :: * -> *) fun ann.
Ord name =>
Term tyname name uni fun ann -> Set name
fvTerm Term tyname name uni fun ann
t1 Set name -> Set name -> Set name
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun ann -> Set name
forall name tyname (uni :: * -> *) fun ann.
Ord name =>
Term tyname name uni fun ann -> Set name
fvTerm Term tyname name uni fun ann
t2
    Var ann
_ name
n -> name -> Set name
forall a. a -> Set a
singleton name
n
    TyAbs ann
_ tyname
_ Kind ann
_ Term tyname name uni fun ann
t ->   Term tyname name uni fun ann -> Set name
forall name tyname (uni :: * -> *) fun ann.
Ord name =>
Term tyname name uni fun ann -> Set name
fvTerm Term tyname name uni fun ann
t
    TyInst ann
_ Term tyname name uni fun ann
t Type tyname uni ann
_ ->    Term tyname name uni fun ann -> Set name
forall name tyname (uni :: * -> *) fun ann.
Ord name =>
Term tyname name uni fun ann -> Set name
fvTerm Term tyname name uni fun ann
t
    Unwrap ann
_ Term tyname name uni fun ann
t ->      Term tyname name uni fun ann -> Set name
forall name tyname (uni :: * -> *) fun ann.
Ord name =>
Term tyname name uni fun ann -> Set name
fvTerm Term tyname name uni fun ann
t
    IWrap ann
_ Type tyname uni ann
_ Type tyname uni ann
_ Term tyname name uni fun ann
t ->   Term tyname name uni fun ann -> Set name
forall name tyname (uni :: * -> *) fun ann.
Ord name =>
Term tyname name uni fun ann -> Set name
fvTerm Term tyname name uni fun ann
t
    Constant{}       -> Set name
forall a. Monoid a => a
mempty
    Builtin{}        -> Set name
forall a. Monoid a => a
mempty
    Error{}          -> Set name
forall a. Monoid a => a
mempty

-- | Get all the free type variables in a PIR term.
ftvTerm :: Ord tyname => Term tyname name uni fun ann -> Set tyname
ftvTerm :: Term tyname name uni fun ann -> Set tyname
ftvTerm = \case
    Let ann
_ r :: Recursivity
r@Recursivity
NonRec NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
tIn ->
        let ftvLinearScope :: Binding a name uni fun a -> Set a -> Set a
ftvLinearScope Binding a name uni fun a
b Set a
acc = Recursivity -> Binding a name uni fun a -> Set a
forall tyname name (uni :: * -> *) fun ann.
Ord tyname =>
Recursivity -> Binding tyname name uni fun ann -> Set tyname
ftvBinding Recursivity
r Binding a name uni fun a
b
                                   Set a -> Set a -> Set a
forall a. Semigroup a => a -> a -> a
<> (Set a
acc Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
\\ Getting (Set a) (Binding a name uni fun a) a
-> Binding a name uni fun a -> Set a
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set a) (Binding a name uni fun a) a
forall tyname name (uni :: * -> *) fun a.
Traversal' (Binding tyname name uni fun a) tyname
bindingTyNames Binding a name uni fun a
b)
        in (Binding tyname name uni fun ann -> Set tyname -> Set tyname)
-> Set tyname
-> NonEmpty (Binding tyname name uni fun ann)
-> Set tyname
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding tyname name uni fun ann -> Set tyname -> Set tyname
forall a name (uni :: * -> *) fun a.
Ord a =>
Binding a name uni fun a -> Set a -> Set a
ftvLinearScope (Term tyname name uni fun ann -> Set tyname
forall tyname name (uni :: * -> *) fun ann.
Ord tyname =>
Term tyname name uni fun ann -> Set tyname
ftvTerm Term tyname name uni fun ann
tIn) NonEmpty (Binding tyname name uni fun ann)
bs

    Let ann
_ r :: Recursivity
r@Recursivity
Rec NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
tIn ->
        (Term tyname name uni fun ann -> Set tyname
forall tyname name (uni :: * -> *) fun ann.
Ord tyname =>
Term tyname name uni fun ann -> Set tyname
ftvTerm Term tyname name uni fun ann
tIn Set tyname -> Set tyname -> Set tyname
forall a. Semigroup a => a -> a -> a
<> (Binding tyname name uni fun ann -> Set tyname)
-> NonEmpty (Binding tyname name uni fun ann) -> Set tyname
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Recursivity -> Binding tyname name uni fun ann -> Set tyname
forall tyname name (uni :: * -> *) fun ann.
Ord tyname =>
Recursivity -> Binding tyname name uni fun ann -> Set tyname
ftvBinding Recursivity
r) NonEmpty (Binding tyname name uni fun ann)
bs)
        Set tyname -> Set tyname -> Set tyname
forall a. Ord a => Set a -> Set a -> Set a
\\ Getting
  (Set tyname) (NonEmpty (Binding tyname name uni fun ann)) tyname
-> NonEmpty (Binding tyname name uni fun ann) -> Set tyname
forall a s. Getting (Set a) s a -> s -> Set a
setOf ((Binding tyname name uni fun ann
 -> Const (Set tyname) (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> Const (Set tyname) (NonEmpty (Binding tyname name uni fun ann))
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
traversed((Binding tyname name uni fun ann
  -> Const (Set tyname) (Binding tyname name uni fun ann))
 -> NonEmpty (Binding tyname name uni fun ann)
 -> Const (Set tyname) (NonEmpty (Binding tyname name uni fun ann)))
-> ((tyname -> Const (Set tyname) tyname)
    -> Binding tyname name uni fun ann
    -> Const (Set tyname) (Binding tyname name uni fun ann))
-> Getting
     (Set tyname) (NonEmpty (Binding tyname name uni fun ann)) tyname
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(tyname -> Const (Set tyname) tyname)
-> Binding tyname name uni fun ann
-> Const (Set tyname) (Binding tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a.
Traversal' (Binding tyname name uni fun a) tyname
bindingTyNames) NonEmpty (Binding tyname name uni fun ann)
bs
    TyAbs ann
_ tyname
ty Kind ann
_ Term tyname name uni fun ann
t    -> tyname -> Set tyname -> Set tyname
forall a. Ord a => a -> Set a -> Set a
delete tyname
ty (Set tyname -> Set tyname) -> Set tyname -> Set tyname
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann -> Set tyname
forall tyname name (uni :: * -> *) fun ann.
Ord tyname =>
Term tyname name uni fun ann -> Set tyname
ftvTerm Term tyname name uni fun ann
t
    LamAbs ann
_ name
_ Type tyname uni ann
ty Term tyname name uni fun ann
t   -> Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy Type tyname uni ann
ty Set tyname -> Set tyname -> Set tyname
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun ann -> Set tyname
forall tyname name (uni :: * -> *) fun ann.
Ord tyname =>
Term tyname name uni fun ann -> Set tyname
ftvTerm Term tyname name uni fun ann
t
    Apply ann
_ Term tyname name uni fun ann
t1 Term tyname name uni fun ann
t2     -> Term tyname name uni fun ann -> Set tyname
forall tyname name (uni :: * -> *) fun ann.
Ord tyname =>
Term tyname name uni fun ann -> Set tyname
ftvTerm Term tyname name uni fun ann
t1 Set tyname -> Set tyname -> Set tyname
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun ann -> Set tyname
forall tyname name (uni :: * -> *) fun ann.
Ord tyname =>
Term tyname name uni fun ann -> Set tyname
ftvTerm Term tyname name uni fun ann
t2
    TyInst ann
_ Term tyname name uni fun ann
t Type tyname uni ann
ty     -> Term tyname name uni fun ann -> Set tyname
forall tyname name (uni :: * -> *) fun ann.
Ord tyname =>
Term tyname name uni fun ann -> Set tyname
ftvTerm Term tyname name uni fun ann
t Set tyname -> Set tyname -> Set tyname
forall a. Semigroup a => a -> a -> a
<> Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy Type tyname uni ann
ty
    Unwrap ann
_ Term tyname name uni fun ann
t        -> Term tyname name uni fun ann -> Set tyname
forall tyname name (uni :: * -> *) fun ann.
Ord tyname =>
Term tyname name uni fun ann -> Set tyname
ftvTerm Term tyname name uni fun ann
t
    IWrap ann
_ Type tyname uni ann
pat Type tyname uni ann
arg Term tyname name uni fun ann
t -> Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy Type tyname uni ann
pat Set tyname -> Set tyname -> Set tyname
forall a. Semigroup a => a -> a -> a
<> Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy Type tyname uni ann
arg Set tyname -> Set tyname -> Set tyname
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun ann -> Set tyname
forall tyname name (uni :: * -> *) fun ann.
Ord tyname =>
Term tyname name uni fun ann -> Set tyname
ftvTerm Term tyname name uni fun ann
t
    Error ann
_ Type tyname uni ann
ty        -> Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy Type tyname uni ann
ty
    Var{}               -> Set tyname
forall a. Monoid a => a
mempty
    Constant{}          -> Set tyname
forall a. Monoid a => a
mempty
    Builtin{}           -> Set tyname
forall a. Monoid a => a
mempty

-- | Get all the free variables in a PIR single let-binding.
fvBinding :: Ord name => Binding tyname name uni fun ann -> Set name
fvBinding :: Binding tyname name uni fun ann -> Set name
fvBinding Binding tyname name uni fun ann
b = [Set name] -> Set name
forall a. Monoid a => [a] -> a
mconcat ([Set name] -> Set name) -> [Set name] -> Set name
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann -> Set name
forall name tyname (uni :: * -> *) fun ann.
Ord name =>
Term tyname name uni fun ann -> Set name
fvTerm (Term tyname name uni fun ann -> Set name)
-> [Term tyname name uni fun ann] -> [Set name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( Binding tyname name uni fun ann
bBinding tyname name uni fun ann
-> Getting
     (Endo [Term tyname name uni fun ann])
     (Binding tyname name uni fun ann)
     (Term tyname name uni fun ann)
-> [Term tyname name uni fun ann]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^..Getting
  (Endo [Term tyname name uni fun ann])
  (Binding tyname name uni fun ann)
  (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a.
Traversal'
  (Binding tyname name uni fun a) (Term tyname name uni fun a)
bindingSubterms)

-- | Get all the free type variables in a PIR single let-binding.
ftvBinding :: forall tyname name uni fun ann.
             Ord tyname => Recursivity -> Binding tyname name uni fun ann -> Set tyname
ftvBinding :: Recursivity -> Binding tyname name uni fun ann -> Set tyname
ftvBinding Recursivity
r Binding tyname name uni fun ann
b = [Set tyname] -> Set tyname
forall a. Monoid a => [a] -> a
mconcat ([Set tyname] -> Set tyname) -> [Set tyname] -> Set tyname
forall a b. (a -> b) -> a -> b
$ [Set tyname]
ftvTs [Set tyname] -> [Set tyname] -> [Set tyname]
forall a. [a] -> [a] -> [a]
++ [Set tyname]
ftvTys
 where
    ftvTs :: [Set tyname]
ftvTs = Term tyname name uni fun ann -> Set tyname
forall tyname name (uni :: * -> *) fun ann.
Ord tyname =>
Term tyname name uni fun ann -> Set tyname
ftvTerm (Term tyname name uni fun ann -> Set tyname)
-> [Term tyname name uni fun ann] -> [Set tyname]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binding tyname name uni fun ann
bBinding tyname name uni fun ann
-> Getting
     (Endo [Term tyname name uni fun ann])
     (Binding tyname name uni fun ann)
     (Term tyname name uni fun ann)
-> [Term tyname name uni fun ann]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^..Getting
  (Endo [Term tyname name uni fun ann])
  (Binding tyname name uni fun ann)
  (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a.
Traversal'
  (Binding tyname name uni fun a) (Term tyname name uni fun a)
bindingSubterms
    ftvTys :: [Set tyname]
ftvTys = Type tyname uni ann -> Set tyname
ftvTyDataSpecial (Type tyname uni ann -> Set tyname)
-> [Type tyname uni ann] -> [Set tyname]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binding tyname name uni fun ann
bBinding tyname name uni fun ann
-> Getting
     (Endo [Type tyname uni ann])
     (Binding tyname name uni fun ann)
     (Type tyname uni ann)
-> [Type tyname uni ann]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^..Getting
  (Endo [Type tyname uni ann])
  (Binding tyname name uni fun ann)
  (Type tyname uni ann)
forall tyname name (uni :: * -> *) fun a.
Traversal' (Binding tyname name uni fun a) (Type tyname uni a)
bindingSubtypes

    -- like ftvTy but specialized for the datatypebind case
    ftvTyDataSpecial :: Type tyname uni ann -> Set tyname
    ftvTyDataSpecial :: Type tyname uni ann -> Set tyname
ftvTyDataSpecial Type tyname uni ann
ty = case Binding tyname name uni fun ann
b of
        DatatypeBind ann
_ (Datatype ann
_ TyVarDecl tyname ann
tyconstr [TyVarDecl tyname ann]
tyvars name
_ [VarDecl tyname name uni fun ann]
_) -> case Recursivity
r of
            -- for rec, both tyconstr+tyvars are in scope in *WHOLE* dataconstructors
            Recursivity
Rec -> Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy Type tyname uni ann
ty Set tyname -> Set tyname -> Set tyname
forall a. Ord a => Set a -> Set a -> Set a
\\ Getting (Set tyname) (Binding tyname name uni fun ann) tyname
-> Binding tyname name uni fun ann -> Set tyname
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set tyname) (Binding tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun a.
Traversal' (Binding tyname name uni fun a) tyname
bindingTyNames Binding tyname name uni fun ann
b
            Recursivity
NonRec ->
                let tyvarsNames :: Set tyname
tyvarsNames = Getting (Set tyname) [TyVarDecl tyname ann] tyname
-> [TyVarDecl tyname ann] -> Set tyname
forall a s. Getting (Set a) s a -> s -> Set a
setOf ((TyVarDecl tyname ann -> Const (Set tyname) (TyVarDecl tyname ann))
-> [TyVarDecl tyname ann]
-> Const (Set tyname) [TyVarDecl tyname ann]
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
traversed((TyVarDecl tyname ann
  -> Const (Set tyname) (TyVarDecl tyname ann))
 -> [TyVarDecl tyname ann]
 -> Const (Set tyname) [TyVarDecl tyname ann])
-> ((tyname -> Const (Set tyname) tyname)
    -> TyVarDecl tyname ann
    -> Const (Set tyname) (TyVarDecl tyname ann))
-> Getting (Set tyname) [TyVarDecl tyname ann] tyname
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(tyname -> Const (Set tyname) tyname)
-> TyVarDecl tyname ann
-> Const (Set tyname) (TyVarDecl tyname ann)
forall tyname1 ann tyname2.
Lens
  (TyVarDecl tyname1 ann) (TyVarDecl tyname2 ann) tyname1 tyname2
PLC.tyVarDeclName) [TyVarDecl tyname ann]
tyvars
                    ftvDom :: Set tyname
ftvDom = [Set tyname] -> Set tyname
forall a. Monoid a => [a] -> a
mconcat ([Set tyname] -> Set tyname) -> [Set tyname] -> Set tyname
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy (Type tyname uni ann -> Set tyname)
-> [Type tyname uni ann] -> [Set tyname]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> [Type tyname uni ann]
forall tyname (uni :: * -> *) a.
Type tyname uni a -> [Type tyname uni a]
funTyArgs Type tyname uni ann
ty
                    -- tyconstr is in scope *only* in the result type codomain
                    ftvCod :: Set tyname
ftvCod = Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy (Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) a.
Type tyname uni a -> Type tyname uni a
funResultType Type tyname uni ann
ty) Set tyname -> Set tyname -> Set tyname
forall a. Ord a => Set a -> Set a -> Set a
\\ ((tyname -> Const (Set tyname) tyname)
 -> TyVarDecl tyname ann
 -> Const (Set tyname) (TyVarDecl tyname ann))
-> TyVarDecl tyname ann -> Set tyname
forall a s. Getting (Set a) s a -> s -> Set a
setOf (tyname -> Const (Set tyname) tyname)
-> TyVarDecl tyname ann
-> Const (Set tyname) (TyVarDecl tyname ann)
forall tyname1 ann tyname2.
Lens
  (TyVarDecl tyname1 ann) (TyVarDecl tyname2 ann) tyname1 tyname2
PLC.tyVarDeclName TyVarDecl tyname ann
tyconstr
                -- for nonrec, the tyvars are in scope in *WHOLE* dataconstructors
                in (Set tyname
ftvDom Set tyname -> Set tyname -> Set tyname
forall a. Semigroup a => a -> a -> a
<> Set tyname
ftvCod) Set tyname -> Set tyname -> Set tyname
forall a. Ord a => Set a -> Set a -> Set a
\\ Set tyname
tyvarsNames
        Binding tyname name uni fun ann
_ -> Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy Type tyname uni ann
ty