free-foil 0.4.0 → 0.5.0

raw patch · 24 files changed

+2933/−332 lines, 24 filesdep ~binarydep ~bytestringPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: binary, bytestring

API changes (from Hackage documentation)

Files

• ChangeLog.md +35/−1
• free-foil.cabal +28/−15
• src/Control/Monad/Foil.hs +2/−1
• src/Control/Monad/Foil/Internal.hs +354/−96
• src/Control/Monad/Foil/Relative.hs +6/−28
• src/Control/Monad/Foil/TH/MkInstancesFoil.hs +0/−93
• src/Control/Monad/Foil/Telescope.hs +16/−16
• src/Control/Monad/Free/Foil.hs +0/−47
• src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs +52/−7
• test/Control/Monad/Foil/ExampleLawsSpec.hs +48/−0
• test/Control/Monad/Foil/LawsSpec.hs +73/−0
• test/Control/Monad/Foil/PatternTransportSpec.hs +1/−1
• test/Control/Monad/Foil/TelescopeLawsSpec.hs +138/−0
• test/Control/Monad/Foil/UnifiablePatternSpec.hs +96/−27
• test/Control/Monad/Free/Foil/ExampleSyntax.hs +32/−0
• test/Control/Monad/Free/Foil/LawsSpec.hs +29/−0
• test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Declaration.hs +38/−0
• test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/PatternsConfig.hs +139/−0
• test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/PatternsSyntax.hs +64/−0
• test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Syntax.hs +3/−0
• test/Control/Monad/Free/Foil/TH/PatternTypesSpec.hs +237/−0
• test/laws/Control/Monad/Foil/Laws.hs +651/−0
• test/laws/Control/Monad/Free/Foil/Laws.hs +695/−0
• test/laws/Control/Monad/Free/Foil/Laws/Mirror.hs +196/−0

@@ -1,6 +1,40 @@ # CHANGELOG for `free-foil` -# Unreleased+# 0.5.0 — 2026-10-07++A release about *binders*. The law tests added after 0.4.0 ([#100](https://github.com/fizruk/free-foil/pull/100)) found bugs in how binders are sunk, ordered, paired and transported, and this release fixes them. The fixes change α-equivalence for patterns of several binders, so the release is major. It also generates single-binder pattern types as newtypes and removes the functions deprecated in 0.3.3 and 0.4.0.++Breaking changes:++- **The default `unifyPatterns` is structural, and it requires `GenericK`** ([#101](https://github.com/fizruk/free-foil/pull/101), [#98](https://github.com/fizruk/free-foil/issues/98)). It is the new `gunifyPatterns`. Two patterns unify when they consist of the same constructors, nested in the same way, and their binders are then paired in order. The old default compared only the binders, so it unified `(x, _)` with `(_, y)`, and the conversion check of `mltt` accepted ill-typed programs. Non-binding fields are still ignored.+  - This changes α-equivalence for every client that takes the default, and reverses the plan in the 0.3.3 entry below to make structural derivation opt-in.+  - A pattern type that takes the default and has no `GenericK` instance no longer compiles. Derive `GenericK` for it or write `unifyPatterns` by hand.+  - `mltt`, `soas` and `Impl.FreeFoilTH` of `lambda-pi` take the default. For `soas`, whose binders form a flat list, the result is the same as before.++- **`transportPayload` takes the ambient scope and requires `RelMonad Name e` instead of `Sinkable e`, and `CoSinkable (Telescope label e)` requires `RelMonad Name e` too** ([#101](https://github.com/fizruk/free-foil/pull/101), [#99](https://github.com/fizruk/free-foil/issues/99)). A refreshed binder renames the payloads after it, and renaming a payload with binders needs the scope. For instance, if `x0` is refreshed to `x1`, a later payload `λx1. x0` becomes `λx2. x1`. A hand-written `withPattern` passes the scope it holds before the payload's binder (see the recipe in the documentation of `transportPayload`), and an instance carrying payloads of type `e` adds `RelMonad Name e` to its context.+  - The new `instance RelMonad Name Name` keeps telescopes of names working.+  - `RelMonad` is now defined in `Control.Monad.Foil.Internal`. `Control.Monad.Foil.Relative` re-exports it, so imports need no change.+  - `telescopeParams` and `telescopePayloads` keep their constraints.++- **`mkFreeFoil` generates a pattern type as a `newtype` when its raw type has exactly one constructor with exactly one field, and that field is an identifier or a nested pattern**, as in `newtype Pattern = PatternVar VarIdent` ([#106](https://github.com/fizruk/free-foil/pull/106), [#85](https://github.com/fizruk/free-foil/issues/85)). Such a pattern costs no heap object of its own. Code that matches on the constructor or derives instances needs no change, but Template Haskell that `reify`s the generated type now sees a `NewtypeD` and has to accept it.++- **The deprecated functions are removed** ([#104](https://github.com/fizruk/free-foil/pull/104)). Use `sink1` instead of `sinkContainer`, and `unsafeConvertToAST` and `unsafeConvertToScopedAST` instead of `convertToAST` and `convertToScopedAST` (or `tryConvertToAST`, which reports unresolved identifiers instead of calling `error`). `deriveUnifiablePattern` is removed without a replacement: derive `GenericK` and take an empty `UnifiablePattern` instance, or write the instance by hand with `unsafeUnifyPatternBinders`, as `Language.LambdaPi.Impl.Foil` does.++New:++- `unsafeUnifyPatternBinders` pairs the binders of two patterns in order, for a hand-written `unifyPatterns` of a pattern with several binders. It is unsafe: call it only once the two patterns are known to agree on everything except the names of their binders, as `gunifyPatterns` does after its shape check and as `Language.LambdaPi.Impl.Foil` does in `lambda-pi` ([#103](https://github.com/fizruk/free-foil/pull/103), [#102](https://github.com/fizruk/free-foil/issues/102)).++Fixes:++- The generic `sinkabilityProof` no longer fails with `Non-exhaustive patterns in function sinkabilityProofK` on a term with a binder ([#101](https://github.com/fizruk/free-foil/pull/101), [#94](https://github.com/fizruk/free-foil/issues/94)). This also fixes the default `coSinkabilityProof` of every pattern that derives `CoSinkable` generically, and `transportPayload` on such a payload.++- `alphaEquiv` is correct for patterns of two or more binders ([#101](https://github.com/fizruk/free-foil/pull/101), [#95](https://github.com/fizruk/free-foil/issues/95)). It used to pair the binders of the two sides wrongly, with both false negatives and false positives (`λ[x0 x1]. x0` and `λ[x1 x2]. x2` were α-equivalent). This affected the default `unifyPatterns` of every pattern type, the conversion check of `mltt` and `isSolutionFor` in `soas`.+  - `NameBinderList`, `Telescope` and the default `unifyPatterns` pair the binders of two patterns by position, all at once, and rename the binders of the right pattern to those of the left one. A single pair of binders keeps the convention of `unifyNameBinders`.+  - `andThenUnifyPatterns` and `andThenUnifyNameBinders` no longer compose renamings. A chain of verdicts that gives two binders the same name now answers `NotUnifiable` instead of a wrong verdict. With `andThenUnifyNameBinders`, a chain of two pairs always unifies.++- The generic `withPattern`, the default for a pattern type that derives `HasNameBinders`, keeps the binders of a pattern in their order ([#101](https://github.com/fizruk/free-foil/pull/101), [#97](https://github.com/fizruk/free-foil/issues/97)). It used to put them in ascending order of names, which permuted the binders of a pattern whose names do not ascend, such as one that `substitute`, `liftRM` or `refreshAST` produces, and changed the meaning of the term. `nameBinderListOf`, `addSubstPattern`, the default `unifyPatterns` and `alphaEquivRefreshed` were affected through it. The instances that `mkFreeFoil` generates were not.++- In `lambda-pi`, `alphaEquiv` of `Impl.Foil` no longer captures a free name when a binder is already in the scope, as for a term built in a smaller scope and sunk ([#101](https://github.com/fizruk/free-foil/pull/101), [#96](https://github.com/fizruk/free-foil/issues/96)). It falls back to `alphaEquivRefreshed` in that case.  # 0.4.0 — 2026-08-29 

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           free-foil-version:        0.4.0+version:        0.5.0 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@@ -68,8 +68,8 @@       array >=0.5.3.0 && <0.6     , base >=4.19 && <5     , bifunctors >=5.5 && <5.7-    , binary >=0.8-    , bytestring >=0.11+    , binary ==0.8.*+    , bytestring >=0.11 && <0.13     , containers >=0.6.8 && <0.9     , deepseq >=1.4 && <1.6     , kind-generics >=0.5.0 && <0.6@@ -88,8 +88,8 @@       array >=0.5.3.0 && <0.6     , base >=4.19 && <5     , bifunctors >=5.5 && <5.7-    , binary >=0.8-    , bytestring >=0.11+    , binary ==0.8.*+    , bytestring >=0.11 && <0.13     , containers >=0.6.8 && <0.9     , deepseq >=1.4 && <1.6     , doctest-parallel@@ -104,31 +104,44 @@   main-is: Spec.hs   other-modules:       Control.Monad.Foil.BlocksSpec+      Control.Monad.Foil.ExampleLawsSpec+      Control.Monad.Foil.LawsSpec       Control.Monad.Foil.NameMapSpec       Control.Monad.Foil.NameRangeSpec       Control.Monad.Foil.PatternTransportSpec       Control.Monad.Foil.SinkableSpec+      Control.Monad.Foil.TelescopeLawsSpec       Control.Monad.Foil.UnifiablePatternSpec       Control.Monad.Foil.UnifyNameBindersSpec       Control.Monad.Free.Foil.AlphaEquivSpec       Control.Monad.Free.Foil.AnnotatedSpec+      Control.Monad.Free.Foil.ExampleSyntax+      Control.Monad.Free.Foil.LawsSpec       Control.Monad.Free.Foil.SupportSpec       Control.Monad.Free.Foil.TH.MkFreeFoilSpec       Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config+      Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Declaration+      Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsConfig+      Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsSyntax       Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax+      Control.Monad.Free.Foil.TH.PatternTypesSpec       Data.ZipMatchK.THSpec       SpecHook+      Control.Monad.Foil.Laws+      Control.Monad.Free.Foil.Laws+      Control.Monad.Free.Foil.Laws.Mirror       Paths_free_foil   hs-source-dirs:       test+      test/laws   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N   build-depends:       QuickCheck     , array >=0.5.3.0 && <0.6     , base >=4.19 && <5     , bifunctors >=5.5 && <5.7-    , binary >=0.8-    , bytestring >=0.11+    , binary ==0.8.*+    , bytestring >=0.11 && <0.13     , containers     , deepseq >=1.4 && <1.6     , free-foil@@ -152,8 +165,8 @@       array >=0.5.3.0 && <0.6     , base >=4.19 && <5     , bifunctors >=5.5 && <5.7-    , binary >=0.8-    , bytestring >=0.11+    , binary ==0.8.*+    , bytestring >=0.11 && <0.13     , containers >=0.6.8 && <0.9     , deepseq >=1.4 && <1.6     , free-foil@@ -175,8 +188,8 @@       array >=0.5.3.0 && <0.6     , base >=4.19 && <5     , bifunctors >=5.5 && <5.7-    , binary >=0.8-    , bytestring >=0.11+    , binary ==0.8.*+    , bytestring >=0.11 && <0.13     , containers >=0.6.8 && <0.9     , deepseq >=1.4 && <1.6     , free-foil@@ -198,8 +211,8 @@       array >=0.5.3.0 && <0.6     , base >=4.19 && <5     , bifunctors >=5.5 && <5.7-    , binary >=0.8-    , bytestring >=0.11+    , binary ==0.8.*+    , bytestring >=0.11 && <0.13     , containers >=0.6.8 && <0.9     , deepseq >=1.4 && <1.6     , free-foil@@ -222,8 +235,8 @@       array >=0.5.3.0 && <0.6     , base >=4.19 && <5     , bifunctors >=5.5 && <5.7-    , binary >=0.8-    , bytestring >=0.11+    , binary ==0.8.*+    , bytestring >=0.11 && <0.13     , containers >=0.6.8 && <0.9     , deepseq >=1.4 && <1.6     , free-foil

@@ -71,7 +71,6 @@   sink1,   sink2,   sinkabilityProof2,-  sinkContainer,   extendRenaming,   extendNameBinderRenaming,   composeNameBinderRenamings,@@ -92,6 +91,8 @@   unifyNameBinders,   andThenUnifyPatterns,   andThenUnifyNameBinders,+  gunifyPatterns,+  unsafeUnifyPatternBinders,   UnifiablePattern(..),   UnifiableInPattern(..),   AlphaEquiv(..),

