{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}

module PlutusCore.Check.Scoping where

import PlutusCore.Name
import PlutusCore.Quote

import Control.Monad.Except
import Data.Coerce
import Data.List.NonEmpty (NonEmpty)
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict as Map
import Data.Maybe
import Data.Set as Set

{- Note [Example of a scoping check]
Consider the following type:

    \(x_42 :: *) -> x_42

This Note describes how we can use this type to check that a renamer handles scoping correctly.
Any other type could be used as well (and in property tests we generate random ones), but the type
above is the simplest example, so we're going to use it.

First, we traverse the type and freshen every single name in it, which gives us

    \(x_0 :: *) -> x_1

After this procedure all names in the new type are distinct, not just globally unique -- completely
distinct: all variables are free variables with different uniques and all bindings are distinct and
never referenced.

Now for each binder we insert one in-scope variable and one out-of-scope one by referencing them
in an added constructor (we could use 'TyFun', but we use 'TyApp', 'cause it has an analogue at the
term level -- 'Apply' and we can also reference a type variable in a 'Term' via a similar
constructor -- 'TyInst'). That gives us

    (\(x_0 :: *) -> x_1 x_0) x_0

(currently we just decorate the binder with those constructors. In future we could employ a fancier
strategy and go under to the leaves of the term being processed etc).

The next step is to annotate each name with what is supposed to happen to it once the renaming is
performed.

1. the @x_0@ binding is supposed to be renamed and hence will disappear
2. the @x_1@ variable is free, so it's supposed to stay free
3. the inner @x_0@ variable is in scope and so is supposed to be renamed
4. the outer @x_0@ is out of scope and so is free and is supposed to stay

In the actual implementation everything that we did above happens in a single definition.

After this initial scoping setup is performed, we run the provided renamer (which is not supposed
to touch any annotations) and collect all the available information: which names disappeared,
which didn't, which appeared etc, simultaneously checking that the names that were supposed to
disappear indeed disappeared and the names that were supposed to stay indeed stayed.

Once all this scoping information is collected, we run 'checkScopeInfo' to check that the
information is coherent. See its docs for the details on what exactly the checked invariants are.

The advantage of this approach is that we can pinpoint exactly where what is visible and, just
as importantly, what is not.
-}

data ScopedName
    = TypeName TyName
    | TermName Name
    deriving stock (Int -> ScopedName -> ShowS
[ScopedName] -> ShowS
ScopedName -> String
(Int -> ScopedName -> ShowS)
-> (ScopedName -> String)
-> ([ScopedName] -> ShowS)
-> Show ScopedName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ScopedName] -> ShowS
$cshowList :: [ScopedName] -> ShowS
show :: ScopedName -> String
$cshow :: ScopedName -> String
showsPrec :: Int -> ScopedName -> ShowS
$cshowsPrec :: Int -> ScopedName -> ShowS
Show, ScopedName -> ScopedName -> Bool
(ScopedName -> ScopedName -> Bool)
-> (ScopedName -> ScopedName -> Bool) -> Eq ScopedName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ScopedName -> ScopedName -> Bool
$c/= :: ScopedName -> ScopedName -> Bool
== :: ScopedName -> ScopedName -> Bool
$c== :: ScopedName -> ScopedName -> Bool
Eq, Eq ScopedName
Eq ScopedName
-> (ScopedName -> ScopedName -> Ordering)
-> (ScopedName -> ScopedName -> Bool)
-> (ScopedName -> ScopedName -> Bool)
-> (ScopedName -> ScopedName -> Bool)
-> (ScopedName -> ScopedName -> Bool)
-> (ScopedName -> ScopedName -> ScopedName)
-> (ScopedName -> ScopedName -> ScopedName)
-> Ord ScopedName
ScopedName -> ScopedName -> Bool
ScopedName -> ScopedName -> Ordering
ScopedName -> ScopedName -> ScopedName
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ScopedName -> ScopedName -> ScopedName
$cmin :: ScopedName -> ScopedName -> ScopedName
max :: ScopedName -> ScopedName -> ScopedName
$cmax :: ScopedName -> ScopedName -> ScopedName
>= :: ScopedName -> ScopedName -> Bool
$c>= :: ScopedName -> ScopedName -> Bool
> :: ScopedName -> ScopedName -> Bool
$c> :: ScopedName -> ScopedName -> Bool
<= :: ScopedName -> ScopedName -> Bool
$c<= :: ScopedName -> ScopedName -> Bool
< :: ScopedName -> ScopedName -> Bool
$c< :: ScopedName -> ScopedName -> Bool
compare :: ScopedName -> ScopedName -> Ordering
$ccompare :: ScopedName -> ScopedName -> Ordering
$cp1Ord :: Eq ScopedName
Ord)

isSameScope :: ScopedName -> ScopedName -> Bool
isSameScope :: ScopedName -> ScopedName -> Bool
isSameScope TypeName{} TypeName{} = Bool
True
isSameScope TermName{} TermName{} = Bool
True
isSameScope TypeName{} TermName{} = Bool
False
isSameScope TermName{} TypeName{} = Bool
False

