free-foil 0.6.0 → 0.6.1

raw patch · 16 files changed

+1522/−1078 lines, 16 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• ChangeLog.md +31/−0
• free-foil.cabal +4/−2
• src/Control/Monad/Foil.hs +8/−8
• src/Control/Monad/Foil/Internal.hs +9/−5
• src/Control/Monad/Foil/TH/MkFoilData.hs +1/−1
• src/Control/Monad/Foil/TH/MkInstancesFoil.hs +14/−14
• src/Control/Monad/Foil/Telescope.hs +3/−2
• src/Control/Monad/Free/Foil.hs +61/−1000
• src/Control/Monad/Free/Foil/Binary.hs +1/−1
• src/Control/Monad/Free/Foil/Internal.hs +1222/−0
• src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs +25/−25
• src/Data/ZipMatchK.hs +7/−15
• test/Control/Monad/Free/Foil/AlphaEquivSpec.hs +58/−1
• test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs +3/−3
• test/Control/Monad/Free/Foil/UnresolvedNamesSpec.hs +74/−0
• test/laws/Control/Monad/Free/Foil/Laws.hs +1/−1

@@ -1,5 +1,36 @@ # CHANGELOG for `free-foil` +# 0.6.1 — 2026-10-27++This release lets `substitute`, `alphaEquiv` and `unsafeEqAST` specialise in client code, and fixes problems found by an audit of the documentation. One of the fixes changes the types of `unsinkAST` and `nameSetSubsetOfScope`, described first.++Breaking changes:++- `unsinkAST` requires `DExt n l` instead of `Distinct l`, and `nameSetSubsetOfScope` requires `Ext n l`: the scope `l` of the term (or set) must extend the scope `n` it is restricted to. Both compare raw identifiers, which identify a name only within one chain of scope extensions, so with unrelated scopes the answer was meaningless (see [#127](https://github.com/fizruk/free-foil/pull/127)).+  - To migrate, bring `Ext n l` into scope where it is missing, e.g. with `assertExt` on the binder that leads from `n` to `l`, or from `withFresh` and `withThinnedNameBinderList`, which provide it.++Changed:++- `zipMatchWith1`, `zipMatch1`, `zipMatchWith2` and `zipMatch2` no longer require `Traversable` (or `Bitraversable`). `alphaEquiv`, `unsafeEqAST` and the functions behind them no longer require `Bitraversable` or `SinkableK`, and `alphaEquivRefreshed` requires `Bifunctor` instead of `Bitraversable`. None of them used these instances (see [#125](https://github.com/fizruk/free-foil/pull/125)).++Fixes:++- `alphaEquivRefreshed` compares patterns with `unifyPatternsIn`, as `alphaEquiv` does (through the new `unsafeEqASTIn`). It compared them with `unifyPatterns`, which compares binders only, so it accepted terms whose binders differ in a payload (such as a type annotation) that `alphaEquiv` rejects (see [#127](https://github.com/fizruk/free-foil/pull/127)).++Performance:++- `substitute`, `alphaEquiv`, `unsafeEqAST` and the functions behind them are `INLINE` wrappers around local loops, which take the instances from the wrapper. Inlined at a known signature, the loops use its instances directly. Before, they looked the instances up at every node, and a `SPECIALIZE` pragma in a client did not help: GHC split each function into a wrapper and a worker, since some of its dictionaries (such as `Distinct`) are never used at runtime, and the pragma reached only the wrapper. On the library's benchmarks, α-equivalence takes 0.54–0.91 of the time and normalisation 0.58–0.85 (see [#125](https://github.com/fizruk/free-foil/pull/125)).++New:++- `unsafeEqASTIn` and `unsafeEqScopedASTIn` compare two terms in one scope, like `unsafeEqAST`, but compare patterns with `unifyPatternsIn`, so the payloads of patterns are compared as well (see [#127](https://github.com/fizruk/free-foil/pull/127)).+- `unresolvedNamesWith` is `unresolvedNames` for the arguments of `tryConvertToASTWith`: it also takes the table of constants, so that the constants no longer count as unresolved (see [#127](https://github.com/fizruk/free-foil/pull/127)).+- `Control.Monad.Free.Foil.Internal` holds the implementation of `Control.Monad.Free.Foil`, which now has an export list. The loops behind α-equivalence, `unsafeEqAST` and `unsafeEqASTIn` (`AlphaEquivLoops`, `alphaEquivLoops`, `EqLoops`, `unsafeEqLoops`, `EqInLoops`, `unsafeEqInLoops`) are exported only from the internal module (see [#125](https://github.com/fizruk/free-foil/pull/125), [#127](https://github.com/fizruk/free-foil/pull/127)).++Documentation:++- Doc comments and README passages that the code contradicted are corrected, among them the equation given for `substituteRefreshed` and the `zipMatchK` example. Haddock links written through a module alias (such as `'Foil.sink'`) resolve, where in 0.6.0 they pointed to a nonexistent page (see [#126](https://github.com/fizruk/free-foil/pull/126)).+ # 0.6.0 — 2026-10-26  This release lets `mkFreeFoil` generate most instances of a signature, and adds folds that traverse terms without rebuilding them. Several breaking changes come with it, described first.

@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.37.0.+-- This file has been generated from package.yaml by hpack version 0.39.1. -- -- see: https://github.com/sol/hpack  name:           free-foil-version:        0.6.0+version:        0.6.1 synopsis:       Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads) description:    Please see the README on GitHub at <https://github.com/fizruk/free-foil#readme> category:       Parsing@@ -48,6 +48,7 @@       Control.Monad.Free.Foil.Binary       Control.Monad.Free.Foil.Binary.TH       Control.Monad.Free.Foil.Example+      Control.Monad.Free.Foil.Internal       Control.Monad.Free.Foil.TH       Control.Monad.Free.Foil.TH.Convert       Control.Monad.Free.Foil.TH.MkFreeFoil@@ -129,6 +130,7 @@       Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsSyntax       Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax       Control.Monad.Free.Foil.TH.PatternTypesSpec+      Control.Monad.Free.Foil.UnresolvedNamesSpec       Data.ZipMatchK.SumProductSpec       Data.ZipMatchK.THSpec       SpecHook

@@ -1,8 +1,8 @@ -- | Main definitions of the foil that can be -- reused for specific implementations. ----- The original description of this approach--- is described in the IFL 2022 paper by Maclaurin, Radul, and Paszke+-- This approach was originally described+-- in the IFL 2022 paper by Maclaurin, Radul, and Paszke -- [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224). -- This module also introduces 'CoSinkable' class, -- generalizing handling of patterns, as described in@@ -60,12 +60,6 @@   SinkableK(..),   Sinkable(..),   CoSinkable(..),-  -- ** Transporting a pattern's payloads-  PatternTransport,-  verbatimTransport,-  transportUnderBinder,-  transportPayload,-  transportName,   HasNameBinders(getNameBinders),   sink,   sink1,@@ -76,6 +70,12 @@   composeNameBinderRenamings,   fromNameBinderRenaming,   extendRenamingNameBinder,+  -- ** Transporting a pattern's payloads+  PatternTransport,+  verbatimTransport,+  transportUnderBinder,+  transportPayload,+  transportName,   -- * Safe substitutions   Substitution,   lookupSubst,