@@ -778,6 +778,11 @@ -- always grow with depth: a term built in a small scope keeps its small binder -- names when 'sink' places it in a larger one. --+-- This convention is for a single pair of binders. For patterns of several+-- binders, those of the right pattern are renamed to those of the left one+-- instead (see 'unsafeUnifyPatternBinders'), since choosing the smaller name pair by+-- pair can give two binders of one pattern the same name.+-- -- @since 0.0.3 unifyNameBinders   :: forall i l r pattern. Distinct i@@ -795,42 +800,97 @@ -- | Unsafely merge results of unification for nested binders/patterns. -- Used in 'andThenUnifyPatterns'. --+-- Each binder is renamed by the verdict it belongs to, not by a composition of+-- the two renamings (see 'unsafeOverrideBinderRenaming').+--+-- The two verdicts choose their unified names independently, so they may give+-- two binders of one pattern the same name (for @[x0 x1]@ against @[x1 x0]@,+-- both pairs are unified as @x0@). The result is then 'NotUnifiable'.+-- -- @since 0.1.0 unsafeMergeUnifyBinders :: UnifyNameBinders pattern a a' a'' -> UnifyNameBinders pattern a''' b' b'' -> UnifyNameBinders pattern a b' b''-unsafeMergeUnifyBinders = \case+unsafeMergeUnifyBinders outer inner =+  case unsafeTryMergeUnifyBinders outer inner of+    Just merged -> merged+    Nothing     -> NotUnifiable -  SameNameBinders x -> \case-    SameNameBinders y -> SameNameBinders (x `unsafeMergeNameBinders` y)-    RenameLeftNameBinder y f -> RenameLeftNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce f)-    RenameRightNameBinder y g -> RenameRightNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce g)-    RenameBothBinders y f g -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)-    NotUnifiable -> NotUnifiable+-- | 'unsafeMergeUnifyBinders', or 'Nothing' if the unified names of the two+-- verdicts intersect, i.e. if they give two binders the same name.+--+-- @since 0.5.0+unsafeTryMergeUnifyBinders :: UnifyNameBinders pattern a a' a'' -> UnifyNameBinders pattern a''' b' b'' -> Maybe (UnifyNameBinders pattern a b' b'')+unsafeTryMergeUnifyBinders outer inner+  | collide (unifiedRawNames outer) (unifiedRawNames inner) = Nothing+  | otherwise = Just (merge outer inner)+  where+    collide (Just xs) (Just ys) = not (IntSet.disjoint xs ys)+    collide _ _                 = False -  RenameLeftNameBinder x f -> \case-    SameNameBinders y -> RenameLeftNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce f)-    RenameLeftNameBinder y g -> RenameLeftNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce f . unsafeCoerce g)-    RenameRightNameBinder y g -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)-    RenameBothBinders y f' g -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g)-    NotUnifiable -> NotUnifiable+    unifiedRawNames :: UnifyNameBinders pattern n l r -> Maybe IntSet+    unifiedRawNames = \case+      SameNameBinders (UnsafeNameBinders xs)         -> Just xs+      RenameLeftNameBinder (UnsafeNameBinders xs) _  -> Just xs+      RenameRightNameBinder (UnsafeNameBinders xs) _ -> Just xs+      RenameBothBinders (UnsafeNameBinders xs) _ _   -> Just xs+      NotUnifiable                                   -> Nothing -  RenameRightNameBinder x g -> \case-    SameNameBinders y -> RenameRightNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce g)-    RenameLeftNameBinder y f -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)-    RenameRightNameBinder y g' -> RenameRightNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce g . unsafeCoerce g')-    RenameBothBinders y f g' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g . unsafeCoerce g')-    NotUnifiable -> NotUnifiable+    merge :: UnifyNameBinders pattern a a' a'' -> UnifyNameBinders pattern a''' b' b'' -> UnifyNameBinders pattern a b' b''+    merge = \case -  RenameBothBinders x f g -> \case-    SameNameBinders y -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)-    RenameLeftNameBinder y f' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g)-    RenameRightNameBinder y g' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g . unsafeCoerce g')-    RenameBothBinders y f' g' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g . unsafeCoerce g')-    NotUnifiable -> NotUnifiable+      SameNameBinders x -> \case+        SameNameBinders y -> SameNameBinders (x `unsafeMergeNameBinders` y)+        RenameLeftNameBinder y f -> RenameLeftNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce f)+        RenameRightNameBinder y g -> RenameRightNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce g)+        RenameBothBinders y f g -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)+        NotUnifiable -> NotUnifiable -  NotUnifiable -> const (NotUnifiable)+      RenameLeftNameBinder x f -> \case+        SameNameBinders y -> RenameLeftNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce f)+        RenameLeftNameBinder y g -> RenameLeftNameBinder (x `unsafeMergeNameBinders` y) (unsafeOverrideBinderRenaming f g)+        RenameRightNameBinder y g -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)+        RenameBothBinders y f' g -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeOverrideBinderRenaming f f') (unsafeCoerce g)+        NotUnifiable -> NotUnifiable +      RenameRightNameBinder x g -> \case+        SameNameBinders y -> RenameRightNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce g)+        RenameLeftNameBinder y f -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)+        RenameRightNameBinder y g' -> RenameRightNameBinder (x `unsafeMergeNameBinders` y) (unsafeOverrideBinderRenaming g g')+        RenameBothBinders y f g' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeOverrideBinderRenaming g g')+        NotUnifiable -> NotUnifiable++      RenameBothBinders x f g -> \case+        SameNameBinders y -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)+        RenameLeftNameBinder y f' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeOverrideBinderRenaming f f') (unsafeCoerce g)+        RenameRightNameBinder y g' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeOverrideBinderRenaming g g')+        RenameBothBinders y f' g' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeOverrideBinderRenaming f f') (unsafeOverrideBinderRenaming g g')+        NotUnifiable -> NotUnifiable++      NotUnifiable -> const NotUnifiable++-- | Combine the binder renamings of an outer and an inner verdict, for+-- 'unsafeMergeUnifyBinders'.+--+-- The inner renaming decides for the binders it moves, and the outer one for+-- the rest. This is sound since each verdict renames only its own binders.+--+-- @since 0.5.0+unsafeOverrideBinderRenaming+  :: forall a b c d e f n l r.+     (NameBinder a b -> NameBinder a c)  -- ^ Renaming of the outer verdict.+  -> (NameBinder d e -> NameBinder d f)  -- ^ Renaming of the inner verdict.+  -> NameBinder n l -> NameBinder n r+unsafeOverrideBinderRenaming outer inner binder+  | nameId (nameOf binder') /= nameId (nameOf binder) = binder'+  | otherwise = (unsafeCoerce outer :: NameBinder n l -> NameBinder n r) binder+  where+    binder' = (unsafeCoerce inner :: NameBinder n l -> NameBinder n r) binder+ -- | Chain unification of nested patterns. --+-- Note that a chain answers 'NotUnifiable' when two of its verdicts give+-- different binders the same name. The default 'unifyPatterns'+-- ('gunifyPatterns') unifies all binders of a pattern at once and avoids this.+-- -- @since 0.1.0 andThenUnifyPatterns   :: (UnifiablePattern pattern, Distinct l, Distinct l')@@ -841,14 +901,39 @@  -- | Chain unification of nested patterns with 'NameBinder's. --+-- If the name that 'unifyNameBinders' chooses for the new pair is taken by an+-- outer binder, the pair is unified in the other direction. So a chain of two+-- pairs always unifies, while a longer one may answer 'NotUnifiable'.+-- -- @since 0.1.0 andThenUnifyNameBinders   :: (UnifiablePattern pattern, Distinct l, Distinct l')   => UnifyNameBinders pattern n l l'    -- ^ Unifying action for some outer patterns.   -> (NameBinder l r, NameBinder l' r') -- ^ Two nested binders (cannot be unified directly since they extend different scopes).   -> UnifyNameBinders pattern n r r'-andThenUnifyNameBinders u (l, r) = unsafeMergeUnifyBinders u (unifyNameBinders (unsafeCoerce l) r)+andThenUnifyNameBinders u (l, r) =+  case unsafeTryMergeUnifyBinders u (unifyNameBinders l' r) of+    Just merged -> merged+    Nothing     -> unsafeMergeUnifyBinders u (unifyNameBindersTowardsLarger l' r)+  where+    l' = unsafeCoerce l +-- | 'unifyNameBinders' in the other direction: when the binders differ, the+-- one with the /smaller/ name is renamed towards the one with the larger name.+--+-- @since 0.5.0+unifyNameBindersTowardsLarger+  :: forall i l r pattern. Distinct i+  => NameBinder i l -- ^ Left pattern.+  -> NameBinder i r -- ^ Right pattern.+  -> UnifyNameBinders pattern i l r+unifyNameBindersTowardsLarger l@(UnsafeNameBinder (UnsafeName i1)) r@(UnsafeNameBinder (UnsafeName i2))+  | i1 < i2   = RenameLeftNameBinder (nameBindersSingleton r) $ \(UnsafeNameBinder (UnsafeName i')) ->+      if i'  == i1 then UnsafeNameBinder (UnsafeName i2) else UnsafeNameBinder (UnsafeName i')+  | i1 > i2   = RenameRightNameBinder (nameBindersSingleton l) $ \(UnsafeNameBinder (UnsafeName i'')) ->+      if i'' == i2 then UnsafeNameBinder (UnsafeName i1) else UnsafeNameBinder (UnsafeName i'')+  | otherwise = unifyNameBinders l r+ -- | An /unordered/ collection of 'NameBinder's, that together extend scope @n@ to scope @l@. -- -- For an ordered version see 'NameBinderList'.@@ -1056,8 +1141,9 @@ -- | A pattern type is unifiable if it is possible to match two -- patterns and decide how to rename binders. ----- Note that the default implementation compares patterns only up to their--- binders. See 'unifyPatterns' for what that does and does not distinguish.+-- Note that the default implementation compares the constructors of two+-- patterns and their binders, but not their non-binding fields. See+-- 'unifyPatterns' for what that does and does not distinguish. -- -- @since 0.0.1 class CoSinkable pattern => UnifiablePattern pattern where@@ -1066,33 +1152,23 @@   -- @since 0.1.0   unifyPatterns :: Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r -  -- | The default implementation flattens both patterns to their binders (via-  -- 'nameBinderListOf') and unifies the resulting 'NameBinderList's. It therefore-  -- compares only the /number and order/ of binders, and ignores-  ---  -- * the constructor, so two patterns built from /different/ constructors with-  --   the same number of binders unify;-  -- * non-binding fields (locations, sorts, literals), whatever their values;-  -- * the nesting of sub-patterns, so @(x, (y, z))@ unifies with @((x, y), z)@.-  ---  -- For most languages this is the intended notion of α-equivalence: what the-  -- body of a binding construct can refer to is precisely the pattern's binders,-  -- in order. Since α-equivalence is defined in terms of 'unifyPatterns', this-  -- also means that terms differing only in such a pattern are α-equivalent.+  -- | The default implementation is 'gunifyPatterns'. Two patterns unify when+  -- they consist of the same constructors, nested in the same way, and their+  -- binders are then paired in order. So @(x, _)@ and @(_, y)@ do not unify,+  -- although each binds one name, and @λ(x, _). x@ is not α-equivalent to+  -- @λ(_, y). y@.   ---  -- A pattern that carries semantically relevant data needs the instance-  -- written by hand instead. Use 'UnifiableInPattern' to compare non-binding-  -- fields, which also lets an instance ignore some of them deliberately, as a-  -- generated instance does for BNFC source positions.+  -- The default ignores non-binding fields (such as locations, sorts or+  -- literals). A pattern that carries meaningful data in them needs a+  -- hand-written instance, which can compare them with 'UnifiableInPattern'.   ---  -- A field that is /scope-indexed/, such as a telescope step's type, cannot be-  -- compared here at all, since comparing it up to α needs the ambient scope-  -- and this method is given only 'Distinct'. Write 'unifyPatternsIn' for that,-  -- and leave this one as the binder-only approximation.+  -- A /scope-indexed/ field, such as the type in a telescope step, cannot be+  -- compared here, since comparing it up to α needs the ambient scope. Compare+  -- it in 'unifyPatternsIn', and keep this method for the rest of the pattern.   default unifyPatterns-    :: (CoSinkable pattern, Distinct n)+    :: (GenericK pattern, GUnifiablePattern (RepK pattern), Distinct n)     => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r-  unifyPatterns l r = coerce (unifyPatterns (nameBinderListOf l) (nameBinderListOf r))+  unifyPatterns = gunifyPatterns    -- | Unify two patterns with the ambient scope at hand.   --@@ -1110,7 +1186,7 @@   --   -- The default ignores the scope and answers with 'unifyPatterns'. An instance   -- that overrides this one should leave 'unifyPatterns' in place as the-  -- binder-only approximation rather than remove it. That is what+  -- comparison without a scope rather than remove it. That is what   -- 'unsafeEqPattern' and any caller without a scope will get, and it may be   -- more permissive than this one, never less.   unifyPatternsIn@@ -1118,17 +1194,23 @@     => Scope n -> pattern n l -> pattern n r -> UnifyNameBinders pattern n l r   unifyPatternsIn _scope = unifyPatterns +-- | Two lists unify when they have the same length. Their binders are paired+-- by position, and the binders of the right list are renamed to those of the+-- left one, all at once. Since the left binders are distinct, no two positions+-- get the same name. instance UnifiablePattern NameBinderList where-  unifyPatterns NameBinderListEmpty NameBinderListEmpty = SameNameBinders emptyNameBinders-  unifyPatterns (NameBinderListCons x xs) (NameBinderListCons y ys) =-    case (assertDistinct x, assertDistinct y) of-      (Distinct, Distinct) -> unifyNameBinders x y `andThenUnifyPatterns` (xs, ys)-  -- Lists of different lengths are not unifiable. This case is reachable-  -- whenever a language has patterns that bind different numbers of names ---  -- a wildcard and a variable, say -- since the default 'unifyPatterns'-  -- flattens every pattern to a 'NameBinderList'. Note that this module sets-  -- @-Wno-incomplete-patterns@, so its absence was not reported.-  unifyPatterns _ _ = NotUnifiable+  unifyPatterns l r+    -- Reached through 'unsafeUnifyPatternBinders' for patterns that bind different+    -- numbers of names.+    | Prelude.length ls /= Prelude.length rs = NotUnifiable+    | ls == rs  = unsafeCoerce (SameNameBinders (fromNameBindersList l))+    | otherwise = RenameRightNameBinder (fromNameBindersList l) rename+    where+      ls = rawNameBinderList l+      rs = rawNameBinderList r+      leftOf = IntMap.fromList (Prelude.zip rs ls)+      rename (UnsafeNameBinder (UnsafeName i)) =+        UnsafeNameBinder (UnsafeName (IntMap.findWithDefault i i leftOf))  -- | Comparison of scope-indexed values up to α, in a known scope. --@@ -1175,6 +1257,114 @@     SameNameBinders{} -> True     _                 -> False +-- | Unify the binders of two patterns, pairing them in order. Patterns that+-- bind different numbers of names do not unify. When the binders differ, those+-- of the right pattern are renamed to those of the left one.+--+-- This is a building block for a hand-written 'unifyPatterns', and it is+-- unsafe: use it only once the two patterns are known to agree on everything+-- else (constructors, nesting and non-binding fields), as 'gunifyPatterns'+-- does. On its own it ignores all of these, so it unifies @(x, _)@ with+-- @(_, y)@. See @Language.LambdaPi.Impl.Foil@ in the @lambda-pi@ example for+-- an instance that checks the shape of two patterns first.+--+-- @since 0.5.0+unsafeUnifyPatternBinders+  :: (CoSinkable pattern, Distinct n)+  => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r+unsafeUnifyPatternBinders l r = coerce (unifyPatterns (nameBinderListOf l) (nameBinderListOf r))++-- | Do two patterns unify? The patterns may extend different scopes, as+-- sub-patterns do once a binder before them has been renamed. This is safe+-- since only the constructor of the verdict is consulted.+--+-- @since 0.5.0+unsafeUnifiablePatterns+  :: forall pattern n l n' r. UnifiablePattern pattern+  => pattern n l -> pattern n' r -> Bool+unsafeUnifiablePatterns l r =+  case unifyPatterns @pattern @VoidS (unsafeCoerce l) (unsafeCoerce r) of+    NotUnifiable -> False+    _            -> True++-- ** Structural unification of patterns++-- | Unify two patterns structurally, through their "Generics.Kind"+-- representation. They unify when they consist of the same constructors,+-- nested in the same way, and their binders are then paired in order. A+-- sub-pattern is compared with its own 'unifyPatterns'.+--+-- This is the default 'unifyPatterns', so a pattern type that derives+-- 'GenericK' gets it from an empty instance. A hand-written instance can call+-- it after comparing the fields that it ignores:+--+-- * non-binding fields (such as source positions, labels or literals), which+--   can be compared with 'UnifiableInPattern';+-- * fields indexed by a scope (payloads), which need the scope (see+--   'unifyPatternsIn').+--+-- @since 0.5.0+gunifyPatterns+  :: forall pattern n l r.+     (GenericK pattern, GUnifiablePattern (RepK pattern), CoSinkable pattern, Distinct n)+  => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r+gunifyPatterns l r+  | gsamePatternShape (fromK @_ @pattern @(n :&&: l :&&: LoT0) l)+                      (fromK @_ @pattern @(n :&&: r :&&: LoT0) r)+              = unsafeUnifyPatternBinders l r+  | otherwise = NotUnifiable++-- | The shape of a pattern on its "Generics.Kind" representation, which is+-- what 'gunifyPatterns' compares.+--+-- @since 0.5.0+class GUnifiablePattern f where+  -- | Do two values consist of the same constructors, nested in the same way?+  --+  -- @since 0.5.0+  gsamePatternShape :: f as -> f bs -> Bool++instance GUnifiablePattern V1 where+  gsamePatternShape _ _ = True++instance GUnifiablePattern U1 where+  gsamePatternShape U1 U1 = True++instance GUnifiablePattern f => GUnifiablePattern (M1 i c f) where+  gsamePatternShape (M1 x) (M1 y) = gsamePatternShape x y++instance (GUnifiablePattern f, GUnifiablePattern g) => GUnifiablePattern (f :+: g) where+  gsamePatternShape (L1 x) (L1 y) = gsamePatternShape x y+  gsamePatternShape (R1 x) (R1 y) = gsamePatternShape x y+  gsamePatternShape _      _      = False++instance (GUnifiablePattern f, GUnifiablePattern g) => GUnifiablePattern (f :*: g) where+  gsamePatternShape (x :*: y) (x' :*: y') = gsamePatternShape x x' && gsamePatternShape y y'++instance GUnifiablePattern f => GUnifiablePattern (c :=>: f) where+  gsamePatternShape (SuchThat x) (SuchThat y) = gsamePatternShape x y++instance GUnifiablePattern f => GUnifiablePattern (Exists k f) where+  gsamePatternShape (Exists x) (Exists y) = gsamePatternShape x y++-- | A non-binding field is ignored.+instance GUnifiablePattern (Field (Kon a)) where+  gsamePatternShape _ _ = True++-- | A non-binding field is ignored.+instance GUnifiablePattern (Field (Var x)) where+  gsamePatternShape _ _ = True++-- | A field indexed by one scope is a payload, and comparing it needs the+-- scope (see 'unifyPatternsIn'), so it is ignored here.+instance GUnifiablePattern (Field (Kon f :@: Var i)) where+  gsamePatternShape _ _ = True++-- | A binder or a sub-pattern is compared with its own 'unifyPatterns'. Two+-- binders always unify.+instance UnifiablePattern f => GUnifiablePattern (Field (Kon f :@: Var i :@: Var j)) where+  gsamePatternShape (Field x) (Field y) = unsafeUnifiablePatterns x y+ -- * Safe sinking  -- | Sinking an expression from scope @n@ into a (usualy extended) scope @l@,@@ -1201,7 +1391,7 @@  -- | A container of sinkable expressions is sinkable, elementwise. ----- The point of this instance is 'sinkContainer': since the proof typechecks,+-- The point of this instance is 'sink1': since the proof typechecks, -- sinking the whole container is a coercion, and does not walk its spine. instance (Functor f, Sinkable e) => Sinkable (Compose f e) where   sinkabilityProof rename (Compose xs) = Compose (fmap (sinkabilityProof rename) xs)@@ -1290,13 +1480,6 @@ sink1 :: (Functor f, Sinkable e, DExt n l) => f (e n) -> f (e l) sink1 = getCompose . sink . Compose --- | The name 'sink1' had before the family existed.------ @since 0.3.2-sinkContainer :: (Functor f, Sinkable e, DExt n l) => f (e n) -> f (e l)-sinkContainer = sink1-{-# DEPRECATED sinkContainer "Use sink1, its name in the sink family" #-}- -- | The sinkability proof lifted through a 'Bifunctor', with one renaming -- per slot. Once this typechecks, sinking both slots at once is a coercion; -- 'sink2' is to this proof exactly what 'sink' is to 'sinkabilityProof'.@@ -1544,35 +1727,45 @@   where     unchanged = nameId (nameOf binder) == nameId (nameOf binder') --- | Carry a payload along a transport.+-- | Carry a payload along a transport, into the ambient scope. ----- The 'Sinkable' instance does the walking, and only when it has to. While no--- binder has been refreshed the payload is taken over as it stands, so the--- traversals that never rename ('extendScopePattern', 'namesOfPattern',+-- While no binder has been refreshed, the payload is taken over as it stands,+-- so the traversals that never rename ('extendScopePattern', 'namesOfPattern', -- 'nameBinderListOf') do not walk payloads at all. --+-- Otherwise the payload is renamed with 'rbind', which refreshes the payload's+-- own binders where they would capture. For instance, if a binder @x0@ of the+-- pattern is refreshed to @x1@, a later payload @λx1. x0@ becomes @λx2. x1@,+-- and choosing @x2@ needs the ambient scope.+-- -- The whole recipe for a payload-carrying pattern, at a telescope of labelled -- steps: ----- > instance Sinkable e => CoSinkable (Telescope label e) where+-- > instance (Sinkable e, RelMonad Name e) => CoSinkable (Telescope label e) where -- >   withPattern withBinder unit comp = go verbatimTransport -- >     where--- >       go _transport _scope TelescopeEmpty cont = cont unit TelescopeEmpty+-- >       go _transport scope TelescopeEmpty cont = cont unit TelescopeEmpty scope -- >       go transport scope (TelescopeCons label payload binder rest) cont = -- >         withBinder scope binder $ \fbinder binder' -> -- >           go (transportUnderBinder transport binder binder')--- >              (extendScope binder' scope) rest $ \frest rest' ->+-- >              (extendScope binder' scope) rest $ \frest rest' scope'' -> -- >             cont (comp fbinder frest)--- >               (TelescopeCons label (transportPayload transport payload)+-- >               (TelescopeCons label (transportPayload scope transport payload) -- >                              binder' rest')+-- >               scope'' ----- Note which transport each payload takes: the one accumulated /before/ its own--- binder, since that is the scope the payload lives in.+-- Note which transport and which scope each payload takes: those reached+-- /before/ its own binder, since that is the scope the payload lives in. -- -- @since 0.4.0-transportPayload :: Sinkable e => PatternTransport n o -> e n -> e o-transportPayload TransportVerbatim         = unsafeCoerce-transportPayload (TransportRenamed rename) = sinkabilityProof rename+transportPayload+  :: (RelMonad Name e, Distinct o)+  => Scope o                -- ^ The ambient scope the payload is carried into.+  -> PatternTransport n o+  -> e n+  -> e o+transportPayload _scope TransportVerbatim         payload = unsafeCoerce payload+transportPayload scope  (TransportRenamed rename) payload = rbind scope payload (rreturn . rename)  -- | Carry a single name along a transport. --@@ -2006,6 +2199,37 @@   -- @since 0.0.1   injectName :: Name n -> e n +-- | Relative monads, restricted to types indexed by scopes in kind 'S'.+--+-- @since 0.0.1+class RelMonad (f :: S -> Type) (m :: S -> Type) where+  -- | Relative version of 'return'.+  --+  -- @since 0.0.1+  rreturn :: f a -> m a++  -- | Relative version of '>>='.+  --+  -- Note the two special additions to the usual definition of a relative binding operation:+  --+  -- 1. @'Scope' b@ is added since it corresponds to the runtime counterpart of the type parameter @b@.+  -- 2. @t'Distinct' b@ constraint helps to ensure we only work with scopes that are distinct.+  --+  -- Technically, it is also possible to add similar components for @a@ parameter.+  -- Also, we could probably treat types in 'S' as singletons and extract distinct scopes that way,+  -- preserving the more general type signature for 'rbind'.+  --+  -- @since 0.0.1+  rbind :: Distinct b => Scope b -> m a -> (f a -> m b) -> m b++-- | A name has no binders, so renaming it needs no scope. This lets a pattern+-- carry names as payloads (see 'transportPayload').+--+-- @since 0.5.0+instance RelMonad Name Name where+  rreturn = id+  rbind _scope name f = f name+ -- * Kind-polymorphic sinkability  -- | One renaming per scope index of a kind-polymorphic type, which is what@@ -2052,12 +2276,17 @@  instance SinkableK Name where   sinkabilityProofK renameK@(RCons rename RNil) name cont = cont renameK (rename name)+-- | A binder has two scope indices, so it is handed two renamings, for the+-- outer and the inner scope. The binder keeps its name, and the renaming of+-- the inner scope is a coercion, as in 'extendRenaming', so this agrees with+-- 'sink' on inclusions. instance SinkableK NameBinder where-  sinkabilityProofK (RCons _ RNil) (UnsafeNameBinder name) cont =-    cont (RCons unsafeCoerce RNil) (UnsafeNameBinder name)+  sinkabilityProofK (RCons rename (RCons _ RNil)) (UnsafeNameBinder name) cont =+    cont (RCons rename (RCons unsafeCoerce RNil)) (UnsafeNameBinder name)+-- | Two renamings, as for 'NameBinder'. instance SinkableK NameBinders where-  sinkabilityProofK (RCons _ RNil) (UnsafeNameBinders s) cont =-    cont (RCons unsafeCoerce RNil) (UnsafeNameBinders s)+  sinkabilityProofK (RCons rename (RCons _ RNil)) (UnsafeNameBinders s) cont =+    cont (RCons rename (RCons unsafeCoerce RNil)) (UnsafeNameBinders s)  instance GenericK NameBinderList where   type RepK NameBinderList = ((Var0 :~~: Var1) :=>: U1) :+: Exists S@@ -2197,15 +2426,22 @@       RCons rename' RNil -> \x' ->         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+-- 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-  gsinkabilityProofK irename@(RCons _ RNil) (Field x) cont =-    sinkabilityProofK irename x $ \rename' x' ->-      cont rename' (Field x')+  gsinkabilityProofK irename (Field x) cont =+    sinkabilityProofK (RCons (extractRenamingK @_ @VZ irename) RNil) x $ \case+      RCons rename' RNil -> \x' ->+        cont (putBackRenamingK @_ @VZ rename' irename) (Field (unsafeCoerce x')) +-- | As for @t'Field' ('Kon' f ':@:' 'Kon' a ':@:' 'Var0')@. instance SinkableK (f a b) => GSinkableK (Field (Kon f :@: Kon a :@: Kon b :@: Var0)) where-  gsinkabilityProofK irename@(RCons _ RNil) (Field x) cont =-    sinkabilityProofK irename x $ \rename' x' ->-      cont rename' (Field x')+  gsinkabilityProofK irename (Field x) cont =+    sinkabilityProofK (RCons (extractRenamingK @_ @VZ irename) RNil) x $ \case+      RCons rename' RNil -> \x' ->+        cont (putBackRenamingK @_ @VZ rename' irename) (Field (unsafeCoerce x'))  -- | Reading one scope index out of a list of them, and putting a renaming -- back at that position. This is what lets a generic traversal work on the@@ -2306,8 +2542,30 @@   -- ^ Continuation, accepting the result for the entire pattern, a (possibly refreshed) pattern, and the scope extended by that pattern.   -> r gunsafeWithPatternViaHasNameBinders withBinder id_ comp_ scope pat cont =-  withPattern withBinder id_ comp_ scope (ggetNameBinders pat) $ \result binders scope' ->-    cont result (gunsafeSetNameBinders (unsafeCoerce pat) binders) scope' -- FIXME: safer version+  withPattern withBinder id_ comp_ scope (unsafeNameBinderListFromRaw raw) $ \result binders scope' ->+    cont result (gunsafeSetNameBinderList (unsafeCoerce pat) binders) scope' -- FIXME: safer version+  where+    -- The binders in the order of the pattern. 'NameBinders' is a set, so+    -- going through it would put them back in ascending order of names.+    raw = ggetNameBindersRaw (fromK @_ @pattern @(n :&&: l :&&: LoT0) pat)++-- | The binders of a pattern, in the order of the pattern, from their raw names.+--+-- @since 0.5.0+unsafeNameBinderListFromRaw :: [RawName] -> NameBinderList n l+unsafeNameBinderListFromRaw []       = unsafeCoerce NameBinderListEmpty+unsafeNameBinderListFromRaw (x : xs) =+  NameBinderListCons (UnsafeNameBinder (UnsafeName x)) (unsafeNameBinderListFromRaw xs)++-- | Replace the binders of a pattern by position, the first binder of the+-- list going to the first binder of the pattern, and so on.+--+-- @since 0.5.0+gunsafeSetNameBinderList+  :: forall f n l l'. (GenericK f, GValidNameBinders f (RepK f), GHasNameBinders (RepK f))+  => f n l -> NameBinderList n l' -> f n l'+gunsafeSetNameBinderList e binders = toK @_ @f @(n :&&: l' :&&: LoT0) $+  fst (greallyUnsafeSetNameBindersRaw (fromK @_ @f @(n :&&: l :&&: LoT0) e) (rawNameBinderList binders))  -- ** Manipulating nested 'NameBinder's -- | If @'HasNameBinders' f@, then @f n l@ is expected to act as a binder,

@@ -1,33 +1,11 @@-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE KindSignatures        #-}-{-# LANGUAGE MultiParamTypeClasses #-}-module Control.Monad.Foil.Relative where+-- | Relative monads over scopes, and 'liftRM' for renaming with them.+module Control.Monad.Foil.Relative (+  RelMonad (..),+  liftRM,+) where  import           Control.Monad.Foil-import           Data.Kind          (Type)---- | Relative monads, restricted to types indexed by scopes in kind 'S'.------ @since 0.0.1-class RelMonad (f :: S -> Type) (m :: S -> Type) where-  -- | Relative version of 'return'.-  ---  -- @since 0.0.1-  rreturn :: f a -> m a--  -- | Relative version of '>>='.-  ---  -- Note the two special additions to the usual definition of a relative binding operation:-  ---  -- 1. @'Scope' b@ is added since is corresponds to the runtime counterpart of the type parameter @b@.-  -- 2. @t'Distinct' b@ constraint helps to ensure we only work with scopes that are distinct.-  ---  -- Technically, it is also possible add similar components for @a@ parameter.-  -- Also, we could probably treat types in 'S' as singletons and extract distinct scopes that way,-  -- preserving the more general type signature for 'rbind'.-  ---  -- @since 0.0.1-  rbind :: Distinct b => Scope b -> m a -> (f a -> m b) -> m b+import           Control.Monad.Foil.Internal (RelMonad (..))  -- | Relative version of @liftM@ (an 'fmap' restricted to 'Monad'). --

@@ -9,7 +9,6 @@  import qualified Control.Monad.Foil         as Foil import           Control.Monad.Foil.TH.Util-import           Data.List                  (nub)  -- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances. --@@ -170,95 +169,3 @@           go (i + 1) scope' rename' (AppE p (VarE xi)) conPatterns           where             xi = mkName ("x" ++ show i)---- | Generate a structural 'Foil.UnifiablePattern' instance, comparing--- constructors and non-binding fields rather than only the binders.------ This deriver does not work and has no call sites. See the deprecation note.------ @since 0.1.0-deriveUnifiablePattern-  :: Name -- ^ Type name for raw variable identifiers.-  -> Name -- ^ Type name for raw patterns.-  -> Q [Dec]-{-# DEPRECATED deriveUnifiablePattern-  "This deriver does not work and has no call sites. It reifies the raw \-  \(BNFC) pattern type and guesses the scope-safe type and constructor names \-  \by prefixing \"Foil\", and it rejects GADT constructors -- so it cannot \-  \handle the pattern types that mkFoilPattern and mkFreeFoil generate, nor a \-  \hand-written pattern GADT. Instead, derive GenericK and take an empty \-  \instance (see Control.Monad.Foil), or write the instance by hand as \-  \Language.LambdaPi.Impl.Foil does. Note that the empty instance compares \-  \only the binders; see UnifiablePattern. Structural derivation is tracked \-  \in https://github.com/fizruk/free-foil/issues/23. To be removed in the \-  \next major release." #-}-deriveUnifiablePattern nameT patternT = do-  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT--  let (eqTypes, clauses) = mapM clauseUnifyPatterns patternCons-      ctx = nub [ AppT (ConT ''Foil.UnifiableInPattern) type_ | type_ <- eqTypes, type_ `elem` map (VarT . tvarName) patternTVars ]-  return-    [ InstanceD Nothing ctx (AppT (ConT ''Foil.UnifiablePattern) (PeelConT foilPatternT (map (VarT . tvarName) patternTVars)))-        [ FunD 'Foil.unifyPatterns (clauses ++ [notUnifiableClause]) ]-    ]--  where-    foilPatternT = mkName ("Foil" ++ nameBase patternT)--    notUnifiableClause :: Clause-    notUnifiableClause = Clause [WildP, WildP] (NormalB (ConE 'Foil.NotUnifiable)) []--    clauseUnifyPatterns :: Con -> ([Type], Clause)-    clauseUnifyPatterns RecC{} = error "Record constructors (RecC) are not supported yet!"-    clauseUnifyPatterns InfixC{} = error "Infix constructors (InfixC) are not supported yet!"-    clauseUnifyPatterns ForallC{} = error "Existential constructors (ForallC) are not supported yet!"-    clauseUnifyPatterns GadtC{} = error "GADT constructors (GadtC) are not supported yet!"-    clauseUnifyPatterns RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"-    clauseUnifyPatterns (NormalC conName params) =-      case go 1 [] [] params of-        (body, eqTypes) ->-          (eqTypes, Clause-            [ConP foilConName [] paramsL, ConP foilConName [] paramsR]-            (NormalB body)-            [])-      where-        foilConName = mkName ("Foil" ++ nameBase conName)-        paramsL = zipWith (mkConParamPattern "l") params [1..]-        paramsR = zipWith (mkConParamPattern "r") params [1..]-        mkConParamPattern s _ i = VarP (mkName (s ++ show i))--        mkUnifyAllPairsRev [] = AppE (ConE 'Foil.SameNameBinders) (VarE 'Foil.emptyNameBinders)-        mkUnifyAllPairsRev [(isNameBinder, l, r)]-          | isNameBinder = AppE (AppE (VarE 'Foil.unifyNameBinders) l) r-          | otherwise    = AppE (AppE (VarE 'Foil.unifyPatterns) l) r-        mkUnifyAllPairsRev ((isNameBinder, l, r) : pairs) =-          InfixE-            (Just (mkUnifyAllPairsRev pairs))-            (VarE (if isNameBinder then 'Foil.andThenUnifyNameBinders else 'Foil.andThenUnifyPatterns))-            (Just (TupE [Just l, Just r]))---        go _i eqTypes pairsRev [] = (mkUnifyAllPairsRev pairsRev, eqTypes)-        go i eqTypes pairsRev ((_bang, PeelConT tyName _tyParams) : conParams)-          | tyName == nameT || tyName == patternT =-            case go (i + 1) eqTypes ((isNameBinder, l, r) : pairsRev) conParams of-              (next, eqTypes') ->-                (CaseE (TupE [Just (AppE (VarE 'Foil.assertDistinct) l), Just (AppE (VarE 'Foil.assertDistinct) r)])-                  [Match-                    (TupP [ConP 'Foil.Distinct [] [], ConP 'Foil.Distinct [] []])-                    (NormalB next)-                    []], eqTypes')-          where-            isNameBinder = tyName == nameT-            l = VarE (mkName ("l" ++ show i))-            r = VarE (mkName ("r" ++ show i))-        go i eqTypes pairsRev ((_bang, type_) : conPatterns) =-          case go (i + 1) eqTypes pairsRev conPatterns of-            (next, eqTypes') ->-              (CondE-                (InfixE (Just l) (VarE 'Foil.unifyInPattern) (Just r))-                next-                (ConE 'Foil.NotUnifiable), type_ : eqTypes')-          where-            l = VarE (mkName ("l" ++ show i))-            r = VarE (mkName ("r" ++ show i))

@@ -25,7 +25,8 @@ module Control.Monad.Foil.Telescope where  import           Control.Monad.Foil.Internal-import           Control.Monad.Foil.Relative (RelMonad, liftRM)+import           Control.Monad.Foil.Relative (liftRM)+import           Data.Coerce                 (coerce)  -- | A labelled telescope: a chain of binders, each carrying a label and a -- payload in the scope before it.@@ -58,9 +59,10 @@ -- would leave a payload that names a refreshed binder pointing at the name -- that binder used to have. This instance follows the recipe in -- 'transportPayload': a 'PatternTransport' threaded through the traversal,--- with each payload moved by the transport accumulated /before/ its own--- binder, that being the scope the payload lives in.-instance Sinkable e => CoSinkable (Telescope label e) where+-- with each payload moved by the transport and the scope reached /before/ its+-- own binder. Moving a payload may refresh its own binders, which is why the+-- instance needs @'RelMonad' 'Name' e@.+instance (Sinkable e, RelMonad Name e) => CoSinkable (Telescope label e) where   coSinkabilityProof rename TelescopeEmpty cont = cont rename TelescopeEmpty   coSinkabilityProof rename (TelescopeCons label payload binder rest) cont =     coSinkabilityProof rename binder $ \rename' binder' ->@@ -98,7 +100,7 @@              (extendScope binder' scope)              rest $ \frest rest' scope'' ->             cont (comp fbinder frest)-              (TelescopeCons label (transportPayload transport payload) binder' rest')+              (TelescopeCons label (transportPayload scope transport payload) binder' rest')               scope''  -- | Two telescopes unify when their binders line up and their payloads agree.@@ -107,19 +109,15 @@ -- parameter's spelling is no more relevant than a bound variable's. Payloads -- are not, since two telescopes agreeing on binders may well disagree on types. ----- 'unifyPatterns' is the binder-only approximation, which is all a caller--- without a scope can be given. 'unifyPatternsIn' is the real answer, and+-- 'unifyPatterns' compares the binders only, which is all a caller without a+-- scope can be given. 'unifyPatternsIn' is the real answer, and -- it is what the library's α-equivalence calls. instance (Sinkable e, AlphaEquiv e, RelMonad Name e)     => UnifiablePattern (Telescope label e) where-  unifyPatterns TelescopeEmpty TelescopeEmpty =-    SameNameBinders emptyNameBinders-  unifyPatterns (TelescopeCons _ _ x xs) (TelescopeCons _ _ y ys) =-    case (assertDistinct x, assertDistinct y) of-      (Distinct, Distinct) ->-        unifyNameBinders x y `andThenUnifyPatterns` (xs, ys)-  -- Telescopes of different lengths bind different numbers of names.-  unifyPatterns _ _ = NotUnifiable+  -- The shape of a telescope is its length, so pairing its binders in order is+  -- enough here.+  unifyPatterns tele1 tele2 =+    coerce (unifyPatterns (telescopeBinders tele1) (telescopeBinders tele2))    unifyPatternsIn scope tele1 tele2     | payloadsAgree scope tele1 tele2 verdict = verdict@@ -214,7 +212,9 @@   => Telescope label e n l -> [Param label e l] telescopeParams TelescopeEmpty = [] telescopeParams (TelescopeCons label ty binder rest) =-  case (assertExt binder, assertExt rest) of+  -- 'assertExt' does not look at its argument. The binders of the rest are a+  -- pattern without the 'RelMonad' constraint that the telescope itself needs.+  case (assertExt binder, assertExt (telescopeBinders rest)) of     (Ext, Ext) ->       Param label (sink (nameOf binder)) (sink ty)         : telescopeParams rest

@@ -26,7 +26,6 @@  import           Control.DeepSeq import qualified Control.Monad.Foil.Internal as Foil-import qualified Control.Monad.Foil.Relative as Foil import           Data.Bifoldable import           Data.Bitraversable import           Data.Bifunctor@@ -759,52 +758,6 @@   fromRawPattern scope names pat $ \binder' names' ->     let scope' = Foil.extendScopePattern binder' scope      in ScopedAST binder' (unsafeConvertToAST toSig fromRawPattern getScopedTerm scope' names' (getScopedTerm scopedTerm))---- | Convert a raw term into a scope-safe term.------ @since 0.0.3-convertToAST-  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)-  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))-  -> (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)-  -> (rawScopedTerm -> rawTerm)-  -> Foil.Scope n-  -> Map rawIdent (Foil.Name n)-  -> rawTerm-  -> AST binder sig n-convertToAST = unsafeConvertToAST-{-# DEPRECATED convertToAST "Renamed to unsafeConvertToAST, since it calls error on an unresolved identifier. Use tryConvertToAST to report them instead." #-}---- | Same as 'convertToAST' but for scoped terms.------ @since 0.0.3-convertToScopedAST-  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)-  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))-  -> (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)-  -> (rawScopedTerm -> rawTerm)-  -> Foil.Scope n-  -> Map rawIdent (Foil.Name n)-  -> (rawPattern, rawScopedTerm)-  -> ScopedAST binder sig n-convertToScopedAST = unsafeConvertToScopedAST-{-# DEPRECATED convertToScopedAST "Renamed to unsafeConvertToScopedAST, since it calls error on an unresolved identifier." #-}  -- ** Convert from free foil 

@@ -312,11 +312,23 @@       ForallC params ctx con -> fmap (ForallC params ctx) <$> go con       RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) -toFreeFoilBindingCon :: FreeFoilConfig -> Type -> Type -> Con -> Q Con-toFreeFoilBindingCon config rawRetType theOuterScope = go+-- | How a generated binding type is declared.+data BindingFlavour+  = BindingNewtype+    -- ^ A @newtype@, whose one field takes no strictness annotation.+  | BindingData+    -- ^ A @data@ type.++toFreeFoilBindingCon :: FreeFoilConfig -> BindingFlavour -> Type -> Type -> Con -> Q Con+toFreeFoilBindingCon config flavour rawRetType theOuterScope = go   where     goType = toFreeFoilType SortBinder config theOuterScope +    -- The fields keep the annotations of the raw fields.+    fieldBang rawBang = case flavour of+      BindingNewtype -> Bang NoSourceUnpackedness NoSourceStrictness+      BindingData    -> rawBang+     goTypeArgs :: Int -> Type -> [BangType] -> Q (Type, [BangType])     goTypeArgs _ outerScope [] = pure (outerScope, [])     goTypeArgs i outerScope ((bang_, rawArgType) : rawArgs) = do@@ -326,18 +338,18 @@             innerScope <- VarT <$> newName ("i" <> show i)             let argType = toFreeFoilType SortBinder config outerScope innerScope rawArgType             (theInnerScope, argTypes) <- goTypeArgs (i + 1) innerScope rawArgs-            return (theInnerScope, ((bang_, argType) : argTypes))+            return (theInnerScope, ((fieldBang bang_, argType) : argTypes))            | Just _ <- lookupBindingName rawTypeName (freeFoilTermConfigs config) -> do             innerScope <- VarT <$> newName ("i" <> show i)             let argType = toFreeFoilType SortBinder config outerScope innerScope rawArgType             (theInnerScope, argTypes) <- goTypeArgs (i + 1) innerScope rawArgs-            return (theInnerScope, ((bang_, argType) : argTypes))+            return (theInnerScope, ((fieldBang bang_, argType) : argTypes))          _ -> do           let argType = toFreeFoilType SortBinder config outerScope outerScope rawArgType           (theInnerScope, argTypes) <- goTypeArgs (i + 1) outerScope rawArgs-          return (theInnerScope, ((bang_, argType) : argTypes))+          return (theInnerScope, ((fieldBang bang_, argType) : argTypes))      go :: Con -> Q Con     go = \case@@ -354,6 +366,28 @@       ForallC params ctx con -> ForallC params ctx <$> go con       RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) +-- | Is the binding type generated from these raw constructors a @newtype@?+--+-- 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+-- 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.+isNewtypeBinding :: FreeFoilConfig -> [Con] -> Bool+isNewtypeBinding config = \case+  [con] | Just [rawFieldType] <- singleConFields con ->+    isBindingFieldSort (bindingFieldSortOf config rawFieldType)+  _ -> False+  where+    singleConFields = \case+      NormalC _ types         -> Just (map snd types)+      RecC _ types            -> Just (map (\(_, _, t) -> t) types)+      InfixC{}                -> Nothing+      GadtC [_] types _       -> Just (map snd types)+      RecGadtC [_] types _    -> Just (map (\(_, _, t) -> t) types)+      _                       -> Nothing+ -- | Is this raw field a binding (pattern) field? -- -- Such a field has no counterpart in the free foil node: the binder it stands for@@ -883,6 +917,12 @@ --  4. Signatures for terms, subterms, and scoped subterms. --  5. Pattern synonyms for terms, subterms, and scoped subterms. --+-- A scope-safe pattern type is a @newtype@ when its raw type has exactly one+-- constructor with exactly one field, and that field is an identifier or a+-- nested pattern (e.g. @newtype Pattern = PatternVar VarIdent@). Such a+-- pattern has the runtime representation of the field it wraps. Otherwise the+-- pattern type is @data@.+-- -- @since 0.2.0 mkFreeFoil :: FreeFoilConfig -> Q [Dec] mkFreeFoil config@FreeFoilConfig{..} = concat <$> sequence@@ -928,11 +968,16 @@       let bindingName = toFreeFoilName config rawBindingName           rawRetType = PeelConT rawBindingName (map (VarT . tvarName) tvars)           newParams = tvars ++ [PlainTV outerScope BndrReq, PlainTV innerScope BndrReq]-          toCon = toFreeFoilBindingCon config rawRetType (VarT outerScope)+          flavour+            | isNewtypeBinding config cons = BindingNewtype+            | otherwise                    = BindingData+          toCon = toFreeFoilBindingCon config flavour rawRetType (VarT outerScope)       newCons <- mapM toCon cons       addModFinalizer $ putDoc (DeclDoc bindingName)         ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A binding type, scope-safe version of '" ++ show rawBindingName ++ "'.")-      return (DataD [] bindingName newParams Nothing newCons [])+      return $ case (flavour, newCons) of+        (BindingNewtype, [newCon]) -> NewtypeD [] bindingName newParams Nothing newCon []+        _                          -> DataD [] bindingName newParams Nothing newCons []      -- A concrete 'Foil.CoSinkable' instance for the generated binding type,     -- one clause per constructor, delegating to the fields' instances. The

@@ -0,0 +1,48 @@+{-# LANGUAGE DataKinds  #-}+{-# LANGUAGE GADTs      #-}+{-# LANGUAGE LambdaCase #-}+-- | The laws for the λ-calculus of "Control.Monad.Foil.Example", the plain+-- foil without the free monad: its hand-written 'Foil.Sinkable' instance,+-- its relative monad ('rbind'), and its 'F.substitute'. Terms are+-- generated and compared through the free foil version of the same+-- language, which has the same constructors.+module Control.Monad.Foil.ExampleLawsSpec (spec) where++import           Test.Hspec++import qualified Control.Monad.Foil                    as Foil+import qualified Control.Monad.Foil.Example            as F+import           Control.Monad.Foil.Laws+import           Control.Monad.Free.Foil               (AST (..))+import qualified Control.Monad.Free.Foil.Example       as FF+import           Control.Monad.Free.Foil.ExampleSyntax (exprSyntax)+import           Control.Monad.Free.Foil.Laws.Mirror++-- | The free foil term with the same structure.+toAST :: F.Expr n -> FF.Expr n+toAST = \case+  F.VarE x      -> Var x+  F.AppE f x    -> FF.AppE (toAST f) (toAST x)+  F.LamE b body -> FF.LamE b (toAST body)++-- | The plain foil term with the same structure.+fromAST :: FF.Expr n -> F.Expr n+fromAST = \case+  Var x          -> F.VarE x+  FF.AppE f x    -> F.AppE (fromAST f) (fromAST x)+  FF.LamE b body -> F.LamE b (fromAST body)++mirror :: Mirror Foil.NameBinder FF.ExprF F.Expr+mirror = Mirror+  { mirrorSyntax = exprSyntax genNameBinder nameBinderNames+  , mirrorFrom = fromAST+  , mirrorTo = toAST+  , mirrorSubstitute = F.substitute+  , mirrorAlphaEquiv = Nothing+  }++spec :: Spec+spec = mirrorSpec mirror $ \cls -> \case+  MirrorSinkAgreesWithLiftRM | cls /= Inclusions -> ByDesign+    "extendRenaming is a coercion, so free names under a binder are not renamed"+  _ -> Holds

@@ -0,0 +1,73 @@+{-# LANGUAGE DataKinds  #-}+{-# LANGUAGE GADTs      #-}+{-# LANGUAGE RankNTypes #-}+-- | The laws of 'Foil.Sinkable' and 'Foil.CoSinkable' for the types of the+-- foil itself: names, sets of names, and the shipped pattern types.+--+-- See "Control.Monad.Foil.Laws" for the statements, and+-- "Control.Monad.Free.Foil.LawsSpec" for terms.+module Control.Monad.Foil.LawsSpec (spec) where++import           Data.Functor.Compose        (Compose (..))+import           Test.Hspec+import           Test.QuickCheck++import qualified Control.Monad.Foil          as Foil+import           Control.Monad.Foil.Internal (U2 (..))+import           Control.Monad.Foil.Laws++-- | Lists of names, through the 'Compose' instance.+genNames :: Ctx n -> Gen (Compose [] Foil.Name n)+genNames ctx = case ctxNames ctx of+  [] -> pure (Compose [])+  xs -> Compose <$> listOf (elements xs)++-- | Sets of names.+genNameSet :: Ctx n -> Gen (Foil.NameSet n)+genNameSet ctx = Foil.nameSetFromList <$> sublistOf (ctxNames ctx)++-- | Unordered sets of binders, from a list.+genNameBinders :: GenPattern Foil.NameBinders+genNameBinders ctx = do+  PatIn binders <- genNameBinderList ctx+  pure (PatIn (Foil.fromNameBindersList binders))++-- | The wildcard pattern.+genU2 :: GenPattern U2+genU2 ctx = withCtx ctx $ \_ -> pure (PatIn U2)++spec :: Spec+spec = do+  describe "Sinkable" $ do+    describe "[Name] (via Compose)" $+      sinkableSpec+        (\_ (Compose xs) (Compose ys) -> map Foil.nameId xs == map Foil.nameId ys)+        (\(Compose xs) -> unwords (map showName xs))+        genNames+        (\(Compose xs) -> map Compose (shrinkList (const []) xs))+        (\_ _ -> Holds)+    describe "NameSet" $+      sinkableSpec+        (\_ xs ys -> map Foil.nameId (Foil.nameSetToList xs) == map Foil.nameId (Foil.nameSetToList ys))+        (unwords . map showName . Foil.nameSetToList)+        genNameSet+        (const [])+        (\_ _ -> Holds)++  describe "CoSinkable" $ do+    describe "NameBinder" $ coSinkableSpec nameBinderNames genNameBinder extensionByCoercion+    describe "NameBinderList" $ coSinkableSpec nameBinderListNames genNameBinderList extensionByCoercion+    describe "NameBinders" $ coSinkableSpec patternRawNames genNameBinders extensionByCoercion+    describe "U2" $ coSinkableSpec (const []) genU2 (\_ _ -> Holds)++  describe "UnifiablePattern" $ do+    describe "NameBinder" $ unifyPatternsSpec nameBinderNames genNameBinderPair Holds+    describe "NameBinderList" $+      unifyPatternsSpec nameBinderListNames genNameBinderListPair Holds++-- | Two single binders out of the same scope.+genNameBinderPair :: GenPatternPair Foil.NameBinder+genNameBinderPair ctx = do+  PatIn l <- genNameBinder ctx+  PatIn r <- genNameBinder ctx+  pure (PatPair l r)

@@ -79,7 +79,7 @@              (Foil.extendScope binder' scope)              rest $ \frest rest' scope'' ->             cont (comp fbinder frest)-              (ChainCons (Foil.transportPayload transport payload) binder' rest')+              (ChainCons (Foil.transportPayload scope transport payload) binder' rest')               scope''  -- | The result of processing one binder, when there is nothing to carry.

@@ -0,0 +1,138 @@+{-# LANGUAGE DataKinds  #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs      #-}+{-# LANGUAGE LambdaCase      #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes      #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- | The laws of "Control.Monad.Foil.Laws" for telescopes, and one law that+-- only patterns with payloads have: refreshing a telescope transports its+-- payloads along the refreshed binders ('Foil.PatternTransport'). Payloads+-- are names or terms of the λ-calculus of "Control.Monad.Free.Foil.Example".+module Control.Monad.Foil.TelescopeLawsSpec (spec) where++import           Test.Hspec+import           Test.QuickCheck++import           Control.Monad.Foil+import           Control.Monad.Foil.Internal           (Name (..))+import           Control.Monad.Foil.Laws+import           Control.Monad.Foil.Relative           (RelMonad)+import           Control.Monad.Foil.Telescope          (Telescope (..))+import           Control.Monad.Free.Foil               (AST (..), substitute)+import           Control.Monad.Free.Foil.Example       (Expr, ExprF, pattern AppE, pattern LamE)+import           Control.Monad.Free.Foil.ExampleSyntax (exprSyntax)+import           Control.Monad.Free.Foil.Laws++-- | Telescopes of up to three steps, with payloads from a generator. The+-- telescope stops early where there is no payload to give.+genTelescope :: forall e. (forall n. Ctx n -> Gen (Maybe (e n))) -> GenPattern (Telescope () e)+genTelescope genE ctx0 = do+  k <- chooseInt (0, 3)+  go k ctx0+  where+    go :: Int -> Ctx n -> Gen (PatIn (Telescope () e) n)+    go k ctx = withCtx ctx $ \scope ->+      if k <= 0+        then pure (PatIn TelescopeEmpty)+        else genE ctx >>= \case+          Nothing -> pure (PatIn TelescopeEmpty)+          Just payload ->+            withHintedBinder scope $ \binder -> do+              PatIn rest <- go (k - 1) (extendCtx ctx binder)+              pure (PatIn (TelescopeCons () payload binder rest))++-- | The binders of a telescope, in order.+telescopeNames :: PatternNames (Telescope label e)+telescopeNames = \case+  TelescopeEmpty              -> []+  TelescopeCons _ _ b rest    -> nameId (nameOf b) : telescopeNames rest++-- | Payloads that are names of the scope before the step, if it has any.+genNamePayload :: Ctx n -> Gen (Maybe (Name n))+genNamePayload ctx = case ctxNames ctx of+  [] -> pure Nothing+  xs -> Just <$> elements xs++sg :: SyntaxGen NameBinder ExprF+sg = exprSyntax genNameBinder nameBinderNames++-- | Payloads that are λ-terms.+genTermPayload :: Ctx n -> Gen (Maybe (Expr n))+genTermPayload ctx = Just <$> sized (genAST sg ctx . min 8)++-- | A telescope with a body, as one λ-term: each step @(x : A)@ becomes+-- @A (λx. …)@, so that α-equivalence of the encodings is α-equivalence of+-- the telescopes with their bodies.+encode :: (forall x. e x -> Expr x) -> Telescope () e n l -> Expr l -> Expr n+encode f = \case+  TelescopeEmpty -> id+  TelescopeCons () payload binder rest -> \body ->+    AppE (f payload) (LamE binder (encode f rest body))++-- | A telescope with a body, decoded from its encoding.+data Decoded e n where+  Decoded :: Telescope () e n l -> Expr l -> Decoded e n++-- | Decode @k@ steps of an encoding.+decode :: (forall x. Expr x -> Maybe (e x)) -> Int -> Expr n -> Maybe (Decoded e n)+decode f k t+  | k <= 0 = Just (Decoded TelescopeEmpty t)+  | AppE a (LamE binder rest) <- t = do+      payload <- f a+      Decoded tele body <- decode f (k - 1) rest+      Just (Decoded (TelescopeCons () payload binder tele) body)+  | otherwise = Nothing++-- | Refreshing a telescope with 'withRefreshedPattern', and its body with+-- the substitution it returns, gives an α-variant. The telescope is built+-- in a scope @n@ and sunk (through its encoding) into an extension @o@ of+-- @n@ that binds the names of its binders, so that every binder clashes.+transportLaw+  :: (Sinkable e, RelMonad Name e)+  => (forall x. e x -> Expr x) -> (forall x. Expr x -> Maybe (e x))+  -> (forall x. Ctx x -> Gen (Maybe (e x)))+  -> Property+transportLaw toE fromE genE =+  forAllShow genCase showCase $ \(TransportCase o k enc) -> withCtx o $ \scopeO ->+    case decode fromE k enc of+      Nothing -> counterexample "the encoding does not decode" False+      Just (Decoded tele body) ->+        withRefreshedPattern scopeO tele $ \extend tele' scope' ->+          let body' = substitute scope' (extend identitySubst) body+              refreshed = encode toE tele' body'+           in counterexample ("refreshed = " <> showAST sg refreshed) $+                alphaEqNameless nameBinderNames enc refreshed+  where+    genCase = do+      SomeCtx n <- genCtx+      PatIn tele <- genTelescope genE n+      body <- sized (genAST sg (extendCtx n tele) . min 8)+      let names = telescopeNames tele+      withCtx n $ \scopeN ->+        clashWith names scopeN $ \o ->+          let enc = sink (encode toE tele body)+           in pure (TransportCase (extendCtx n o) (length names) enc)++    -- Extend a scope by binders with the given names, which are fresh for it.+    clashWith :: Distinct n => [Int] -> Scope n -> (forall o. DExt n o => NameBinderList n o -> r) -> r+    clashWith [] _ cont = cont NameBinderListEmpty+    clashWith (x : xs) scope cont = withRefreshed scope (UnsafeName x) $ \b ->+      clashWith xs (extendScope b scope) $ \bs -> cont (NameBinderListCons b bs)++    showCase (TransportCase o _ enc) = unlines [ "o = " <> showCtx o, "encoding = " <> showAST sg enc ]++-- | An encoded telescope of @k@ steps in a scope @o@.+data TransportCase where+  TransportCase :: Ctx o -> Int -> Expr o -> TransportCase++spec :: Spec+spec = do+  describe "Telescope () Name" $ do+    coSinkableSpec telescopeNames (genTelescope genNamePayload) extensionByCoercion+    law Holds "withRefreshedPattern transports payloads along refreshed binders" $+      transportLaw Var (\case Var x -> Just x; _ -> Nothing) genNamePayload+  describe "Telescope () Expr" $ do+    coSinkableSpec telescopeNames (genTelescope genTermPayload) extensionByCoercion+    law Holds "withRefreshedPattern transports payloads along refreshed binders" $+      transportLaw id Just genTermPayload

@@ -5,26 +5,18 @@ {-# LANGUAGE TemplateHaskell   #-} {-# LANGUAGE TypeFamilies      #-} --- | The default 'Foil.unifyPatterns' compares two patterns only up to their--- binders: it flattens both to a 'Foil.NameBinderList' and unifies those. This--- module pins down what that does /not/ distinguish, because the default is what--- every client gets from an empty instance, and because two of its consequences--- are surprising the first time they are met.+-- | What the default 'Foil.unifyPatterns' ('Foil.gunifyPatterns') tells+-- apart, and what 'Foil.unsafeUnifyPatternBinders' ignores when used on its+-- own. -- -- Since α-equivalence is defined in terms of 'Foil.unifyPatterns', these are also -- statements about which terms the library considers α-equivalent.------ None of this is a defect. What the body of a binding construct can refer to is--- exactly the pattern's binders, in order, so for most languages the default is--- the intended notion. It is a defect only for a language whose patterns carry--- semantically relevant data — a constructor name in a @match@ branch, say — and--- such a language should write 'Foil.unifyPatterns' by hand. module Control.Monad.Foil.UnifiablePatternSpec (spec) where  import           Test.Hspec -import qualified Control.Monad.Foil as Foil-import           Generics.Kind.TH   (deriveGenericK)+import qualified Control.Monad.Foil          as Foil+import           Generics.Kind.TH            (deriveGenericK)  -- | A pattern type with just enough structure to observe the default: -- two constructors binding one name each, a nesting constructor, and a@@ -43,6 +35,30 @@ instance Foil.CoSinkable DemoPattern instance Foil.UnifiablePattern DemoPattern +-- | The same pattern type, with 'Foil.unsafeUnifyPatternBinders' used on+-- its own, to show what it ignores when its precondition is not checked.+data BinderPattern (n :: Foil.S) (l :: Foil.S) where+  BinderVar   :: Foil.NameBinder n l -> BinderPattern n l+  BinderBox   :: Foil.NameBinder n l -> BinderPattern n l+  BinderPair  :: BinderPattern n i -> BinderPattern i l -> BinderPattern n l+  BinderLabel :: String -> Foil.NameBinder n l -> BinderPattern n l++deriveGenericK ''BinderPattern+instance Foil.SinkableK BinderPattern+instance Foil.HasNameBinders BinderPattern+instance Foil.CoSinkable BinderPattern+instance Foil.UnifiablePattern BinderPattern where+  unifyPatterns = Foil.unsafeUnifyPatternBinders++-- | Do the two patterns unify, with or without a renaming?+unifies+  :: (Foil.UnifiablePattern pattern, Foil.Distinct n)+  => pattern n l -> pattern n r -> Bool+unifies l r =+  case Foil.unifyPatterns l r of+    Foil.NotUnifiable -> False+    _                 -> True+ -- | Do the two patterns unify with no renaming required? This is the observation -- α-equivalence makes, phrased in the public API. unifiesWithoutRenaming@@ -72,35 +88,88 @@                 cont x y z  spec :: Spec-spec = describe "the default unifyPatterns" $ do+spec = do+  defaultSpec+  binderSpec++-- | What the default 'Foil.unifyPatterns' tells apart: constructors and their+-- nesting, as well as binders.+defaultSpec :: Spec+defaultSpec = describe "the default unifyPatterns" $ do+  it "tells apart different constructors with equal binders" $+    Foil.withFresh Foil.emptyScope (\x ->+      unifies (DemoVar x) (DemoBox x))+      `shouldBe` False++  it "tells apart different constructors under a common one" $+    withThreeBinders (\x y _z ->+      unifies+        (DemoPair (DemoVar x) (DemoVar y))+        (DemoPair (DemoBox x) (DemoVar y)))+      `shouldBe` False++  it "tells apart (x, (y, z)) and ((x, y), z)" $+    withThreeBinders (\x y z ->+      unifies+        (DemoPair (DemoVar x) (DemoPair (DemoVar y) (DemoVar z)))+        (DemoPair (DemoPair (DemoVar x) (DemoVar y)) (DemoVar z)))+      `shouldBe` False++  it "tells apart patterns binding different numbers of names" $+    withThreeBinders (\x y _z ->+      unifies+        (DemoVar x)+        (DemoPair (DemoVar x) (DemoVar y)))+      `shouldBe` False++  it "ignores non-binding fields, whatever their values" $+    Foil.withFresh Foil.emptyScope (\x ->+      unifiesWithoutRenaming (DemoLabel "left" x) (DemoLabel "right" x))+      `shouldBe` True++  it "pairs the binders of two patterns of one shape in order" $+    -- For (x0, x1) against (x1, x0), the right binders are renamed to the+    -- left ones by position, so x1 goes to x0 and x0 to x1.+    withThreeBinders (\x y _z ->+      Foil.withRefreshed Foil.emptyScope (Foil.nameOf y) (\x' ->+        Foil.withRefreshed (Foil.extendScope x' Foil.emptyScope) (Foil.nameOf x) (\y' ->+          case Foil.unifyPatterns+                 (DemoPair (DemoVar x) (DemoVar y))+                 (DemoPair (DemoVar x') (DemoVar y')) of+            Foil.RenameRightNameBinder _ rename ->+              map (Foil.nameId . Foil.fromNameBinderRenaming rename)+                  [Foil.sink (Foil.nameOf x'), Foil.nameOf y']+            _ -> [])))+      `shouldBe` [0, 1]++-- | What 'Foil.unsafeUnifyPatternBinders' does not tell apart.+binderSpec :: Spec+binderSpec = describe "unsafeUnifyPatternBinders" $ do   it "ignores the constructor, so different constructors with equal binders unify" $-    -- The consequence worth knowing: for a pattern type whose constructors mean-    -- different things -- the branches of a @match@, say -- the default calls two-    -- of them equal, and no type error says so.+    -- For a pattern type whose constructors mean different things (the+    -- branches of a @match@, say), this calls two of them equal.     Foil.withFresh Foil.emptyScope (\x ->-      unifiesWithoutRenaming (DemoVar x) (DemoBox x))+      unifiesWithoutRenaming (BinderVar x) (BinderBox x))       `shouldBe` True    it "ignores non-binding fields, whatever their values" $     Foil.withFresh Foil.emptyScope (\x ->-      unifiesWithoutRenaming (DemoLabel "left" x) (DemoLabel "right" x))+      unifiesWithoutRenaming (BinderLabel "left" x) (BinderLabel "right" x))       `shouldBe` True    it "ignores nesting, so (x, (y, z)) unifies with ((x, y), z)" $     -- Both flatten to the same three binders in the same order.     withThreeBinders (\x y z ->       unifiesWithoutRenaming-        (DemoPair (DemoVar x) (DemoPair (DemoVar y) (DemoVar z)))-        (DemoPair (DemoPair (DemoVar x) (DemoVar y)) (DemoVar z)))+        (BinderPair (BinderVar x) (BinderPair (BinderVar y) (BinderVar z)))+        (BinderPair (BinderPair (BinderVar x) (BinderVar y)) (BinderVar z)))       `shouldBe` True    it "still tells apart patterns binding different numbers of names" $-    -- The default is not vacuous: the binders themselves are compared. This case-    -- used to throw 'PatternMatchFail', because the 'NameBinderList' instance had-    -- no case for lists of unequal length and this module disables-    -- @-Wincomplete-patterns@.+    -- The binders themselves are compared. This is a regression test for a+    -- missing case of the 'NameBinderList' instance.     withThreeBinders (\x y _z ->       unifiesWithoutRenaming-        (DemoVar x)-        (DemoPair (DemoVar x) (DemoVar y)))+        (BinderVar x)+        (BinderPair (BinderVar x) (BinderVar y)))       `shouldBe` False

@@ -0,0 +1,32 @@+{-# LANGUAGE DataKinds       #-}+{-# LANGUAGE GADTs           #-}+{-# LANGUAGE LambdaCase      #-}+{-# LANGUAGE RankNTypes      #-}+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -Wno-orphans #-}+-- | The untyped λ-calculus of "Control.Monad.Free.Foil.Example", made ready+-- for the law tests: the instances its signature lacks, and its+-- 'SyntaxGen'.+module Control.Monad.Free.Foil.ExampleSyntax (exprSyntax) where++import           Data.Bifunctor.TH               (deriveBifoldable, deriveBitraversable)++import           Control.Monad.Foil.Laws         (GenPattern, PatternNames)+import           Control.Monad.Free.Foil.Example (ExprF (..))+import           Control.Monad.Free.Foil.Laws    (SyntaxGen (..))+import           Data.ZipMatchK.TH               (deriveZipMatchK)++deriveBifoldable ''ExprF+deriveBitraversable ''ExprF+deriveZipMatchK ''ExprF++-- | The λ-calculus, with a given kind of pattern.+exprSyntax :: GenPattern binder -> PatternNames binder -> SyntaxGen binder ExprF+exprSyntax genPat names = SyntaxGen+  { sgShapes = [AppF () (), LamF ()]+  , sgPattern = genPat+  , sgPatternNames = names+  , sgShowNode = \case+      AppF f x  -> "(" <> f <> " " <> x <> ")"+      LamF body -> body+  }

@@ -0,0 +1,29 @@+-- | The laws of the relative monad @'AST' binder sig@ and of renaming of+-- terms, for the untyped λ-calculus of "Control.Monad.Free.Foil.Example",+-- with single binders and with lists of binders as patterns.+--+-- See "Control.Monad.Free.Foil.Laws" for the statements.+module Control.Monad.Free.Foil.LawsSpec (spec) where++import           Test.Hspec++import           Control.Monad.Foil.Laws+import           Control.Monad.Free.Foil.ExampleSyntax (exprSyntax)+import           Control.Monad.Free.Foil.Laws++spec :: Spec+spec = do+  describe "λ-calculus with NameBinder (Control.Monad.Free.Foil.Example)" $ do+    let sg = exprSyntax genNameBinder nameBinderNames+    describe "α-equivalence" $ alphaSpec sg (const Holds)+    describe "relative monad" $ relMonadSpec sg (\_ _ -> Holds)+    describe "functor" $ functorSpec sg (\_ _ -> Holds) functorVerdict+  describe "λ-calculus with NameBinderList" $ do+    let sg = exprSyntax genNameBinderList nameBinderListNames+    describe "α-equivalence" $ alphaSpec sg (const Holds)+    describe "relative monad" $ relMonadSpec sg (\_ _ -> Holds)+    describe "functor" $ functorSpec sg (\_ _ -> Holds) functorVerdict+  where+    -- 'liftRM' is lawful; 'sinkabilityProof' agrees with it on inclusions.+    functorVerdict cls SinkAgreesWithLiftRM = sinkAgreesOnInclusions cls+    functorVerdict _   _                    = Holds

@@ -0,0 +1,38 @@+{-# LANGUAGE LambdaCase      #-}+{-# LANGUAGE TemplateHaskell #-}++-- | How a type is declared, read back with 'reify', for the tests of the pattern+-- types that 'Control.Monad.Free.Foil.TH.MkFreeFoil.mkFreeFoil' generates.+module Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Declaration (declarationOf) where++import           Language.Haskell.TH+import           Language.Haskell.TH.Syntax (lift)++-- | A splice for the declaration of a type: @"newtype"@ or @"data"@, and the+-- source strictness of every field of every constructor, as+-- @"{-# UNPACK #-} !"@, @"!"@ or @""@.+declarationOf :: Name -> Q Exp+declarationOf name = reify name >>= \case+  TyConI (NewtypeD _ _ _ _ con _) -> lift ("newtype", fieldsOf con)+  TyConI (DataD _ _ _ _ cons _)   -> lift ("data", concatMap fieldsOf cons)+  _ -> fail ("declarationOf: " <> show name <> " is not a data type or a newtype")+  where+    fieldsOf :: Con -> [(String, [String])]+    fieldsOf = \case+      ForallC _ _ con        -> fieldsOf con+      NormalC con bts        -> [(nameBase con, map (bangOf . fst) bts)]+      RecC con vbts          -> [(nameBase con, [ bangOf b | (_, b, _) <- vbts ])]+      InfixC l con r         -> [(nameBase con, map (bangOf . fst) [l, r])]+      GadtC cons bts _       -> [ (nameBase con, map (bangOf . fst) bts) | con <- cons ]+      RecGadtC cons vbts _   -> [ (nameBase con, [ bangOf b | (_, b, _) <- vbts ]) | con <- cons ]++    bangOf (Bang unpackedness strictness) =+      unwords (filter (not . null) [unpackednessOf unpackedness, strictnessOf strictness])+    unpackednessOf = \case+      SourceUnpack   -> "{-# UNPACK #-}"+      SourceNoUnpack -> "{-# NOUNPACK #-}"+      NoSourceUnpackedness -> ""+    strictnessOf = \case+      SourceStrict -> "!"+      SourceLazy   -> "~"+      NoSourceStrictness -> ""

@@ -0,0 +1,139 @@+{-# LANGUAGE TemplateHaskell #-}++-- | Raw syntaxes whose pattern types are not a single binder, used to test the+-- pattern types that 'mkFreeFoil' generates (see+-- "Control.Monad.Free.Foil.TH.PatternTypesSpec"):+--+-- * @MPattern@ has several constructors (a wildcard, a variable and a pair),+--   so its scope-safe version is @data@;+-- * @APattern@ has one constructor with two fields (an annotation and a+--   variable, the shape BNFC produces), so its scope-safe version is @data@ too;+-- * @NPattern@ has one constructor whose one field is a nested pattern, so its+--   scope-safe version is a @newtype@.+--+-- The single-binder case is "Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config".+module Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsConfig where++import           Control.Monad.Free.Foil.TH.MkFreeFoil+import           Language.Haskell.TH                   (Name)++newtype MVarIdent = MVarIdent String+  deriving (Eq, Ord, Show)++data MPattern+  = MPatternWild+  | MPatternVar MVarIdent+  | MPatternPair MPattern MPattern+  deriving (Eq, Show)++newtype MScopedTerm = MScopedTerm MTerm+  deriving (Eq, Show)++data MTerm+  = MVar MVarIdent+  | MApp MTerm MTerm+  | MFun MPattern MScopedTerm+  deriving (Eq, Show)++newtype AVarIdent = AVarIdent String+  deriving (Eq, Ord, Show)++data APattern = APatternVar Int AVarIdent+  deriving (Eq, Show)++newtype AScopedTerm = AScopedTerm ATerm+  deriving (Eq, Show)++data ATerm+  = AVar AVarIdent+  | AFun APattern AScopedTerm+  deriving (Eq, Show)++newtype NVarIdent = NVarIdent String+  deriving (Eq, Ord, Show)++newtype NPattern = NPatternWrap MPattern+  deriving (Eq, Show)++newtype NScopedTerm = NScopedTerm NTerm+  deriving (Eq, Show)++data NTerm+  = NVar NVarIdent+  | NFun NPattern NScopedTerm+  deriving (Eq, Show)++intToMVarIdent :: Int -> MVarIdent+intToMVarIdent i = MVarIdent ("x" <> show i)++intToAVarIdent :: Int -> AVarIdent+intToAVarIdent i = AVarIdent ("x" <> show i)++intToNVarIdent :: Int -> NVarIdent+intToNVarIdent i = NVarIdent ("x" <> show i)++-- The conversions call these by name, so they are functions rather than+-- constructors.+mVar :: MVarIdent -> MTerm+mVar = MVar++aVar :: AVarIdent -> ATerm+aVar = AVar++nVar :: NVarIdent -> NTerm+nVar = NVar++mTermToScope :: MTerm -> MScopedTerm+mTermToScope = MScopedTerm++aTermToScope :: ATerm -> AScopedTerm+aTermToScope = AScopedTerm++nTermToScope :: NTerm -> NScopedTerm+nTermToScope = NScopedTerm++mScopeToTerm :: MScopedTerm -> MTerm+mScopeToTerm (MScopedTerm t) = t++aScopeToTerm :: AScopedTerm -> ATerm+aScopeToTerm (AScopedTerm t) = t++nScopeToTerm :: NScopedTerm -> NTerm+nScopeToTerm (NScopedTerm t) = t++termConfig :: Name -> Name -> Name -> Name -> Name -> Name -> Name -> Name -> Name -> FreeFoilTermConfig+termConfig ident term binding scope varCon var intToIdent termToScope scopeToTerm = FreeFoilTermConfig+  { rawIdentName = ident+  , rawTermName = term+  , rawBindingName = binding+  , rawScopeName = scope+  , rawVarConName = varCon+  , rawSubTermNames = []+  , rawSubScopeNames = []+  , intToRawIdentName = intToIdent+  , rawVarIdentToTermName = var+  , rawTermToScopeName = termToScope+  , rawScopeToTermName = scopeToTerm+  }++-- | The config for the conversions: all languages but the one of @NPattern@,+-- since the conversions do not support a pattern that nests the pattern of+-- another language.+conversionsConfig :: FreeFoilConfig+conversionsConfig = patternsConfig { freeFoilTermConfigs = take 2 (freeFoilTermConfigs patternsConfig) }++patternsConfig :: FreeFoilConfig+patternsConfig = FreeFoilConfig+  { rawQuantifiedNames = []+  , freeFoilTermConfigs =+      [ termConfig ''MVarIdent ''MTerm ''MPattern ''MScopedTerm 'MVar 'mVar 'intToMVarIdent 'mTermToScope 'mScopeToTerm+      , termConfig ''AVarIdent ''ATerm ''APattern ''AScopedTerm 'AVar 'aVar 'intToAVarIdent 'aTermToScope 'aScopeToTerm+      , termConfig ''NVarIdent ''NTerm ''NPattern ''NScopedTerm 'NVar 'nVar 'intToNVarIdent 'nTermToScope 'nScopeToTerm+      ]+  , freeFoilNameModifier = ("FF" ++)+  , freeFoilScopeNameModifier = ("FFScoped" ++)+  , freeFoilConNameModifier = ("FF" ++)+  , freeFoilConvertFromName = ("from" ++)+  , freeFoilConvertToName = ("to" ++)+  , signatureNameModifier = (++ "Sig")+  }

@@ -0,0 +1,64 @@+{-# LANGUAGE DataKinds         #-}+{-# LANGUAGE DeriveGeneric     #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleContexts  #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs             #-}+{-# LANGUAGE KindSignatures    #-}+{-# LANGUAGE LambdaCase        #-}+{-# LANGUAGE PatternSynonyms   #-}+{-# LANGUAGE RankNTypes        #-}+{-# LANGUAGE TemplateHaskell   #-}+{-# LANGUAGE TypeFamilies      #-}+{-# OPTIONS_GHC -Wno-missing-signatures -Wno-redundant-constraints -Wno-orphans #-}++-- | The scope-safe syntax generated from+-- "Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsConfig". The pattern+-- instances other than 'Foil.CoSinkable' take their "Generics.Kind" defaults.+module Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsSyntax where++import qualified Control.Monad.Foil                                       as Foil+import           Control.Monad.Free.Foil.Binary                          ()+import           Control.Monad.Free.Foil.Binary.TH                       (deriveBinaryPattern)+import           Control.Monad.Free.Foil.TH.MkFreeFoil+import           Data.Bifunctor.TH+import           Data.ZipMatchK+import           Generics.Kind.TH                                         (deriveGenericK)++import           Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsConfig++mkFreeFoil patternsConfig++deriveGenericK ''FFMPattern+instance Foil.SinkableK FFMPattern+instance Foil.HasNameBinders FFMPattern+instance Foil.UnifiablePattern FFMPattern+deriveBinaryPattern ''FFMPattern++deriveGenericK ''FFAPattern+instance Foil.SinkableK FFAPattern+instance Foil.HasNameBinders FFAPattern+instance Foil.UnifiablePattern FFAPattern+deriveBinaryPattern ''FFAPattern++deriveGenericK ''FFNPattern+instance Foil.SinkableK FFNPattern+instance Foil.HasNameBinders FFNPattern+instance Foil.UnifiablePattern FFNPattern+deriveBinaryPattern ''FFNPattern++deriveBifunctor ''MTermSig+deriveBifoldable ''MTermSig+deriveBitraversable ''MTermSig+deriveGenericK ''MTermSig+instance ZipMatchK MTermSig++deriveBifunctor ''ATermSig+deriveBifoldable ''ATermSig+deriveBitraversable ''ATermSig++deriveBifunctor ''NTermSig+deriveBifoldable ''NTermSig+deriveBitraversable ''NTermSig++mkFreeFoilConversions conversionsConfig

@@ -26,6 +26,8 @@ module Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax where  import qualified Control.Monad.Foil                              as Foil+import           Control.Monad.Free.Foil.Binary          ()+import           Control.Monad.Free.Foil.Binary.TH       (deriveBinaryPattern) import           Control.Monad.Free.Foil.TH.MkFreeFoil import           Data.Bifunctor.TH import           Data.ZipMatchK@@ -40,6 +42,7 @@ instance Foil.HasNameBinders FFPattern -- Foil.CoSinkable FFPattern is generated by mkFreeFoil. instance Foil.UnifiablePattern FFPattern+deriveBinaryPattern ''FFPattern  deriveBifunctor ''TermSig deriveBifoldable ''TermSig

@@ -0,0 +1,237 @@+{-# LANGUAGE DataKinds        #-}+{-# LANGUAGE GADTs            #-}+{-# LANGUAGE LambdaCase       #-}+{-# LANGUAGE PatternSynonyms  #-}+{-# LANGUAGE RankNTypes       #-}+{-# LANGUAGE TemplateHaskell  #-}++-- | The pattern types that 'Control.Monad.Free.Foil.TH.MkFreeFoil.mkFreeFoil'+-- generates: a @newtype@ for a pattern of one constructor with one binding+-- field, and @data@ otherwise. The instances+-- that are not generated take their "Generics.Kind" defaults, which must work+-- for both.+module Control.Monad.Free.Foil.TH.PatternTypesSpec (spec) where++import           Control.Exception                                        (evaluate)+import qualified Control.Monad.Foil                                       as Foil+import           Control.Monad.Foil.Laws+import qualified Control.Monad.Free.Foil                                  as FreeFoil+import           Data.Binary                                              (decode, encode)+import           Data.Coerce                                              (coerce)+import qualified Data.Map                                                 as Map+import           Test.Hspec+import           Test.QuickCheck                                          (Gen, arbitrary, frequency)++import           Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config+import           Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Declaration+import           Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsConfig+import           Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsSyntax+import           Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax++spec :: Spec+spec = do+  describe "a pattern of one constructor with one binder (FFPattern)" $ do+    it "is a newtype" $+      $(declarationOf ''FFPattern) `shouldBe` ("newtype", [("FFPatternVar", [""])])+    it "is coercible to its binder" $+      Foil.withFresh Foil.emptyScope $ \binder ->+        case coerce binder of+          FFPatternVar binder' -> Foil.nameOf binder' `shouldBe` Foil.nameOf binder+    it "is as strict as its binder" $+      evaluate (FFPatternVar undefined) `shouldThrow` anyErrorCall+    describe "CoSinkable (generated)" $+      coSinkableSpec namesOfP genP extensionByCoercion+    describe "UnifiablePattern (GenericK default)" $+      unifyPatternsSpec namesOfP genPPair Holds+    it "gives its binder to getNameBinders (HasNameBinders, GenericK default)" $+      Foil.withFresh Foil.emptyScope $ \binder ->+        namesOfNameBinderList (Foil.nameBindersList (Foil.getNameBinders (FFPatternVar binder)))+          `shouldBe` [Foil.nameId (Foil.nameOf binder)]+    it "round-trips through Binary (deriveBinaryPattern)" $+      Foil.withFresh Foil.emptyScope $ \binder ->+        namesOfP (decode (encode (FFPatternVar binder)) :: FFPattern Foil.VoidS Foil.VoidS)+          `shouldBe` namesOfP (FFPatternVar binder)+    describe "α-equivalence (needs SinkableK and UnifiablePattern)" $ do+      it "identifies λx. x and λy. y" $+        alphaEquivTerms (fun x (Var x)) (fun y (Var y)) `shouldBe` True+      it "tells λx. λy. x from λx. λy. y" $+        alphaEquivTerms (fun x (fun y (Var x))) (fun x (fun y (Var y))) `shouldBe` False++  describe "a pattern of one constructor with one nested pattern (FFNPattern)" $ do+    it "is a newtype" $+      $(declarationOf ''FFNPattern) `shouldBe` ("newtype", [("FFNPatternWrap", [""])])+    describe "CoSinkable (generated)" $+      coSinkableSpec (namesOfM . unwrapN) genN extensionByCoercion+    describe "UnifiablePattern (GenericK default)" $+      unifyPatternsSpec (namesOfM . unwrapN) genNPair Holds+    it "round-trips through Binary (deriveBinaryPattern)" $+      withPair $ \pat ->+        namesOfM (unwrapN (decode (encode (FFNPatternWrap pat)) :: FFNPattern Foil.VoidS Foil.VoidS))+          `shouldBe` namesOfM pat++  describe "a pattern of several constructors (FFMPattern)" $ do+    it "is data" $+      $(declarationOf ''FFMPattern) `shouldBe`+        ("data",+          [ ("FFMPatternWild", [])+          , ("FFMPatternVar", [""])+          , ("FFMPatternPair", ["", ""]) ])+    describe "CoSinkable (generated)" $+      coSinkableSpec namesOfM genM extensionByCoercion+    describe "UnifiablePattern (GenericK default)" $+      unifyPatternsSpec namesOfM genMPair Holds+    it "round-trips through Binary (deriveBinaryPattern)" $+      withPair $ \pat ->+        namesOfM (decode (encode pat) :: FFMPattern Foil.VoidS Foil.VoidS)+          `shouldBe` namesOfM pat+    describe "α-equivalence (needs SinkableK and UnifiablePattern)" $ do+      let pair a b = MPatternPair (MPatternVar a) (MPatternVar b)+          funM p body = MFun p (MScopedTerm body)+      it "identifies λ(x, y). x and λ(y, x). y" $+        alphaEquivMTerms (funM (pair mx my) (MVar mx)) (funM (pair my mx) (MVar my)) `shouldBe` True+      it "tells λ(x, y). x from λ(x, y). y" $+        alphaEquivMTerms (funM (pair mx my) (MVar mx)) (funM (pair mx my) (MVar my)) `shouldBe` False+      it "tells λ(x, _). x from λ(_, x). x" $+        alphaEquivMTerms+          (funM (MPatternPair (MPatternVar mx) MPatternWild) (MVar mx))+          (funM (MPatternPair MPatternWild (MPatternVar mx)) (MVar mx))+          `shouldBe` False++  describe "a pattern of one constructor with a binder and an annotation (FFAPattern)" $ do+    it "is data" $+      $(declarationOf ''FFAPattern) `shouldBe` ("data", [("FFAPatternVar", ["", ""])])+    describe "CoSinkable (generated)" $+      coSinkableSpec namesOfA genA extensionByCoercion+    describe "UnifiablePattern (GenericK default)" $+      unifyPatternsSpec namesOfA genAPair Holds+    it "round-trips through Binary (deriveBinaryPattern)" $+      Foil.withFresh Foil.emptyScope $ \binder ->+        case decode (encode (FFAPatternVar 7 binder)) :: FFAPattern Foil.VoidS Foil.VoidS of+          FFAPatternVar annotation binder' -> do+            annotation `shouldBe` 7+            Foil.nameId (Foil.nameOf binder') `shouldBe` Foil.nameId (Foil.nameOf binder)+    it "round-trips through the conversions" $ do+      let term = AFun (APatternVar 7 ax) (AScopedTerm (AVar ax))+      case roundtripA term of+        AFun (APatternVar 7 binder) (AScopedTerm (AVar v)) -> v `shouldBe` binder+        other -> expectationFailure ("unexpected shape: " <> show other)+  where+    x = VarIdent "x"+    y = VarIdent "y"+    fun v body = Fun (PatternVar v) (ScopedTerm body)+    mx = MVarIdent "x"+    my = MVarIdent "y"+    ax = AVarIdent "x"++-- * Single binders++namesOfP :: PatternNames FFPattern+namesOfP (FFPatternVar binder) = [Foil.nameId (Foil.nameOf binder)]++genP :: GenPattern FFPattern+genP ctx = do+  PatIn binder <- genNameBinder ctx+  pure (PatIn (FFPatternVar binder))++genPPair :: GenPatternPair FFPattern+genPPair ctx = do+  PatIn l <- genP ctx+  PatIn r <- genP ctx+  pure (PatPair l r)++alphaEquivTerms :: Term -> Term -> Bool+alphaEquivTerms l r =+  FreeFoil.alphaEquiv Foil.emptyScope+    (toTerm Foil.emptyScope Map.empty l)+    (toTerm Foil.emptyScope Map.empty r)++namesOfNameBinderList :: Foil.NameBinderList n l -> [Int]+namesOfNameBinderList = \case+  Foil.NameBinderListEmpty       -> []+  Foil.NameBinderListCons b rest -> Foil.nameId (Foil.nameOf b) : namesOfNameBinderList rest++-- * Several constructors++namesOfM :: PatternNames FFMPattern+namesOfM = \case+  FFMPatternWild     -> []+  FFMPatternVar b    -> [Foil.nameId (Foil.nameOf b)]+  FFMPatternPair l r -> namesOfM l ++ namesOfM r++-- | Run a test on @(x, _)@ with a fresh @x@.+withPair :: (forall l. FFMPattern Foil.VoidS l -> r) -> r+withPair k = Foil.withFresh Foil.emptyScope $ \binder ->+  k (FFMPatternPair (FFMPatternVar binder) FFMPatternWild)++-- | The shape of a pattern: where the wildcards, variables and pairs are. This+-- follows the generators of @lambda-pi@'s @LawsSyntax@.+data Shape = Wildcard | Variable | Pair Shape Shape++-- | A shape of nesting depth at most @d@.+genShape :: Int -> Gen Shape+genShape d = frequency $+  [ (1, pure Wildcard), (3, pure Variable) ] +++  [ (2, Pair <$> genShape (d - 1) <*> genShape (d - 1)) | d > 0 ]++-- | A pattern of the given shape, with hinted names.+instantiate :: Foil.Distinct n => Shape -> Foil.Scope n -> Gen (PatIn FFMPattern n)+instantiate shape scope = case shape of+  Wildcard -> pure (PatIn FFMPatternWild)+  Variable -> withHintedBinder scope (pure . PatIn . FFMPatternVar)+  Pair left right -> do+    PatIn l <- instantiate left scope+    PatIn r <- instantiate right (Foil.extendScopePattern l scope)+    pure (PatIn (FFMPatternPair l r))++genM :: GenPattern FFMPattern+genM ctx = withCtx ctx $ \scope -> do+  shape <- genShape 2+  instantiate shape scope++genMPair :: GenPatternPair FFMPattern+genMPair ctx = withCtx ctx $ \scope -> do+  shape <- genShape 2+  PatIn l <- instantiate shape scope+  PatIn r <- instantiate shape scope+  pure (PatPair l r)++alphaEquivMTerms :: MTerm -> MTerm -> Bool+alphaEquivMTerms l r =+  FreeFoil.alphaEquiv Foil.emptyScope+    (toMTerm Foil.emptyScope Map.empty l)+    (toMTerm Foil.emptyScope Map.empty r)++-- * A nested pattern++unwrapN :: FFNPattern n l -> FFMPattern n l+unwrapN (FFNPatternWrap p) = p++genN :: GenPattern FFNPattern+genN ctx = do+  PatIn p <- genM ctx+  pure (PatIn (FFNPatternWrap p))++genNPair :: GenPatternPair FFNPattern+genNPair ctx = do+  PatPair l r <- genMPair ctx+  pure (PatPair (FFNPatternWrap l) (FFNPatternWrap r))++-- * A binder with an annotation++namesOfA :: PatternNames FFAPattern+namesOfA (FFAPatternVar _ binder) = [Foil.nameId (Foil.nameOf binder)]++genA :: GenPattern FFAPattern+genA ctx = do+  annotation <- arbitrary+  PatIn binder <- genNameBinder ctx+  pure (PatIn (FFAPatternVar annotation binder))++genAPair :: GenPatternPair FFAPattern+genAPair ctx = do+  PatIn l <- genA ctx+  PatIn r <- genA ctx+  pure (PatPair l r)++roundtripA :: ATerm -> ATerm+roundtripA = fromATerm . toATerm Foil.emptyScope Map.empty

@@ -0,0 +1,651 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE KindSignatures      #-}+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- | Generators and laws for the foil: scopes, renamings between them, and+-- the laws of 'Sinkable', 'CoSinkable' and 'UnifiablePattern'.+--+-- 'Sinkable' @e@ is read as a functor from scopes to sets, with+-- 'sinkabilityProof' its action on renamings. 'coSinkabilityProof' lifts a+-- renaming of the outer scope of a pattern to its inner scope,+-- functorially. Both methods are typing witnesses for 'sink' (Maclaurin,+-- Radul and Paszke, "The Foil", §3.3 and §3.5), and the instances for+-- binders extend a renaming by a coercion, which is right on inclusions+-- only. So renamings come in three classes (inclusions, injections and+-- arbitrary functions), and a law that holds on inclusions only is pinned+-- as failing by design on the other two.+--+-- The generators are scope-safe by construction. Scopes grow from the empty+-- scope through 'withRefreshed', and a binder shadows a name of the scope+-- only after 'sink', as in real code. The unsafe ingredients are+-- 'UnsafeName' for the hint given to 'withRefreshed' and, in the law of+-- 'unifyPatterns', 'UnsafeNameBinder' to read the renaming of a verdict.+module Control.Monad.Foil.Laws (+  -- * Scopes+  Ctx (..),+  SomeCtx (..),+  ctxScope,+  withCtx,+  ctxChain,+  ctxNames,+  extendCtx,+  genHint,+  withHintedBinder,+  withHintedBinders,+  extendCtxBy,+  genCtx,+  genCtxAtLeast,+  showCtx,+  showName,+  -- * Patterns+  PatIn (..),+  GenPattern,+  genNameBinder,+  genNameBinderList,+  PatternNames,+  nameBinderNames,+  nameBinderListNames,+  patternRawNames,+  showPattern,+  showPatternWith,+  -- * Renamings+  Renaming (..),+  rename,+  identityRenaming,+  inclusionRenaming,+  composeRenaming,+  genFunction,+  genInjection,+  RenamingClass (..),+  allRenamingClasses,+  Includes (..),+  Chain' (..),+  Chain (..),+  genChain,+  showChain,+  -- * Laws of 'Sinkable'+  SinkableLaws (..),+  sinkableLaws,+  SinkLaw (..),+  SinkCase (..),+  genSinkCase,+  sinkableSpec,+  -- * Laws of 'CoSinkable'+  PatternCase (..),+  genPatternCase,+  CoSinkableLaws (..),+  coSinkableLaws,+  CoSinkLaw (..),+  coSinkableSpec,+  -- * Laws of 'UnifiablePattern'+  PatPair (..),+  GenPatternPair,+  genNameBinderListPair,+  unifyPatternsLaw,+  unifyPatternsSpec,+  -- * Running laws+  Verdict (..),+  law,+  extensionByCoercion,+) where++import           Control.Monad               (forM_)+import           Data.IntMap                 (IntMap)+import           Data.Kind                   (Type)+import qualified Data.IntMap                 as IntMap+import           Data.List                   (intercalate)+import           Test.Hspec+import           Test.Hspec.QuickCheck       (modifyMaxSuccess)+import           Test.QuickCheck++import           Control.Monad.Foil+import           Control.Monad.Foil.Internal (Name (..), NameBinder (..))++-- * Scopes++-- | A scope together with the way it was reached from the empty scope.+-- Every step is a 'DExt', so a value built at any step can be 'sink'ed to+-- the end, and the chain of binders lets us build maps out of the scope+-- ('NameMap', 'Substitution').+data Ctx (n :: S) where+  Root  :: Ctx VoidS+  Under :: DExt m n => Ctx m -> NameBinderList m n -> Scope n -> Ctx n++-- | A context at an unknown scope.+data SomeCtx where+  SomeCtx :: Ctx n -> SomeCtx++-- | The scope a context ends at.+ctxScope :: Ctx n -> Scope n+ctxScope Root              = emptyScope+ctxScope (Under _ _ scope) = scope++-- | Every scope reached by a context is distinct.+withCtx :: Ctx n -> (Distinct n => Scope n -> r) -> r+withCtx Root k              = k emptyScope+withCtx (Under _ _ scope) k = k scope++-- | All binders from the empty scope to the end of the context.+ctxChain :: Ctx n -> NameBinderList VoidS n+ctxChain Root                  = NameBinderListEmpty+ctxChain (Under parent step _) = concatNameBinderLists (ctxChain parent) step++-- | The names of the scope, in the order in which they were bound.+ctxNames :: Ctx n -> [Name n]+ctxNames ctx = namesOfPattern (ctxChain ctx)++-- | Extend a context by a pattern.+extendCtx :: (CoSinkable p, DExt n l) => Ctx n -> p n l -> Ctx l+extendCtx ctx pat = withCtx ctx $ \scope ->+  Under ctx (nameBinderListOf pat) (extendScopePattern pat scope)++-- | A hint for 'withRefreshed'. The range is small, so hints often clash+-- with the scope and the binder falls back to a fresh name, and scopes are+-- not contiguous ranges of raw names.+genHint :: Gen Int+genHint = chooseInt (0, 15)++-- | Bind a name: the hint if it is free in the scope, and a fresh name+-- otherwise.+withHintedBinder+  :: Distinct n+  => Scope n+  -> (forall l. DExt n l => NameBinder n l -> Gen r)+  -> Gen r+withHintedBinder scope cont = do+  hint <- genHint+  withRefreshed scope (UnsafeName hint) cont++-- | Bind @k@ names, each one the hint if it is free in the scope and a+-- fresh name otherwise.+withHintedBinders+  :: Distinct n+  => Int -> Scope n+  -> (forall l. DExt n l => NameBinderList n l -> Gen r)+  -> Gen r+withHintedBinders k scope cont+  | k <= 0 = cont NameBinderListEmpty+  | otherwise =+      withHintedBinder scope $ \binder ->+        withHintedBinders (k - 1) (extendScope binder scope) $ \binders ->+          cont (NameBinderListCons binder binders)++-- | Extend a context by @k@ steps of one or two binders each.+extendCtxBy :: Int -> Ctx n -> (forall l. Ctx l -> Gen r) -> Gen r+extendCtxBy k ctx cont+  | k <= 0 = cont ctx+  | otherwise = withCtx ctx $ \scope -> do+      width <- chooseInt (1, 2)+      withHintedBinders width scope $ \binders ->+        extendCtxBy (k - 1) (extendCtx ctx binders) cont++-- | A context of up to four steps (up to eight names).+genCtx :: Gen SomeCtx+genCtx = do+  steps <- chooseInt (0, 4)+  extendCtxBy steps Root (pure . SomeCtx)++-- | A context with at least @k@ names, so that a renaming into it of the+-- required kind exists.+genCtxAtLeast :: Int -> Gen SomeCtx+genCtxAtLeast k = do+  SomeCtx ctx <- genCtx+  grow ctx+  where+    grow :: Ctx n -> Gen SomeCtx+    grow ctx+      | length (ctxNames ctx) >= k = pure (SomeCtx ctx)+      | otherwise = extendCtxBy 1 ctx grow++-- | Show the names of a scope.+showCtx :: Ctx n -> String+showCtx ctx = "{" <> intercalate ", " (map showName (ctxNames ctx)) <> "}"++-- | Show a name by its raw identifier.+showName :: Name n -> String+showName x = "x" <> show (nameId x)++-- * Patterns++-- | A pattern out of scope @n@, binding names fresh for @n@.+data PatIn p n where+  PatIn :: DExt n l => p n l -> PatIn p n++-- | A generator of patterns out of a given scope.+type GenPattern p = forall n. Ctx n -> Gen (PatIn p n)++-- | A single binder with a hinted name.+genNameBinder :: GenPattern NameBinder+genNameBinder ctx = withCtx ctx $ \scope -> withHintedBinder scope (pure . PatIn)++-- | Up to three binders with hinted names.+genNameBinderList :: GenPattern NameBinderList+genNameBinderList ctx = withCtx ctx $ \scope -> do+  k <- chooseInt (0, 3)+  withHintedBinders k scope (pure . PatIn)++-- | The raw names a pattern binds, in the order of its structure (left to+-- right). Each pattern type gives its own, since the library's traversal+-- ('patternRawNames') does not follow the structure for every type.+type PatternNames (p :: S -> S -> Type) = forall n l. p n l -> [Int]++-- | The name of a single binder.+nameBinderNames :: PatternNames NameBinder+nameBinderNames b = [nameId (nameOf b)]++-- | The names of a list of binders, in order.+nameBinderListNames :: PatternNames NameBinderList+nameBinderListNames = \case+  NameBinderListEmpty         -> []+  NameBinderListCons b rest -> nameId (nameOf b) : nameBinderListNames rest++-- | The raw names a pattern binds, in the order in which 'withPattern'+-- visits them (through 'nameBinderListOf').+patternRawNames :: CoSinkable p => p n l -> [Int]+patternRawNames = nameBinderListNames . nameBinderListOf++-- | Show the names a pattern binds, in the library's order.+showPattern :: CoSinkable p => p n l -> String+showPattern = showPatternWith patternRawNames++-- | Show the names a pattern binds, in a given order.+showPatternWith :: PatternNames p -> p n l -> String+showPatternWith names pat = "[" <> unwords (map (("x" <>) . show) (names pat)) <> "]"++-- * Renamings++-- | A renaming of scope @n@ into scope @l@, as a finite table so that it+-- can be shown and composed. It is total on the names of the scope it was+-- generated for.+newtype Renaming (n :: S) (l :: S) = Renaming (IntMap (Name l))++instance Show (Renaming n l) where+  show (Renaming table) = "{" <> intercalate ", "+    [ "x" <> show x <> " ↦ " <> showName y | (x, y) <- IntMap.toList table ] <> "}"++-- | Apply a renaming.+rename :: Renaming n l -> Name n -> Name l+rename (Renaming table) x = case IntMap.lookup (nameId x) table of+  Just y  -> y+  Nothing -> error ("the renaming is not defined at " <> showName x)++-- | The identity renaming of a scope.+identityRenaming :: Ctx n -> Renaming n n+identityRenaming ctx = Renaming (IntMap.fromList [ (nameId x, x) | x <- ctxNames ctx ])++-- | The inclusion of a scope into an extension of it, i.e. 'sink'.+inclusionRenaming :: DExt n l => Ctx n -> Renaming n l+inclusionRenaming ctx = Renaming (IntMap.fromList [ (nameId x, sink x) | x <- ctxNames ctx ])++-- | Composition in diagrammatic order: first @f@, then @g@.+composeRenaming :: Renaming n l -> Renaming l k -> Renaming n k+composeRenaming (Renaming f) g = Renaming (fmap (rename g) f)++-- | An arbitrary renaming. The target must have a name if the source has.+genFunction :: Ctx n -> Ctx l -> Gen (Renaming n l)+genFunction from to = do+  let targets = ctxNames to+  pairs <- mapM (\x -> (,) (nameId x) <$> elements targets) (ctxNames from)+  pure (Renaming (IntMap.fromList pairs))++-- | An injective renaming. The target must have at least as many names as+-- the source.+genInjection :: Ctx n -> Ctx l -> Gen (Renaming n l)+genInjection from to = do+  targets <- shuffle (ctxNames to)+  pure (Renaming (IntMap.fromList (zip (map nameId (ctxNames from)) targets)))++-- | The three classes of renamings over which a law is checked, each+-- contained in the next.+data RenamingClass+  = Inclusions  -- ^ Thinnings: the identity on raw names, as 'sink' does.+  | Injections  -- ^ Injective renamings (the category \(\mathbb{I}\)).+  | Functions   -- ^ All renamings (the category \(\mathbb{F}\)).+  deriving (Eq, Show, Enum, Bounded)++-- | All classes, smallest first.+allRenamingClasses :: [RenamingClass]+allRenamingClasses = [minBound .. maxBound]++-- | Evidence that the second scope extends the first.+data Includes (n :: S) (l :: S) where+  Includes :: DExt n l => Includes n l++-- | Three scopes and two composable renamings between them, of one class,+-- starting at scope @n@. For 'Inclusions' each scope extends the previous+-- one, and the evidence for the first step is kept.+data Chain' (n :: S) where+  Chain'+    :: Ctx n -> Ctx l -> Ctx k+    -> Renaming n l -> Renaming l k+    -> Maybe (Includes n l)+    -> Chain' n++-- | A 'Chain'' starting at an unknown scope.+data Chain where+  Chain :: Chain' n -> Chain++-- | Generate a 'Chain' of the given class.+genChain :: RenamingClass -> Gen Chain+genChain cls = do+  SomeCtx n <- genCtx+  case cls of+    Inclusions -> withCtx n $ \_ -> do+      k1 <- chooseInt (0, 2)+      k2 <- chooseInt (0, 2)+      extendBy k1 n $ \l -> extendBy k2 l $ \k ->+        pure (Chain (Chain' n l k (inclusionRenaming n) (inclusionRenaming l) (Just Includes)))+    Injections -> do+      SomeCtx l <- genCtxAtLeast (length (ctxNames n))+      SomeCtx k <- genCtxAtLeast (length (ctxNames l))+      f <- genInjection n l+      g <- genInjection l k+      pure (Chain (Chain' n l k f g Nothing))+    Functions -> do+      SomeCtx l <- genCtxAtLeast (min 1 (length (ctxNames n)))+      SomeCtx k <- genCtxAtLeast (min 1 (length (ctxNames l)))+      f <- genFunction n l+      g <- genFunction l k+      pure (Chain (Chain' n l k f g Nothing))+  where+    -- 'extendCtxBy' with the inclusion visible to the continuation.+    extendBy :: Distinct n => Int -> Ctx n -> (forall l. DExt n l => Ctx l -> Gen r) -> Gen r+    extendBy steps ctx cont+      | steps <= 0 = cont ctx+      | otherwise = do+          width <- chooseInt (1, 2)+          withHintedBinders width (ctxScope ctx) $ \binders ->+            let ctx' = extendCtx ctx binders+             in extendBy (steps - 1) ctx' cont++-- | Show the scopes and renamings of a chain.+showChain :: Chain' n -> String+showChain (Chain' n l k f g _) = unlines+  [ "n = " <> showCtx n, "l = " <> showCtx l, "k = " <> showCtx k+  , "f : n → l = " <> show f, "g : l → k = " <> show g ]++-- * Laws of 'Sinkable'++-- | The laws of a 'Sinkable' type @e@, read as a functor from scopes to+-- sets. The equality is a parameter, since for terms it is α-equivalence.+data SinkableLaws e = SinkableLaws+  { -- | @sinkabilityProof id = id@.+    sinkIdentity    :: forall n. Ctx n -> e n -> Property+    -- | @sinkabilityProof (g . f) = sinkabilityProof g . sinkabilityProof f@.+  , sinkComposition :: forall n l k. Ctx k -> Renaming n l -> Renaming l k -> e n -> Property+    -- | On an inclusion, @sinkabilityProof sink = sink@.+  , sinkInclusion   :: forall n l. Includes n l -> Ctx l -> e n -> Property+  }++-- | The laws, for a given equality and printer.+sinkableLaws+  :: Sinkable e+  => (forall n. Ctx n -> e n -> e n -> Bool)+  -> (forall n. e n -> String)+  -> SinkableLaws e+sinkableLaws eq showE = SinkableLaws+  { sinkIdentity = \ctx t ->+      let lhs = sinkabilityProof id t+       in counterexample ("sinkabilityProof id t = " <> showE lhs) (eq ctx lhs t)+  , sinkComposition = \ctxK f g t ->+      let lhs = sinkabilityProof (rename g . rename f) t+          rhs = sinkabilityProof (rename g) (sinkabilityProof (rename f) t)+       in counterexample ("sinkabilityProof (g . f) t = " <> showE lhs) $+            counterexample ("sinkabilityProof g (sinkabilityProof f t) = " <> showE rhs) $+              eq ctxK lhs rhs+  , sinkInclusion = \Includes ctxL t ->+      let lhs = sinkabilityProof sink t+          rhs = sink t+       in counterexample ("sinkabilityProof sink t = " <> showE lhs) $+            counterexample ("sink t = " <> showE rhs) $+              eq ctxL lhs rhs+  }++-- | The laws of 'SinkableLaws', by name.+data SinkLaw = SinkIdentity | SinkComposition | SinkInclusion+  deriving (Eq, Show, Enum, Bounded)++-- | A value in the first scope of a chain.+data SinkCase e where+  SinkCase :: Chain' n -> e n -> SinkCase e++-- | A chain of the given class with a value in its first scope.+genSinkCase :: (forall n. Ctx n -> Gen (e n)) -> RenamingClass -> Gen (SinkCase e)+genSinkCase genE cls = do+  Chain chain@(Chain' n _ _ _ _ _) <- genChain cls+  SinkCase chain <$> genE n++-- | The laws of 'Sinkable' for one type: the identity law once, and the+-- composition law along each class of renamings. The inclusion law is+-- checked along inclusions only.+sinkableSpec+  :: Sinkable e+  => (forall n. Ctx n -> e n -> e n -> Bool)   -- ^ Equality.+  -> (forall n. e n -> String)                 -- ^ Printer.+  -> (forall n. Ctx n -> Gen (e n))            -- ^ Generator.+  -> (forall n. e n -> [e n])                  -- ^ Shrinker.+  -> (RenamingClass -> SinkLaw -> Verdict)+  -> Spec+sinkableSpec eq showE genE shrinkE verdict = do+  let laws = sinkableLaws eq showE+      cases cls = forAllShrinkShow (genSinkCase genE cls) shrinkCase showCase+      shrinkCase (SinkCase chain t) = map (SinkCase chain) (shrinkE t)+      showCase (SinkCase chain t) = showChain chain <> "t = " <> showE t+  law (verdict Inclusions SinkIdentity) (show SinkIdentity) $+    cases Inclusions $ \(SinkCase (Chain' n _ _ _ _ _) t) -> sinkIdentity laws n t+  forM_ allRenamingClasses $ \cls -> describe ("along " <> show cls) $ do+    law (verdict cls SinkComposition) (show SinkComposition) $+      cases cls $ \(SinkCase (Chain' _ _ k f g _) t) -> sinkComposition laws k f g t+    case cls of+      Inclusions -> law (verdict cls SinkInclusion) (show SinkInclusion) $+        cases cls $ \(SinkCase (Chain' _ l _ _ _ incl) t) -> case incl of+          Just evidence -> sinkInclusion laws evidence l t+          Nothing       -> property Discard+      _ -> pure ()++-- * Laws of 'CoSinkable'++-- | A pattern out of the first scope of a chain.+data PatternCase p where+  PatternCase :: DExt n i => Chain' n -> p n i -> PatternCase p++-- | Show a 'PatternCase'.+showPatternCase :: PatternNames p -> PatternCase p -> String+showPatternCase names (PatternCase chain p) = showChain chain <> "p : n → i = " <> showPatternWith names p++-- | A chain of the given class with a pattern out of its first scope.+genPatternCase :: GenPattern p -> RenamingClass -> Gen (PatternCase p)+genPatternCase genPat cls = do+  Chain chain@(Chain' n _ _ _ _ _) <- genChain cls+  PatIn pat <- genPat n+  pure (PatternCase chain pat)++-- | The laws of 'coSinkabilityProof', for a pattern @p : n → i@ and the+-- renamings @f : n → l@ and @g : l → k@ of a 'PatternCase'. Write+-- @(f', p')@ for the result of @coSinkabilityProof f p@: the extended+-- renaming @f' : i → i'@ and the pushed pattern @p' : l → i'@.+data CoSinkableLaws p = CoSinkableLaws+  { -- | Pushing along the identity changes nothing: @p' = p@ and @f' = id@.+    coSinkIdentity    :: PatternCase p -> Property+    -- | Pushing along @g . f@ is pushing along @f@ and then along @g@: the+    -- pushed patterns agree and the extended renamings compose.+  , coSinkComposition :: PatternCase p -> Property+    -- | The extended renaming extends @f@: @f' (sink x) = f x@ for every+    -- name @x@ of @n@.+  , coSinkExtension   :: PatternCase p -> Property+    -- | The extended renaming sends the binders of @p@ to the binders of+    -- @p'@, in order.+  , coSinkBinders     :: PatternCase p -> Property+  }++-- | The laws of 'coSinkabilityProof' for any 'CoSinkable' pattern type.+-- Names in different scopes are compared by their raw identifiers, and the+-- binders of a pattern are listed by the given function.+coSinkableLaws :: CoSinkable p => PatternNames p -> CoSinkableLaws p+coSinkableLaws binders = CoSinkableLaws+  { coSinkIdentity = \(PatternCase (Chain' n _ _ _ _ _) p) ->+      coSinkabilityProof id p $ \f' p' ->+        let xs = namesUnder n p+         in counterexample ("pushed pattern p' = " <> showPatternWith binders p') $+              counterexample ("f' on i = " <> showOn f' xs) $+                binders p' === binders p+                  .&&. map (nameId . f') xs === map nameId xs+  , coSinkComposition = \(PatternCase (Chain' n _ _ f g _) p) ->+      coSinkabilityProof (rename g . rename f) p $ \h q ->+        coSinkabilityProof (rename f) p $ \f' p' ->+          coSinkabilityProof (rename g) p' $ \g' p'' ->+            let xs = namesUnder n p+             in counterexample ("pushed along g . f: " <> showPatternWith binders q) $+                  counterexample ("pushed along f, then g: " <> showPatternWith binders p'') $+                    counterexample ("(g . f)' on i = " <> showOn h xs) $+                      counterexample ("g' . f' on i = " <> showOn (g' . f') xs) $+                        binders q === binders p''+                          .&&. map (nameId . h) xs === map (nameId . g' . f') xs+  , coSinkExtension = \(PatternCase (Chain' n _ _ f _ _) p) ->+      coSinkabilityProof (rename f) p $ \f' _p' ->+        let outer = ctxNames n+         in counterexample ("f' on n = " <> showOn (f' . sink) outer) $+              map (nameId . f' . sink) outer === map (nameId . rename f) outer+  , coSinkBinders = \(PatternCase (Chain' _ _ _ f _ _) p) ->+      coSinkabilityProof (rename f) p $ \f' p' ->+        counterexample ("pushed pattern p' = " <> showPatternWith binders p') $+          map (nameId . f' . UnsafeName) (binders p) === binders p'+  }+  where+    -- The names of the scope a pattern extends to: the outer ones, then+    -- the bound ones.+    namesUnder :: (CoSinkable p, DExt n i) => Ctx n -> p n i -> [Name i]+    namesUnder n p = ctxNames (extendCtx n p)++    showOn :: (Name a -> Name b) -> [Name a] -> String+    showOn h xs = "{" <> intercalate ", " [ showName x <> " ↦ " <> showName (h x) | x <- xs ] <> "}"++-- | The laws of 'CoSinkableLaws', by name, and the law of the traversal+-- order of 'withPattern'.+data CoSinkLaw+  = CoSinkIdentity | CoSinkComposition | CoSinkExtension | CoSinkBinders+  | WithPatternOrder+  deriving (Eq, Show, Enum, Bounded)++-- | 'withPattern' visits the binders of a pattern in the order of its+-- structure. 'addSubstPattern', 'nameBinderListOf' and+-- 'withRefreshedPattern' rely on this.+withPatternOrderLaw :: CoSinkable p => PatternNames p -> p n l -> Property+withPatternOrderLaw binders p =+  counterexample "the order of the pattern is on the left, the order of withPattern on the right" $+    binders p === patternRawNames p++-- | All laws of 'coSinkabilityProof' for a pattern type, along each class+-- of renamings, and the law of the traversal order of 'withPattern'.+coSinkableSpec+  :: CoSinkable p+  => PatternNames p -> GenPattern p -> (RenamingClass -> CoSinkLaw -> Verdict) -> Spec+coSinkableSpec binders genPat verdict = do+  law (verdict Inclusions WithPatternOrder) "withPattern visits binders in the order of the pattern" $+    forAllShow (genPatternCase genPat Inclusions) (showPatternCase binders) $+      \(PatternCase _ p) -> withPatternOrderLaw binders p+  forM_ allRenamingClasses $ \cls -> describe ("along " <> show cls) $+    forM_ [CoSinkIdentity, CoSinkComposition, CoSinkExtension, CoSinkBinders] $ \name ->+      law (verdict cls name) (show name) $+        forAllShow (genPatternCase genPat cls) (showPatternCase binders) (lawOf name)+  where+    laws = coSinkableLaws binders+    lawOf CoSinkIdentity    = coSinkIdentity laws+    lawOf CoSinkComposition = coSinkComposition laws+    lawOf CoSinkExtension   = coSinkExtension laws+    lawOf CoSinkBinders     = coSinkBinders laws+    lawOf WithPatternOrder  = \(PatternCase _ p) -> withPatternOrderLaw binders p++-- * Laws of 'UnifiablePattern'++-- | Two patterns out of the same scope, which bind the same number of names.+data PatPair p n where+  PatPair :: (DExt n l, DExt n r) => p n l -> p n r -> PatPair p n++-- | A generator of pairs of patterns of the same shape.+type GenPatternPair p = forall n. Ctx n -> Gen (PatPair p n)++-- | Two lists of the same length, of up to three hinted binders each.+genNameBinderListPair :: GenPatternPair NameBinderList+genNameBinderListPair ctx = withCtx ctx $ \scope -> do+  k <- chooseInt (0, 3)+  withHintedBinders k scope $ \l ->+    withHintedBinders k scope $ \r -> pure (PatPair l r)++-- | The verdict of 'unifyPatternsIn' on two patterns of the same shape+-- pairs their binders by position: its renamings send the @j@-th binder of+-- each side to the same name, and distinct positions to distinct names.+unifyPatternsLaw :: UnifiablePattern p => PatternNames p -> Ctx n -> PatPair p n -> Property+unifyPatternsLaw binders ctx (PatPair l r) = withCtx ctx $ \scope ->+  let xs = binders l+      ys = binders r+      positional us vs =+        counterexample ("left binders become " <> show us) $+          counterexample ("right binders become " <> show vs) $+            us === vs .&&. counterexample "two positions are merged" (distinct us)+   in counterexample ("left pattern = " <> showPatternWith binders l) $+        counterexample ("right pattern = " <> showPatternWith binders r) $+          case unifyPatternsIn scope l r of+            SameNameBinders _ ->+              counterexample "SameNameBinders" $ positional xs ys+            RenameLeftNameBinder _ f ->+              counterexample "RenameLeftNameBinder" $ positional (map (renamed f) xs) ys+            RenameRightNameBinder _ g ->+              counterexample "RenameRightNameBinder" $ positional xs (map (renamed g) ys)+            RenameBothBinders _ f g ->+              counterexample "RenameBothBinders" $ positional (map (renamed f) xs) (map (renamed g) ys)+            NotUnifiable ->+              counterexample "NotUnifiable" False+  where+    -- The name a binder renaming assigns to a bound name.+    renamed :: (NameBinder a b -> NameBinder a c) -> Int -> Int+    renamed f x = nameId (nameOf (f (UnsafeNameBinder (UnsafeName x))))+    distinct us = and [ u /= v | (i, u) <- zip [0 :: Int ..] us, (j, v) <- zip [0 :: Int ..] us, i < j ]++-- | The positional law of 'unifyPatternsIn' on pairs of patterns.+unifyPatternsSpec :: UnifiablePattern p => PatternNames p -> GenPatternPair p -> Verdict -> Spec+unifyPatternsSpec binders genPair verdict =+  law verdict "unifyPatternsIn pairs binders position by position" $+    forAllShow (genSomePair genPair) showSomePair $ \(SomePair ctx pair) -> unifyPatternsLaw binders ctx pair+  where+    showSomePair (SomePair ctx _) = "n = " <> showCtx ctx++-- | A pair of patterns out of an unknown scope.+data SomePair p where+  SomePair :: Ctx n -> PatPair p n -> SomePair p++genSomePair :: GenPatternPair p -> Gen (SomePair p)+genSomePair genPair = do+  SomeCtx ctx <- genCtx+  SomePair ctx <$> genPair ctx++-- * Running laws++-- | What we expect of a law.+data Verdict+  = Holds+    -- | The law fails by design, for the reason given. The test checks that+    -- it still fails ('expectFailure'), so that the suite notices a change.+    -- Some counterexamples are rare, so the search runs up to 50000 cases+    -- and stops at the first.+  | ByDesign String++-- | The verdicts for a pattern type whose 'coSinkabilityProof' returns a+-- coercion as the extended renaming, as those of 'NameBinder',+-- 'NameBinders' and 'NameBinderList' do. Such a renaming extends @f@ only+-- when @f@ is an inclusion.+extensionByCoercion :: RenamingClass -> CoSinkLaw -> Verdict+extensionByCoercion Inclusions _ = Holds+extensionByCoercion _ CoSinkExtension = ByDesign+  "the extended renaming is a coercion, so it extends inclusions only"+extensionByCoercion _ _ = Holds++-- | Check a law on at least 1000 cases, or check that a law that fails by+-- design still fails.+law :: Testable p => Verdict -> String -> p -> Spec+law Holds name p =+  modifyMaxSuccess (max 1000) (it name (property p))+law (ByDesign why) name p =+  it (name <> " (fails by design: " <> why <> ")") (expectFailure (withMaxSuccess 50000 p))

@@ -0,0 +1,695 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE KindSignatures      #-}+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- | Generators of scope-safe terms of any free foil signature, and the laws+-- of the relative monad @'AST' binder sig@ on 'Name' (in the sense of+-- Altenkirch, Chapman and Uustalu), with unit 'Var' and bind 'substitute'+-- (and 'rbind').+--+-- A language plugs in with a 'SyntaxGen'. 'genAST' fills its node shapes,+-- and sometimes builds a subterm in an outer scope and 'sink's it. This is+-- how real code produces binders that shadow names of the scope, which+-- 'substitute' has to handle.+module Control.Monad.Free.Foil.Laws (+  -- * Terms+  SyntaxGen (..),+  genAST,+  shrinkAST,+  mutations,+  hasShadowing,+  boundNames,+  showAST,+  showNodeVia,+  -- * α-equivalence+  alphaEqNameless,+  AlphaLaw (..),+  alphaSpec,+  PairCase (..),+  genPairCase,+  showPairCase,+  sinkAgreesOnInclusions,+  -- * Substitutions+  SubstKind (..),+  Subst (..),+  genSubstInto,+  showSubst,+  composeSubst,+  explicitIdentitySubst,+  -- * Test cases+  TermCase (..),+  genTermCase,+  shrinkTermCase,+  showTermCase,+  SubstCase (..),+  genSubstCase,+  shrinkSubstCase,+  showSubstCase,+  RenamingCase (..),+  genRenamingCase,+  shrinkRenamingCase,+  showRenamingCase,+  -- * Laws of the relative monad+  RelMonadLaws (..),+  relMonadLaws,+  RelMonadLaw (..),+  relMonadSpec,+  -- * Functoriality of terms+  FunctorLaws (..),+  functorLaws,+  FunctorLaw (..),+  functorSpec,+) where++import           Control.Monad               (forM_, guard)+import           Data.Bifoldable             (bifoldr)+import           Data.Bifunctor              (Bifunctor, bimap)+import           Data.Bitraversable          (Bitraversable, bitraverse)+import qualified Data.IntMap                 as IntMap+import           Data.IntSet                 (IntSet)+import qualified Data.IntSet                 as IntSet+import           Data.List                   (intercalate)+import           Data.Maybe                  (isJust)+import           Test.Hspec                  (Spec, describe)+import           Test.QuickCheck++import           Control.Monad.Foil+import           Control.Monad.Foil.Laws+import           Control.Monad.Foil.Relative (RelMonad (..), liftRM)+import           Control.Monad.Free.Foil+import           Data.ZipMatchK              (ZipMatchK, zipMatchWith2)++-- * Terms++-- | What 'genAST' needs to know about a language.+data SyntaxGen binder sig = SyntaxGen+  { -- | The shapes of the nodes. A shape with no holes is a leaf. When a+    -- scope has no names and the signature has no leaves, a shape whose+    -- holes are all scoped is used, so its patterns must bind something.+    sgShapes   :: [sig () ()]+    -- | Patterns out of a given scope.+  , sgPattern  :: GenPattern binder+    -- | The names a pattern binds, in the order of its structure.+  , sgPatternNames :: PatternNames binder+    -- | Print a node whose subterms are already printed.+  , sgShowNode :: sig String String -> String+  }++-- | The number of scoped and of unscoped holes of a node.+holes :: Bitraversable sig => sig a b -> (Int, Int)+holes = bifoldr (\_ (s, t) -> (s + 1, t)) (\_ (s, t) -> (s, t + 1)) (0, 0)++-- | A term of about the given size in the scope of the context.+genAST+  :: forall binder sig n. (Bitraversable sig, CoSinkable binder, SinkableK binder)+  => SyntaxGen binder sig -> Ctx n -> Int -> Gen (AST binder sig n)+genAST sg ctx size = case ctx of+  Under parent _ _ | size > 0 ->+    frequency [ (1, sink1 (genAST sg parent size)), (6, here) ]+  _ -> here+  where+    vars = ctxNames ctx+    shapes = sgShapes sg+    leaves = [ s | s <- shapes, holes s == (0, 0) ]+    nodes = [ s | s <- shapes, holes s /= (0, 0) ]+    binding = [ s | s <- nodes, snd (holes s) == 0 ]++    here+      | size <= 0 = case (vars, leaves) of+          ([], []) -> elements binding >>= fill 0+          _ -> oneof $+            [ Var <$> elements vars | not (null vars) ] +++            [ elements leaves >>= fill 0 | not (null leaves) ]+      | otherwise = frequency $+          [ (2, Var <$> elements vars) | not (null vars) ] +++          [ (1, elements leaves >>= fill 0) | not (null leaves) ] +++          [ (6, elements nodes >>= fill (size - 1)) | not (null nodes) ]++    fill :: Int -> sig () () -> Gen (AST binder sig n)+    fill budget shape =+      let (s, t) = holes shape+          each = budget `div` max 1 (s + t)+       in Node <$> bitraverse (\() -> genScoped each) (\() -> genAST sg ctx each) shape++    genScoped :: Int -> Gen (ScopedAST binder sig n)+    genScoped each = do+      PatIn pat <- sgPattern sg ctx+      ScopedAST pat <$> genAST sg (extendCtx ctx pat) each++-- | Shrink a term within its scope: replace a node by one of its unscoped+-- subterms, or shrink one subterm (under its binder if it is scoped).+shrinkAST :: forall binder sig n. Bitraversable sig => AST binder sig n -> [AST binder sig n]+shrinkAST = \case+  Var _ -> []+  Node node -> unscopedChildren node ++ map Node (shrinkOne node)+  where+    unscopedChildren = bifoldr (\_ acc -> acc) (:) []++    shrinkOne :: forall x. sig (ScopedAST binder sig x) (AST binder sig x) -> [sig (ScopedAST binder sig x) (AST binder sig x)]+    shrinkOne = alterOneHole shrinkScoped shrinkAST++    shrinkScoped :: forall x. ScopedAST binder sig x -> [ScopedAST binder sig x]+    shrinkScoped (ScopedAST pat body) = [ ScopedAST pat body' | body' <- shrinkAST body ]++-- | All nodes that differ from the given one in exactly one subterm, given+-- the alternatives for each kind of subterm.+alterOneHole+  :: Bitraversable sig+  => (s -> [s]) -> (t -> [t]) -> sig s t -> [sig s t]+alterOneHole onScoped onTerm node = concat+  [ fst (runAt (bitraverse (at i onScoped) (at i onTerm) node) 0)+  | i <- [0 .. uncurry (+) (holes node) - 1] ]+  where+    -- At the @i@-th hole, the alternatives for the subterm; elsewhere, the+    -- subterm itself.+    at :: Int -> (a -> [a]) -> a -> At a+    at i alts x = At $ \j -> (if i == j then alts x else [x], j + 1)++-- | All terms that differ from the given one in exactly one occurrence of a+-- variable, replaced by another name in scope at that point. Most of them+-- are not α-equivalent to the original.+mutations+  :: forall binder sig n. (Bitraversable sig, CoSinkable binder, Distinct n)+  => [Name n] -> AST binder sig n -> [AST binder sig n]+mutations names = \case+  Var x -> [ Var y | y <- names, y /= x ]+  Node node -> map Node (alterOneHole scoped (mutations names) node)+  where+    scoped :: ScopedAST binder sig n -> [ScopedAST binder sig n]+    scoped (ScopedAST pat body) = case (assertDistinct pat, assertExt pat) of+      (Distinct, Ext) ->+        [ ScopedAST pat body' | body' <- mutations (sink1 names ++ namesOfPattern pat) body ]++-- | Whether some binder of the term binds a name that is already in scope+-- at that point, given the raw names of the scope of the term. Such binders+-- arise from 'sink' and are what capture-avoidance has to handle.+hasShadowing :: (Bitraversable sig, CoSinkable binder) => IntSet -> AST binder sig n -> Bool+hasShadowing scope = \case+  Var _ -> False+  Node node -> bifoldr (\s acc -> scoped s || acc) (\t acc -> hasShadowing scope t || acc) False node+  where+    scoped (ScopedAST pat body) =+      let names = patternRawNames pat+       in any (`IntSet.member` scope) names+            || hasShadowing (IntSet.union scope (IntSet.fromList names)) body++-- | The raw names bound anywhere in a term.+boundNames :: (Bitraversable sig, CoSinkable binder) => AST binder sig n -> IntSet+boundNames = \case+  Var _ -> IntSet.empty+  Node node -> bifoldr (\s acc -> scoped s <> acc) (\t acc -> boundNames t <> acc) IntSet.empty node+  where+    scoped (ScopedAST pat body) = IntSet.fromList (patternRawNames pat) <> boundNames body++-- | The raw names of a context.+ctxRawNames :: Ctx n -> IntSet+ctxRawNames = IntSet.fromList . map nameId . ctxNames++-- | Label a test case of a term in a context by whether it shadows.+termCoverage :: (Bitraversable sig, CoSinkable binder) => Ctx n -> AST binder sig n -> Property -> Property+termCoverage n t = classify (hasShadowing (ctxRawNames n) t) "t has a shadowing binder"++-- | Label a test case of substitution by whether the term shadows, and by+-- whether one of its binders is a name of the target scope, so that+-- 'substitute' has to rename it.+substCoverage :: (Bitraversable sig, CoSinkable binder) => SubstCase binder sig -> Property -> Property+substCoverage (SubstCase i o1 _ _ _ t) =+  termCoverage i t+    . classify (not (IntSet.disjoint (boundNames t) (ctxRawNames o1))) "a binder of t is a name of o1"++-- | An applicative that numbers the holes of a traversal and collects the+-- alternatives at each of them.+newtype At a = At { runAt :: Int -> ([a], Int) }++instance Functor At where+  fmap f (At g) = At $ \j -> let (xs, j') = g j in (map f xs, j')++instance Applicative At where+  pure x = At $ \j -> ([x], j)+  At f <*> At x = At $ \j ->+    let (fs, j') = f j+        (xs, j'') = x j'+     in ([ g y | g <- fs, y <- xs ], j'')++-- | Print a term with raw names (@x3@), and scoped terms as @λ[x3 x4]. t@.+showAST :: Bifunctor sig => SyntaxGen binder sig -> AST binder sig n -> String+showAST sg = \case+  Var x -> showName x+  Node node -> sgShowNode sg (bimap showScoped (showAST sg) node)+  where+    showScoped (ScopedAST pat body) = "λ" <> showPatternWith (sgPatternNames sg) pat <> ". " <> showAST sg body++-- | A node printer from a derived 'Show' instance. The subterms are shown+-- verbatim, in parentheses when they contain a space.+showNodeVia :: (Bifunctor sig, Show (sig Shown Shown)) => sig String String -> String+showNodeVia = show . bimap Shown Shown++-- | A string that 'show' prints as it is.+newtype Shown = Shown String++instance Show Shown where+  showsPrec d (Shown s)+    | d > 10 && ' ' `elem` s = showString ("(" <> s <> ")")+    | otherwise = showString s++-- * Substitutions++-- | How a substitution is built.+data SubstKind+  = Total  -- ^ Every name of the domain is mapped explicitly, into an unrelated scope.+  | Beta   -- ^ The domain extends the codomain by some binders, and only these+           --   are mapped ('addSubstList' on 'identitySubst'), as in a β-reduction.+  deriving (Eq, Show, Enum, Bounded)++-- | A substitution together with its explicit entries, for printing.+data Subst binder sig i o = Subst+  { substKind  :: SubstKind+  , substValue :: Substitution (AST binder sig) i o+  , substTable :: [(Name i, AST binder sig o)]+  }++-- | Show the explicit entries of a substitution.+showSubst :: Bifunctor sig => SyntaxGen binder sig -> Subst binder sig i o -> String+showSubst sg s = show (substKind s) <> " {" <> intercalate ", "+  [ showName x <> " ↦ " <> showAST sg t | (x, t) <- substTable s ] <> "}"++-- | Generate a substitution into the given scope, and its domain. A 'Total'+-- substitution comes from an independent scope, a 'Beta' one from an+-- extension of the codomain.+genSubstInto+  :: (Bitraversable sig, CoSinkable binder, SinkableK binder)+  => SyntaxGen binder sig -> SubstKind -> Ctx o+  -> (forall i. Ctx i -> Subst binder sig i o -> Gen r) -> Gen r+genSubstInto sg kind o cont = case kind of+  Total -> do+    SomeCtx i <- genCtx+    ts <- mapM (const (genAST sg o 4)) (ctxNames i)+    let value = nameMapToSubstitution (addNameBinderList (ctxChain i) ts emptyNameMap)+    cont i (Subst Total value (zip (ctxNames i) ts))+  Beta -> withCtx o $ \scope -> do+    k <- chooseInt (1, 3)+    withHintedBinders k scope $ \binders -> do+      ts <- mapM (const (genAST sg o 4)) (namesOfPattern binders)+      let value = addSubstList identitySubst binders ts+      cont (extendCtx o binders) (Subst Beta value (zip (namesOfPattern binders) ts))++-- | Kleisli composition @s2 ⊙ s1@: substitute with @s1@, then with @s2@.+-- The result maps every name of @i@ explicitly.+composeSubst+  :: (Bifunctor sig, CoSinkable binder, SinkableK binder, Distinct o2)+  => Ctx i -> Scope o2+  -> Substitution (AST binder sig) i o1+  -> Substitution (AST binder sig) o1 o2+  -> Substitution (AST binder sig) i o2+composeSubst i scope2 s1 s2 =+  nameMapToSubstitution $ addNameBinderList (ctxChain i)+    [ substitute scope2 s2 (lookupSubst s1 x) | x <- ctxNames i ] emptyNameMap++-- | The identity substitution with every name mapped explicitly, so that+-- 'substitute' cannot take its shortcut for the empty substitution.+explicitIdentitySubst :: Ctx n -> Substitution (AST binder sig) n n+explicitIdentitySubst n =+  nameMapToSubstitution (addNameBinderList (ctxChain n) (map Var (ctxNames n)) emptyNameMap)++-- * Test cases++-- | A term in a scope.+data TermCase binder sig where+  TermCase :: Ctx n -> AST binder sig n -> TermCase binder sig++-- | A term in a random scope.+genTermCase+  :: (Bitraversable sig, CoSinkable binder, SinkableK binder)+  => SyntaxGen binder sig -> Gen (TermCase binder sig)+genTermCase sg = do+  SomeCtx n <- genCtx+  TermCase n <$> sized (genAST sg n . min 30)++-- | Shrink the term of a 'TermCase'.+shrinkTermCase :: Bitraversable sig => TermCase binder sig -> [TermCase binder sig]+shrinkTermCase (TermCase n t) = map (TermCase n) (shrinkAST t)++-- | Show a 'TermCase'.+showTermCase :: Bifunctor sig => SyntaxGen binder sig -> TermCase binder sig -> String+showTermCase sg (TermCase n t) = unlines [ "n = " <> showCtx n, "t = " <> showAST sg t ]++-- | Two composable substitutions and a term: @t : i@, @s1 : i → o1@ and+-- @s2 : o1 → o2@.+data SubstCase binder sig where+  SubstCase+    :: Ctx i -> Ctx o1 -> Ctx o2+    -> Subst binder sig i o1 -> Subst binder sig o1 o2+    -> AST binder sig i+    -> SubstCase binder sig++-- | Generate a 'SubstCase' with substitutions of the given kinds.+genSubstCase+  :: (Bitraversable sig, CoSinkable binder, SinkableK binder)+  => SyntaxGen binder sig -> SubstKind -> SubstKind -> Gen (SubstCase binder sig)+genSubstCase sg kind1 kind2 = do+  SomeCtx o2 <- genCtx+  genSubstInto sg kind2 o2 $ \o1 s2 ->+    genSubstInto sg kind1 o1 $ \i s1 -> do+      t <- sized (genAST sg i . min 30)+      pure (SubstCase i o1 o2 s1 s2 t)++-- | Shrink the term of a 'SubstCase'.+shrinkSubstCase :: Bitraversable sig => SubstCase binder sig -> [SubstCase binder sig]+shrinkSubstCase (SubstCase i o1 o2 s1 s2 t) = map (SubstCase i o1 o2 s1 s2) (shrinkAST t)++-- | Show a 'SubstCase'.+showSubstCase :: Bifunctor sig => SyntaxGen binder sig -> SubstCase binder sig -> String+showSubstCase sg (SubstCase i o1 o2 s1 s2 t) = unlines+  [ "i = " <> showCtx i, "o1 = " <> showCtx o1, "o2 = " <> showCtx o2+  , "s1 : i → o1 = " <> showSubst sg s1+  , "s2 : o1 → o2 = " <> showSubst sg s2+  , "t = " <> showAST sg t ]++-- | A chain of renamings and a term in its first scope.+data RenamingCase binder sig where+  RenamingCase :: Chain' n -> AST binder sig n -> RenamingCase binder sig++-- | Generate a 'RenamingCase' of the given class.+genRenamingCase+  :: (Bitraversable sig, CoSinkable binder, SinkableK binder)+  => SyntaxGen binder sig -> RenamingClass -> Gen (RenamingCase binder sig)+genRenamingCase sg cls = do+  Chain chain@(Chain' n _ _ _ _ _) <- genChain cls+  RenamingCase chain <$> sized (genAST sg n . min 30)++-- | Shrink the term of a 'RenamingCase'.+shrinkRenamingCase :: Bitraversable sig => RenamingCase binder sig -> [RenamingCase binder sig]+shrinkRenamingCase (RenamingCase chain t) = map (RenamingCase chain) (shrinkAST t)++-- | Show a 'RenamingCase'.+showRenamingCase :: Bifunctor sig => SyntaxGen binder sig -> RenamingCase binder sig -> String+showRenamingCase sg (RenamingCase chain t) = showChain chain <> "t = " <> showAST sg t++-- * Laws of the relative monad++-- | 'rbind' at 'Name'.+rbindN+  :: (Bifunctor sig, CoSinkable binder, SinkableK binder, Distinct b)+  => Scope b -> AST binder sig a -> (Name a -> AST binder sig b) -> AST binder sig b+rbindN = rbind++-- | 'rreturn' at 'Name'.+rreturnN+  :: (Bifunctor sig, CoSinkable binder, SinkableK binder)+  => Name a -> AST binder sig a+rreturnN = rreturn++-- | 'liftRM' at 'Name'.+liftRMN+  :: (Bifunctor sig, CoSinkable binder, SinkableK binder, Distinct b)+  => Scope b -> (Name a -> Name b) -> AST binder sig a -> AST binder sig b+liftRMN = liftRM++-- | The laws of 'substitute' and of 'rbind', up to α-equivalence.+data RelMonadLaws binder sig = RelMonadLaws+  { -- | Left unit: @substitute o s (Var x) = lookupSubst s x@.+    substLeftUnit             :: SubstCase binder sig -> Property+    -- | Right unit: @substitute n identitySubst t ≡α t@.+  , substRightUnit            :: TermCase binder sig -> Property+    -- | Right unit, with every name mapped explicitly (so no shortcut).+  , substRightUnitExplicit    :: TermCase binder sig -> Property+    -- | Associativity:+    -- @substitute o2 s2 (substitute o1 s1 t) ≡α substitute o2 (s2 ⊙ s1) t@.+  , substAssociativity        :: SubstCase binder sig -> Property+    -- | Left unit of 'rbind': @rbind o (rreturn x) f = f x@.+  , rbindLeftUnit             :: SubstCase binder sig -> Property+    -- | Right unit of 'rbind': @rbind n t rreturn ≡α t@.+  , rbindRightUnit            :: TermCase binder sig -> Property+    -- | Associativity of 'rbind'.+  , rbindAssociativity        :: SubstCase binder sig -> Property+    -- | 'substitute' and 'rbind' are the same Kleisli extension.+  , substituteAgreesWithRbind :: SubstCase binder sig -> Property+  }++-- | The laws for a language, with α-equivalence ('alphaEquiv') as the+-- equality.+relMonadLaws+  :: forall binder sig.+     (Bitraversable sig, ZipMatchK sig, CoSinkable binder, SinkableK binder)+  => SyntaxGen binder sig -> RelMonadLaws binder sig+relMonadLaws sg = RelMonadLaws+  { substLeftUnit = \(SubstCase i o1 _ s1 _ _) -> withCtx o1 $ \scope1 ->+      conjoin+        [ cmp scope1+            "substitute o1 s1 (Var x)" (substitute scope1 (substValue s1) (Var x))+            "lookupSubst s1 x" (lookupSubst (substValue s1) x)+        | x <- ctxNames i ]+  , substRightUnit = \(TermCase n t) -> withCtx n $ \scope ->+      cmp scope "substitute n identitySubst t" (substitute scope identitySubst t) "t" t+  , substRightUnitExplicit = \(TermCase n t) -> withCtx n $ \scope ->+      cmp scope+        "substitute n (explicit identity) t" (substitute scope (explicitIdentitySubst n) t)+        "t" t+  , substAssociativity = \(SubstCase i o1 o2 s1 s2 t) ->+      withCtx o1 $ \scope1 -> withCtx o2 $ \scope2 ->+        cmp scope2+          "substitute o2 s2 (substitute o1 s1 t)"+          (substitute scope2 (substValue s2) (substitute scope1 (substValue s1) t))+          "substitute o2 (s2 ⊙ s1) t"+          (substitute scope2 (composeSubst i scope2 (substValue s1) (substValue s2)) t)+  , rbindLeftUnit = \(SubstCase i o1 _ s1 _ _) -> withCtx o1 $ \scope1 ->+      conjoin+        [ cmp scope1+            "rbind o1 (rreturn x) f" (rbindN scope1 (rreturnN x) (lookupSubst (substValue s1)))+            "f x" (lookupSubst (substValue s1) x)+        | x <- ctxNames i ]+  , rbindRightUnit = \(TermCase n t) -> withCtx n $ \scope ->+      cmp scope "rbind n t rreturn" (rbindN scope t rreturnN) "t" t+  , rbindAssociativity = \(SubstCase _ o1 o2 s1 s2 t) ->+      withCtx o1 $ \scope1 -> withCtx o2 $ \scope2 ->+        let f = lookupSubst (substValue s1)+            g = lookupSubst (substValue s2)+         in cmp scope2+              "rbind o2 (rbind o1 t f) g" (rbindN scope2 (rbindN scope1 t f) g)+              "rbind o2 t (\\x -> rbind o2 (f x) g)" (rbindN scope2 t (\x -> rbindN scope2 (f x) g))+  , substituteAgreesWithRbind = \(SubstCase _ o1 _ s1 _ t) -> withCtx o1 $ \scope1 ->+      cmp scope1+        "substitute o1 s1 t" (substitute scope1 (substValue s1) t)+        "rbind o1 t (lookupSubst s1)" (rbindN scope1 t (lookupSubst (substValue s1)))+  }+  where+    cmp :: Scope x -> String -> AST binder sig x -> String -> AST binder sig x -> Property+    cmp = compareUpToAlpha sg++-- | Compare two terms up to α-equivalence, printing both on failure. The+-- comparison is 'alphaEqNameless', so that these laws do not depend on the+-- library's 'alphaEquiv', which 'alphaSpec' tests.+compareUpToAlpha+  :: (Bitraversable sig, ZipMatchK sig)+  => SyntaxGen binder sig+  -> Scope x -> String -> AST binder sig x -> String -> AST binder sig x -> Property+compareUpToAlpha sg _scope lhsName lhs rhsName rhs =+  counterexample (lhsName <> " = " <> showAST sg lhs) $+    counterexample (rhsName <> " = " <> showAST sg rhs) $+      alphaEqNameless (sgPatternNames sg) lhs rhs++-- * Functoriality of terms++-- | Two ways of renaming terms: the 'Sinkable' instance, and 'liftRM',+-- which goes through 'rbind'.+data FunctorLaws binder sig = FunctorLaws+  { -- | The functor laws of 'sinkabilityProof' on terms, up to α.+    termSinkableLaws      :: SinkableLaws (AST binder sig)+    -- | @liftRM n id t ≡α t@.+  , liftRMIdentity        :: TermCase binder sig -> Property+    -- | @liftRM k (g . f) t ≡α liftRM k g (liftRM l f t)@.+  , liftRMComposition     :: RenamingCase binder sig -> Property+    -- | @liftRM l sink t ≡α sink t@ on an inclusion.+  , liftRMInclusion       :: RenamingCase binder sig -> Property+    -- | @sinkabilityProof f t ≡α liftRM l f t@: the action of the functor+    -- 'Sinkable' agrees with the one derived from the relative monad.+  , sinkAgreesWithLiftRM  :: RenamingCase binder sig -> Property+  }++-- | The functor laws for a language.+functorLaws+  :: forall binder sig.+     (Bitraversable sig, ZipMatchK sig, CoSinkable binder, SinkableK binder)+  => SyntaxGen binder sig -> FunctorLaws binder sig+functorLaws sg = FunctorLaws+  { termSinkableLaws =+      sinkableLaws (\_ a b -> alphaEqNameless (sgPatternNames sg) a b) (showAST sg)+  , liftRMIdentity = \(TermCase n t) -> withCtx n $ \scope ->+      cmp scope "liftRM n id t" (liftRMN scope id t) "t" t+  , liftRMComposition = \(RenamingCase (Chain' _ l k f g _) t) ->+      withCtx l $ \scopeL -> withCtx k $ \scopeK ->+        cmp scopeK+          "liftRM k (g . f) t" (liftRMN scopeK (rename g . rename f) t)+          "liftRM k g (liftRM l f t)" (liftRMN scopeK (rename g) (liftRMN scopeL (rename f) t))+  , liftRMInclusion = \(RenamingCase (Chain' _ l _ _ _ incl) t) -> case incl of+      Nothing -> property Discard+      Just Includes -> withCtx l $ \scopeL ->+        cmp scopeL "liftRM l sink t" (liftRMN scopeL sink t) "sink t" (sink t)+  , sinkAgreesWithLiftRM = \(RenamingCase (Chain' _ l _ f _ _) t) -> withCtx l $ \scopeL ->+      cmp scopeL+        "sinkabilityProof f t" (sinkabilityProof (rename f) t)+        "liftRM l f t" (liftRMN scopeL (rename f) t)+  }+  where+    cmp :: Scope x -> String -> AST binder sig x -> String -> AST binder sig x -> Property+    cmp = compareUpToAlpha sg++-- * Running the laws++-- | The laws of 'RelMonadLaws', by name.+data RelMonadLaw+  = SubstLeftUnit | SubstRightUnit | SubstRightUnitExplicit | SubstAssociativity+  | RbindLeftUnit | RbindRightUnit | RbindAssociativity | SubstituteAgreesWithRbind+  deriving (Eq, Show, Enum, Bounded)++-- | All relative monad laws for a language. The laws on substitutions are+-- checked for each combination of 'SubstKind's, which the verdict is given+-- (it is given 'Nothing' for the laws on terms).+relMonadSpec+  :: (Bitraversable sig, ZipMatchK sig, CoSinkable binder, SinkableK binder)+  => SyntaxGen binder sig -> (RelMonadLaw -> Maybe (SubstKind, SubstKind) -> Verdict) -> Spec+relMonadSpec sg verdict = do+  let laws = relMonadLaws sg+      onTerms name p = law (verdict name Nothing) (show name) $+        forAllShrinkShow (genTermCase sg) shrinkTermCase (showTermCase sg) $ \c@(TermCase n t) ->+          termCoverage n t (p c)+      onSubsts name p = describe (show name) $+        forM_ [ (k1, k2) | k1 <- [minBound .. maxBound], k2 <- [minBound .. maxBound] ] $ \(k1, k2) ->+          law (verdict name (Just (k1, k2))) ("s1 " <> show k1 <> ", s2 " <> show k2) $+            forAllShrinkShow (genSubstCase sg k1 k2) shrinkSubstCase (showSubstCase sg) $ \c ->+              substCoverage c (p c)+  onSubsts SubstLeftUnit (substLeftUnit laws)+  onTerms SubstRightUnit (substRightUnit laws)+  onTerms SubstRightUnitExplicit (substRightUnitExplicit laws)+  onSubsts SubstAssociativity (substAssociativity laws)+  onSubsts RbindLeftUnit (rbindLeftUnit laws)+  onTerms RbindRightUnit (rbindRightUnit laws)+  onSubsts RbindAssociativity (rbindAssociativity laws)+  onSubsts SubstituteAgreesWithRbind (substituteAgreesWithRbind laws)++-- | The laws of 'FunctorLaws' other than those of 'SinkableLaws', by name.+data FunctorLaw = LiftRMIdentity | LiftRMComposition | LiftRMInclusion | SinkAgreesWithLiftRM+  deriving (Eq, Show, Enum, Bounded)++-- | The functor laws of terms: 'sinkabilityProof', 'liftRM', and their+-- agreement, along each class of renamings.+functorSpec+  :: (Bitraversable sig, ZipMatchK sig, CoSinkable binder, SinkableK binder)+  => SyntaxGen binder sig+  -> (RenamingClass -> SinkLaw -> Verdict)+  -> (RenamingClass -> FunctorLaw -> Verdict)+  -> Spec+functorSpec sg sinkVerdict verdict = do+  let laws = functorLaws sg+      onRenamings cls name p = law (verdict cls name) (show name) $+        forAllShrinkShow (genRenamingCase sg cls) shrinkRenamingCase (showRenamingCase sg) $+          \c@(RenamingCase (Chain' n _ _ _ _ _) t) -> termCoverage n t (p c)+  describe "sinkabilityProof" $+    sinkableSpec+      (\_ a b -> alphaEqNameless (sgPatternNames sg) a b)+      (showAST sg)+      (\ctx -> sized (genAST sg ctx . min 30))+      shrinkAST+      sinkVerdict+  describe "liftRM" $ do+    law (verdict Inclusions LiftRMIdentity) (show LiftRMIdentity) $+      forAllShrinkShow (genTermCase sg) shrinkTermCase (showTermCase sg) (liftRMIdentity laws)+    forM_ allRenamingClasses $ \cls -> describe ("along " <> show cls) $ do+      onRenamings cls LiftRMComposition (liftRMComposition laws)+      case cls of+        Inclusions -> onRenamings cls LiftRMInclusion (liftRMInclusion laws)+        _          -> pure ()+  describe "sinkabilityProof and liftRM" $+    forM_ allRenamingClasses $ \cls -> describe ("along " <> show cls) $+      onRenamings cls SinkAgreesWithLiftRM (sinkAgreesWithLiftRM laws)++-- * α-equivalence++-- | α-equivalence by a nameless comparison, independent of the library's+-- 'unifyPatterns'. A bound name is compared by the level of its binder, and+-- 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)+  => PatternNames binder -> AST binder sig x -> AST binder sig y -> Bool+alphaEqNameless binders = go 0 IntMap.empty IntMap.empty+  where+    go :: Int -> IntMap.IntMap Int -> IntMap.IntMap Int -> AST binder sig a -> AST binder sig b -> Bool+    go _ envL envR (Var a) (Var b) =+      case (IntMap.lookup (nameId a) envL, IntMap.lookup (nameId b) envR) of+        (Just i, Just j)   -> i == j+        (Nothing, Nothing) -> nameId a == nameId b+        _                  -> False+    go lvl envL envR (Node l) (Node r) = isJust $+      zipMatchWith2+        (\a b -> guard (scoped lvl envL envR a b))+        (\a b -> guard (go lvl envL envR a b))+        l r+    go _ _ _ _ _ = False++    scoped :: Int -> IntMap.IntMap Int -> IntMap.IntMap Int -> ScopedAST binder sig a -> ScopedAST binder sig b -> Bool+    scoped lvl envL envR (ScopedAST p body1) (ScopedAST q body2) =+      let xs = binders p+          ys = binders q+          k = length xs+          bind env names = foldl (\e (name, i) -> IntMap.insert name i e) env (zip names [lvl ..])+       in length ys == k && go (lvl + k) (bind envL xs) (bind envR ys) body1 body2++-- | The verdict for the agreement of 'sinkabilityProof' with 'liftRM'. Under+-- a binder, 'sinkabilityProof' extends the renaming by a coercion, so the two+-- agree on inclusions only, which is the domain of the laws.+sinkAgreesOnInclusions :: RenamingClass -> Verdict+sinkAgreesOnInclusions Inclusions = Holds+sinkAgreesOnInclusions _          = ByDesign+  "under a binder the renaming is a coercion, so sinkabilityProof agrees with liftRM on inclusions only"++-- | Checks of the library's α-equivalence against 'alphaEqNameless'.+data AlphaLaw+  = AlphaEquivRefreshed'  -- ^ @alphaEquiv n t (refreshAST n t)@: completeness on an α-variant.+  | AlphaEquivAgrees      -- ^ @alphaEquiv@ agrees with 'alphaEqNameless'.+  | AlphaEquivRefreshedAgrees  -- ^ @alphaEquivRefreshed@ agrees with 'alphaEqNameless'.+  deriving (Eq, Show, Enum, Bounded)++-- | A term and a variant of it: an α-variant ('refreshAST'), or an+-- α-variant with one variable occurrence changed.+data PairCase binder sig where+  PairCase :: Ctx n -> AST binder sig n -> AST binder sig n -> PairCase binder sig++genPairCase+  :: (Bitraversable sig, CoSinkable binder, SinkableK binder)+  => SyntaxGen binder sig -> Gen (PairCase binder sig)+genPairCase sg = do+  SomeCtx n <- genCtx+  withCtx n $ \scope -> do+    t <- sized (genAST sg n . min 30)+    let t' = refreshAST scope t+    mutate <- arbitrary+    t'' <- case mutations (ctxNames n) t' of+      ts@(_ : _) | mutate -> elements ts+      _                   -> pure t'+    pure (PairCase n t t'')++-- | The library's α-equivalence checks against 'alphaEqNameless'.+alphaSpec+  :: (Bitraversable sig, ZipMatchK sig, UnifiablePattern binder, SinkableK binder)+  => SyntaxGen binder sig -> (AlphaLaw -> Verdict) -> Spec+alphaSpec sg verdict = do+  law (verdict AlphaEquivRefreshed') "alphaEquiv n t (refreshAST n t)" $+    forAllShrinkShow (genTermCase sg) shrinkTermCase (showTermCase sg) $ \(TermCase n t) ->+      withCtx n $ \scope ->+        counterexample ("refreshAST n t = " <> showAST sg (refreshAST scope t)) $+          alphaEquiv scope t (refreshAST scope t)+  law (verdict AlphaEquivAgrees) "alphaEquiv agrees with a nameless comparison" $+    forAllShow (genPairCase sg) (showPairCase sg) $ \(PairCase n t1 t2) ->+      withCtx n $ \scope -> alphaEquiv scope t1 t2 === alphaEqNameless (sgPatternNames sg) t1 t2+  law (verdict AlphaEquivRefreshedAgrees) "alphaEquivRefreshed agrees with a nameless comparison" $+    forAllShow (genPairCase sg) (showPairCase sg) $ \(PairCase n t1 t2) ->+      withCtx n $ \scope -> alphaEquivRefreshed scope t1 t2 === alphaEqNameless (sgPatternNames sg) t1 t2++-- | Show a 'PairCase'.+showPairCase :: Bifunctor sig => SyntaxGen binder sig -> PairCase binder sig -> String+showPairCase sg (PairCase n t1 t2) = unlines+  [ "n = " <> showCtx n, "t1 = " <> showAST sg t1, "t2 = " <> showAST sg t2 ]

@@ -0,0 +1,196 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- | The laws of "Control.Monad.Free.Foil.Laws" for a language written with+-- the plain foil: its 'Sinkable' instance, 'rbind', 'substitute' and+-- α-equivalence. Terms are generated in a /mirror/, a free foil syntax with+-- the same constructors, and compared by converting them back and using+-- 'alphaEqNameless'.+module Control.Monad.Free.Foil.Laws.Mirror (+  Mirror (..),+  AlphaEquivOf (..),+  MirrorLaw (..),+  mirrorSpec,+) where++import           Control.Monad                (forM_)+import           Data.Bitraversable           (Bitraversable)+import           Test.Hspec+import           Test.QuickCheck++import           Control.Monad.Foil+import           Control.Monad.Foil.Internal  (Substitution (..))+import           Control.Monad.Foil.Laws+import           Control.Monad.Foil.Relative  (RelMonad, liftRM, rbind, rreturn)+import           Control.Monad.Free.Foil      (AST, refreshAST)+import           Control.Monad.Free.Foil.Laws+import           Data.ZipMatchK               (ZipMatchK)++-- | A plain foil language @e@ and its free foil mirror.+data Mirror binder sig e = Mirror+  { mirrorSyntax     :: SyntaxGen binder sig+    -- | From the mirror.+  , mirrorFrom       :: forall n. AST binder sig n -> e n+    -- | To the mirror.+  , mirrorTo         :: forall n. e n -> AST binder sig n+    -- | The language's 'substitute'.+  , mirrorSubstitute :: forall i o. Distinct o => Scope o -> Substitution e i o -> e i -> e o+    -- | The language's α-equivalence, if it has one.+  , mirrorAlphaEquiv :: Maybe (AlphaEquivOf e)+  }++-- | An α-equivalence check of a language.+newtype AlphaEquivOf e = AlphaEquivOf (forall n. Distinct n => Scope n -> e n -> e n -> Bool)++-- | The laws checked by 'mirrorSpec', by name.+data MirrorLaw+  = MirrorSinkable SinkLaw+  | MirrorLiftRMIdentity+  | MirrorLiftRMComposition+  | MirrorSinkAgreesWithLiftRM+  | MirrorSubstLeftUnit+  | MirrorSubstRightUnit+  | MirrorSubstRightUnitExplicit+  | MirrorSubstAssociativity+  | MirrorRbindRightUnit+  | MirrorRbindAssociativity+  | MirrorSubstituteAgreesWithRbind+  | MirrorAlphaEquivRefresh+  | MirrorAlphaEquivAgrees+  deriving (Eq, Show)++-- | Convert the values of a substitution.+mapSubst :: (e o -> e' o) -> Substitution e i o -> Substitution e' i o+mapSubst f (UnsafeSubstitution env) = UnsafeSubstitution (fmap f env)++-- | All the laws for a plain foil language, given a verdict for each law+-- along each class of renamings (the class is 'Inclusions' for the laws+-- that take no renaming).+mirrorSpec+  :: forall binder sig e.+     ( Bitraversable sig, ZipMatchK sig, UnifiablePattern binder, SinkableK binder+     , Sinkable e, InjectName e, RelMonad Name e )+  => Mirror binder sig e+  -> (RenamingClass -> MirrorLaw -> Verdict)+  -> Spec+mirrorSpec m verdict = do+  describe "Sinkable" $+    sinkableSpec (const eqE) showE+      (\ctx -> from <$> sized (genAST sg ctx . min 30))+      (map from . shrinkAST . to)+      (\cls name -> verdict cls (MirrorSinkable name))++  describe "liftRM (through rbind)" $ do+    onTerms MirrorLiftRMIdentity "liftRM n id t ≡α t" $ \n t -> withCtx n $ \scope ->+      cmp "liftRM n id t" (liftRME scope id t) "t" t+    onRenamings MirrorLiftRMComposition "liftRM k (g . f) t ≡α liftRM k g (liftRM l f t)" $+      \(Chain' _ l k f g _) t -> withCtx l $ \scopeL -> withCtx k $ \scopeK ->+        cmp "liftRM k (g . f) t" (liftRME scopeK (rename g . rename f) t)+            "liftRM k g (liftRM l f t)" (liftRME scopeK (rename g) (liftRME scopeL (rename f) t))++  describe "sinkabilityProof and liftRM" $+    onRenamings MirrorSinkAgreesWithLiftRM "sinkabilityProof f t ≡α liftRM l f t" $+      \(Chain' _ l _ f _ _) t -> withCtx l $ \scopeL ->+        cmp "sinkabilityProof f t" (sinkabilityProof (rename f) t)+            "liftRM l f t" (liftRME scopeL (rename f) t)++  describe "substitute" $ do+    onSubsts MirrorSubstLeftUnit "left unit" $ \i scope1 _ s1 _ _ ->+      conjoin [ cmp "substitute o1 s1 x" (subst scope1 s1 (injectName x))+                    "lookupSubst s1 x" (lookupSubst s1 x)+              | x <- ctxNames i ]+    onTerms MirrorSubstRightUnit "right unit" $ \n t -> withCtx n $ \scope ->+      cmp "substitute n identitySubst t" (subst scope identitySubst t) "t" t+    onTerms MirrorSubstRightUnitExplicit "right unit (explicit identity)" $ \n t -> withCtx n $ \scope ->+      cmp "substitute n (explicit identity) t" (subst scope (explicitIdentity n) t) "t" t+    onSubsts MirrorSubstAssociativity "associativity" $ \i scope1 scope2 s1 s2 t ->+      let composite = nameMapToSubstitution $ addNameBinderList (ctxChain i)+            [ subst scope2 s2 (lookupSubst s1 x) | x <- ctxNames i ] emptyNameMap+       in cmp "substitute o2 s2 (substitute o1 s1 t)" (subst scope2 s2 (subst scope1 s1 t))+              "substitute o2 (s2 ⊙ s1) t" (subst scope2 composite t)++  describe "rbind" $ do+    onTerms MirrorRbindRightUnit "right unit" $ \n t -> withCtx n $ \scope ->+      cmp "rbind n t rreturn" (rbindE scope t rreturnE) "t" t+    onSubsts MirrorRbindAssociativity "associativity" $ \_ scope1 scope2 s1 s2 t ->+      let f = lookupSubst s1+          g = lookupSubst s2+       in cmp "rbind o2 (rbind o1 t f) g" (rbindE scope2 (rbindE scope1 t f) g)+              "rbind o2 t (\\x -> rbind o2 (f x) g)" (rbindE scope2 t (\x -> rbindE scope2 (f x) g))+    onSubsts MirrorSubstituteAgreesWithRbind "agrees with substitute" $ \_ scope1 _ s1 _ t ->+      cmp "substitute o1 s1 t" (subst scope1 s1 t)+          "rbind o1 t (lookupSubst s1)" (rbindE scope1 t (lookupSubst s1))++  case mirrorAlphaEquiv m of+    Nothing -> pure ()+    Just (AlphaEquivOf alphaEquivE) -> describe "α-equivalence" $ do+      onTerms MirrorAlphaEquivRefresh "alphaEquiv n t t' for an α-variant t' (refreshAST of the mirror)" $+        \n t -> withCtx n $ \scope ->+          let t' = from (refreshAST scope (to t))+           in counterexample ("t' = " <> showE t') $+                alphaEquivE scope t t'+      law (verdict Inclusions MirrorAlphaEquivAgrees) "alphaEquiv agrees with a nameless comparison" $+        forAllShow (genPairCase sg) (showPairCase sg) $ \(PairCase n t1 t2) -> withCtx n $ \scope ->+          alphaEquivE scope (from t1) (from t2) === alphaEqNameless (sgPatternNames sg) t1 t2+  where+    sg = mirrorSyntax m+    from :: AST binder sig n -> e n+    from = mirrorFrom m+    to :: e n -> AST binder sig n+    to = mirrorTo m+    subst :: Distinct o => Scope o -> Substitution e i o -> e i -> e o+    subst = mirrorSubstitute m++    showE :: e n -> String+    showE = showAST sg . to++    eqE :: e n -> e n -> Bool+    eqE a b = alphaEqNameless (sgPatternNames sg) (to a) (to b)++    cmp :: String -> e n -> String -> e n -> Property+    cmp lhsName lhs rhsName rhs =+      counterexample (lhsName <> " = " <> showE lhs) $+        counterexample (rhsName <> " = " <> showE rhs) $+          eqE lhs rhs++    rbindE :: Distinct o => Scope o -> e i -> (Name i -> e o) -> e o+    rbindE = rbind++    rreturnE :: Name n -> e n+    rreturnE = rreturn++    liftRME :: Distinct o => Scope o -> (Name i -> Name o) -> e i -> e o+    liftRME = liftRM++    explicitIdentity :: Ctx n -> Substitution e n n+    explicitIdentity n =+      nameMapToSubstitution (addNameBinderList (ctxChain n) (map injectName (ctxNames n)) emptyNameMap)++    onTerms :: MirrorLaw -> String -> (forall n. Ctx n -> e n -> Property) -> Spec+    onTerms name title p = law (verdict Inclusions name) title $+      forAllShrinkShow (genTermCase sg) shrinkTermCase (showTermCase sg) $ \(TermCase n t) ->+        p n (from t)++    onRenamings :: MirrorLaw -> String -> (forall n. Chain' n -> e n -> Property) -> Spec+    onRenamings name title p = forM_ allRenamingClasses $ \cls ->+      describe ("along " <> show cls) $ law (verdict cls name) title $+        forAllShrinkShow (genRenamingCase sg cls) shrinkRenamingCase (showRenamingCase sg) $+          \(RenamingCase chain t) -> p chain (from t)++    onSubsts+      :: MirrorLaw -> String+      -> (forall i o1 o2. (Distinct o1, Distinct o2)+            => Ctx i -> Scope o1 -> Scope o2+            -> Substitution e i o1 -> Substitution e o1 o2+            -> e i -> Property)+      -> Spec+    onSubsts name title p = describe title $+      forM_ [ (k1, k2) | k1 <- [minBound .. maxBound], k2 <- [minBound .. maxBound] ] $ \(k1, k2) ->+        law (verdict Inclusions name) ("s1 " <> show k1 <> ", s2 " <> show k2) $+          forAllShrinkShow (genSubstCase sg k1 k2) shrinkSubstCase (showSubstCase sg) $+            \(SubstCase i o1 o2 s1 s2 t) -> withCtx o1 $ \scope1 -> withCtx o2 $ \scope2 ->+              p i scope1 scope2+                (mapSubst from (substValue s1)) (mapSubst from (substValue s2)) (from t)