-- | Staying names.
data Stays
    = StaysOutOfScopeVariable  -- ^ An out-of-scope variable does not get renamed and hence stays.
    | StaysFreeVariable        -- ^ A free variable does not get renamed and hence stays.
    deriving stock (Int -> Stays -> ShowS
[Stays] -> ShowS
Stays -> String
(Int -> Stays -> ShowS)
-> (Stays -> String) -> ([Stays] -> ShowS) -> Show Stays
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Stays] -> ShowS
$cshowList :: [Stays] -> ShowS
show :: Stays -> String
$cshow :: Stays -> String
showsPrec :: Int -> Stays -> ShowS
$cshowsPrec :: Int -> Stays -> ShowS
Show)

-- | Changing names.
data Disappears
    = DisappearsBinding   -- ^ A binding gets renamed and hence the name that it binds disappears.
    | DisappearsVariable  -- ^ A bound variable gets renamed and hence its name disappears.
    deriving stock (Int -> Disappears -> ShowS
[Disappears] -> ShowS
Disappears -> String
(Int -> Disappears -> ShowS)
-> (Disappears -> String)
-> ([Disappears] -> ShowS)
-> Show Disappears
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Disappears] -> ShowS
$cshowList :: [Disappears] -> ShowS
show :: Disappears -> String
$cshow :: Disappears -> String
showsPrec :: Int -> Disappears -> ShowS
$cshowsPrec :: Int -> Disappears -> ShowS
Show)

-- | A name either stays or disappears.
data NameAction
    = Stays Stays
    | Disappears Disappears
    deriving stock (Int -> NameAction -> ShowS
[NameAction] -> ShowS
NameAction -> String
(Int -> NameAction -> ShowS)
-> (NameAction -> String)
-> ([NameAction] -> ShowS)
-> Show NameAction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NameAction] -> ShowS
$cshowList :: [NameAction] -> ShowS
show :: NameAction -> String
$cshow :: NameAction -> String
showsPrec :: Int -> NameAction -> ShowS
$cshowsPrec :: Int -> NameAction -> ShowS
Show)

data NameAnn
    = NameAction NameAction ScopedName
    | NotAName
    deriving stock (Int -> NameAnn -> ShowS
[NameAnn] -> ShowS
NameAnn -> String
(Int -> NameAnn -> ShowS)
-> (NameAnn -> String) -> ([NameAnn] -> ShowS) -> Show NameAnn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NameAnn] -> ShowS
$cshowList :: [NameAnn] -> ShowS
show :: NameAnn -> String
$cshow :: NameAnn -> String
showsPrec :: Int -> NameAnn -> ShowS
$cshowsPrec :: Int -> NameAnn -> ShowS
Show)

class ToScopedName name where
    toScopedName :: name -> ScopedName

instance ToScopedName TyName where
    toScopedName :: TyName -> ScopedName
toScopedName = TyName -> ScopedName
TypeName

instance ToScopedName Name where
    toScopedName :: Name -> ScopedName
toScopedName = Name -> ScopedName
TermName

-- Naming: @introduce*@ for bindings and @register*@ for variables.

-- | Annotation for a binding saying \"supposed to disappear\".
introduceBound :: ToScopedName name => name -> NameAnn
introduceBound :: name -> NameAnn
introduceBound = NameAction -> ScopedName -> NameAnn
NameAction (Disappears -> NameAction
Disappears Disappears
DisappearsBinding) (ScopedName -> NameAnn) -> (name -> ScopedName) -> name -> NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. name -> ScopedName
forall name. ToScopedName name => name -> ScopedName
toScopedName

-- | Annotation for a bound variable saying \"supposed to disappear\".
registerBound :: ToScopedName name => name -> NameAnn
registerBound :: name -> NameAnn
registerBound = NameAction -> ScopedName -> NameAnn
NameAction (Disappears -> NameAction
Disappears Disappears
DisappearsVariable) (ScopedName -> NameAnn) -> (name -> ScopedName) -> name -> NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. name -> ScopedName
forall name. ToScopedName name => name -> ScopedName
toScopedName

-- | Annotation for an out-of-scope variable saying \"supposed to stay out of scope\".
registerOutOfScope :: ToScopedName name => name -> NameAnn
registerOutOfScope :: name -> NameAnn
registerOutOfScope = NameAction -> ScopedName -> NameAnn
NameAction (Stays -> NameAction
Stays Stays
StaysOutOfScopeVariable) (ScopedName -> NameAnn) -> (name -> ScopedName) -> name -> NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. name -> ScopedName
forall name. ToScopedName name => name -> ScopedName
toScopedName

-- | Annotation for a free variable saying \"supposed to stay free\".
registerFree :: ToScopedName name => name -> NameAnn
registerFree :: name -> NameAnn
registerFree = NameAction -> ScopedName -> NameAnn
NameAction (Stays -> NameAction
Stays Stays
StaysFreeVariable) (ScopedName -> NameAnn) -> (name -> ScopedName) -> name -> NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. name -> ScopedName
forall name. ToScopedName name => name -> ScopedName
toScopedName

class Reference n t where
    -- | Take a registering function, apply it to the provided name, create a type\/term variable
    -- out of the resulting annotation and the original name and reference that variable in the
    -- provided type\/term by prepending a constructor to it mentioning the variable.
    referenceVia
        :: (forall name. ToScopedName name => name -> NameAnn)
        -> n
        -> t NameAnn
        -> t NameAnn