@@ -680,8 +680,12 @@ -- place a restriction is paid for: compare a term\'s support against the scope -- it is to be restricted to. --+-- The scope @l@ of the set must extend @n@, since names are compared by their+-- raw identifiers, which identify a name only within one chain of scope+-- extensions.+-- -- @since 0.4.0-nameSetSubsetOfScope :: NameSet l -> Scope n -> Bool+nameSetSubsetOfScope :: Ext n l => NameSet l -> Scope n -> Bool nameSetSubsetOfScope (UnsafeNameSet names) (UnsafeScope scope) =   names `IntSet.isSubsetOf` scope @@ -1215,9 +1219,9 @@   -- pattern that carries them does: 'alphaEquivIn' asks for a 'Scope'.   --   -- Note that the verdict speaks about binders, so an instance comparing-  -- payloads has to apply the renaming the verdict prescribes before it-  -- compares them, exactly as 'Control.Monad.Free.Foil.alphaEquivScoped'-  -- applies it to the body of a scoped term. Two telescopes @(A : 𝕌) (x : A)@+  -- payloads has to take the renaming the verdict prescribes into account when+  -- it compares them, as 'Control.Monad.Free.Foil.alphaEquivScoped' does for+  -- the body of a scoped term. Two telescopes @(A : 𝕌) (x : A)@   -- and @(B : 𝕌) (y : B)@ are α-equivalent, and their second payloads are only   -- equal once the first binders have been identified.   --@@ -2497,7 +2501,7 @@         cont (putBackRenamingK @_ @i rename' irename) (Field (unsafeCoerce x')) -- unsafeCoerce?  -- | A field indexed by the innermost scope variable only, such as the body of--- 'Control.Monad.Free.Foil.ScopedAST'. Under a binder the traversal holds one+-- t'Control.Monad.Free.Foil.ScopedAST'. Under a binder the traversal holds one -- renaming per scope variable, so the field takes the innermost one, as -- @t'Field' ('Kon' f ':@:' 'Var' i)@ does. instance SinkableK (f a) => GSinkableK (Field (Kon f :@: Kon a :@: Var0)) where

@@ -116,7 +116,7 @@         toPatternConParams i p (param@(bang_, type_) : conParams) =           case type_ of             -- if the current component is a variable identifier-            -- then treat it as a single name binder (see 'Foil.NameBinder')+            -- then treat it as a single name binder (see t'Control.Monad.Foil.NameBinder')             PeelConT tyName _tyParams | tyName == nameT -> do               l <- newName ("n" <> show i)               let type' = AppT (AppT (ConT ''Foil.NameBinder) (VarT p)) (VarT l)

@@ -14,7 +14,7 @@ import qualified Control.Monad.Foil         as Foil import           Control.Monad.Foil.TH.Util --- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances.+-- | Generate t'Control.Monad.Foil.Sinkable' and t'Control.Monad.Foil.CoSinkable' instances. -- -- @since 0.0.1 mkInstancesFoil@@ -83,7 +83,7 @@           where             xi = mkName ("x" ++ show i) --- | Generate the 'Foil.CoSinkable' instance of the pattern type that+-- | Generate the t'Control.Monad.Foil.CoSinkable' instance of the pattern type that -- 'Control.Monad.Foil.TH.MkFoilData.mkFoilPattern' generates from a raw -- pattern type, given the raw types of identifiers and patterns. -- 'deriveCoSinkable' takes the scope-safe pattern type itself.@@ -143,7 +143,7 @@             xi = mkName ("x" ++ show i)      -- The binders of the binding fields, in order, without going through-    -- 'Foil.withPattern'.+    -- 'Control.Monad.Foil.withPattern'.     clauseNameBinderListOf :: Con -> Clause     clauseNameBinderListOf (NormalC conName params) =       Clause [ConP foilConName [] conParamPatterns] (NormalB body) []@@ -201,7 +201,7 @@           where             xi = mkName ("x" ++ show i) --- | Generate the 'Foil.CoSinkable' instance of a scope-safe pattern type.+-- | Generate the t'Control.Monad.Foil.CoSinkable' instance of a scope-safe pattern type. -- 'mkCoSinkableFoilPattern' takes the raw pattern type instead. -- -- > data Pat (n :: S) (l :: S) where@@ -210,9 +210,9 @@ -- > -- > deriveCoSinkable ''Pat ----- A field is a 'Foil.NameBinder', a nested pattern, or a payload that+-- A field is a t'Control.Monad.Foil.NameBinder', a nested pattern, or a payload that -- mentions no scope. A payload indexed by a scope needs a hand-written--- instance (see 'Foil.transportPayload').+-- instance (see 'Control.Monad.Foil.transportPayload'). -- -- @since 0.6.0 deriveCoSinkable :: Name -> Q [Dec]@@ -229,7 +229,7 @@       coSinkClauses <- mapM patternCoSinkabilityProofClause fields       withPatClauses <- mapM patternWithPatternClause fields       listClauses <- mapM patternNameBinderListOfClause fields-      -- A pattern that nests itself has a recursive 'Foil.withPattern', which+      -- A pattern that nests itself has a recursive 'Control.Monad.Foil.withPattern', which       -- cannot inline.       let recursive = or [ h == ConT patternT | (_, sorts) <- fields, PatternNested h <- sorts ]           inline = [ PragmaD (InlineP 'Foil.withPattern Inline FunLike AllPhases) | not recursive ]@@ -243,8 +243,8 @@  -- | How a field of a pattern constructor takes part in its instance. data PatternField-  = PatternBinder        -- ^ A 'Foil.NameBinder'.-  | PatternNested Type   -- ^ A nested pattern, with its own 'Foil.CoSinkable'; its type's head.+  = PatternBinder        -- ^ A t'Control.Monad.Foil.NameBinder'.+  | PatternNested Type   -- ^ A nested pattern, with its own t'Control.Monad.Foil.CoSinkable'; its type's head.   | PatternPayload       -- ^ A field that mentions no scope.  -- | The constructors of a pattern type, each with the sorts of its fields.@@ -305,7 +305,7 @@   PatternPayload -> False   _              -> True --- | One 'Foil.coSinkabilityProof' clause: the binding fields are renamed in+-- | One 'Control.Monad.Foil.coSinkabilityProof' clause: the binding fields are renamed in -- turn, each with the renaming the previous one extended. patternCoSinkabilityProofClause :: (Name, [PatternField]) -> Q Clause patternCoSinkabilityProofClause (conName, sorts) = do@@ -323,10 +323,10 @@   body <- go rename (zip sorts xs) id   return (Clause [VarP rename, ConP conName [] (map VarP xs), VarP cont] (NormalB body) []) --- | One 'Foil.withPattern' clause, in the form of+-- | One 'Control.Monad.Foil.withPattern' clause, in the form of -- 'Control.Monad.Free.Foil.TH.MkFreeFoil.mkFreeFoil': a binder field goes -- through @withBinder@ and extends the scope for the fields to its right, a--- nested pattern through its own 'Foil.withPattern', and the results compose+-- nested pattern through its own 'Control.Monad.Foil.withPattern', and the results compose -- left to right. patternWithPatternClause :: (Name, [PatternField]) -> Q Clause patternWithPatternClause (conName, sorts) = do@@ -368,13 +368,13 @@     [VarP withBinder, VarP unit_, VarP comp_, VarP scope, ConP conName [] (map VarP xs), VarP cont]     (NormalB body) []) --- | One 'Foil.nameBinderListOf' clause: the binding fields, left to right.+-- | One 'Control.Monad.Foil.nameBinderListOf' clause: the binding fields, left to right. patternNameBinderListOfClause :: (Name, [PatternField]) -> Q Clause patternNameBinderListOfClause (conName, sorts) = do   xs <- mapM (\i -> newName ("x" ++ show i)) [1 .. length sorts]   let pats = [ if isBindingField s then VarP x else WildP | (s, x) <- zip sorts xs ]       -- A binder is consed on directly. Only a nested pattern's list is-      -- concatenated, since 'Foil.concatNameBinderLists' is recursive and+      -- concatenated, since 'Control.Monad.Foil.concatNameBinderLists' is recursive and       -- copies its first argument.       list = \case         [] -> ConE 'Foil.NameBinderListEmpty

@@ -144,8 +144,9 @@ -- unified? -- -- The verdict speaks about binders only, so the renaming it prescribes has to--- be applied before the payloads are compared, which is exactly what--- 'Control.Monad.Free.alphaEquivScoped' does to the body of a scoped term.+-- be applied before the payloads are compared, much as+-- 'Control.Monad.Free.Foil.alphaEquivScoped' takes it into account for the+-- body of a scoped term. -- Comparing them as they stand would report @(A : 𝕌) (x : A)@ and -- @(B : 𝕌) (y : B)@ as different, since the second payloads name different -- binders until the first ones have been identified.

@@ -1,1000 +1,61 @@-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE TypeFamilies         #-}-{-# LANGUAGE DeriveAnyClass        #-}-{-# LANGUAGE DeriveFoldable        #-}-{-# LANGUAGE DeriveFunctor         #-}-{-# LANGUAGE DeriveTraversable     #-}-{-# LANGUAGE DeriveGeneric         #-}-{-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE GADTs                 #-}-{-# LANGUAGE LambdaCase            #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds             #-}-{-# LANGUAGE QuantifiedConstraints #-}-{-# LANGUAGE RankNTypes            #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE StandaloneDeriving    #-}-{-# LANGUAGE UndecidableInstances  #-}--- | This module defines a variation of--- free scoped (relative) monads relying on the foil for--- the scope-safe efficient handling of the binders.------ See description of the approach in [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384).-module Control.Monad.Free.Foil where--import           Control.DeepSeq-import qualified Control.Monad.Foil.Internal as Foil-import           Data.Bifoldable-import           Data.Bitraversable-import           Data.Bifunctor-import Data.ZipMatchK-import qualified Generics.Kind as Kind-import Generics.Kind (GenericK(..), Field, Exists, Var0, Var1, (:$:), Atom((:@:), Kon), (:+:), (:*:))-import           Data.IntMap.Strict          (IntMap)-import qualified Data.IntMap.Strict          as IntMap-import           Data.Map                    (Map)-import qualified Data.Map                    as Map-import           GHC.Generics                (Generic)-import           Unsafe.Coerce               (unsafeCoerce)---- | Scoped term under a (single) name binder.------ @since 0.0.1-data ScopedAST binder sig n where-  ScopedAST :: binder n l -> AST binder sig l -> ScopedAST binder sig n---- INLINABLE, so that it specialises together with the instance for AST.-instance (forall x y. NFData (binder x y), forall l. NFData (AST binder sig l)) => NFData (ScopedAST binder sig n) where-  {-# INLINABLE rnf #-}-  rnf (ScopedAST binder body) = rnf binder `seq` rnf body---- | A term, generated by a signature 'Bifunctor' @sig@,--- with (free) variables in scope @n@.------ @since 0.0.1-data AST binder sig n where-  -- | A (free) variable in scope @n@.-  Var :: {-# UNPACK #-} !(Foil.Name n) -> AST binder sig n-  -- | A non-variable syntactic construction specified by the signature 'Bifunctor' @sig@.-  Node :: sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n--deriving instance Generic (AST binder sig n)---- | 'rnf' forces the names, the binders, and the nodes through the 'NFData'--- instance of the signature. GHC specialises it where the binder and the--- signature are known. On the λ-terms of the @nfdata@ benchmark, the--- specialised 'rnf' is about four times faster than the general one.-instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term))-  => NFData (AST binder sig n) where-  -- Without a specialisation, each node is forced through dictionaries built-  -- from the quantified constraints. The specialised rnf calls itself on the-  -- subterms and inlines the signature's rnf.-  {-# INLINABLE rnf #-}-  rnf (Var name)  = rnf name-  rnf (Node node) = rnf node--instance GenericK (ScopedAST binder sig) where-  type RepK (ScopedAST binder sig) =-    Exists Foil.S-      (Field (Kon binder :@: Var1 :@: Var0) :*: Field (Kon AST :@: Kon binder :@: Kon sig :@: Var0))-  toK (Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast)) = ScopedAST binder ast-  fromK (ScopedAST binder ast) = Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast)--instance GenericK (AST binder sig) where-  type RepK (AST binder sig) =-    Field (Foil.Name :$: Var0)-    :+: Field (sig-                :$: (Kon ScopedAST :@: Kon binder :@: Kon sig :@: Var0)-                :@: (Kon AST :@: Kon binder :@: Kon sig :@: Var0))--instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (ScopedAST binder sig)-instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (AST binder sig)--instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (ScopedAST binder sig)-instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (AST binder sig)--instance Foil.InjectName (AST binder sig) where-  injectName = Var---- * Substitution---- | Substitution for free (scoped monads).------ @since 0.0.1-{-# INLINABLE substitute #-}-substitute-  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)-  => Foil.Scope o-  -> Foil.Substitution (AST binder sig) i o-  -> AST binder sig i-  -> AST binder sig o-substitute scope subst term-  -- An empty substitution maps every name to itself ('addRename' deletes-  -- identity renames), so the result is the very term, and the coercion is-  -- the one 'Foil.sink' performs. Substitutions go empty often: opening a-  -- scoped term with its own binder's name is an identity rename, and under-  -- a deterministic allocation policy a refreshed binder usually keeps its-  -- name, deleting its entry. Binders that shadow the ambient scope are-  -- left as they stand, as on the no-clash path below. A caller that wants-  -- them refreshed asks 'substituteRefreshed'.-  | Foil.nullSubst subst = unsafeCoerce term-  | otherwise = go term-  where-    -- The substitution is known non-empty here, and it can only change-    -- under a binder, so the walk between binders is unchecked and each-    -- binder entry re-enters 'substitute', testing emptiness exactly once.-    go = \case-      Var name -> Foil.lookupSubst subst name-      Node node -> Node (bimap f go node)-    f (ScopedAST binder body) =-      Foil.withRefreshedPattern scope binder $ \extendSubst binder' scope' ->-        let subst' = extendSubst (Foil.sink subst)-            body' = substitute scope' subst' body-        in ScopedAST binder' body'---- | Substitution for free (scoped monads).------ This is a version of 'substitute' that forces refreshing of all name binders,--- resulting in a term with normalized binders:------ > substituteRefreshed scope subst = refreshAST scope . subtitute scope subst------ In general, 'substitute' is more efficient since it does not always refresh binders.------ @since 0.0.3-{-# INLINABLE substituteRefreshed #-}-substituteRefreshed-  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)-  => Foil.Scope o-  -> Foil.Substitution (AST binder sig) i o-  -> AST binder sig i-  -> AST binder sig o-substituteRefreshed scope subst = \case-  Var name -> Foil.lookupSubst subst name-  Node node -> Node (bimap f (substituteRefreshed scope subst) node)-  where-    f (ScopedAST binder body) =-      Foil.withFreshPattern scope binder $ \extendSubst binder' scope' ->-        let subst' = extendSubst (Foil.sink subst)-            body' = substituteRefreshed scope' subst' body-        in ScopedAST binder' body'---- | @'AST' sig@ is a monad relative to 'Foil.Name'.-instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder)-  => Foil.RelMonad Foil.Name (AST binder sig) where-  rreturn = Var-  rbind scope term subst =-    case term of-      Var name  -> subst name-      Node node -> Node (bimap g' g node)-    where-      g x = Foil.rbind scope x subst-      g' (ScopedAST binder body) =-        Foil.withRefreshedPattern' scope binder $ \extendSubst binder' scope' ->-          let subst' = extendSubst subst-           in ScopedAST binder' (Foil.rbind scope' body subst')---- | Substitution for a single generalized pattern.------ @since 0.2.0-{-# INLINABLE substitutePattern #-}-substitutePattern-  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder, Foil.SinkableK binder)-  => Foil.Scope o                           -- ^ Resulting scope.-  -> Foil.Substitution (AST binder sig) n o -- ^ Environment mapping names in scope @n@.-  -> binder' n i                            -- ^ Binders that extend scope @n@ to scope @i@.-  -> [AST binder sig o]                     -- ^ A list of terms intended to serve as-  -> AST binder sig i-  -> AST binder sig o-substitutePattern scope env binders args body =-  substitute scope env' body-  where-    env' = Foil.addSubstPattern env binders args---- * Transformations between signatures---- | Fold a term bottom-up into a scope-indexed carrier @r@. A variable goes--- through the first function, a scoped subterm through the second, given its--- binder and the fold of its body, and a node through the third, once its--- subterms are folded. The scope indices stay as they are, so the carrier--- can be another kind of term, as in 'hoistAST', or anything indexed by the--- scope, such as @'Const' Int@ for a node count.------ To change the binder type as well, map it in the second function:------ > foldAST Var (\binder body -> ScopedAST (toBinder binder) body) Node------ @since 0.6.0-{-# INLINABLE foldAST #-}-foldAST-  :: forall binder sig r s n. Bifunctor sig-  => (forall m. Foil.Name m -> r m)             -- ^ A variable.-  -> (forall m l. binder m l -> r l -> s m)     -- ^ A scoped subterm, from its binder and the fold of its body.-  -> (forall m. sig (s m) (r m) -> r m)         -- ^ A node, its subterms folded.-  -> AST binder sig n-  -> r n-foldAST var scoped node = go-  where-    go :: forall m. AST binder sig m -> r m-    go (Var x)  = var x-    go (Node t) = node (bimap (\(ScopedAST binder body) -> scoped binder (go body)) go t)---- | Change the signature of a term by a natural transformation of--- signatures, keeping the binders, as @hoistFree@ of the free package does--- for a free monad. Each node is rebuilt, so this costs a traversal.------ @since 0.6.0-{-# INLINABLE hoistAST #-}-hoistAST-  :: Bifunctor sig-  => (forall a b. sig a b -> sig' a b)-  -> AST binder sig n-  -> AST binder sig' n-hoistAST f = foldAST Var ScopedAST (Node . f)---- * \(\alpha\)-equivalence---- | Refresh (force) all binders in a term, minimizing the used indices.------ @since 0.0.3-{-# INLINABLE refreshAST #-}-refreshAST-  :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)-  => Foil.Scope n-  -> AST binder sig n-  -> AST binder sig n-refreshAST scope = \case-  t@Var{} -> t-  Node t -> Node (bimap (refreshScopedAST scope) (refreshAST scope) t)---- | Similar to `refreshAST`, but for scoped terms.------ @since 0.0.3-{-# INLINABLE refreshScopedAST #-}-refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)-  => Foil.Scope n-  -> ScopedAST binder sig n-  -> ScopedAST binder sig n-refreshScopedAST scope (ScopedAST binder body) =-  Foil.withFreshPattern scope binder $ \extendSubst binder' scope' ->-    let subst = extendSubst (Foil.sink Foil.identitySubst)-    in ScopedAST binder' (substituteRefreshed scope' subst body)---- | \(\alpha\)-equivalence check for two terms in one scope--- via normalization of bound identifiers (via 'refreshAST').------ Compared to 'alphaEquiv', this function renames every binder on both sides--- unconditionally, so it does strictly more work. It remains as an--- independent implementation of the same test.------ @since 0.0.3-{-# INLINABLE alphaEquivRefreshed #-}-alphaEquivRefreshed-  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)-  => Foil.Scope n-  -> AST binder sig n-  -> AST binder sig n-  -> Bool-alphaEquivRefreshed scope t1 t2 = refreshAST scope t1 `unsafeEqAST` refreshAST scope t2---- | A term is a scope-indexed value that can be compared up to α, which is what--- a pattern carrying terms as payloads needs of them.-instance (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.SinkableK binder)-    => Foil.AlphaEquiv (AST binder sig) where-  alphaEquivIn = alphaEquiv---- | \(\alpha\)-equivalence check for two terms in one scope--- via unification of bound variables (via 'unifyNameBinders').------ When two matching binders coincide, comparison continues with no work at--- all. When they differ, the prescribed renaming is /threaded down the--- recursion/ (see 'alphaEquivEnv') and consulted at variables only, so--- nothing is ever copied. Applying the renaming eagerly instead would--- materialise a renamed copy of the remaining body at every mismatched--- binder, which is quadratic on a chain of them.------ @since 0.0.3-{-# INLINABLE alphaEquiv #-}-alphaEquiv-  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)-  => Foil.Scope n-  -> AST binder sig n-  -> AST binder sig n-  -> Bool-alphaEquiv _scope (Var x) (Var y) = x == y-alphaEquiv scope (Node l) (Node r) =-  case zipMatchWith2 (unit . alphaEquivScoped scope) (unit . alphaEquiv scope) l r of-    Nothing -> False-    Just _  -> True-  where-    unit f x = if f x then Just () else Nothing-alphaEquiv _ _ _ = False---- | Same as 'alphaEquiv' but for scoped terms.------ While the binders of the two sides coincide, this runs with no renaming--- state at all. The first pair that differs switches to 'alphaEquivEnv',--- which threads the renamings down and switches back when they empty out.------ @since 0.0.3-{-# INLINABLE alphaEquivScoped #-}-alphaEquivScoped-  :: forall sig binder n. (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)-  => Foil.Scope n-  -> ScopedAST binder sig n-  -> ScopedAST binder sig n-  -> Bool-alphaEquivScoped scope-  (ScopedAST binder1 body1)-  (ScopedAST binder2 body2) =-    case Foil.unifyPatternsIn scope binder1 binder2 of-      -- the binders coincide: compare the bodies as they stand-      Foil.SameNameBinders{} ->  -- after seeing this we know that body scopes are the same-        case Foil.assertDistinct binder1 of-          Foil.Distinct ->-            let scope1 = Foil.extendScopePattern binder1 scope-            in alphaEquiv scope1 body1 body2-      -- the left binder is renamed towards the right one-      Foil.RenameLeftNameBinder _ rename1to2 ->-        case Foil.assertDistinct binder2 of-          Foil.Distinct ->-            let scope2 = Foil.extendScopePattern binder2 scope-                pairs = [ (Foil.nameId x, renamedId rename1to2 x)-                        | x <- Foil.namesOfPattern binder1 ]-            in enterEnv pairs scope2 body1 body2-      -- the right binder is renamed towards the left one-      Foil.RenameRightNameBinder _ rename2to1 ->-        case Foil.assertDistinct binder1 of-          Foil.Distinct ->-            let scope1 = Foil.extendScopePattern binder1 scope-                pairs = [ (renamedId rename2to1 y, Foil.nameId y)-                        | y <- Foil.namesOfPattern binder2 ]-            in enterEnv pairs scope1 body1 body2-      -- both are renamed towards a unified pattern: pair the two sides'-      -- names through the unified name each maps to-      Foil.RenameBothBinders binder' rename1 rename2 ->-        case Foil.assertDistinct binder' of-          Foil.Distinct ->-            let scope' = Foil.extendScopePattern binder' scope-                leftU = IntMap.fromList-                  [ (renamedId rename1 x, Foil.nameId x)-                  | x <- Foil.namesOfPattern binder1 ]-                rightU = IntMap.fromList-                  [ (renamedId rename2 y, Foil.nameId y)-                  | y <- Foil.namesOfPattern binder2 ]-                pairs = IntMap.elems (IntMap.intersectionWith (,) leftU rightU)-            in enterEnv pairs scope' body1 body2-      -- if we cannot unify patterns then scopes are not alpha-equivalent-      Foil.NotUnifiable -> False-  where-    enterEnv-      :: forall m l1 l2. Foil.Distinct m-      => [(Int, Int)] -> Foil.Scope m-      -> AST binder sig l1 -> AST binder sig l2 -> Bool-    enterEnv pairs scope' = bindPairs 0 IntMap.empty IntMap.empty pairs scope'---- | The raw name a verdict's renaming assigns to a pattern's name.------ @since 0.4.0-renamedId :: (Foil.NameBinder n a -> Foil.NameBinder n b) -> Foil.Name a -> Int-renamedId rename = Foil.nameId . Foil.nameOf . rename . Foil.UnsafeNameBinder---- | Bind the paired names of a binder pair. A pair whose names coincide--- shadows both sides identically and is deleted from the environments. A pair--- whose names differ binds both to one fresh level. Continues with--- 'alphaEquivEnv' on the bodies.------ @since 0.4.0-bindPairs-  :: forall sig binder m l1 l2. (Bitraversable sig, ZipMatchK sig, Foil.Distinct m, Foil.UnifiablePattern binder, Foil.SinkableK binder)-  => Int -> IntMap Int -> IntMap Int -> [(Int, Int)]-  -> Foil.Scope m-  -> AST binder sig l1 -> AST binder sig l2 -> Bool-bindPairs lvl envL envR pairs scope body1 body2 = case pairs of-  [] -> alphaEquivEnv lvl envL envR scope body1 body2-  ((x, y) : rest)-    | x == y    -> bindPairs lvl (IntMap.delete x envL) (IntMap.delete y envR) rest scope body1 body2-    | otherwise -> bindPairs (lvl + 1) (IntMap.insert x lvl envL) (IntMap.insert y lvl envR) rest scope body1 body2---- | The renaming-threading worker behind 'alphaEquiv': compare two terms--- under partial renamings of their names into shared /levels/.------ Each environment maps a raw name to the level of the binder pair that bound--- it on the comparison path, and a name outside its environment stands for--- itself. A variable occurrence then compares as a level against a level, or--- as a raw name against a raw name, and the two can never be conflated. This--- is what makes threading sound where applying a raw renaming at the variables--- would not be, since a renamed name could collide with one that passes--- through unchanged and happens to share the target spelling. Levels are also--- why no capture check is needed: a level is never a name, so there is nothing--- for a binder to capture.------ A binder pair whose names coincide /deletes/ those names from both--- environments, the pair shadowing both sides identically. When the--- environments empty out the comparison drops back to the stateless--- 'alphaEquiv', so only the region of the terms below a mismatched binder,--- and above the point where the mismatch is shadowed away, pays for the--- threading at all.------ The indices of the two terms are deliberately independent, in the style--- of 'unsafeEqAST': the terms are never renamed into a common scope, so--- no common index exists to give them.------ @since 0.4.0-{-# INLINABLE alphaEquivEnv #-}-alphaEquivEnv-  :: forall sig binder n n1 n2. (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)-  => Int          -- ^ Next fresh level.-  -> IntMap Int   -- ^ Left renaming: raw name to the level that bound it.-  -> IntMap Int   -- ^ Right renaming.-  -> Foil.Scope n -- ^ Scope along the unified path (consulted by 'Foil.unifyPatternsIn').-  -> AST binder sig n1-  -> AST binder sig n2-  -> Bool-alphaEquivEnv lvl envL envR scope t1 t2-  | IntMap.null envL && IntMap.null envR =-      -- The renamings have emptied out (or never held anything): the-      -- terms coincide raw-for-raw from here on, so compare them where-      -- they stand. The coercion brings both indices to the scope's,-      -- which is the unified path the comparison speaks of.-      alphaEquiv scope (unsafeCoerce t1 :: AST binder sig n) (unsafeCoerce t2 :: AST binder sig n)-  | otherwise = case (t1, t2) of-      (Var x, Var y) ->-        case (IntMap.lookup (Foil.nameId x) envL, IntMap.lookup (Foil.nameId y) envR) of-          (Just k1, Just k2) -> k1 == k2-          (Nothing, Nothing) -> Foil.nameId x == Foil.nameId y-          _                  -> False-      (Node l, Node r) ->-        case zipMatchWith2-               (unit . alphaEquivScopedEnv lvl envL envR scope)-               (unit . alphaEquivEnv lvl envL envR scope) l r of-          Nothing -> False-          Just _  -> True-      _ -> False-  where-    unit f x = if f x then Just () else Nothing---- | The scoped half of 'alphaEquivEnv': get the verdict from--- 'Foil.unifyPatternsIn', extend the environments as it prescribes, and--- recurse into the bodies as they stand.------ @since 0.4.0-{-# INLINABLE alphaEquivScopedEnv #-}-alphaEquivScopedEnv-  :: forall sig binder n n1 n2. (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)-  => Int-  -> IntMap Int-  -> IntMap Int-  -> Foil.Scope n-  -> ScopedAST binder sig n1-  -> ScopedAST binder sig n2-  -> Bool-alphaEquivScopedEnv lvl envL envR scope scoped1 scoped2 =-  -- The scoped terms are compared where they stand; the coercion only-  -- brings their indices to the scope's, which is the unified path the-  -- environments and the verdicts speak of.-  case (unsafeCoerce scoped1 :: ScopedAST binder sig n, unsafeCoerce scoped2 :: ScopedAST binder sig n) of-    (ScopedAST binder1 body1, ScopedAST binder2 body2) ->-      case Foil.unifyPatternsIn scope binder1 binder2 of-        -- the binders coincide: the pair shadows both sides identically-        Foil.SameNameBinders{} ->-          case Foil.assertDistinct binder1 of-            Foil.Distinct ->-              let scope' = Foil.extendScopePattern binder1 scope-                  names = map Foil.nameId (Foil.namesOfPattern binder1)-                  envL' = deleteAll names envL-                  envR' = deleteAll names envR-               in alphaEquivEnv lvl envL' envR' scope' body1 body2-        -- the left binder is renamed towards the right one-        Foil.RenameLeftNameBinder _ rename1to2 ->-          case Foil.assertDistinct binder2 of-            Foil.Distinct ->-              let scope' = Foil.extendScopePattern binder2 scope-                  pairs = [ (Foil.nameId x, renamedId rename1to2 x)-                          | x <- Foil.namesOfPattern binder1 ]-               in bindPairs lvl envL envR pairs scope' body1 body2-        -- the right binder is renamed towards the left one-        Foil.RenameRightNameBinder _ rename2to1 ->-          case Foil.assertDistinct binder1 of-            Foil.Distinct ->-              let scope' = Foil.extendScopePattern binder1 scope-                  pairs = [ (renamedId rename2to1 y, Foil.nameId y)-                          | y <- Foil.namesOfPattern binder2 ]-               in bindPairs lvl envL envR pairs scope' body1 body2-        -- both are renamed towards a unified pattern: pair the two sides'-        -- names through the unified name each maps to-        Foil.RenameBothBinders binder' rename1 rename2 ->-          case Foil.assertDistinct binder' of-            Foil.Distinct ->-              let scope' = Foil.extendScopePattern binder' scope-                  leftU = IntMap.fromList-                    [ (renamedId rename1 x, Foil.nameId x)-                    | x <- Foil.namesOfPattern binder1 ]-                  rightU = IntMap.fromList-                    [ (renamedId rename2 y, Foil.nameId y)-                    | y <- Foil.namesOfPattern binder2 ]-                  pairs = IntMap.elems (IntMap.intersectionWith (,) leftU rightU)-               in bindPairs lvl envL envR pairs scope' body1 body2-        Foil.NotUnifiable -> False-  where-    deleteAll names env = case names of-      []       -> env-      (i : is) -> deleteAll is (IntMap.delete i env)---- ** Unsafe equality checks---- | /Unsafe/ equality check for two terms.--- This check ignores the possibility that two terms might have different--- scope extensions under binders (which might happen due to substitution--- under a binder in absence of name conflicts).------ @since 0.0.3-{-# INLINABLE unsafeEqAST #-}-unsafeEqAST-  :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)-  => AST binder sig n-  -> AST binder sig l-  -> Bool-unsafeEqAST (Var x) (Var y) = Foil.nameId x == Foil.nameId y-unsafeEqAST (Node t1) (Node t2) =-  case zipMatchWith2 (unit . unsafeEqScopedAST) (unit . unsafeEqAST) t1 t2 of-    Nothing -> False-    Just _  -> True-  where-    unit f x = if f x then Just () else Nothing-unsafeEqAST _ _ = False---- | A version of 'unsafeEqAST' for scoped terms.------ @since 0.0.3-{-# INLINABLE unsafeEqScopedAST #-}-unsafeEqScopedAST-  :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)-  => ScopedAST binder sig n-  -> ScopedAST binder sig l-  -> Bool-unsafeEqScopedAST (ScopedAST binder1 body1) (ScopedAST binder2 body2) = and-  [ Foil.unsafeEqPattern binder1 binder2-  , case (Foil.assertDistinct binder1, Foil.assertDistinct binder2) of-      (Foil.Distinct, Foil.Distinct) -> body1 `unsafeEqAST` body2-  ]---- * Converting to and from free foil---- ** Convert to free foil---- | An identifier a raw term mentions that the names given for conversion do--- not account for.------ Note what this does and does not carry. It cannot carry a position: the--- conversion functions are generic in the raw term and only ever see it through--- @toSig@, so a source location, if the syntax has one, is not theirs to read.--- What they do know, and a caller checking names beforehand does not, is which--- names were in scope /at the occurrence/, the binders passed on the way down--- included. That is what a \"did you mean\" needs.------ @since 0.4.0-data UnresolvedName rawIdent = UnresolvedName-  { unresolvedIdent   :: rawIdent-    -- ^ The identifier that did not resolve.-  , unresolvedInScope :: [rawIdent]-    -- ^ What was in scope where it occurred.-  } deriving (Eq, Show, Functor, Foldable, Traversable)---- | The identifiers a raw term mentions that a set of names cannot resolve, in--- the order they occur.------ This is 'unsafeConvertToAST' with the conversion left out, so it descends--- under binders in the same way and accounts for what they bind.------ @since 0.4.0-unresolvedNames-  :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n.-     (Foil.Distinct n, Bifoldable sig, Ord rawIdent, Foil.CoSinkable binder)-  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))-  -- ^ Unpeel one syntax node (or a variable) from a raw term.-  -> (forall x z. Foil.Distinct x-      => Foil.Scope x-      -> Map rawIdent (Foil.Name x)-      -> rawPattern-      -> (forall y. Foil.DExt x y-          => binder x y-          -> Map rawIdent (Foil.Name y)-          -> z)-      -> z)-  -- ^ Convert raw pattern into a scope-safe pattern.-  -> (rawScopedTerm -> rawTerm)-  -- ^ Extract a term from a scoped term (or crash).-  -> Foil.Scope n-  -- ^ Resulting scope of the constructed term.-  -> Map rawIdent (Foil.Name n)-  -- ^ Known names of free variables in scope @n@.-  -> rawTerm-  -- ^ Raw term.-  -> [UnresolvedName rawIdent]-unresolvedNames toSig fromRawPattern getScopedTerm = go-  where-    go :: forall x. Foil.Distinct x-       => Foil.Scope x -> Map rawIdent (Foil.Name x) -> rawTerm -> [UnresolvedName rawIdent]-    go scope names t = case toSig t of-      Left x-        | Map.member x names -> []-        | otherwise          -> [UnresolvedName x (Map.keys names)]-      Right node -> bifoldMap (goScoped scope names) (go scope names) node--    goScoped :: forall x. Foil.Distinct x-             => Foil.Scope x -> Map rawIdent (Foil.Name x)-             -> (rawPattern, rawScopedTerm) -> [UnresolvedName rawIdent]-    goScoped scope names (pat, scopedTerm) =-      fromRawPattern scope names pat $ \binder' names' ->-        go (Foil.extendScopePattern binder' scope) names' (getScopedTerm scopedTerm)---- | Convert a raw term into a scope-safe term, reporting the first identifier--- that does not resolve.------ One pass, short-circuiting at the first failure, so a term that resolves--- costs no more than 'unsafeConvertToAST' does. The report is complete for--- that one identifier, since 'unresolvedInScope' is built where the conversion--- fails and is never computed on the way through.------ A caller wanting /every/ unresolved identifier rather than the first pays a--- second pass for it, with 'unresolvedNames'. The successful path stays fast--- that way, and a failure can afford to be walked again for a better message.------ @since 0.4.0-tryConvertToAST-  :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n.-     (Foil.Distinct n, Bitraversable sig, Ord rawIdent,-      Foil.CoSinkable binder, Foil.SinkableK binder)-  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))-  -- ^ Unpeel one syntax node (or a variable) from a raw term.-  -> (forall x z. Foil.Distinct x-      => Foil.Scope x-      -> Map rawIdent (Foil.Name x)-      -> rawPattern-      -> (forall y. Foil.DExt x y-          => binder x y-          -> Map rawIdent (Foil.Name y)-          -> z)-      -> z)-  -- ^ Convert raw pattern into a scope-safe pattern.-  -> (rawScopedTerm -> rawTerm)-  -- ^ Extract a term from a scoped term (or crash).-  -> Foil.Scope n-  -- ^ Resulting scope of the constructed term.-  -> Map rawIdent (Foil.Name n)-  -- ^ Known names of free variables in scope @n@.-  -> rawTerm-  -- ^ Raw term.-  -> Either (UnresolvedName rawIdent) (AST binder sig n)-tryConvertToAST toSig fromRawPattern getScopedTerm scope names =-  tryConvertToASTWith toSig fromRawPattern getScopedTerm scope names Map.empty---- | Convert a raw term into a scope-safe term, resolving some identifiers to--- whole terms rather than to variables.------ The extra table is what a language with /constants/ needs: an identifier that--- denotes a top-level declaration, a primitive, or an abbreviation stands for--- something that is not a variable, and resolving it during conversion is the--- only place where the binders are known. Doing it in a pass of one's own means--- writing a binder-aware traversal of the raw syntax by hand.------ Variables win: the table of names is consulted first, so a binder shadows an--- entry here, and an entry here shadows nothing. The table is sunk when going--- under a binder, exactly as the names are, so its entries may mention anything--- in scope where conversion started and need not be closed.------ @since 0.4.0-tryConvertToASTWith-  :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n.-     (Foil.Distinct n, Bitraversable sig, Ord rawIdent,-      Foil.CoSinkable binder, Foil.SinkableK binder)-  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))-  -- ^ Unpeel one syntax node (or a variable) from a raw term.-  -> (forall x z. Foil.Distinct x-      => Foil.Scope x-      -> Map rawIdent (Foil.Name x)-      -> rawPattern-      -> (forall y. Foil.DExt x y-          => binder x y-          -> Map rawIdent (Foil.Name y)-          -> z)-      -> z)-  -- ^ Convert raw pattern into a scope-safe pattern.-  -> (rawScopedTerm -> rawTerm)-  -- ^ Extract a term from a scoped term (or crash).-  -> Foil.Scope n-  -- ^ Resulting scope of the constructed term.-  -> Map rawIdent (Foil.Name n)-  -- ^ Known names of free variables in scope @n@.-  -> Map rawIdent (AST binder sig n)-  -- ^ Identifiers that denote a term rather than a variable.-  -> rawTerm-  -- ^ Raw term.-  -> Either (UnresolvedName rawIdent) (AST binder sig n)-tryConvertToASTWith toSig fromRawPattern getScopedTerm = go-  where-    go :: forall x. Foil.Distinct x-       => Foil.Scope x -> Map rawIdent (Foil.Name x)-       -> Map rawIdent (AST binder sig x) -> rawTerm-       -> Either (UnresolvedName rawIdent) (AST binder sig x)-    go scope names terms t = case toSig t of-      Left x -> case Map.lookup x names of-        Just name -> Right (Var name)-        Nothing   -> case Map.lookup x terms of-          Just term -> Right term-          Nothing   -> Left (UnresolvedName x (Map.keys names <> Map.keys terms))-      Right node ->-        Node <$> bitraverse (goScoped scope names terms) (go scope names terms) node--    goScoped :: forall x. Foil.Distinct x-             => Foil.Scope x -> Map rawIdent (Foil.Name x)-             -> Map rawIdent (AST binder sig x)-             -> (rawPattern, rawScopedTerm)-             -> Either (UnresolvedName rawIdent) (ScopedAST binder sig x)-    goScoped scope names terms (pat, scopedTerm) =-      fromRawPattern scope names pat $ \binder' names' ->-        ScopedAST binder'-          <$> go (Foil.extendScopePattern binder' scope) names'-                 (Foil.sink1 terms) (getScopedTerm scopedTerm)---- | Convert a raw term into a scope-safe term, calling 'error' on an--- identifier that does not resolve.------ Prefer 'tryConvertToAST', which reports such identifiers. This is for callers--- that have already established that every name resolves.------ @since 0.4.0-unsafeConvertToAST-  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)-  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))-  -- ^ Unpeel one syntax node (or a variable) from a raw term.-  -> (forall x z. Foil.Distinct x-      => Foil.Scope x-      -> Map rawIdent (Foil.Name x)-      -> rawPattern-      -> (forall y. Foil.DExt x y-          => binder x y-          -> Map rawIdent (Foil.Name y)-          -> z)-      -> z)-  -- ^ Convert raw pattern into a scope-safe pattern.-  -> (rawScopedTerm -> rawTerm)-  -- ^ Extract a term from a scoped term (or crash).-  -> Foil.Scope n-  -- ^ Resulting scope of the constructed term.-  -> Map rawIdent (Foil.Name n)-  -- ^ Known names of free variables in scope @n@.-  -> rawTerm-  -- ^ Raw term.-  -> AST binder sig n-unsafeConvertToAST toSig fromRawPattern getScopedTerm scope names t =-  case toSig t of-    Left x ->-      case Map.lookup x names of-        Nothing   -> error "undefined variable"-        Just name -> Var name-    Right node -> Node $-      bimap-        (unsafeConvertToScopedAST toSig fromRawPattern getScopedTerm scope names)-        (unsafeConvertToAST toSig fromRawPattern getScopedTerm scope names)-        node---- | Same as 'unsafeConvertToAST' but for scoped terms.------ @since 0.4.0-unsafeConvertToScopedAST-  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)-  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))-  -- ^ Unpeel one syntax node (or a variable) from a raw term.-  -> (forall x z. Foil.Distinct x-      => Foil.Scope x-      -> Map rawIdent (Foil.Name x)-      -> rawPattern-      -> (forall y. Foil.DExt x y-          => binder x y-          -> Map rawIdent (Foil.Name y)-          -> z)-      -> z)-  -- ^ Convert raw pattern into a scope-safe pattern.-  -> (rawScopedTerm -> rawTerm)-  -- ^ Extract a term from a scoped term (or crash).-  -> Foil.Scope n-  -- ^ Resulting scope of the constructed term.-  -> Map rawIdent (Foil.Name n)-  -- ^ Known names of free variables in scope @n@.-  -> (rawPattern, rawScopedTerm)-  -- ^ A pair of a pattern and a corresponding scoped term.-  -> ScopedAST binder sig n-unsafeConvertToScopedAST toSig fromRawPattern getScopedTerm scope names (pat, scopedTerm) =-  fromRawPattern scope names pat $ \binder' names' ->-    let scope' = Foil.extendScopePattern binder' scope-     in ScopedAST binder' (unsafeConvertToAST toSig fromRawPattern getScopedTerm scope' names' (getScopedTerm scopedTerm))---- ** Convert from free foil---- | Convert a scope-safe term back into a raw term.------ @since 0.0.3-convertFromAST-  :: Bifunctor sig-  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)-  -- ^ Peel back one layer of syntax.-  -> (rawIdent -> rawTerm)-  -- ^ Convert identifier into a raw variable term.-  -> (forall x y. binder x y -> rawPattern)-  -- ^ Convert scope-safe pattern into a raw pattern.-  -> (rawTerm -> rawScopedTerm)-  -- ^ Wrap raw term into a scoped term.-  -> (Int -> rawIdent)-  -- ^ Convert underlying integer identifier of a bound variable into a raw identifier.-  -> AST binder sig n-  -- ^ Scope-safe term.-  -> rawTerm-convertFromAST fromSig fromVar makePattern makeScoped f = \case-  Var x -> fromVar (f (Foil.nameId x))-  Node node -> fromSig $-    bimap-      (convertFromScopedAST fromSig fromVar makePattern makeScoped f)-      (convertFromAST fromSig fromVar makePattern makeScoped f)-      node---- | Same as 'convertFromAST' but for scoped terms.------ @since 0.0.3-convertFromScopedAST-  :: Bifunctor sig-  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)-  -- ^ Peel back one layer of syntax.-  -> (rawIdent -> rawTerm)-  -- ^ Convert identifier into a raw variable term.-  -> (forall x y. binder x y -> rawPattern)-  -- ^ Convert scope-safe pattern into a raw pattern.-  -> (rawTerm -> rawScopedTerm)-  -- ^ Wrap raw term into a scoped term.-  -> (Int -> rawIdent)-  -- ^ Convert underlying integer identifier of a bound variable into a raw identifier.-  -> ScopedAST binder sig n-  -- ^ Scope-safe scoped term.-  -> (rawPattern, rawScopedTerm)-convertFromScopedAST fromSig fromVar makePattern makeScoped f = \case-  ScopedAST binder body ->-    ( makePattern binder-    , makeScoped (convertFromAST fromSig fromVar makePattern makeScoped f body))---- | Convert a scope-safe term back into a raw term, naming the variables that--- occur /free in the whole term/ separately from the bound ones.------ 'convertFromAST' applies one naming function to every variable it meets,--- bound or free, and gives it only a raw name. That is often not enough, since--- raw names are not unique across scope indices: a binder inside a term may--- share one with a name of the ambient scope, so naming by raw name alone can--- print a bound variable as whatever the ambient scope calls that name.------ Keeping the typed name is what distinguishes them, and 'Foil.unsinkNamePattern'--- is the operation for it: composing one per binder on the way down builds a--- @'Foil.Name' x -> 'Maybe' ('Foil.Name' n)@ that answers exactly the question.------ @since 0.4.0-convertFromASTWith-  :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n.-     (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder)-  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)-  -- ^ Peel back one layer of syntax.-  -> (rawIdent -> rawTerm)-  -- ^ Convert identifier into a raw variable term.-  -> (forall x y. binder x y -> rawPattern)-  -- ^ Convert scope-safe pattern into a raw pattern.-  -> (rawTerm -> rawScopedTerm)-  -- ^ Wrap raw term into a scoped term.-  -> (Foil.Name n -> rawIdent)-  -- ^ Name a variable that is free in the whole term.-  -> (Int -> rawIdent)-  -- ^ Name a bound variable, from its underlying integer identifier.-  -> AST binder sig n-  -- ^ Scope-safe term.-  -> rawTerm-convertFromASTWith fromSig fromVar makePattern makeScoped freeName boundName =-    go Just-  where-    go :: forall x. Foil.Distinct x-       => (Foil.Name x -> Maybe (Foil.Name n)) -> AST binder sig x -> rawTerm-    go unsink = \case-      Var x -> fromVar $ case unsink x of-        Just name -> freeName name-        Nothing   -> boundName (Foil.nameId x)-      Node node -> fromSig (bimap (goScoped unsink) (go unsink) node)--    goScoped :: forall x. Foil.Distinct x-             => (Foil.Name x -> Maybe (Foil.Name n))-             -> ScopedAST binder sig x -> (rawPattern, rawScopedTerm)-    goScoped unsink (ScopedAST binder body) =-      case Foil.assertDistinct binder of-        Foil.Distinct ->-          ( makePattern binder-          , makeScoped-              (go (\name -> Foil.unsinkNamePattern binder name >>= unsink) body) )---- ** Unsinking AST---- | The support of a term: exactly the names that occur free in it.------ This is the annotation that co-de-Bruijn syntax carries intrinsically and--- that the foil, having global names and therefore free weakening, does not.--- Computing it is \(O(size)\); a client that restricts often should cache it.------ @since 0.4.0-supportOf-  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig)-  => AST binder sig n -> Foil.NameSet n-supportOf = \case-  Var name  -> Foil.nameSetSingleton name-  Node node -> bifoldMap supportOfScopedAST supportOf node---- | The support of a scoped term, in the scope /outside/ its binder.------ @since 0.4.0-supportOfScopedAST-  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig)-  => ScopedAST binder sig n -> Foil.NameSet n-supportOfScopedAST (ScopedAST binder body) =-  case Foil.assertDistinct binder of-    Foil.Distinct -> Foil.unsinkNameSet binder (supportOf body)---- | Cut a term down to the scope of exactly the names it uses.------ This is the a-priori form of restriction, and the cheap one: the term--- inhabits the smaller scope /by construction/, so nothing is tested and--- nothing can fail. @'Foil.Ext' m n@ comes back with it, so the term can be--- 'Foil.sink'ed to where it came from for free.------ Verifying a declared dependency, such as a @uses@ clause or a module's--- parameters, is this plus a comparison: compute the scope a term really--- inhabits, and check the declared one against it.------ @since 0.4.0-withRelevantScope-  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig)-  => AST binder sig n-  -> (forall m. (Foil.Ext m n, Foil.Distinct m)-      => Foil.Scope m -> AST binder sig m -> r)-  -> r-withRelevantScope term cont =-  Foil.withRestrictedScope (supportOf term) $ \scope ->-    cont scope (unsafeCoerce term)---- | Unsink an AST from a larger scope to a smaller scope.------ This is the a-posteriori form, and the one that has to be paid for: the--- term's support is computed and compared against the scope. When it succeeds--- the term itself is untouched, since restriction of a term that does inhabit--- the smaller scope is a coercion.------ @since 0.3.0-unsinkAST-  :: (Foil.Distinct l, Foil.CoSinkable binder, Bifoldable sig)-  => Foil.Scope n -> AST binder sig l -> Maybe (AST binder sig n)-unsinkAST scope term-  | Foil.nameSetSubsetOfScope (supportOf term) scope = Just (unsafeCoerce term)-  | otherwise = Nothing---- | Get the free variables of an AST.------ These come from 'supportOf', so they are distinct and in ascending order of--- their identifiers.------ @since 0.3.0-freeVarsOf-  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig)-  => AST binder sig n -> [Foil.Name n]-freeVarsOf = Foil.nameSetToList . supportOf---- | Get the free variables of a scoped AST, in the scope outside its binder.------ @since 0.3.0-freeVarsOfScopedAST-  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig)-  => ScopedAST binder sig n -> [Foil.Name n]-freeVarsOfScopedAST = Foil.nameSetToList . supportOfScopedAST+-- | This module defines a variation of+-- free scoped (relative) monads relying on the foil for+-- the scope-safe efficient handling of the binders.+--+-- See description of the approach in [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384).+module Control.Monad.Free.Foil (+  -- * Terms+  AST(..),+  ScopedAST(..),++  -- * Substitution+  substitute,+  substituteRefreshed,+  substitutePattern,++  -- * Transformations between signatures+  foldAST,+  hoistAST,++  -- * \(\alpha\)-equivalence+  refreshAST,+  refreshScopedAST,+  alphaEquivRefreshed,+  alphaEquiv,+  alphaEquivScoped,+  renamedId,+  bindPairs,+  alphaEquivEnv,+  alphaEquivScopedEnv,++  -- ** Unsafe equality checks+  unsafeEqAST,+  unsafeEqScopedAST,+  unsafeEqASTIn,+  unsafeEqScopedASTIn,++  -- * Converting to and from free foil+  -- ** Convert to free foil+  UnresolvedName(..),+  unresolvedNames,+  unresolvedNamesWith,+  tryConvertToAST,+  tryConvertToASTWith,+  unsafeConvertToAST,+  unsafeConvertToScopedAST,++  -- ** Convert from free foil+  convertFromAST,+  convertFromScopedAST,+  convertFromASTWith,++  -- ** Unsinking AST+  supportOf,+  supportOfScopedAST,+  withRelevantScope,+  unsinkAST,+  freeVarsOf,+  freeVarsOfScopedAST,+) where++import           Control.Monad.Free.Foil.Internal

@@ -16,7 +16,7 @@ -- and nothing else in the library does. (The dependency this costs is -- @binary@, a GHC boot library.) ----- Note that decoding /mints/ scope evidence: a 'Foil.Name' comes back at+-- Note that decoding /mints/ scope evidence: a t'Control.Monad.Foil.Name' comes back at -- whatever scope index the context asks for, and the existential scope -- under a binder is chosen arbitrarily. Thus the instances are a trust -- boundary, in the sense of 'Control.Monad.Foil.Blocks.checkExtScope'. The

@@ -0,0 +1,1222 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE DeriveAnyClass        #-}+{-# LANGUAGE DeriveFoldable        #-}+{-# LANGUAGE DeriveFunctor         #-}+{-# LANGUAGE DeriveTraversable     #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE UndecidableInstances  #-}+-- | The implementation of "Control.Monad.Free.Foil", together with the+-- definitions it does not export, such as the loops behind α-equivalence.+-- Use "Control.Monad.Free.Foil" instead, unless you need those.+--+-- @since 0.6.1+module Control.Monad.Free.Foil.Internal where++import           Control.DeepSeq+import qualified Control.Monad.Foil.Internal as Foil+import           Data.Bifoldable+import           Data.Bitraversable+import           Data.Bifunctor+import Data.ZipMatchK+import qualified Generics.Kind as Kind+import Generics.Kind (GenericK(..), Field, Exists, Var0, Var1, (:$:), Atom((:@:), Kon), (:+:), (:*:))+import           Data.IntMap.Strict          (IntMap)+import qualified Data.IntMap.Strict          as IntMap+import           Data.Map                    (Map)+import qualified Data.Map                    as Map+import           GHC.Generics                (Generic)+import           Unsafe.Coerce               (unsafeCoerce)++-- | Scoped term under a binder, which may be a pattern binding several names.+--+-- @since 0.0.1+data ScopedAST binder sig n where+  ScopedAST :: binder n l -> AST binder sig l -> ScopedAST binder sig n++-- INLINABLE, so that it specialises together with the instance for AST.+instance (forall x y. NFData (binder x y), forall l. NFData (AST binder sig l)) => NFData (ScopedAST binder sig n) where+  {-# INLINABLE rnf #-}+  rnf (ScopedAST binder body) = rnf binder `seq` rnf body++-- | A term, generated by a signature 'Bifunctor' @sig@,+-- with (free) variables in scope @n@.+--+-- @since 0.0.1+data AST binder sig n where+  -- | A (free) variable in scope @n@.+  Var :: {-# UNPACK #-} !(Foil.Name n) -> AST binder sig n+  -- | A non-variable syntactic construction specified by the signature 'Bifunctor' @sig@.+  Node :: sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n++deriving instance Generic (AST binder sig n)++-- | 'rnf' forces the names, the binders, and the nodes through the 'NFData'+-- instance of the signature. GHC specialises it where the binder and the+-- signature are known. On the λ-terms of the @nfdata@ benchmark, the+-- specialised 'rnf' is about four times faster than the general one.+instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term))+  => NFData (AST binder sig n) where+  -- Without a specialisation, each node is forced through dictionaries built+  -- from the quantified constraints. The specialised rnf calls itself on the+  -- subterms and inlines the signature's rnf.+  {-# INLINABLE rnf #-}+  rnf (Var name)  = rnf name+  rnf (Node node) = rnf node++instance GenericK (ScopedAST binder sig) where+  type RepK (ScopedAST binder sig) =+    Exists Foil.S+      (Field (Kon binder :@: Var1 :@: Var0) :*: Field (Kon AST :@: Kon binder :@: Kon sig :@: Var0))+  toK (Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast)) = ScopedAST binder ast+  fromK (ScopedAST binder ast) = Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast)++instance GenericK (AST binder sig) where+  type RepK (AST binder sig) =+    Field (Foil.Name :$: Var0)+    :+: Field (sig+                :$: (Kon ScopedAST :@: Kon binder :@: Kon sig :@: Var0)+                :@: (Kon AST :@: Kon binder :@: Kon sig :@: Var0))++instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (ScopedAST binder sig)+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (AST binder sig)++instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (ScopedAST binder sig)+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (AST binder sig)++instance Foil.InjectName (AST binder sig) where+  injectName = Var++-- * Substitution++-- | Substitution for free (scoped monads).+--+-- @since 0.0.1+{-# INLINE substitute #-}+substitute+  :: forall sig binder o i. (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)+  => Foil.Scope o+  -> Foil.Substitution (AST binder sig) i o+  -> AST binder sig i+  -> AST binder sig o+substitute = goSubst+  where+    -- The loop is local and takes the instances from 'substitute', so once+    -- 'substitute' is inlined at a known signature, the loop uses that+    -- signature's instances directly.+    goSubst+      :: Foil.Distinct o'+      => Foil.Scope o'+      -> Foil.Substitution (AST binder sig) i' o'+      -> AST binder sig i'+      -> AST binder sig o'+    goSubst scope subst term+      -- An empty substitution maps every name to itself ('addRename' deletes+      -- identity renames), so the result is the very term, and the coercion is+      -- the one 'Control.Monad.Foil.sink' performs. Substitutions go empty often: opening a+      -- scoped term with its own binder's name is an identity rename, and under+      -- a deterministic allocation policy a refreshed binder usually keeps its+      -- name, deleting its entry. Binders that shadow the ambient scope are+      -- left as they stand, as on the no-clash path below. A caller that wants+      -- them refreshed asks 'substituteRefreshed'.+      | Foil.nullSubst subst = unsafeCoerce term+      | otherwise = go term+      where+        -- The substitution is known non-empty here, and it can only change+        -- under a binder, so the walk between binders is unchecked and each+        -- binder entry re-enters 'goSubst', testing emptiness exactly once.+        go = \case+          Var name -> Foil.lookupSubst subst name+          Node node -> Node (bimap f go node)+        f (ScopedAST binder body) =+          Foil.withRefreshedPattern scope binder $ \extendSubst binder' scope' ->+            let subst' = extendSubst (Foil.sink subst)+                body' = goSubst scope' subst' body+            in ScopedAST binder' body'++-- | A version of 'substitute' that refreshes every binder of the input term.+--+-- The substituted terms are inserted as they are, so their binders are not+-- refreshed. Apply 'refreshAST' to the result to normalize all of its binders.+--+-- In general, 'substitute' is more efficient since it does not always refresh binders.+--+-- @since 0.0.3+{-# INLINABLE substituteRefreshed #-}+substituteRefreshed+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)+  => Foil.Scope o+  -> Foil.Substitution (AST binder sig) i o+  -> AST binder sig i+  -> AST binder sig o+substituteRefreshed scope subst = \case+  Var name -> Foil.lookupSubst subst name+  Node node -> Node (bimap f (substituteRefreshed scope subst) node)+  where+    f (ScopedAST binder body) =+      Foil.withFreshPattern scope binder $ \extendSubst binder' scope' ->+        let subst' = extendSubst (Foil.sink subst)+            body' = substituteRefreshed scope' subst' body+        in ScopedAST binder' body'++-- | @'AST' binder sig@ is a monad relative to t'Control.Monad.Foil.Name'.+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder)+  => Foil.RelMonad Foil.Name (AST binder sig) where+  rreturn = Var+  rbind scope term subst =+    case term of+      Var name  -> subst name+      Node node -> Node (bimap g' g node)+    where+      g x = Foil.rbind scope x subst+      g' (ScopedAST binder body) =+        Foil.withRefreshedPattern' scope binder $ \extendSubst binder' scope' ->+          let subst' = extendSubst subst+           in ScopedAST binder' (Foil.rbind scope' body subst')++-- | Substitute terms for the names a pattern binds in a body, and apply an+-- environment to the body's other names.+--+-- @since 0.2.0+{-# INLINABLE substitutePattern #-}+substitutePattern+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder, Foil.SinkableK binder)+  => Foil.Scope o                           -- ^ Resulting scope.+  -> Foil.Substitution (AST binder sig) n o -- ^ Environment mapping names in scope @n@.+  -> binder' n i                            -- ^ Binders that extend scope @n@ to scope @i@.+  -> [AST binder sig o]                     -- ^ Terms for the bound names, in binding order ('error' if too few, extras ignored).+  -> AST binder sig i+  -> AST binder sig o+substitutePattern scope env binders args body =+  substitute scope env' body+  where+    env' = Foil.addSubstPattern env binders args++-- * Transformations between signatures++-- | Fold a term bottom-up into a scope-indexed carrier @r@. A variable goes+-- through the first function, a scoped subterm through the second, given its+-- binder and the fold of its body, and a node through the third, once its+-- subterms are folded. The scope indices stay as they are, so the carrier+-- can be another kind of term, as in 'hoistAST', or anything indexed by the+-- scope, such as @'Const' Int@ for a node count.+--+-- To change the binder type as well, map it in the second function:+--+-- > foldAST Var (\binder body -> ScopedAST (toBinder binder) body) Node+--+-- @since 0.6.0+{-# INLINABLE foldAST #-}+foldAST+  :: forall binder sig r s n. Bifunctor sig+  => (forall m. Foil.Name m -> r m)             -- ^ A variable.+  -> (forall m l. binder m l -> r l -> s m)     -- ^ A scoped subterm, from its binder and the fold of its body.+  -> (forall m. sig (s m) (r m) -> r m)         -- ^ A node, its subterms folded.+  -> AST binder sig n+  -> r n+foldAST var scoped node = go+  where+    go :: forall m. AST binder sig m -> r m+    go (Var x)  = var x+    go (Node t) = node (bimap (\(ScopedAST binder body) -> scoped binder (go body)) go t)++-- | Change the signature of a term by a natural transformation of+-- signatures, keeping the binders, as @hoistFree@ of the free package does+-- for a free monad. Each node is rebuilt, so this costs a traversal.+--+-- @since 0.6.0+{-# INLINABLE hoistAST #-}+hoistAST+  :: Bifunctor sig+  => (forall a b. sig a b -> sig' a b)+  -> AST binder sig n+  -> AST binder sig' n+hoistAST f = foldAST Var ScopedAST (Node . f)++-- * \(\alpha\)-equivalence++-- | Refresh (force) all binders in a term, minimizing the used indices.+--+-- @since 0.0.3+{-# INLINABLE refreshAST #-}+refreshAST+  :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)+  => Foil.Scope n+  -> AST binder sig n+  -> AST binder sig n+refreshAST scope = \case+  t@Var{} -> t+  Node t -> Node (bimap (refreshScopedAST scope) (refreshAST scope) t)++-- | Similar to `refreshAST`, but for scoped terms.+--+-- @since 0.0.3+{-# INLINABLE refreshScopedAST #-}+refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)+  => Foil.Scope n+  -> ScopedAST binder sig n+  -> ScopedAST binder sig n+refreshScopedAST scope (ScopedAST binder body) =+  Foil.withFreshPattern scope binder $ \extendSubst binder' scope' ->+    let subst = extendSubst (Foil.sink Foil.identitySubst)+    in ScopedAST binder' (substituteRefreshed scope' subst body)++-- | \(\alpha\)-equivalence check for two terms in one scope+-- via normalization of bound identifiers (via 'refreshAST').+--+-- Compared to 'alphaEquiv', this function renames every binder on both sides+-- unconditionally, so it does strictly more work. It remains as an+-- independent implementation of the same test. Like 'alphaEquiv', it compares+-- patterns with 'Control.Monad.Foil.unifyPatternsIn', so the payloads of a+-- pattern are compared as well.+--+-- @since 0.0.3+{-# INLINABLE alphaEquivRefreshed #-}+alphaEquivRefreshed+  :: (Bifunctor sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)+  => Foil.Scope n+  -> AST binder sig n+  -> AST binder sig n+  -> Bool+alphaEquivRefreshed scope t1 t2 =+  unsafeEqASTIn scope (refreshAST scope t1) (refreshAST scope t2)++-- | A term is a scope-indexed value that can be compared up to α, which is what+-- a pattern carrying terms as payloads needs of them.+instance (ZipMatchK sig, Foil.UnifiablePattern binder)+    => Foil.AlphaEquiv (AST binder sig) where+  alphaEquivIn = alphaEquiv++-- | \(\alpha\)-equivalence check for two terms in one scope+-- via unification of bound variables (via 'unifyNameBinders').+--+-- When two matching binders coincide, comparison continues with no work at+-- all. When they differ, the prescribed renaming is /threaded down the+-- recursion/ (see 'alphaEquivEnv') and consulted at variables only, so+-- nothing is ever copied. Applying the renaming eagerly instead would+-- materialise a renamed copy of the remaining body at every mismatched+-- binder, which is quadratic on a chain of them.+--+-- @since 0.0.3+{-# INLINE alphaEquiv #-}+alphaEquiv+  :: (ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)+  => Foil.Scope n+  -> AST binder sig n+  -> AST binder sig n+  -> Bool+alphaEquiv = aeAlphaEquiv alphaEquivLoops++-- | Same as 'alphaEquiv' but for scoped terms.+--+-- While the binders of the two sides coincide, this runs with no renaming+-- state at all. The first pair that differs switches to 'alphaEquivEnv',+-- which threads the renamings down and switches back when they empty out.+--+-- @since 0.0.3+{-# INLINE alphaEquivScoped #-}+alphaEquivScoped+  :: forall sig binder n. (ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)+  => Foil.Scope n+  -> ScopedAST binder sig n+  -> ScopedAST binder sig n+  -> Bool+alphaEquivScoped = aeAlphaEquivScoped alphaEquivLoops++-- | The raw name a verdict's renaming assigns to a pattern's name.+--+-- @since 0.4.0+renamedId :: (Foil.NameBinder n a -> Foil.NameBinder n b) -> Foil.Name a -> Int+renamedId rename = Foil.nameId . Foil.nameOf . rename . Foil.UnsafeNameBinder++-- | Bind the paired names of a binder pair. A pair whose names coincide+-- shadows both sides identically and is deleted from the environments. A pair+-- whose names differ binds both to one fresh level. Continues with+-- 'alphaEquivEnv' on the bodies.+--+-- @since 0.4.0+{-# INLINE bindPairs #-}+bindPairs+  :: forall sig binder m l1 l2. (ZipMatchK sig, Foil.Distinct m, Foil.UnifiablePattern binder)+  => Int -> IntMap Int -> IntMap Int -> [(Int, Int)]+  -> Foil.Scope m+  -> AST binder sig l1 -> AST binder sig l2 -> Bool+bindPairs = aeBindPairs alphaEquivLoops++-- | The renaming-threading worker behind 'alphaEquiv': compare two terms+-- under partial renamings of their names into shared /levels/.+--+-- Each environment maps a raw name to the level of the binder pair that bound+-- it on the comparison path, and a name outside its environment stands for+-- itself. A variable occurrence then compares as a level against a level, or+-- as a raw name against a raw name, and the two can never be conflated. This+-- is what makes threading sound where applying a raw renaming at the variables+-- would not be, since a renamed name could collide with one that passes+-- through unchanged and happens to share the target spelling. Levels are also+-- why no capture check is needed: a level is never a name, so there is nothing+-- for a binder to capture.+--+-- A binder pair whose names coincide /deletes/ those names from both+-- environments, the pair shadowing both sides identically. When the+-- environments empty out the comparison drops back to the stateless+-- 'alphaEquiv', so only the region of the terms below a mismatched binder,+-- and above the point where the mismatch is shadowed away, pays for the+-- threading at all.+--+-- The indices of the two terms are deliberately independent, in the style+-- of 'unsafeEqAST': the terms are never renamed into a common scope, so+-- no common index exists to give them.+--+-- @since 0.4.0+{-# INLINE alphaEquivEnv #-}+alphaEquivEnv+  :: forall sig binder n n1 n2. (ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)+  => Int          -- ^ Next fresh level.+  -> IntMap Int   -- ^ Left renaming: raw name to the level that bound it.+  -> IntMap Int   -- ^ Right renaming.+  -> Foil.Scope n -- ^ Scope along the unified path (consulted by 'Control.Monad.Foil.unifyPatternsIn').+  -> AST binder sig n1+  -> AST binder sig n2+  -> Bool+alphaEquivEnv = aeAlphaEquivEnv alphaEquivLoops++-- | The scoped half of 'alphaEquivEnv': get the verdict from+-- 'Control.Monad.Foil.unifyPatternsIn', extend the environments as it prescribes, and+-- recurse into the bodies as they stand.+--+-- @since 0.4.0+{-# INLINE alphaEquivScopedEnv #-}+alphaEquivScopedEnv+  :: forall sig binder n n1 n2. (ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)+  => Int+  -> IntMap Int+  -> IntMap Int+  -> Foil.Scope n+  -> ScopedAST binder sig n1+  -> ScopedAST binder sig n2+  -> Bool+alphaEquivScopedEnv = aeAlphaEquivScopedEnv alphaEquivLoops++-- | The mutually recursive loops behind α-equivalence, one field per+-- function above.+--+-- @since 0.6.1+data AlphaEquivLoops binder sig = AlphaEquivLoops+  { aeAlphaEquiv :: forall n. Foil.Distinct n => Foil.Scope n -> AST binder sig n -> AST binder sig n -> Bool+  , aeAlphaEquivScoped :: forall n. Foil.Distinct n => Foil.Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool+  , aeBindPairs :: forall m l1 l2. Foil.Distinct m => Int -> IntMap Int -> IntMap Int -> [(Int, Int)] -> Foil.Scope m -> AST binder sig l1 -> AST binder sig l2 -> Bool+  , aeAlphaEquivEnv :: forall n n1 n2. Foil.Distinct n => Int -> IntMap Int -> IntMap Int -> Foil.Scope n -> AST binder sig n1 -> AST binder sig n2 -> Bool+  , aeAlphaEquivScopedEnv :: forall n n1 n2. Foil.Distinct n => Int -> IntMap Int -> IntMap Int -> Foil.Scope n -> ScopedAST binder sig n1 -> ScopedAST binder sig n2 -> Bool+  }++-- | The loops behind α-equivalence. They are local and take the instances+-- from this function, so once it is inlined at a known signature, they use+-- that signature's instances directly. A recursive function with class+-- constraints would instead be split by GHC into a wrapper and a worker+-- (some of its dictionaries, such as t'Control.Monad.Foil.Distinct', are never used at+-- runtime), and a client's @SPECIALIZE@ pragma would reach only the wrapper.+--+-- @since 0.6.1+{-# INLINE alphaEquivLoops #-}+alphaEquivLoops+  :: forall sig binder. (ZipMatchK sig, Foil.UnifiablePattern binder)+  => AlphaEquivLoops binder sig+alphaEquivLoops = AlphaEquivLoops goAlpha goScoped goPairs goEnv goScopedEnv+  where+    goAlpha+      :: Foil.Distinct n+      => Foil.Scope n+      -> AST binder sig n+      -> AST binder sig n+      -> Bool+    goAlpha _scope (Var x) (Var y) = x == y+    goAlpha scope (Node l) (Node r) =+      case zipMatchWith2 (unit . goScoped scope) (unit . goAlpha scope) l r of+        Nothing -> False+        Just _  -> True+      where+        unit f x = if f x then Just () else Nothing+    goAlpha _ _ _ = False++    goScoped+      :: forall n. Foil.Distinct n+      => Foil.Scope n+      -> ScopedAST binder sig n+      -> ScopedAST binder sig n+      -> Bool+    goScoped scope+      (ScopedAST binder1 body1)+      (ScopedAST binder2 body2) =+        case Foil.unifyPatternsIn scope binder1 binder2 of+          -- the binders coincide: compare the bodies as they stand+          Foil.SameNameBinders{} ->  -- after seeing this we know that body scopes are the same+            case Foil.assertDistinct binder1 of+              Foil.Distinct ->+                let scope1 = Foil.extendScopePattern binder1 scope+                in goAlpha scope1 body1 body2+          -- the left binder is renamed towards the right one+          Foil.RenameLeftNameBinder _ rename1to2 ->+            case Foil.assertDistinct binder2 of+              Foil.Distinct ->+                let scope2 = Foil.extendScopePattern binder2 scope+                    pairs = [ (Foil.nameId x, renamedId rename1to2 x)+                            | x <- Foil.namesOfPattern binder1 ]+                in enterEnv pairs scope2 body1 body2+          -- the right binder is renamed towards the left one+          Foil.RenameRightNameBinder _ rename2to1 ->+            case Foil.assertDistinct binder1 of+              Foil.Distinct ->+                let scope1 = Foil.extendScopePattern binder1 scope+                    pairs = [ (renamedId rename2to1 y, Foil.nameId y)+                            | y <- Foil.namesOfPattern binder2 ]+                in enterEnv pairs scope1 body1 body2+          -- both are renamed towards a unified pattern: pair the two sides'+          -- names through the unified name each maps to+          Foil.RenameBothBinders binder' rename1 rename2 ->+            case Foil.assertDistinct binder' of+              Foil.Distinct ->+                let scope' = Foil.extendScopePattern binder' scope+                    leftU = IntMap.fromList+                      [ (renamedId rename1 x, Foil.nameId x)+                      | x <- Foil.namesOfPattern binder1 ]+                    rightU = IntMap.fromList+                      [ (renamedId rename2 y, Foil.nameId y)+                      | y <- Foil.namesOfPattern binder2 ]+                    pairs = IntMap.elems (IntMap.intersectionWith (,) leftU rightU)+                in enterEnv pairs scope' body1 body2+          -- if we cannot unify patterns then scopes are not alpha-equivalent+          Foil.NotUnifiable -> False+      where+        enterEnv+          :: forall m l1 l2. Foil.Distinct m+          => [(Int, Int)] -> Foil.Scope m+          -> AST binder sig l1 -> AST binder sig l2 -> Bool+        enterEnv pairs scope' = goPairs 0 IntMap.empty IntMap.empty pairs scope'++    goPairs+      :: forall m l1 l2. Foil.Distinct m+      => Int -> IntMap Int -> IntMap Int -> [(Int, Int)]+      -> Foil.Scope m+      -> AST binder sig l1 -> AST binder sig l2 -> Bool+    goPairs lvl envL envR pairs scope body1 body2 = case pairs of+      [] -> goEnv lvl envL envR scope body1 body2+      ((x, y) : rest)+        | x == y    -> goPairs lvl (IntMap.delete x envL) (IntMap.delete y envR) rest scope body1 body2+        | otherwise -> goPairs (lvl + 1) (IntMap.insert x lvl envL) (IntMap.insert y lvl envR) rest scope body1 body2++    goEnv+      :: forall n n1 n2. Foil.Distinct n+      => Int          -- ^ Next fresh level.+      -> IntMap Int   -- ^ Left renaming: raw name to the level that bound it.+      -> IntMap Int   -- ^ Right renaming.+      -> Foil.Scope n -- ^ Scope along the unified path (consulted by 'Control.Monad.Foil.unifyPatternsIn').+      -> AST binder sig n1+      -> AST binder sig n2+      -> Bool+    goEnv lvl envL envR scope t1 t2+      | IntMap.null envL && IntMap.null envR =+          -- The renamings have emptied out (or never held anything): the+          -- terms coincide raw-for-raw from here on, so compare them where+          -- they stand. The coercion brings both indices to the scope's,+          -- which is the unified path the comparison speaks of.+          goAlpha scope (unsafeCoerce t1 :: AST binder sig n) (unsafeCoerce t2 :: AST binder sig n)+      | otherwise = case (t1, t2) of+          (Var x, Var y) ->+            case (IntMap.lookup (Foil.nameId x) envL, IntMap.lookup (Foil.nameId y) envR) of+              (Just k1, Just k2) -> k1 == k2+              (Nothing, Nothing) -> Foil.nameId x == Foil.nameId y+              _                  -> False+          (Node l, Node r) ->+            case zipMatchWith2+                   (unit . goScopedEnv lvl envL envR scope)+                   (unit . goEnv lvl envL envR scope) l r of+              Nothing -> False+              Just _  -> True+          _ -> False+      where+        unit f x = if f x then Just () else Nothing++    goScopedEnv+      :: forall n n1 n2. Foil.Distinct n+      => Int+      -> IntMap Int+      -> IntMap Int+      -> Foil.Scope n+      -> ScopedAST binder sig n1+      -> ScopedAST binder sig n2+      -> Bool+    goScopedEnv lvl envL envR scope scoped1 scoped2 =+      -- The scoped terms are compared where they stand; the coercion only+      -- brings their indices to the scope's, which is the unified path the+      -- environments and the verdicts speak of.+      case (unsafeCoerce scoped1 :: ScopedAST binder sig n, unsafeCoerce scoped2 :: ScopedAST binder sig n) of+        (ScopedAST binder1 body1, ScopedAST binder2 body2) ->+          case Foil.unifyPatternsIn scope binder1 binder2 of+            -- the binders coincide: the pair shadows both sides identically+            Foil.SameNameBinders{} ->+              case Foil.assertDistinct binder1 of+                Foil.Distinct ->+                  let scope' = Foil.extendScopePattern binder1 scope+                      names = map Foil.nameId (Foil.namesOfPattern binder1)+                      envL' = deleteAll names envL+                      envR' = deleteAll names envR+                   in goEnv lvl envL' envR' scope' body1 body2+            -- the left binder is renamed towards the right one+            Foil.RenameLeftNameBinder _ rename1to2 ->+              case Foil.assertDistinct binder2 of+                Foil.Distinct ->+                  let scope' = Foil.extendScopePattern binder2 scope+                      pairs = [ (Foil.nameId x, renamedId rename1to2 x)+                              | x <- Foil.namesOfPattern binder1 ]+                   in goPairs lvl envL envR pairs scope' body1 body2+            -- the right binder is renamed towards the left one+            Foil.RenameRightNameBinder _ rename2to1 ->+              case Foil.assertDistinct binder1 of+                Foil.Distinct ->+                  let scope' = Foil.extendScopePattern binder1 scope+                      pairs = [ (renamedId rename2to1 y, Foil.nameId y)+                              | y <- Foil.namesOfPattern binder2 ]+                   in goPairs lvl envL envR pairs scope' body1 body2+            -- both are renamed towards a unified pattern: pair the two sides'+            -- names through the unified name each maps to+            Foil.RenameBothBinders binder' rename1 rename2 ->+              case Foil.assertDistinct binder' of+                Foil.Distinct ->+                  let scope' = Foil.extendScopePattern binder' scope+                      leftU = IntMap.fromList+                        [ (renamedId rename1 x, Foil.nameId x)+                        | x <- Foil.namesOfPattern binder1 ]+                      rightU = IntMap.fromList+                        [ (renamedId rename2 y, Foil.nameId y)+                        | y <- Foil.namesOfPattern binder2 ]+                      pairs = IntMap.elems (IntMap.intersectionWith (,) leftU rightU)+                   in goPairs lvl envL envR pairs scope' body1 body2+            Foil.NotUnifiable -> False+      where+        deleteAll names env = case names of+          []       -> env+          (i : is) -> deleteAll is (IntMap.delete i env)++-- ** Unsafe equality checks++-- | /Unsafe/ equality check for two terms. Names are compared by their raw+-- identifiers, and patterns by 'Control.Monad.Foil.Internal.unsafeEqPattern', which uses the+-- binder-only 'Control.Monad.Foil.unifyPatterns'. Thus α-equivalent terms whose binders+-- differ compare unequal, so normalize both sides with 'refreshAST' first.+--+-- @since 0.0.3+{-# INLINE unsafeEqAST #-}+unsafeEqAST+  :: (ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)+  => AST binder sig n+  -> AST binder sig l+  -> Bool+unsafeEqAST = eqAST unsafeEqLoops++-- | A version of 'unsafeEqAST' for scoped terms.+--+-- @since 0.0.3+{-# INLINE unsafeEqScopedAST #-}+unsafeEqScopedAST+  :: (ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)+  => ScopedAST binder sig n+  -> ScopedAST binder sig l+  -> Bool+unsafeEqScopedAST = eqScopedAST unsafeEqLoops++-- | The two mutually recursive loops behind 'unsafeEqAST' and+-- 'unsafeEqScopedAST'.+--+-- @since 0.6.1+data EqLoops binder sig = EqLoops+  { eqAST       :: forall n l. (Foil.Distinct n, Foil.Distinct l) => AST binder sig n -> AST binder sig l -> Bool+  , eqScopedAST :: forall n l. (Foil.Distinct n, Foil.Distinct l) => ScopedAST binder sig n -> ScopedAST binder sig l -> Bool+  }++-- | The loops behind 'unsafeEqAST' and 'unsafeEqScopedAST', local for the+-- same reason as those of 'alphaEquivLoops'.+--+-- @since 0.6.1+{-# INLINE unsafeEqLoops #-}+unsafeEqLoops+  :: forall sig binder. (ZipMatchK sig, Foil.UnifiablePattern binder)+  => EqLoops binder sig+unsafeEqLoops = EqLoops goAST goScoped+  where+    goAST :: forall n l. (Foil.Distinct n, Foil.Distinct l) => AST binder sig n -> AST binder sig l -> Bool+    goAST (Var x) (Var y) = Foil.nameId x == Foil.nameId y+    goAST (Node t1) (Node t2) =+      case zipMatchWith2 (unit . goScoped) (unit . goAST) t1 t2 of+        Nothing -> False+        Just _  -> True+    goAST _ _ = False++    goScoped :: forall n l. (Foil.Distinct n, Foil.Distinct l) => ScopedAST binder sig n -> ScopedAST binder sig l -> Bool+    goScoped (ScopedAST binder1 body1) (ScopedAST binder2 body2) = and+      [ Foil.unsafeEqPattern binder1 binder2+      , case (Foil.assertDistinct binder1, Foil.assertDistinct binder2) of+          (Foil.Distinct, Foil.Distinct) -> body1 `goAST` body2+      ]++    unit f x = if f x then Just () else Nothing++-- | /Unsafe/ equality check for two terms in one scope. Names are compared+-- directly, and patterns by 'Control.Monad.Foil.unifyPatternsIn', which must+-- find their binders the same. Thus α-equivalent terms whose binders differ+-- compare unequal, so normalize both sides with 'refreshAST' first, as+-- 'alphaEquivRefreshed' does.+--+-- Unlike 'unsafeEqAST', this compares the payloads of patterns, which+-- 'Control.Monad.Foil.unifyPatternsIn' needs the scope for.+--+-- @since 0.6.1+{-# INLINE unsafeEqASTIn #-}+unsafeEqASTIn+  :: (ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n)+  => Foil.Scope n+  -> AST binder sig n+  -> AST binder sig n+  -> Bool+unsafeEqASTIn = eqASTIn unsafeEqInLoops++-- | A version of 'unsafeEqASTIn' for scoped terms.+--+-- @since 0.6.1+{-# INLINE unsafeEqScopedASTIn #-}+unsafeEqScopedASTIn+  :: (ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n)+  => Foil.Scope n+  -> ScopedAST binder sig n+  -> ScopedAST binder sig n+  -> Bool+unsafeEqScopedASTIn = eqScopedASTIn unsafeEqInLoops++-- | The two mutually recursive loops behind 'unsafeEqASTIn' and+-- 'unsafeEqScopedASTIn'.+--+-- @since 0.6.1+data EqInLoops binder sig = EqInLoops+  { eqASTIn       :: forall n. Foil.Distinct n => Foil.Scope n -> AST binder sig n -> AST binder sig n -> Bool+  , eqScopedASTIn :: forall n. Foil.Distinct n => Foil.Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool+  }++-- | The loops behind 'unsafeEqASTIn' and 'unsafeEqScopedASTIn', local for+-- the same reason as those of 'alphaEquivLoops'.+--+-- @since 0.6.1+{-# INLINE unsafeEqInLoops #-}+unsafeEqInLoops+  :: forall sig binder. (ZipMatchK sig, Foil.UnifiablePattern binder)+  => EqInLoops binder sig+unsafeEqInLoops = EqInLoops goAST goScoped+  where+    goAST :: forall n. Foil.Distinct n => Foil.Scope n -> AST binder sig n -> AST binder sig n -> Bool+    goAST _ (Var x) (Var y) = x == y+    goAST scope (Node t1) (Node t2) =+      case zipMatchWith2 (unit . goScoped scope) (unit . goAST scope) t1 t2 of+        Nothing -> False+        Just _  -> True+    goAST _ _ _ = False++    goScoped :: forall n. Foil.Distinct n => Foil.Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool+    goScoped scope (ScopedAST binder1 body1) (ScopedAST binder2 body2) =+      case Foil.unifyPatternsIn scope binder1 binder2 of+        Foil.SameNameBinders{} -> case Foil.assertDistinct binder1 of+          Foil.Distinct -> goAST (Foil.extendScopePattern binder1 scope) body1 body2+        _ -> False++    unit f x = if f x then Just () else Nothing++-- * Converting to and from free foil++-- ** Convert to free foil++-- | An identifier a raw term mentions that the names given for conversion do+-- not account for.+--+-- Note what this does and does not carry. It cannot carry a position: the+-- conversion functions are generic in the raw term and only ever see it through+-- @toSig@, so a source location, if the syntax has one, is not theirs to read.+-- What they do know, and a caller checking names beforehand does not, is which+-- names were in scope /at the occurrence/, the binders passed on the way down+-- included. That is what a \"did you mean\" needs.+--+-- @since 0.4.0+data UnresolvedName rawIdent = UnresolvedName+  { unresolvedIdent   :: rawIdent+    -- ^ The identifier that did not resolve.+  , unresolvedInScope :: [rawIdent]+    -- ^ What was in scope where it occurred.+  } deriving (Eq, Show, Functor, Foldable, Traversable)++-- | The identifiers a raw term mentions that a set of names cannot resolve, in+-- the order they occur.+--+-- This is 'unsafeConvertToAST' with the conversion left out, so it descends+-- under binders in the same way and accounts for what they bind. A caller+-- that converts with 'tryConvertToASTWith' should use 'unresolvedNamesWith'+-- instead, so that its constants do not count as unresolved.+--+-- @since 0.4.0+unresolvedNames+  :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n.+     (Foil.Distinct n, Bifoldable sig, Ord rawIdent, Foil.CoSinkable binder)+  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))+  -- ^ Unpeel one syntax node (or a variable) from a raw term.+  -> (forall x z. Foil.Distinct x+      => Foil.Scope x+      -> Map rawIdent (Foil.Name x)+      -> rawPattern+      -> (forall y. Foil.DExt x y+          => binder x y+          -> Map rawIdent (Foil.Name y)+          -> z)+      -> z)+  -- ^ Convert raw pattern into a scope-safe pattern.+  -> (rawScopedTerm -> rawTerm)+  -- ^ Extract a term from a scoped term (or crash).+  -> Foil.Scope n+  -- ^ Resulting scope of the constructed term.+  -> Map rawIdent (Foil.Name n)+  -- ^ Known names of free variables in scope @n@.+  -> rawTerm+  -- ^ Raw term.+  -> [UnresolvedName rawIdent]+unresolvedNames toSig fromRawPattern getScopedTerm scope names =+  unresolvedNamesWith toSig fromRawPattern getScopedTerm scope names Map.empty++-- | The identifiers a raw term mentions that neither a set of names nor a+-- table of constants can resolve, in the order they occur. This is+-- 'unresolvedNames' for the arguments of 'tryConvertToASTWith': given the same+-- names and constants, it reports every identifier that+-- 'tryConvertToASTWith' would fail on, and the first of them is the one that+-- 'tryConvertToASTWith' reports.+--+-- @since 0.6.1+unresolvedNamesWith+  :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n.+     (Foil.Distinct n, Bifoldable sig, Ord rawIdent, Foil.CoSinkable binder)+  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))+  -- ^ Unpeel one syntax node (or a variable) from a raw term.+  -> (forall x z. Foil.Distinct x+      => Foil.Scope x+      -> Map rawIdent (Foil.Name x)+      -> rawPattern+      -> (forall y. Foil.DExt x y+          => binder x y+          -> Map rawIdent (Foil.Name y)+          -> z)+      -> z)+  -- ^ Convert raw pattern into a scope-safe pattern.+  -> (rawScopedTerm -> rawTerm)+  -- ^ Extract a term from a scoped term (or crash).+  -> Foil.Scope n+  -- ^ Resulting scope of the constructed term.+  -> Map rawIdent (Foil.Name n)+  -- ^ Known names of free variables in scope @n@.+  -> Map rawIdent (AST binder sig n)+  -- ^ Identifiers that denote a term rather than a variable.+  -> rawTerm+  -- ^ Raw term.+  -> [UnresolvedName rawIdent]+unresolvedNamesWith toSig fromRawPattern getScopedTerm scope0 names0 terms =+  go scope0 names0+  where+    constants = Map.keys terms++    go :: forall x. Foil.Distinct x+       => Foil.Scope x -> Map rawIdent (Foil.Name x) -> rawTerm -> [UnresolvedName rawIdent]+    go scope names t = case toSig t of+      Left x+        | Map.member x names || Map.member x terms -> []+        | otherwise -> [UnresolvedName x (Map.keys names <> constants)]+      Right node -> bifoldMap (goScoped scope names) (go scope names) node++    goScoped :: forall x. Foil.Distinct x+             => Foil.Scope x -> Map rawIdent (Foil.Name x)+             -> (rawPattern, rawScopedTerm) -> [UnresolvedName rawIdent]+    goScoped scope names (pat, scopedTerm) =+      fromRawPattern scope names pat $ \binder' names' ->+        go (Foil.extendScopePattern binder' scope) names' (getScopedTerm scopedTerm)++-- | Convert a raw term into a scope-safe term, reporting the first identifier+-- that does not resolve.+--+-- One pass, short-circuiting at the first failure, so a term that resolves+-- costs no more than 'unsafeConvertToAST' does. The report is complete for+-- that one identifier, since 'unresolvedInScope' is built where the conversion+-- fails and is never computed on the way through.+--+-- A caller wanting /every/ unresolved identifier rather than the first pays a+-- second pass for it, with 'unresolvedNames'. The successful path stays fast+-- that way, and a failure can afford to be walked again for a better message.+--+-- @since 0.4.0+tryConvertToAST+  :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n.+     (Foil.Distinct n, Bitraversable sig, Ord rawIdent,+      Foil.CoSinkable binder, Foil.SinkableK binder)+  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))+  -- ^ Unpeel one syntax node (or a variable) from a raw term.+  -> (forall x z. Foil.Distinct x+      => Foil.Scope x+      -> Map rawIdent (Foil.Name x)+      -> rawPattern+      -> (forall y. Foil.DExt x y+          => binder x y+          -> Map rawIdent (Foil.Name y)+          -> z)+      -> z)+  -- ^ Convert raw pattern into a scope-safe pattern.+  -> (rawScopedTerm -> rawTerm)+  -- ^ Extract a term from a scoped term (or crash).+  -> Foil.Scope n+  -- ^ Resulting scope of the constructed term.+  -> Map rawIdent (Foil.Name n)+  -- ^ Known names of free variables in scope @n@.+  -> rawTerm+  -- ^ Raw term.+  -> Either (UnresolvedName rawIdent) (AST binder sig n)+tryConvertToAST toSig fromRawPattern getScopedTerm scope names =+  tryConvertToASTWith toSig fromRawPattern getScopedTerm scope names Map.empty++-- | Convert a raw term into a scope-safe term, resolving some identifiers to+-- whole terms rather than to variables.+--+-- The extra table is what a language with /constants/ needs: an identifier that+-- denotes a top-level declaration, a primitive, or an abbreviation stands for+-- something that is not a variable, and resolving it during conversion is the+-- only place where the binders are known. Doing it in a pass of one's own means+-- writing a binder-aware traversal of the raw syntax by hand.+--+-- Variables win: the table of names is consulted first, so a binder shadows an+-- entry here, and an entry here shadows nothing. The table is sunk when going+-- under a binder, exactly as the names are, so its entries may mention anything+-- in scope where conversion started and need not be closed.+--+-- @since 0.4.0+tryConvertToASTWith+  :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n.+     (Foil.Distinct n, Bitraversable sig, Ord rawIdent,+      Foil.CoSinkable binder, Foil.SinkableK binder)+  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))+  -- ^ Unpeel one syntax node (or a variable) from a raw term.+  -> (forall x z. Foil.Distinct x+      => Foil.Scope x+      -> Map rawIdent (Foil.Name x)+      -> rawPattern+      -> (forall y. Foil.DExt x y+          => binder x y+          -> Map rawIdent (Foil.Name y)+          -> z)+      -> z)+  -- ^ Convert raw pattern into a scope-safe pattern.+  -> (rawScopedTerm -> rawTerm)+  -- ^ Extract a term from a scoped term (or crash).+  -> Foil.Scope n+  -- ^ Resulting scope of the constructed term.+  -> Map rawIdent (Foil.Name n)+  -- ^ Known names of free variables in scope @n@.+  -> Map rawIdent (AST binder sig n)+  -- ^ Identifiers that denote a term rather than a variable.+  -> rawTerm+  -- ^ Raw term.+  -> Either (UnresolvedName rawIdent) (AST binder sig n)+tryConvertToASTWith toSig fromRawPattern getScopedTerm = go+  where+    go :: forall x. Foil.Distinct x+       => Foil.Scope x -> Map rawIdent (Foil.Name x)+       -> Map rawIdent (AST binder sig x) -> rawTerm+       -> Either (UnresolvedName rawIdent) (AST binder sig x)+    go scope names terms t = case toSig t of+      Left x -> case Map.lookup x names of+        Just name -> Right (Var name)+        Nothing   -> case Map.lookup x terms of+          Just term -> Right term+          Nothing   -> Left (UnresolvedName x (Map.keys names <> Map.keys terms))+      Right node ->+        Node <$> bitraverse (goScoped scope names terms) (go scope names terms) node++    goScoped :: forall x. Foil.Distinct x+             => Foil.Scope x -> Map rawIdent (Foil.Name x)+             -> Map rawIdent (AST binder sig x)+             -> (rawPattern, rawScopedTerm)+             -> Either (UnresolvedName rawIdent) (ScopedAST binder sig x)+    goScoped scope names terms (pat, scopedTerm) =+      fromRawPattern scope names pat $ \binder' names' ->+        ScopedAST binder'+          <$> go (Foil.extendScopePattern binder' scope) names'+                 (Foil.sink1 terms) (getScopedTerm scopedTerm)++-- | Convert a raw term into a scope-safe term, calling 'error' on an+-- identifier that does not resolve.+--+-- Prefer 'tryConvertToAST', which reports such identifiers. This is for callers+-- that have already established that every name resolves.+--+-- @since 0.4.0+unsafeConvertToAST+  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)+  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))+  -- ^ Unpeel one syntax node (or a variable) from a raw term.+  -> (forall x z. Foil.Distinct x+      => Foil.Scope x+      -> Map rawIdent (Foil.Name x)+      -> rawPattern+      -> (forall y. Foil.DExt x y+          => binder x y+          -> Map rawIdent (Foil.Name y)+          -> z)+      -> z)+  -- ^ Convert raw pattern into a scope-safe pattern.+  -> (rawScopedTerm -> rawTerm)+  -- ^ Extract a term from a scoped term (or crash).+  -> Foil.Scope n+  -- ^ Resulting scope of the constructed term.+  -> Map rawIdent (Foil.Name n)+  -- ^ Known names of free variables in scope @n@.+  -> rawTerm+  -- ^ Raw term.+  -> AST binder sig n+unsafeConvertToAST toSig fromRawPattern getScopedTerm scope names t =+  case toSig t of+    Left x ->+      case Map.lookup x names of+        Nothing   -> error "undefined variable"+        Just name -> Var name+    Right node -> Node $+      bimap+        (unsafeConvertToScopedAST toSig fromRawPattern getScopedTerm scope names)+        (unsafeConvertToAST toSig fromRawPattern getScopedTerm scope names)+        node++-- | Same as 'unsafeConvertToAST' but for scoped terms.+--+-- @since 0.4.0+unsafeConvertToScopedAST+  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)+  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))+  -- ^ Unpeel one syntax node (or a variable) from a raw term.+  -> (forall x z. Foil.Distinct x+      => Foil.Scope x+      -> Map rawIdent (Foil.Name x)+      -> rawPattern+      -> (forall y. Foil.DExt x y+          => binder x y+          -> Map rawIdent (Foil.Name y)+          -> z)+      -> z)+  -- ^ Convert raw pattern into a scope-safe pattern.+  -> (rawScopedTerm -> rawTerm)+  -- ^ Extract a term from a scoped term (or crash).+  -> Foil.Scope n+  -- ^ Resulting scope of the constructed term.+  -> Map rawIdent (Foil.Name n)+  -- ^ Known names of free variables in scope @n@.+  -> (rawPattern, rawScopedTerm)+  -- ^ A pair of a pattern and a corresponding scoped term.+  -> ScopedAST binder sig n+unsafeConvertToScopedAST toSig fromRawPattern getScopedTerm scope names (pat, scopedTerm) =+  fromRawPattern scope names pat $ \binder' names' ->+    let scope' = Foil.extendScopePattern binder' scope+     in ScopedAST binder' (unsafeConvertToAST toSig fromRawPattern getScopedTerm scope' names' (getScopedTerm scopedTerm))++-- ** Convert from free foil++-- | Convert a scope-safe term back into a raw term.+-- Use 'convertFromASTWith' to name free variables separately from bound ones.+--+-- @since 0.0.3+convertFromAST+  :: Bifunctor sig+  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)+  -- ^ Peel back one layer of syntax.+  -> (rawIdent -> rawTerm)+  -- ^ Convert identifier into a raw variable term.+  -> (forall x y. binder x y -> rawPattern)+  -- ^ Convert scope-safe pattern into a raw pattern.+  -> (rawTerm -> rawScopedTerm)+  -- ^ Wrap raw term into a scoped term.+  -> (Int -> rawIdent)+  -- ^ Name a variable, bound or free, from its underlying integer identifier.+  -> AST binder sig n+  -- ^ Scope-safe term.+  -> rawTerm+convertFromAST fromSig fromVar makePattern makeScoped f = \case+  Var x -> fromVar (f (Foil.nameId x))+  Node node -> fromSig $+    bimap+      (convertFromScopedAST fromSig fromVar makePattern makeScoped f)+      (convertFromAST fromSig fromVar makePattern makeScoped f)+      node++-- | Same as 'convertFromAST' but for scoped terms.+--+-- @since 0.0.3+convertFromScopedAST+  :: Bifunctor sig+  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)+  -- ^ Peel back one layer of syntax.+  -> (rawIdent -> rawTerm)+  -- ^ Convert identifier into a raw variable term.+  -> (forall x y. binder x y -> rawPattern)+  -- ^ Convert scope-safe pattern into a raw pattern.+  -> (rawTerm -> rawScopedTerm)+  -- ^ Wrap raw term into a scoped term.+  -> (Int -> rawIdent)+  -- ^ Name a variable, bound or free, from its underlying integer identifier.+  -> ScopedAST binder sig n+  -- ^ Scope-safe scoped term.+  -> (rawPattern, rawScopedTerm)+convertFromScopedAST fromSig fromVar makePattern makeScoped f = \case+  ScopedAST binder body ->+    ( makePattern binder+    , makeScoped (convertFromAST fromSig fromVar makePattern makeScoped f body))++-- | Convert a scope-safe term back into a raw term, naming the variables that+-- occur /free in the whole term/ separately from the bound ones.+--+-- 'convertFromAST' applies one naming function to every variable it meets,+-- bound or free, and gives it only a raw name. That is often not enough, since+-- raw names are not unique across scope indices: a binder inside a term may+-- share one with a name of the ambient scope, so naming by raw name alone can+-- print a bound variable as whatever the ambient scope calls that name.+--+-- Keeping the typed name is what distinguishes them, and 'Control.Monad.Foil.unsinkNamePattern'+-- is the operation for it: composing one per binder on the way down builds a+-- @t'Control.Monad.Foil.Name' x -> 'Maybe' ( t'Control.Monad.Foil.Name' n )@ that answers exactly the question.+--+-- @since 0.4.0+convertFromASTWith+  :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n.+     (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder)+  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)+  -- ^ Peel back one layer of syntax.+  -> (rawIdent -> rawTerm)+  -- ^ Convert identifier into a raw variable term.+  -> (forall x y. binder x y -> rawPattern)+  -- ^ Convert scope-safe pattern into a raw pattern.+  -> (rawTerm -> rawScopedTerm)+  -- ^ Wrap raw term into a scoped term.+  -> (Foil.Name n -> rawIdent)+  -- ^ Name a variable that is free in the whole term.+  -> (Int -> rawIdent)+  -- ^ Name a bound variable, from its underlying integer identifier.+  -> AST binder sig n+  -- ^ Scope-safe term.+  -> rawTerm+convertFromASTWith fromSig fromVar makePattern makeScoped freeName boundName =+    go Just+  where+    go :: forall x. Foil.Distinct x+       => (Foil.Name x -> Maybe (Foil.Name n)) -> AST binder sig x -> rawTerm+    go unsink = \case+      Var x -> fromVar $ case unsink x of+        Just name -> freeName name+        Nothing   -> boundName (Foil.nameId x)+      Node node -> fromSig (bimap (goScoped unsink) (go unsink) node)++    goScoped :: forall x. Foil.Distinct x+             => (Foil.Name x -> Maybe (Foil.Name n))+             -> ScopedAST binder sig x -> (rawPattern, rawScopedTerm)+    goScoped unsink (ScopedAST binder body) =+      case Foil.assertDistinct binder of+        Foil.Distinct ->+          ( makePattern binder+          , makeScoped+              (go (\name -> Foil.unsinkNamePattern binder name >>= unsink) body) )++-- ** Unsinking AST++-- | The support of a term: exactly the names that occur free in it.+--+-- This is the annotation that co-de-Bruijn syntax carries intrinsically and+-- that the foil does not need for weakening, since 'Control.Monad.Foil.sink' is a coercion.+-- Computing it traverses the whole term, so a client that restricts often+-- should cache it.+--+-- @since 0.4.0+supportOf+  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig)+  => AST binder sig n -> Foil.NameSet n+supportOf = \case+  Var name  -> Foil.nameSetSingleton name+  Node node -> bifoldMap supportOfScopedAST supportOf node++-- | The support of a scoped term, in the scope /outside/ its binder.+--+-- @since 0.4.0+supportOfScopedAST+  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig)+  => ScopedAST binder sig n -> Foil.NameSet n+supportOfScopedAST (ScopedAST binder body) =+  case Foil.assertDistinct binder of+    Foil.Distinct -> Foil.unsinkNameSet binder (supportOf body)++-- | Cut a term down to the scope of exactly the names it uses.+--+-- The term's support is computed with 'supportOf', as in 'unsinkAST', but+-- nothing is tested and nothing can fail, since the term inhabits the+-- restricted scope by construction. @t'Control.Monad.Foil.Ext' m n@ comes back with it, so+-- the term can be 'Control.Monad.Foil.sink'ed to where it came from for free.+--+-- Verifying a declared dependency, such as a @uses@ clause or a module's+-- parameters, is this plus a comparison: compute the scope a term really+-- inhabits, and check the declared one against it.+--+-- @since 0.4.0+withRelevantScope+  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig)+  => AST binder sig n+  -> (forall m. (Foil.Ext m n, Foil.Distinct m)+      => Foil.Scope m -> AST binder sig m -> r)+  -> r+withRelevantScope term cont =+  Foil.withRestrictedScope (supportOf term) $ \scope ->+    cont scope (unsafeCoerce term)++-- | Restrict a term from scope @l@ to a smaller scope @n@, if every name that+-- occurs free in it is in @n@.+--+-- The scope @l@ must extend @n@, since names are compared by their raw+-- identifiers, which identify a name only within one chain of scope+-- extensions. On success the term is returned unchanged, since restricting a+-- term that does inhabit @n@ is a coercion.+--+-- @since 0.3.0+unsinkAST+  :: (Foil.DExt n l, Foil.CoSinkable binder, Bifoldable sig)+  => Foil.Scope n -> AST binder sig l -> Maybe (AST binder sig n)+unsinkAST scope term+  | Foil.nameSetSubsetOfScope (supportOf term) scope = Just (unsafeCoerce term)+  | otherwise = Nothing++-- | Get the free variables of an AST.+--+-- These come from 'supportOf', so they are distinct and in ascending order of+-- their identifiers.+--+-- @since 0.3.0+freeVarsOf+  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig)+  => AST binder sig n -> [Foil.Name n]+freeVarsOf = Foil.nameSetToList . supportOf++-- | Get the free variables of a scoped AST, in the scope outside its binder.+--+-- @since 0.3.0+freeVarsOfScopedAST+  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig)+  => ScopedAST binder sig n -> [Foil.Name n]+freeVarsOfScopedAST = Foil.nameSetToList . supportOfScopedAST

@@ -81,21 +81,21 @@ data FreeFoilTermConfig = FreeFoilTermConfig   { rawIdentName          :: Name     -- ^ The type name for the identifiers.-    -- When identifiers occur in a term, they are converted to 'Foil.Name' (with an appropriate type-level scope parameter).-    -- When identifiers occur in a pattern, they are converted to 'Foil.NameBinder' (with appropriate type-level scope parameters).+    -- When identifiers occur in a term, they are converted to t'Control.Monad.Foil.Name' (with an appropriate type-level scope parameter).+    -- When identifiers occur in a pattern, they are converted to t'Control.Monad.Foil.NameBinder' (with appropriate type-level scope parameters).   , rawTermName           :: Name     -- ^ The type name for the term.-    -- This will be the main recursive type to be converted into an 'Foil.AST'.+    -- This will be the main recursive type to be converted into an t'Control.Monad.Free.Foil.AST'.   , rawBindingName        :: Name     -- ^ The type name for the binders (patterns).-    -- This will be the main binder type to used in 'Foil.AST'-representation of the terms.+    -- This will be the main binder type to used in t'Control.Monad.Free.Foil.AST'-representation of the terms.   , rawScopeName          :: Name     -- ^ The type name for the scoped term.-    -- This will be replaced with either 'Foil.ScopedAST' (with outer scope) or 'Foil.AST' (with inner scope)+    -- This will be replaced with either t'Control.Monad.Free.Foil.ScopedAST' (with outer scope) or t'Control.Monad.Free.Foil.AST' (with inner scope)     -- depending on its occurrence in a regular (sub)term or some quantified syntax.   , rawVarConName         :: Name     -- ^ The constructor name for the variables in a term.-    -- This constructor will be replaced with the standard 'Foil.Var'.+    -- This constructor will be replaced with the standard 'Control.Monad.Free.Foil.Var'.     -- It is expected to have exactly one field of type 'rawIdentName'.   , rawSubTermNames       :: [Name]     -- ^ Type names for subterm syntax.@@ -136,7 +136,7 @@ toFreeFoilNameTo FreeFoilConfig{..} name = mkName (freeFoilConvertToName (nameBase name))  -- | The name of the range-parametric sibling of a generated definition--- (see 'Foil.withFreshIn'): @toPatternIn@ beside @toPattern@.+-- (see 'Control.Monad.Foil.withFreshIn'): @toPatternIn@ beside @toPattern@. toNameIn :: Name -> Name toNameIn name = mkName (nameBase name ++ "In") @@ -378,7 +378,7 @@ -- -- It is when there is exactly one constructor, declared without an explicit -- @forall@ or context, and that constructor has exactly one field, which binds:--- an identifier (it becomes a 'Foil.NameBinder') or a nested binding type. A+-- an identifier (it becomes a t'Control.Monad.Foil.NameBinder') or a nested binding type. A -- field that binds gives the constructor the result type @T ... o i@ with -- distinct scope variables, as a newtype requires; a field that binds nothing -- gives @T ... o o@, which only a GADT can express.@@ -399,7 +399,7 @@ -- | Is this raw field a binding (pattern) field? -- -- Such a field has no counterpart in the free foil node: the binder it stands for--- lives inside the 'Foil.ScopedAST' of each scoped child.+-- lives inside the t'Control.Monad.Free.Foil.ScopedAST' of each scoped child. isBindingField :: FreeFoilConfig -> Type -> Bool isBindingField FreeFoilConfig{..} = \case   PeelConT typeName _ | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> True@@ -407,7 +407,7 @@  -- | Is this raw field a scoped-term field? ----- Such a field becomes a 'Foil.ScopedAST', which carries a binder of its own.+-- Such a field becomes a t'Control.Monad.Free.Foil.ScopedAST', which carries a binder of its own. isScopeField :: FreeFoilConfig -> Type -> Bool isScopeField FreeFoilConfig{..} = \case   PeelConT typeName _ | Just _ <- lookupScopeName typeName freeFoilTermConfigs -> True@@ -415,7 +415,7 @@  -- | What a raw binding constructor's field becomes in the scope-safe binding -- type. Mirrors the classification in 'toFreeFoilBindingCon': an identifier--- becomes a 'Foil.NameBinder' and threads the scope; a binding type becomes a+-- becomes a t'Control.Monad.Foil.NameBinder' and threads the scope; a binding type becomes a -- nested binding type and threads the scope; anything else is a payload that -- binds nothing. data BindingFieldSort = FieldBinder | FieldPattern | FieldPayload@@ -437,8 +437,8 @@ -- | Does this raw payload type mention anything that converts to a -- scope-indexed type in the binding type (a term, a scoped term, an -- identifier, or a nested binding under a type constructor)? Such a payload--- cannot be rebuilt by the generated 'Foil.CoSinkable' instance, rebuilding it--- at another scope being what 'Foil.transportPayload' exists for. Generation+-- cannot be rebuilt by the generated t'Control.Monad.Foil.CoSinkable' instance, rebuilding it+-- at another scope being what 'Control.Monad.Foil.transportPayload' exists for. Generation -- refuses such a payload, matching the GenericK-side refusal for derived -- patterns. mentionsScopeIndexed :: FreeFoilConfig -> Type -> Bool@@ -473,7 +473,7 @@       RecGadtC names types _retType -> [ (name, map (\(_, _, t) -> t) types) | name <- names ]       ForallC _ _ con -> go con --- | One 'Foil.coSinkabilityProof' clause for a generated binding constructor:+-- | One 'Control.Monad.Foil.coSinkabilityProof' clause for a generated binding constructor: -- -- > coSinkabilityProof rename (Con x1 x2 x3) cont = -- >   coSinkabilityProof rename x1 $ \rename' x1' ->@@ -481,7 +481,7 @@ -- >       cont rename'' (Con x1' x2' x3) -- -- Binder and nested-pattern fields thread the renaming left to right (each via--- its own 'Foil.CoSinkable' instance); payload fields pass through untouched.+-- its own t'Control.Monad.Foil.CoSinkable' instance); payload fields pass through untouched. mkCoSinkabilityProofClause :: FreeFoilConfig -> (Name, [Type]) -> Q Clause mkCoSinkabilityProofClause config (rawConName, rawFieldTypes) = do   let conName = toConName config rawConName@@ -508,7 +508,7 @@   body <- go rename (zip sorts xs) id   return (Clause [VarP rename, ConP conName [] (map VarP xs), VarP cont] (NormalB body) []) --- | One 'Foil.withPattern' clause for a generated binding constructor:+-- | One 'Control.Monad.Foil.withPattern' clause for a generated binding constructor: -- -- > withPattern withBinder unit_ comp_ scope (Con x1 x2 x3) cont = -- >   withBinder scope x1 $ \f1 x1' ->@@ -516,9 +516,9 @@ -- >     in withPattern withBinder unit_ comp_ scope' x2 $ \f2 x2' scope'' -> -- >          cont (comp_ f1 f2) (Con x1' x2' x3) scope'' ----- A 'Foil.NameBinder' field is processed with @withBinder@ directly and+-- A t'Control.Monad.Foil.NameBinder' field is processed with @withBinder@ directly and -- extends the ambient scope for the fields to its right; a nested binding--- field recurses through its own 'Foil.withPattern', which hands the extended+-- field recurses through its own 'Control.Monad.Foil.withPattern', which hands the extended -- scope to its continuation. Results compose left to right with @comp_@; the -- final continuation receives the scope after the whole constructor, and a -- constructor that binds nothing hands @unit_@ and the ambient scope over.@@ -574,13 +574,13 @@     [VarP withBinder, VarP unit_, VarP comp_, VarP scope, ConP conName [] (map VarP xs), VarP cont]     (NormalB body) []) --- | One 'Foil.nameBinderListOf' clause for a generated binding constructor:+-- | One 'Control.Monad.Foil.nameBinderListOf' clause for a generated binding constructor: -- -- > nameBinderListOf (Con x1 x2 _) = -- >   concatNameBinderLists (nameBinderListOf x1) (nameBinderListOf x2) -- -- The binder and nested-pattern fields are listed left to right, in the order--- in which the 'Foil.withPattern' clause of 'mkWithPatternClause' visits them,+-- in which the 'Control.Monad.Foil.withPattern' clause of 'mkWithPatternClause' visits them, -- and payload fields are skipped. A constructor that binds nothing lists no -- binders. mkNameBinderListOfClause :: FreeFoilConfig -> (Name, [Type]) -> Q Clause@@ -592,7 +592,7 @@         | isBindingFieldSort sort = VarP x         | otherwise               = WildP       -- A binder is consed on directly. Only a nested binding type's list is-      -- concatenated, since 'Foil.concatNameBinderLists' is recursive and+      -- concatenated, since 'Control.Monad.Foil.concatNameBinderLists' is recursive and       -- copies its first argument.       list = \case         [] -> ConE 'Foil.NameBinderListEmpty@@ -829,7 +829,7 @@ -- /arguments/ are, and the two used to disagree: -- -- * a raw binding (pattern) field contributes __no__ argument, since a binder---   in the free foil lives inside the 'Foil.ScopedAST' it binds, not beside it;+--   in the free foil lives inside the t'Control.Monad.Free.Foil.ScopedAST' it binds, not beside it; -- * a raw scoped-term field contributes __two__ arguments, a binder and a body; -- * every other field contributes one argument, as before. --@@ -1067,14 +1067,14 @@         (BindingNewtype, [newCon]) -> NewtypeD [] bindingName newParams Nothing newCon []         _                          -> DataD [] bindingName newParams Nothing newCons [] -    -- A concrete 'Foil.CoSinkable' instance for the generated binding type,+    -- A concrete t'Control.Monad.Foil.CoSinkable' instance for the generated binding type,     -- one clause per constructor, delegating to the fields' instances. The     -- GenericK default routes every binder operation through a generic     -- representation traversal, which costs a measurable constant per binder     -- at runtime (see issue #82); the concrete instance removes it, and a     -- client no longer declares (or hand-writes) the instance itself. The-    -- instance lists its binders directly in 'Foil.nameBinderListOf', since-    -- the default would go through the recursive 'Foil.withPattern'.+    -- instance lists its binders directly in 'Control.Monad.Foil.nameBinderListOf', since+    -- the default would go through the recursive 'Control.Monad.Foil.withPattern'.     mkPatternCoSinkable FreeFoilTermConfig{..} = do       (tvars, cons) <- reifyDataOrNewtype rawBindingName       let bindingName = toFreeFoilName config rawBindingName

@@ -37,14 +37,14 @@ import           Data.Coerce (coerce) import           Data.Monoid (All (..), Any (..)) import           Generics.Kind-import Data.Bitraversable  import Data.ZipMatchK.Generic import Data.ZipMatchK.Mappings --- | Perform one level of equality testing for two values and pair up components using @(,)@:+-- | Perform one level of equality testing for two values and pair up+-- corresponding components using @(,)@, for every type parameter: ----- > zipMatchK = zipMatchWithK (\x y -> Just (,) :^: M0)+-- > zipMatchK = zipMatchWithK pairMappings -- -- @since 0.2.0 zipMatchK :: forall f as bs. (ZipMatchK f, PairMappings as bs) => f :@@: as -> f :@@: bs -> Maybe (f :@@: ZipLoT as bs)@@ -68,29 +68,23 @@  -- | 'zipMatchWithK' specialised to functors. ----- Note: 'Traversable' is a morally correct constraint here.--- -- @since 0.3.0 zipMatchWith1-  :: (Traversable f, ZipMatchK f)+  :: ZipMatchK f   => (a -> a' -> Maybe a'')   -> f a -> f a' -> Maybe (f a'') zipMatchWith1 f = zipMatchWithK (f :^: M0)  -- | 'zipMatchK' specialised to functors. ----- Note: 'Traversable' is a morally correct constraint here.--- -- @since 0.3.0-zipMatch1 :: (Traversable f, ZipMatchK f) => f a -> f a' -> Maybe (f (a, a'))+zipMatch1 :: ZipMatchK f => f a -> f a' -> Maybe (f (a, a')) zipMatch1 = zipMatchWith1 pairA -- | 'zipMatchWithK' specialised to bifunctors. ----- Note: 'Bitraversable' is a morally correct constraint here.--- -- @since 0.3.0 zipMatchWith2-  :: (Bitraversable f, ZipMatchK f)+  :: ZipMatchK f   => (a -> a' -> Maybe a'')   -> (b -> b' -> Maybe b'')   -> f a b -> f a' b' -> Maybe (f a'' b'')@@ -98,10 +92,8 @@  -- | 'zipMatchK' specialised to bifunctors. ----- Note: 'Bitraversable' is a morally correct constraint here.--- -- @since 0.3.0-zipMatch2 :: (Bitraversable f, ZipMatchK f) => f a b -> f a' b' -> Maybe (f (a, a') (b, b'))+zipMatch2 :: ZipMatchK f => f a b -> f a' b' -> Maybe (f (a, a') (b, b')) zipMatch2 = zipMatchWith2 pairA pairA  -- | 'zipMatchFoldK' specialised to functors.

@@ -1,10 +1,13 @@ {-# LANGUAGE DataKinds           #-} {-# LANGUAGE DeriveTraversable   #-}+{-# LANGUAGE FlexibleContexts    #-} {-# LANGUAGE GADTs               #-}+{-# LANGUAGE KindSignatures      #-} {-# LANGUAGE LambdaCase          #-} {-# LANGUAGE RankNTypes          #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell     #-}+{-# LANGUAGE TypeFamilies        #-}  -- | Properties of 'alphaEquiv' with threaded renamings. --@@ -28,6 +31,7 @@                                               unsafeAssertFresh) import           Control.Monad.Free.Foil import           Data.ZipMatchK.TH           (deriveZipMatchK)+import           Generics.Kind.TH            (deriveGenericK)  data LamSig scope term   = App term term@@ -41,6 +45,48 @@  type Term = AST Foil.NameBinder LamSig +-- | A binder annotated with a name of the outer scope, as a binder may be+-- annotated with its type. Only 'Foil.unifyPatternsIn' compares the+-- annotations, as it does the payloads of a telescope.+data AnnBinder (n :: Foil.S) (l :: Foil.S) where+  AnnBinder :: Foil.Name n -> Foil.NameBinder n l -> AnnBinder n l++deriveGenericK ''AnnBinder+instance Foil.SinkableK AnnBinder++-- | The annotation is a payload, so it is moved by hand (see+-- 'Foil.transportPayload').+instance Foil.CoSinkable AnnBinder where+  coSinkabilityProof rename (AnnBinder ann binder) cont =+    Foil.coSinkabilityProof rename binder $ \rename' binder' ->+      cont rename' (AnnBinder (rename ann) binder')+  withPattern withBinder _unit _comp scope (AnnBinder ann binder) cont =+    withBinder scope binder $ \fbinder binder' ->+      cont fbinder+        (AnnBinder (Foil.transportName Foil.verbatimTransport ann) binder')+        (Foil.extendScope binder' scope)+instance Foil.UnifiablePattern AnnBinder where+  unifyPatternsIn _scope l@(AnnBinder x _) r@(AnnBinder y _)+    | x == y    = Foil.unifyPatterns l r+    | otherwise = Foil.NotUnifiable++type AnnTerm = AST AnnBinder LamSig++-- | λ(x : ann). x+annId :: Foil.Distinct n => Foil.Scope n -> Foil.Name n -> AnnTerm n+annId scope ann = Foil.withFresh scope $ \x ->+  Node (Lam (ScopedAST (AnnBinder ann x) (Var (Foil.nameOf x))))++-- | Run a continuation in a scope with two names.+withTwoNames+  :: (forall n. Foil.Distinct n => Foil.Scope n -> Foil.Name n -> Foil.Name n -> r)+  -> r+withTwoNames cont =+  Foil.withFresh Foil.emptyScope $ \a ->+    let scope1 = Foil.extendScope a Foil.emptyScope+     in Foil.withFresh scope1 $ \b ->+          cont (Foil.extendScope b scope1) (Foil.sink (Foil.nameOf a)) (Foil.nameOf b)+ -- * Hand-built terms with chosen binder names  -- | A binder with a chosen raw name — either fresh for the scope, or@@ -121,7 +167,7 @@ renderShifted :: Int -> Skel -> Term Foil.VoidS renderShifted k s = go k Foil.emptyScope   where-    go :: Foil.Distinct n => Int -> Foil.Scope n -> Term Foil.VoidS+    go :: (Foil.Distinct n, Foil.Ext Foil.VoidS n) => Int -> Foil.Scope n -> Term Foil.VoidS     go 0 scope =       fromMaybe (error "the term uses a dummy binder")         (unsinkAST Foil.emptyScope (renderIn scope [] (case s of SLam{} -> s; _ -> SLam s)))@@ -159,6 +205,17 @@       let t1 = lam 7 (\_a -> lam 5 (\b -> Var b))           t2 = lam 5 (\_a -> lam 5 (\b -> Var b))       alphaEquiv Foil.emptyScope t1 t2 `shouldBe` True++  describe "binders with annotations" $ do+    it "rejects λ(x : a). x against λ(x : b). x" $+      withTwoNames $ \scope a b ->+        alphaEquiv scope (annId scope a) (annId scope b) `shouldBe` False+    it "rejects λ(x : a). x against λ(x : b). x with alphaEquivRefreshed" $+      withTwoNames $ \scope a b ->+        alphaEquivRefreshed scope (annId scope a) (annId scope b) `shouldBe` False+    it "accepts λ(x : a). x against λ(y : a). y with alphaEquivRefreshed" $+      withTwoNames $ \scope a _ ->+        alphaEquivRefreshed scope (annId scope a) (annId scope a) `shouldBe` True    describe "agreement with alphaEquivRefreshed" $ do     prop "on a term against its shifted rendering" $ \s (Positive k) ->

@@ -17,7 +17,7 @@ import           Data.Bifunctor                                   (bimap) import           Data.Bitraversable                               (bitraverse) import           Data.Monoid                                      (Sum (..))-import           Data.ZipMatchK                                   (Mappings (..), ZipMatchK (..))+import           Data.ZipMatchK                                   (zipMatchWith2) import           Test.Hspec  import           Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config@@ -50,8 +50,8 @@     it "force a term and its patterns" $       rnf (toTerm Foil.emptyScope Map.empty (Let (PatternVar x) identity (ScopedTerm (Var x)))) `shouldBe` ()     it "match equal constructors and reject different ones" $ do-      zipMatchWithK (zipAdd :^: zipAdd :^: M0) (AppSig 1 2 :: TermSig Int Int) (AppSig 10 20) `shouldBe` Just (AppSig 11 22)-      zipMatchWithK (zipAdd :^: zipAdd :^: M0) (AppSig 1 2 :: TermSig Int Int) (FunSig 3) `shouldBe` Nothing+      zipMatchWith2 zipAdd zipAdd (AppSig 1 2 :: TermSig Int Int) (AppSig 10 20) `shouldBe` Just (AppSig 11 22)+      zipMatchWith2 zipAdd zipAdd (AppSig 1 2 :: TermSig Int Int) (FunSig 3) `shouldBe` Nothing    describe "a pattern adjacent to its scope (Fun)" $     it "round-trips, and the body still refers to the binder" $

@@ -0,0 +1,74 @@+{-# LANGUAGE DataKinds         #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE GADTs             #-}+{-# LANGUAGE LambdaCase        #-}+{-# LANGUAGE RankNTypes        #-}+{-# LANGUAGE TemplateHaskell   #-}++-- | 'unresolvedNames' and 'unresolvedNamesWith' on a small raw λ-calculus,+-- against what 'tryConvertToASTWith' reports.+module Control.Monad.Free.Foil.UnresolvedNamesSpec (spec) where++import           Data.Bifunctor.TH+import           Data.Map                (Map)+import qualified Data.Map                as Map+import           Test.Hspec++import qualified Control.Monad.Foil      as Foil+import           Control.Monad.Free.Foil+import           Data.ZipMatchK.TH       (deriveZipMatchK)++data LamSig scope term+  = App term term+  | Lam scope+  deriving (Functor, Foldable, Traversable)++deriveBifunctor ''LamSig+deriveBifoldable ''LamSig+deriveBitraversable ''LamSig+deriveZipMatchK ''LamSig++type Term = AST Foil.NameBinder LamSig++data Raw = RVar String | RApp Raw Raw | RLam String Raw++toSig :: Raw -> Either String (LamSig (String, Raw) Raw)+toSig = \case+  RVar x   -> Left x+  RApp f a -> Right (App f a)+  RLam x b -> Right (Lam (x, b))++fromRawPattern+  :: Foil.Distinct n+  => Foil.Scope n+  -> Map String (Foil.Name n)+  -> String+  -> (forall l. Foil.DExt n l => Foil.NameBinder n l -> Map String (Foil.Name l) -> r)+  -> r+fromRawPattern scope names x cont = Foil.withFresh scope $ \binder ->+  cont binder (Map.insert x (Foil.nameOf binder) (fmap Foil.sink names))++-- | The constant @c@, which stands for λy. y.+constants :: Map String (Term Foil.VoidS)+constants = Map.singleton "c" $ Foil.withFresh Foil.emptyScope $ \y ->+  Node (Lam (ScopedAST y (Var (Foil.nameOf y))))++-- | c (λx. x d)+raw :: Raw+raw = RApp (RVar "c") (RLam "x" (RApp (RVar "x") (RVar "d")))++spec :: Spec+spec = do+  describe "unresolvedNames" $+    it "reports a constant as unresolved" $+      unresolvedNames toSig fromRawPattern id Foil.emptyScope Map.empty raw+        `shouldBe` [UnresolvedName "c" [], UnresolvedName "d" ["x"]]++  describe "unresolvedNamesWith" $ do+    it "resolves the constants" $+      unresolvedNamesWith toSig fromRawPattern id Foil.emptyScope Map.empty constants raw+        `shouldBe` [UnresolvedName "d" ["x", "c"]]+    it "reports first what tryConvertToASTWith reports" $+      either Just (const Nothing)+        (tryConvertToASTWith toSig fromRawPattern id Foil.emptyScope Map.empty constants raw)+        `shouldBe` Just (UnresolvedName "d" ["x", "c"])

@@ -613,7 +613,7 @@ -- a free name by its raw identifier. Patterns are compared by the names -- they bind, listed by the given function, and not by their shape. alphaEqNameless-  :: forall binder sig x y. (Bitraversable sig, ZipMatchK sig)+  :: forall binder sig x y. ZipMatchK sig   => PatternNames binder -> AST binder sig x -> AST binder sig y -> Bool alphaEqNameless binders = go 0 IntMap.empty IntMap.empty   where