-- | Reference the provided variable in the provided type\/term as an in-scope one.
referenceBound :: Reference n t => n -> t NameAnn -> t NameAnn
referenceBound :: n -> t NameAnn -> t NameAnn
referenceBound = (forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
registerBound

-- | Reference the provided variable in the provided type\/term as an out-of-scope one.
referenceOutOfScope :: Reference n t => n -> t NameAnn -> t NameAnn
referenceOutOfScope :: n -> t NameAnn -> t NameAnn
referenceOutOfScope = (forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
registerOutOfScope

-- #####################################################
-- ## Information about scopes and relevant functions ##
-- #####################################################

-- | Each kind of old and new names.
data ScopeEntry
    = DisappearedBindings
    | DisappearedVariables
    | AppearedBindings
    | AppearedVariables
    | StayedOutOfScopeVariables
    | StayedFreeVariables
    deriving stock (Int -> ScopeEntry -> ShowS
[ScopeEntry] -> ShowS
ScopeEntry -> String
(Int -> ScopeEntry -> ShowS)
-> (ScopeEntry -> String)
-> ([ScopeEntry] -> ShowS)
-> Show ScopeEntry
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ScopeEntry] -> ShowS
$cshowList :: [ScopeEntry] -> ShowS
show :: ScopeEntry -> String
$cshow :: ScopeEntry -> String
showsPrec :: Int -> ScopeEntry -> ShowS
$cshowsPrec :: Int -> ScopeEntry -> ShowS
Show, ScopeEntry -> ScopeEntry -> Bool
(ScopeEntry -> ScopeEntry -> Bool)
-> (ScopeEntry -> ScopeEntry -> Bool) -> Eq ScopeEntry
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ScopeEntry -> ScopeEntry -> Bool
$c/= :: ScopeEntry -> ScopeEntry -> Bool
== :: ScopeEntry -> ScopeEntry -> Bool
$c== :: ScopeEntry -> ScopeEntry -> Bool
Eq, Eq ScopeEntry
Eq ScopeEntry
-> (ScopeEntry -> ScopeEntry -> Ordering)
-> (ScopeEntry -> ScopeEntry -> Bool)
-> (ScopeEntry -> ScopeEntry -> Bool)
-> (ScopeEntry -> ScopeEntry -> Bool)
-> (ScopeEntry -> ScopeEntry -> Bool)
-> (ScopeEntry -> ScopeEntry -> ScopeEntry)
-> (ScopeEntry -> ScopeEntry -> ScopeEntry)
-> Ord ScopeEntry
ScopeEntry -> ScopeEntry -> Bool
ScopeEntry -> ScopeEntry -> Ordering
ScopeEntry -> ScopeEntry -> ScopeEntry
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ScopeEntry -> ScopeEntry -> ScopeEntry
$cmin :: ScopeEntry -> ScopeEntry -> ScopeEntry
max :: ScopeEntry -> ScopeEntry -> ScopeEntry
$cmax :: ScopeEntry -> ScopeEntry -> ScopeEntry
>= :: ScopeEntry -> ScopeEntry -> Bool
$c>= :: ScopeEntry -> ScopeEntry -> Bool
> :: ScopeEntry -> ScopeEntry -> Bool
$c> :: ScopeEntry -> ScopeEntry -> Bool
<= :: ScopeEntry -> ScopeEntry -> Bool
$c<= :: ScopeEntry -> ScopeEntry -> Bool
< :: ScopeEntry -> ScopeEntry -> Bool
$c< :: ScopeEntry -> ScopeEntry -> Bool
compare :: ScopeEntry -> ScopeEntry -> Ordering
$ccompare :: ScopeEntry -> ScopeEntry -> Ordering
$cp1Ord :: Eq ScopeEntry
Ord)

-- | A 'ScopeInfo' is a set of 'ScopedName's for each of the 'ScopeEntry'.
-- If a 'ScopeEntry' is not present in the map, the corresponding set of 'ScopeName's is considered
-- to be empty.
newtype ScopeInfo = ScopeInfo
    { ScopeInfo -> Map ScopeEntry (Set ScopedName)
unScopeInfo :: Map ScopeEntry (Set ScopedName)
    } deriving stock (Int -> ScopeInfo -> ShowS
[ScopeInfo] -> ShowS
ScopeInfo -> String
(Int -> ScopeInfo -> ShowS)
-> (ScopeInfo -> String)
-> ([ScopeInfo] -> ShowS)
-> Show ScopeInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ScopeInfo] -> ShowS
$cshowList :: [ScopeInfo] -> ShowS
show :: ScopeInfo -> String
$cshow :: ScopeInfo -> String
showsPrec :: Int -> ScopeInfo -> ShowS
$cshowsPrec :: Int -> ScopeInfo -> ShowS
Show)

-- | Extract the set stored in the provided 'ScopeInfo' at the provided 'ScopeEntry'.
to :: ScopeEntry -> ScopeInfo -> Set ScopedName
to :: ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
entry = Set ScopedName -> Maybe (Set ScopedName) -> Set ScopedName
forall a. a -> Maybe a -> a
fromMaybe Set ScopedName
forall a. Set a
Set.empty (Maybe (Set ScopedName) -> Set ScopedName)
-> (ScopeInfo -> Maybe (Set ScopedName))
-> ScopeInfo
-> Set ScopedName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeEntry
-> Map ScopeEntry (Set ScopedName) -> Maybe (Set ScopedName)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ScopeEntry
entry (Map ScopeEntry (Set ScopedName) -> Maybe (Set ScopedName))
-> (ScopeInfo -> Map ScopeEntry (Set ScopedName))
-> ScopeInfo
-> Maybe (Set ScopedName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> Map ScopeEntry (Set ScopedName)
unScopeInfo

emptyScopeInfo :: ScopeInfo
emptyScopeInfo :: ScopeInfo
emptyScopeInfo = Map ScopeEntry (Set ScopedName) -> ScopeInfo
ScopeInfo Map ScopeEntry (Set ScopedName)
forall k a. Map k a
Map.empty

-- | Check if a set is empty and report an error with the set embedded in it otherwise.
checkEmpty :: (Set ScopedName -> ScopeError) -> Set ScopedName -> Either ScopeError ()
checkEmpty :: (Set ScopedName -> ScopeError)
-> Set ScopedName -> Either ScopeError ()
checkEmpty Set ScopedName -> ScopeError
err Set ScopedName
s = Bool -> Either ScopeError () -> Either ScopeError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set ScopedName -> Bool
forall a. Set a -> Bool
Set.null Set ScopedName
s) (Either ScopeError () -> Either ScopeError ())
-> (ScopeError -> Either ScopeError ())
-> ScopeError
-> Either ScopeError ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeError -> Either ScopeError ()
forall a b. a -> Either a b
Left (ScopeError -> Either ScopeError ())
-> ScopeError -> Either ScopeError ()
forall a b. (a -> b) -> a -> b
$ Set ScopedName -> ScopeError
err Set ScopedName
s

-- | Merge two 'ScopeInfo's checking that they do not intersect along the way.
mergeScopeInfo :: ScopeInfo -> ScopeInfo -> Either ScopeError ScopeInfo
mergeScopeInfo :: ScopeInfo -> ScopeInfo -> Either ScopeError ScopeInfo
mergeScopeInfo ScopeInfo
si1 ScopeInfo
si2 = do
    let disappearedBindings1 :: Set ScopedName
disappearedBindings1 = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
DisappearedBindings ScopeInfo
si1
        disappearedBindings2 :: Set ScopedName
disappearedBindings2 = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
DisappearedBindings ScopeInfo
si2
        appearedBindings1 :: Set ScopedName
appearedBindings1    = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
AppearedBindings    ScopeInfo
si1
        appearedBindings2 :: Set ScopedName
appearedBindings2    = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
AppearedBindings    ScopeInfo
si2
        duplicateDisappearedBindings :: Set ScopedName
duplicateDisappearedBindings = Set ScopedName
disappearedBindings1 Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set ScopedName
disappearedBindings2
        duplicateAppearedBindings :: Set ScopedName
duplicateAppearedBindings    = Set ScopedName
appearedBindings1    Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set ScopedName
appearedBindings2
    (Set ScopedName -> ScopeError)
-> Set ScopedName -> Either ScopeError ()
checkEmpty Set ScopedName -> ScopeError
DuplicateBindersInTheInput  Set ScopedName
duplicateDisappearedBindings
    (Set ScopedName -> ScopeError)
-> Set ScopedName -> Either ScopeError ()
checkEmpty Set ScopedName -> ScopeError
DuplicateBindersInTheOutput Set ScopedName
duplicateAppearedBindings
    ScopeInfo -> Either ScopeError ScopeInfo
forall a b. b -> Either a b
Right (ScopeInfo -> Either ScopeError ScopeInfo)
-> ScopeInfo -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ (Map ScopeEntry (Set ScopedName)
 -> Map ScopeEntry (Set ScopedName)
 -> Map ScopeEntry (Set ScopedName))
-> ScopeInfo -> ScopeInfo -> ScopeInfo
coerce ((Set ScopedName -> Set ScopedName -> Set ScopedName)
-> Map ScopeEntry (Set ScopedName)
-> Map ScopeEntry (Set ScopedName)
-> Map ScopeEntry (Set ScopedName)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
Set.union) ScopeInfo
si1 ScopeInfo
si2

-- @newtype@-ing it for the sake of providing very convenient 'Semigroup' and 'Monoid' instances.
newtype ScopeErrorOrInfo = ScopeErrorOrInfo
    -- We might want to use @Validation@ or something instead of 'Either'.
    { ScopeErrorOrInfo -> Either ScopeError ScopeInfo
unScopeErrorOrInfo :: Either ScopeError ScopeInfo
    }

instance Semigroup ScopeErrorOrInfo where
    ScopeErrorOrInfo Either ScopeError ScopeInfo
errOrInfo1 <> :: ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
<> ScopeErrorOrInfo Either ScopeError ScopeInfo
errOrInfo2 =
        Either ScopeError ScopeInfo -> ScopeErrorOrInfo
ScopeErrorOrInfo (Either ScopeError ScopeInfo -> ScopeErrorOrInfo)
-> (Either ScopeError (Either ScopeError ScopeInfo)
    -> Either ScopeError ScopeInfo)
-> Either ScopeError (Either ScopeError ScopeInfo)
-> ScopeErrorOrInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either ScopeError (Either ScopeError ScopeInfo)
-> Either ScopeError ScopeInfo
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Either ScopeError (Either ScopeError ScopeInfo)
 -> ScopeErrorOrInfo)
-> Either ScopeError (Either ScopeError ScopeInfo)
-> ScopeErrorOrInfo
forall a b. (a -> b) -> a -> b
$ ScopeInfo -> ScopeInfo -> Either ScopeError ScopeInfo
mergeScopeInfo (ScopeInfo -> ScopeInfo -> Either ScopeError ScopeInfo)
-> Either ScopeError ScopeInfo
-> Either ScopeError (ScopeInfo -> Either ScopeError ScopeInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either ScopeError ScopeInfo
errOrInfo1 Either ScopeError (ScopeInfo -> Either ScopeError ScopeInfo)
-> Either ScopeError ScopeInfo
-> Either ScopeError (Either ScopeError ScopeInfo)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Either ScopeError ScopeInfo
errOrInfo2

instance Monoid ScopeErrorOrInfo where
    mempty :: ScopeErrorOrInfo
mempty = Either ScopeError ScopeInfo -> ScopeErrorOrInfo
ScopeErrorOrInfo (Either ScopeError ScopeInfo -> ScopeErrorOrInfo)
-> Either ScopeError ScopeInfo -> ScopeErrorOrInfo
forall a b. (a -> b) -> a -> b
$ ScopeInfo -> Either ScopeError ScopeInfo
forall a b. b -> Either a b
Right ScopeInfo
emptyScopeInfo

-- ########################################################################
-- ## Main class for collecting scope information and relevant functions ##
-- ########################################################################

class EstablishScoping t where
    {-| Traverse a 't' freshening every name (both at the binding and the use sites)
    and annotating the freshened names with either 'DisappearsBinding' or 'StaysFreeVariable'
    depending on whether the name occurs at the binding or the use site.

    In addition to that every binder should be decorated with one out-of-scope variable (annotated
    with 'StaysOutOfScopeVariable') and one in-scope one (annotated with 'DisappearsVariable').

    Note that no original name occurring in 't' should survive this procedure (and hence we don't
    care if any of the freshened names clashes with an original one as all original ones are
    supposed to be gone).

    How to provide an implementation:

    1. handle bindings with 'freshen*Name' + 'establishScopingBinder' (or similar)
    2. handle variables with 'freshen*Name' + 'registerFree'
    3. everything else is direct recursion + 'Applicative' stuff
    -}
    establishScoping :: t ann -> Quote (t NameAnn)

-- That will retraverse the same type multiple times. Should we have @referenceListVia@ as a
-- primitive instead and derive 'referenceVia' in terms of it for better performance?
-- Should we only pick an arbitrary sublist of the provided list instead of using the whole list
-- for better performance? That requires enhancing 'Reference' with @Hedgehog.Gen@ or something.
instance Reference n t => Reference [n] t where
    referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> [n] -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg = (t NameAnn -> [n] -> t NameAnn) -> [n] -> t NameAnn -> t NameAnn
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((t NameAnn -> [n] -> t NameAnn) -> [n] -> t NameAnn -> t NameAnn)
-> ((n -> t NameAnn -> t NameAnn) -> t NameAnn -> [n] -> t NameAnn)
-> (n -> t NameAnn -> t NameAnn)
-> [n]
-> t NameAnn
-> t NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n -> t NameAnn -> t NameAnn) -> t NameAnn -> [n] -> t NameAnn
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Prelude.foldr ((n -> t NameAnn -> t NameAnn) -> [n] -> t NameAnn -> t NameAnn)
-> (n -> t NameAnn -> t NameAnn) -> [n] -> t NameAnn -> t NameAnn
forall a b. (a -> b) -> a -> b
$ (forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg

instance Reference n t => Reference (NonEmpty n) t where
    referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> NonEmpty n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg = (forall name. ToScopedName name => name -> NameAnn)
-> [n] -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg ([n] -> t NameAnn -> t NameAnn)
-> (NonEmpty n -> [n]) -> NonEmpty n -> t NameAnn -> t NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty n -> [n]
forall a. NonEmpty a -> [a]
NonEmpty.toList

-- Given that it's straightforward to provide an implementation for the method,
-- it would be nice to somehow do that generically by default.
class CollectScopeInfo t where
    {-| Collect scoping information after scoping was established and renaming was performed.

    How to provide an implementation:

    1. handle names (both bindings and variables) with 'handleSname'
    2. everything else is direct recursion + 'Monoid' stuff
    -}
    collectScopeInfo :: t NameAnn -> ScopeErrorOrInfo

-- See Note [Example of a scoping check].
type Scoping t = (EstablishScoping t, CollectScopeInfo t)

-- | Take a constructor for a binder, a name bound by it, a sort (kind\/type), a value of that sort
-- (type\/term) and call 'establishScoping' on both the sort and its value and reassemble the
-- original binder with the annotated sort and its value, but also decorate the reassembled binder
-- with one out-of-scope variable and one in-scope one.
establishScopingBinder
    :: (Reference name value, ToScopedName name, Scoping sort, Scoping value)
    => (NameAnn -> name -> sort NameAnn -> value NameAnn -> value NameAnn)
    -> name
    -> sort ann
    -> value ann
    -> Quote (value NameAnn)
establishScopingBinder :: (NameAnn -> name -> sort NameAnn -> value NameAnn -> value NameAnn)
-> name -> sort ann -> value ann -> Quote (value NameAnn)
establishScopingBinder NameAnn -> name -> sort NameAnn -> value NameAnn -> value NameAnn
binder name
name sort ann
sort value ann
value = do
    sort NameAnn
sortS <- sort ann -> Quote (sort NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping sort ann
sort
    name -> value NameAnn -> value NameAnn
forall n (t :: * -> *).
Reference n t =>
n -> t NameAnn -> t NameAnn
referenceOutOfScope name
name (value NameAnn -> value NameAnn)
-> (value NameAnn -> value NameAnn)
-> value NameAnn
-> value NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        NameAnn -> name -> sort NameAnn -> value NameAnn -> value NameAnn
binder (name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
introduceBound name
name) name
name sort NameAnn
sortS (value NameAnn -> value NameAnn)
-> (value NameAnn -> value NameAnn)
-> value NameAnn
-> value NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            name -> value NameAnn -> value NameAnn
forall n (t :: * -> *).
Reference n t =>
n -> t NameAnn -> t NameAnn
referenceBound name
name (value NameAnn -> value NameAnn)
-> Quote (value NameAnn) -> Quote (value NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                value ann -> Quote (value NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping value ann
value

-- #############################################
-- ## Checking coherence of scope information ##
-- #############################################

-- | Every kind of error thrown by the scope checking machinery at different stages.
data ScopeError
    = UnannotatedName ScopedName
    | NameChangedItsScope ScopedName ScopedName
    | NameUnexpectedlyDisappeared ScopedName ScopedName
    | NameUnexpectedlyStayed ScopedName
    | DuplicateBindersInTheInput (Set ScopedName)
    | DuplicateBindersInTheOutput (Set ScopedName)
    | OldBindingsDiscordWithBoundVariables (Set ScopedName)
    | OldBindingsDiscordWithOutOfScopeVariables (Set ScopedName)
    | NewBindingsDiscordWithBoundVariables (Set ScopedName)
    | OldBindingsClashWithFreeVariables (Set ScopedName)
    | OldBindingsClashWithNewBindings (Set ScopedName)
    | NewBindingsClashWithFreeVariabes (Set ScopedName)
    deriving stock (Int -> ScopeError -> ShowS
[ScopeError] -> ShowS
ScopeError -> String
(Int -> ScopeError -> ShowS)
-> (ScopeError -> String)
-> ([ScopeError] -> ShowS)
-> Show ScopeError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ScopeError] -> ShowS
$cshowList :: [ScopeError] -> ShowS
show :: ScopeError -> String
$cshow :: ScopeError -> String
showsPrec :: Int -> ScopeError -> ShowS
$cshowsPrec :: Int -> ScopeError -> ShowS
Show)

-- | Override the set at the provided 'ScopeEntry' to contain only the provided 'ScopedName'.
overrideSname :: ScopeEntry -> ScopedName -> ScopeInfo -> ScopeInfo
overrideSname :: ScopeEntry -> ScopedName -> ScopeInfo -> ScopeInfo
overrideSname ScopeEntry
key = (Map ScopeEntry (Set ScopedName)
 -> Map ScopeEntry (Set ScopedName))
-> ScopeInfo -> ScopeInfo
coerce ((Map ScopeEntry (Set ScopedName)
  -> Map ScopeEntry (Set ScopedName))
 -> ScopeInfo -> ScopeInfo)
-> (ScopedName
    -> Map ScopeEntry (Set ScopedName)
    -> Map ScopeEntry (Set ScopedName))
-> ScopedName
-> ScopeInfo
-> ScopeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeEntry
-> Set ScopedName
-> Map ScopeEntry (Set ScopedName)
-> Map ScopeEntry (Set ScopedName)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ScopeEntry
key (Set ScopedName
 -> Map ScopeEntry (Set ScopedName)
 -> Map ScopeEntry (Set ScopedName))
-> (ScopedName -> Set ScopedName)
-> ScopedName
-> Map ScopeEntry (Set ScopedName)
-> Map ScopeEntry (Set ScopedName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopedName -> Set ScopedName
forall a. a -> Set a
Set.singleton

-- | Use a 'Stays' to handle an unchanged old name.
applyStays :: Stays -> ScopedName -> ScopeInfo
applyStays :: Stays -> ScopedName -> ScopeInfo
applyStays Stays
stays ScopedName
sname = ScopeEntry -> ScopedName -> ScopeInfo -> ScopeInfo
overrideSname ScopeEntry
key ScopedName
sname ScopeInfo
emptyScopeInfo where
    key :: ScopeEntry
key = case Stays
stays of
        Stays
StaysOutOfScopeVariable -> ScopeEntry
StayedOutOfScopeVariables
        Stays
StaysFreeVariable       -> ScopeEntry
StayedFreeVariables

-- | Use a 'Disappears' to handle differing old and new names.
applyDisappears :: Disappears -> ScopedName -> ScopedName -> ScopeInfo
applyDisappears :: Disappears -> ScopedName -> ScopedName -> ScopeInfo
applyDisappears Disappears
disappears ScopedName
snameOld ScopedName
snameNew =
    ScopeEntry -> ScopedName -> ScopeInfo -> ScopeInfo
overrideSname ScopeEntry
keyNew ScopedName
snameNew (ScopeInfo -> ScopeInfo) -> ScopeInfo -> ScopeInfo
forall a b. (a -> b) -> a -> b
$ ScopeEntry -> ScopedName -> ScopeInfo -> ScopeInfo
overrideSname ScopeEntry
keyOld ScopedName
snameOld ScopeInfo
emptyScopeInfo where
        (ScopeEntry
keyOld, ScopeEntry
keyNew) = case Disappears
disappears of
            Disappears
DisappearsBinding  -> (ScopeEntry
DisappearedBindings, ScopeEntry
AppearedBindings)
            Disappears
DisappearsVariable -> (ScopeEntry
DisappearedVariables, ScopeEntry
AppearedVariables)

-- | Use a 'NameAction' to handle an old and a new name.
applyNameAction
    :: NameAction -> ScopedName -> ScopedName -> Either ScopeError ScopeInfo
applyNameAction :: NameAction
-> ScopedName -> ScopedName -> Either ScopeError ScopeInfo
applyNameAction (Stays Stays
stays) ScopedName
snameOld ScopedName
snameNew
    | ScopedName
snameOld ScopedName -> ScopedName -> Bool
forall a. Eq a => a -> a -> Bool
== ScopedName
snameNew = ScopeInfo -> Either ScopeError ScopeInfo
forall a b. b -> Either a b
Right (ScopeInfo -> Either ScopeError ScopeInfo)
-> ScopeInfo -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ Stays -> ScopedName -> ScopeInfo
applyStays Stays
stays ScopedName
snameOld
    | Bool
otherwise            = ScopeError -> Either ScopeError ScopeInfo
forall a b. a -> Either a b
Left (ScopeError -> Either ScopeError ScopeInfo)
-> ScopeError -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ ScopedName -> ScopedName -> ScopeError
NameUnexpectedlyDisappeared ScopedName
snameOld ScopedName
snameNew
applyNameAction (Disappears Disappears
disappears) ScopedName
snameOld ScopedName
snameNew
    | ScopedName
snameOld ScopedName -> ScopedName -> Bool
forall a. Eq a => a -> a -> Bool
== ScopedName
snameNew = ScopeError -> Either ScopeError ScopeInfo
forall a b. a -> Either a b
Left (ScopeError -> Either ScopeError ScopeInfo)
-> ScopeError -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ ScopedName -> ScopeError
NameUnexpectedlyStayed ScopedName
snameOld
    | Bool
otherwise            = ScopeInfo -> Either ScopeError ScopeInfo
forall a b. b -> Either a b
Right (ScopeInfo -> Either ScopeError ScopeInfo)
-> ScopeInfo -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ Disappears -> ScopedName -> ScopedName -> ScopeInfo
applyDisappears Disappears
disappears ScopedName
snameOld ScopedName
snameNew

-- | Use a 'NameAnn' to handle a new name.
handleSname :: ToScopedName name => NameAnn -> name -> ScopeErrorOrInfo
handleSname :: NameAnn -> name -> ScopeErrorOrInfo
handleSname NameAnn
ann name
nameNew = Either ScopeError ScopeInfo -> ScopeErrorOrInfo
ScopeErrorOrInfo (Either ScopeError ScopeInfo -> ScopeErrorOrInfo)
-> Either ScopeError ScopeInfo -> ScopeErrorOrInfo
forall a b. (a -> b) -> a -> b
$ do
    let snameNew :: ScopedName
snameNew = name -> ScopedName
forall name. ToScopedName name => name -> ScopedName
toScopedName name
nameNew
    case NameAnn
ann of
        NameAnn
NotAName -> ScopeError -> Either ScopeError ScopeInfo
forall a b. a -> Either a b
Left (ScopeError -> Either ScopeError ScopeInfo)
-> ScopeError -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ ScopedName -> ScopeError
UnannotatedName ScopedName
snameNew
        NameAction NameAction
action ScopedName
snameOld ->
            if ScopedName
snameOld ScopedName -> ScopedName -> Bool
`isSameScope` ScopedName
snameNew
                then NameAction
-> ScopedName -> ScopedName -> Either ScopeError ScopeInfo
applyNameAction NameAction
action ScopedName
snameOld ScopedName
snameNew
                else ScopeError -> Either ScopeError ScopeInfo
forall a b. a -> Either a b
Left (ScopeError -> Either ScopeError ScopeInfo)
-> ScopeError -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ ScopedName -> ScopedName -> ScopeError
NameChangedItsScope ScopedName
snameOld ScopedName
snameNew

symmetricDifference :: Ord a => Set a -> Set a -> Set a
symmetricDifference :: Set a -> Set a -> Set a
symmetricDifference Set a
s Set a
t = (Set a
s Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set a
t) Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` (Set a
s Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set a
t)

{-| Check that each kind of 'Set' from 'ScopeInfo' relates to all other ones in a certain way.
We start with these three relations that are based on the assumption that for each binder we add
at least one out-of-scope variable and at least one in-scope one:

1. disappeared bindings should be the same as stayed out of scope variables
     (an internal sanity check)
2. disappeared bindings should be the same as disappeared variables
     (ensures that old names consistently disappear at the binding and use sites)
3. appeared bindings should be the same as appeared variables
     (ensures that new names consistently appear at the binding and use sites)

Once we've ensured all of that, we're left with only three sets and 3C2 equals 3,
so we only need to consider three more relations:

1. disappeared bindings should not intersect with free variables
     (an internal sanity check)
2. appeared bindings should not intersect with disappeared bindings
3. appeared bindings should not intersect with free variables

The last two ensure that no new name has an old name's unique.
-}
checkScopeInfo :: ScopeInfo -> Either ScopeError ()
checkScopeInfo :: ScopeInfo -> Either ScopeError ()
checkScopeInfo ScopeInfo
scopeInfo = do
    let disappearedBindings :: Set ScopedName
disappearedBindings       = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
DisappearedBindings       ScopeInfo
scopeInfo
        disappearedVariables :: Set ScopedName
disappearedVariables      = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
DisappearedVariables      ScopeInfo
scopeInfo
        appearedBindings :: Set ScopedName
appearedBindings          = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
AppearedBindings          ScopeInfo
scopeInfo
        appearedVariables :: Set ScopedName
appearedVariables         = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
AppearedVariables         ScopeInfo
scopeInfo
        stayedOutOfScopeVariables :: Set ScopedName
stayedOutOfScopeVariables = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
StayedOutOfScopeVariables ScopeInfo
scopeInfo
        stayedFreeVariables :: Set ScopedName
stayedFreeVariables       = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
StayedFreeVariables       ScopeInfo
scopeInfo
    (Set ScopedName -> ScopeError)
-> Set ScopedName -> Either ScopeError ()
checkEmpty Set ScopedName -> ScopeError
OldBindingsDiscordWithOutOfScopeVariables (Set ScopedName -> Either ScopeError ())
-> Set ScopedName -> Either ScopeError ()
forall a b. (a -> b) -> a -> b
$
        Set ScopedName
disappearedBindings Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
`symmetricDifference` Set ScopedName
stayedOutOfScopeVariables
    (Set ScopedName -> ScopeError)
-> Set ScopedName -> Either ScopeError ()
checkEmpty Set ScopedName -> ScopeError
OldBindingsDiscordWithBoundVariables (Set ScopedName -> Either ScopeError ())
-> Set ScopedName -> Either ScopeError ()
forall a b. (a -> b) -> a -> b
$
        Set ScopedName
disappearedBindings Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
`symmetricDifference` Set ScopedName
disappearedVariables
    (Set ScopedName -> ScopeError)
-> Set ScopedName -> Either ScopeError ()
checkEmpty Set ScopedName -> ScopeError
NewBindingsDiscordWithBoundVariables (Set ScopedName -> Either ScopeError ())
-> Set ScopedName -> Either ScopeError ()
forall a b. (a -> b) -> a -> b
$
        Set ScopedName
appearedBindings Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
`symmetricDifference` Set ScopedName
appearedVariables
    (Set ScopedName -> ScopeError)
-> Set ScopedName -> Either ScopeError ()
checkEmpty Set ScopedName -> ScopeError
OldBindingsClashWithFreeVariables (Set ScopedName -> Either ScopeError ())
-> Set ScopedName -> Either ScopeError ()
forall a b. (a -> b) -> a -> b
$
        Set ScopedName
disappearedBindings Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set ScopedName
stayedFreeVariables
    (Set ScopedName -> ScopeError)
-> Set ScopedName -> Either ScopeError ()
checkEmpty Set ScopedName -> ScopeError
OldBindingsClashWithNewBindings (Set ScopedName -> Either ScopeError ())
-> Set ScopedName -> Either ScopeError ()
forall a b. (a -> b) -> a -> b
$
        Set ScopedName
appearedBindings  Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set ScopedName
disappearedBindings
    (Set ScopedName -> ScopeError)
-> Set ScopedName -> Either ScopeError ()
checkEmpty Set ScopedName -> ScopeError
NewBindingsClashWithFreeVariabes (Set ScopedName -> Either ScopeError ())
-> Set ScopedName -> Either ScopeError ()
forall a b. (a -> b) -> a -> b
$
        Set ScopedName
appearedBindings Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set ScopedName
stayedFreeVariables

-- See Note [Example of a scoping check].
-- | Check if a renamer respects scoping.
checkRespectsScoping :: Scoping t => (t NameAnn -> t NameAnn) -> t ann -> Either ScopeError ()
checkRespectsScoping :: (t NameAnn -> t NameAnn) -> t ann -> Either ScopeError ()
checkRespectsScoping t NameAnn -> t NameAnn
ren =
    ScopeInfo -> Either ScopeError ()
checkScopeInfo (ScopeInfo -> Either ScopeError ())
-> (t ann -> Either ScopeError ScopeInfo)
-> t ann
-> Either ScopeError ()
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ScopeErrorOrInfo -> Either ScopeError ScopeInfo
unScopeErrorOrInfo (ScopeErrorOrInfo -> Either ScopeError ScopeInfo)
-> (t ann -> ScopeErrorOrInfo)
-> t ann
-> Either ScopeError ScopeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo (t NameAnn -> ScopeErrorOrInfo)
-> (t ann -> t NameAnn) -> t ann -> ScopeErrorOrInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t NameAnn -> t NameAnn
ren (t NameAnn -> t NameAnn)
-> (t ann -> t NameAnn) -> t ann -> t NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quote (t NameAnn) -> t NameAnn
forall a. Quote a -> a
runQuote (Quote (t NameAnn) -> t NameAnn)
-> (t ann -> Quote (t NameAnn)) -> t ann -> t NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t ann -> Quote (t NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping