free-foil 0.3.0 → 0.3.1

raw patch · 11 files changed

+554/−9 lines, 11 filesdep +hspecdep +hspec-discoverdep +kind-generics-thPVP ok

version bump matches the API change (PVP)

Dependencies added: hspec, hspec-discover, kind-generics-th

API changes (from Hackage documentation)

Files

• ChangeLog.md +30/−0
• free-foil.cabal +9/−1
• src/Control/Monad/Foil.hs +7/−0
• src/Control/Monad/Foil/Internal.hs +70/−0
• src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs +118/−6
• test/Control/Monad/Foil/NameMapSpec.hs +53/−0
• test/Control/Monad/Foil/UnifyNameBindersSpec.hs +68/−0
• test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs +73/−0
• test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Config.hs +73/−0
• test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Syntax.hs +52/−0
• test/Spec.hs +1/−2

@@ -1,5 +1,35 @@ # CHANGELOG for `free-foil` +# 0.3.1 — 2026-07-14++A bug fix and a set of additions, all of them prompted by the projects built on free-foil. Nothing is removed or changed, so upgrading from 0.3.0 needs no work.++Fixes:++- `mkFreeFoil` and `mkFreeFoilConversions` generated ill-typed code for a raw constructor whose shape does not line up with the free foil node it becomes (see [#38](https://github.com/fizruk/free-foil/pull/38)):++  ```+  Let    ::= Pattern Term ScopedTerm        -- a term between the pattern and its scope+  LetRec ::= Pattern ScopedTerm ScopedTerm  -- one pattern binding two scopes+  ```++  - The pattern synonym's arguments and its type signature were computed by two traversals that disagreed, and the conversions had the mirror problem.+  - A constructor binding several scopes binds the same raw name in each of them, so raw-to-foil now sends that one binder into every scoped child, and foil-to-raw reads it back from the first.+  - Constructors with at most one scoped child generate exactly what they did before.+  - Reported and diagnosed by [@AbsoluteNikola](https://github.com/AbsoluteNikola), who had to vendor the generated code by hand in [free-foil-refinement-types](https://github.com/AbsoluteNikola/free-foil-refinement-types).++New functions, absorbed from the projects built on free-foil, several of which were importing `Control.Monad.Foil.Internal` to get at them (see [#40](https://github.com/fizruk/free-foil/pull/40)):++- `popNameBinder` — the inverse of `addNameBinder`, for leaving a binder.+- `withFreshNameBinderList` — a fresh binder for each element of a list, bound to it in a `NameMap`.+- `snocNameBinderList` and `concatNameBinderLists`.+- `nameBindersList`, `fromNameBindersList` and `nameMapToScope` are now exported (they existed, but were unreachable).+- With thanks to [@Probirochniy](https://github.com/Probirochniy), [@fedor-ivn](https://github.com/fedor-ivn) and [@snejugal](https://github.com/snejugal) ([free-foil-hou](https://github.com/fedor-ivn/free-foil-hou)), and to [@evermake](https://github.com/evermake), [@frog-da](https://github.com/frog-da) and [@Vikono](https://github.com/Vikono) ([free-foil-typecheck](https://github.com/evermake/free-foil-typecheck)), whose copies of these helpers carried the comment *"Should be in `Control.Monad.Foil`"*.++Documentation:++- `unifyNameBinders` renames the binder with the larger name towards the one with the smaller name. That is safe, since the renaming is pushed through a term with `liftRM`, which refreshes a binder whenever it would capture. The haddock now says so, with a test to match (see [#39](https://github.com/fizruk/free-foil/pull/39)). Raised by [@AbsoluteNikola](https://github.com/AbsoluteNikola).+ # 0.3.0 — 2026-07-14  This release makes generic deriving the default way to instantiate the library:

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           free-foil-version:        0.3.0+version:        0.3.1 synopsis:       Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads) description:    Please see the README on GitHub at <https://github.com/fizruk/free-foil#readme> category:       Parsing@@ -91,6 +91,11 @@   type: exitcode-stdio-1.0   main-is: Spec.hs   other-modules:+      Control.Monad.Foil.NameMapSpec+      Control.Monad.Foil.UnifyNameBindersSpec+      Control.Monad.Free.Foil.TH.MkFreeFoilSpec+      Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config+      Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax       Paths_free_foil   hs-source-dirs:       test@@ -102,7 +107,10 @@     , containers >=0.6 && <0.9     , deepseq >=1.4 && <1.6     , free-foil+    , hspec+    , hspec-discover     , kind-generics >=0.5.0 && <0.6+    , kind-generics-th     , template-haskell >=2.21.0.0 && <2.24     , text >=1.2.3.1 && <2.2   default-language: Haskell2010

@@ -71,10 +71,17 @@   emptyNameMap,   lookupName,   addNameBinder,+  popNameBinder,   nameMapToSubstitution,+  nameMapToScope,   addNameBinders,   addNameBinderList,+  withFreshNameBinderList,   NameBinderList(..),+  nameBindersList,+  fromNameBindersList,+  snocNameBinderList,+  concatNameBinderLists,   -- * Constraints   Ext,   ExtEvidence(..),

@@ -408,6 +408,20 @@  -- | Unify binders either by asserting that they are the same, -- or by providing a /safe/ renaming function to convert one binder to another.+--+-- When the binders differ, the one with the /larger/ name is renamed towards the+-- one with the smaller name. The direction is deliberate, but it is not what makes+-- the renaming safe, and it is worth being explicit about that, since the choice+-- looks arbitrary and has been "fixed" downstream before.+--+-- The renaming returned here is not applied by substituting names blindly: callers+-- push it through a term with 'Control.Monad.Foil.Relative.liftRM', which refreshes+-- a binder whenever it would capture. So the target name may perfectly well be used+-- by a binder /inside/ the term being renamed — a term built in a small scope keeps+-- its small binder names when 'sink' places it in a larger one, so binder names do+-- not always grow with depth — and the result is still correct. See+-- @Control.Monad.Foil.UnifyNameBindersSpec@ for the term that exercises exactly+-- this. unifyNameBinders   :: forall i l r pattern. Distinct i   => NameBinder i l -- ^ Left pattern.@@ -512,6 +526,23 @@     go []     = unsafeCoerce NameBinderListEmpty     go (x:xs) = NameBinderListCons (UnsafeNameBinder (UnsafeName x)) (go xs) +-- | Add a binder to the end of an (ordered) list of binders.+--+-- Note that 'NameBinderListCons' adds a binder to the /front/ of the list, which+-- is the outermost position. This adds one to the innermost position instead.+snocNameBinderList :: NameBinderList n i -> NameBinder i l -> NameBinderList n l+snocNameBinderList NameBinderListEmpty binder =+  NameBinderListCons binder NameBinderListEmpty+snocNameBinderList (NameBinderListCons binder binders) binder' =+  NameBinderListCons binder (snocNameBinderList binders binder')++-- | Concatenate two (ordered) lists of binders, the second extending the scope+-- that the first extends to.+concatNameBinderLists :: NameBinderList n i -> NameBinderList i l -> NameBinderList n l+concatNameBinderLists NameBinderListEmpty binders = binders+concatNameBinderLists (NameBinderListCons binder binders) binders' =+  NameBinderListCons binder (concatNameBinderLists binders binders')+ -- | Convert an ordered list of name binders into an unordered set. fromNameBindersList :: NameBinderList n l -> NameBinders n l fromNameBindersList = UnsafeNameBinders . IntSet.fromList . go@@ -901,6 +932,45 @@ -- Note that the scope parameter of the result differs from the initial map. addNameBinder :: NameBinder n l -> a -> NameMap n a -> NameMap l a addNameBinder name x (NameMap m) = NameMap (IntMap.insert (nameId (nameOf name)) x m)++-- | Remove the mapping for a binder, shrinking the map back to the outer scope.+--+-- This is the inverse of 'addNameBinder', and is what a type checker wants when+-- it leaves a binder it has entered.+popNameBinder :: NameBinder n l -> NameMap l a -> NameMap n a+popNameBinder binder (NameMap m) = NameMap (IntMap.delete (nameId (nameOf binder)) m)++-- | Allocate a fresh binder for each element of a list, binding each element to+-- its binder in the map.+--+-- The continuation receives the extended scope, the binders in the order of the+-- input list, and the extended map. This is the list-shaped counterpart of+-- 'withFresh', and saves a caller from threading the scope, the binders, and the+-- map through a recursion by hand.+withFreshNameBinderList+  :: forall n a r. Distinct n+  => [a]                  -- ^ A value to bind to each fresh binder.+  -> Scope n              -- ^ The ambient scope.+  -> NameMap n a          -- ^ The map to extend.+  -> (forall l. DExt n l => Scope l -> NameBinderList n l -> NameMap l a -> r)+  -> r+withFreshNameBinderList xs0 scope0 nameMap0 cont =+    go xs0 scope0 NameBinderListEmpty nameMap0 cont+  where+    go :: forall i r'. Distinct i+       => [a] -> Scope i -> NameBinderList n i -> NameMap i a+       -> (forall l. DExt n l => Scope l -> NameBinderList n l -> NameMap l a -> r')+       -> r'+    go [] scope binders nameMap cont' =+      case (assertDistinct binders, assertExt binders) of+        (Distinct, Ext) -> cont' scope binders nameMap+    go (x:xs) scope binders nameMap cont' =+      withFresh scope $ \binder ->+        go xs+           (extendScope binder scope)+           (snocNameBinderList binders binder)+           (addNameBinder binder x nameMap)+           cont'  -- * Raw types and operations 

@@ -21,7 +21,8 @@ import qualified Control.Monad.Free.Foil    as Foil import           Data.Bifunctor import           Data.List                  (find, unzip4, (\\), nub)-import           Data.Maybe                 (catMaybes, mapMaybe)+import           Data.Maybe                 (catMaybes, listToMaybe, mapMaybe,+                                             maybeToList) import Data.Map (Map) import qualified Data.Map as Map import qualified GHC.Generics               as GHC@@ -333,6 +334,23 @@       ForallC params ctx con -> ForallC params ctx <$> go con       RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) +-- | Is this raw field a binding (pattern) field?+--+-- Such a field has no counterpart in the free foil node: the binder it stands for+-- lives inside the 'Foil.ScopedAST' of each scoped child.+isBindingField :: FreeFoilConfig -> Type -> Bool+isBindingField FreeFoilConfig{..} = \case+  PeelConT typeName _ | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> True+  _ -> False++-- | Is this raw field a scoped-term field?+--+-- Such a field becomes a 'Foil.ScopedAST', which carries a binder of its own.+isScopeField :: FreeFoilConfig -> Type -> Bool+isScopeField FreeFoilConfig{..} = \case+  PeelConT typeName _ | Just _ <- lookupScopeName typeName freeFoilTermConfigs -> True+  _ -> False+ termConToPat :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [([Name], Pat, Pat, [Exp])] termConToPat rawTypeName config@FreeFoilConfig{..} FreeFoilTermConfig{..} = go   where@@ -384,8 +402,40 @@       GadtC conNames rawArgTypes _rawRetType -> concat <$> do         forM conNames $ \conName -> do           let newConName = toSignatureName config conName-          (concat -> vars, concat -> pats, concat -> pats', concat -> exps) <- unzip4 <$>-            mapM (fromArgType . snd) rawArgTypes+          perField <- mapM (fromArgType . snd) rawArgTypes+          let (concat -> vars, concat -> pats, _, _) = unzip4 perField+              -- These expressions rebuild the /raw/ constructor, whose fields are+              -- shaped differently from the free foil node's: the raw constructor+              -- has a single binding (pattern) field and its scoped fields carry+              -- no binder of their own, whereas in the free foil every scoped+              -- child carries its own binder. So a scoped child contributes only+              -- its body here, and the binding field is filled from the first+              -- scoped child's binder -- the raw syntax can name only one binder,+              -- and a constructor that binds several scopes binds the same name+              -- in each of them.+              firstScopeBinder = listToMaybe+                [ binder+                | (rawArgType, (binder : _, _, _, _)) <- zip (map snd rawArgTypes) perField+                , isScopeField config rawArgType ]+              rawFieldExp rawArgType (_, _, _, fieldExps)+                | isBindingField config rawArgType = map VarE (maybeToList firstScopeBinder)+                | isScopeField config rawArgType   = drop 1 fieldExps  -- the body; the binder is not a raw field+                | otherwise                        = fieldExps+              exps = concat (zipWith rawFieldExp (map snd rawArgTypes) perField)+              -- Only the first scoped child's binder makes it back into the raw+              -- syntax (see above), so matching the others' binders would bind a+              -- variable we never use.+              sigPats = goSigPats True (zip (map snd rawArgTypes) perField)+              goSigPats _ [] = []+              goSigPats isFirstScope ((rawArgType, (_, _, fieldPats, _)) : rest)+                | isScopeField config rawArgType =+                    (if isFirstScope then fieldPats else map ignoreBinder fieldPats)+                      ++ goSigPats False rest+                | otherwise = fieldPats ++ goSigPats isFirstScope rest+              ignoreBinder = \case+                TupP [_binder, body] -> TupP [WildP, body]+                p                    -> p+              pats' = sigPats           return $             if rawTypeName == rawTermName               then [ (vars, ConP 'Foil.Node [] [ConP newConName [] pats], ConP newConName [] pats', exps) ]@@ -521,6 +571,52 @@       ForallC _params _ctx con -> go con       RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) +-- | Argument types of a pattern synonym for a single raw constructor.+--+-- This has to agree with 'termConToPat', which decides what the synonym's+-- /arguments/ are, and the two used to disagree:+--+-- * a raw binding (pattern) field contributes __no__ argument, since a binder+--   in the free foil lives inside the 'Foil.ScopedAST' it binds, not beside it;+-- * a raw scoped-term field contributes __two__ arguments, a binder and a body;+-- * every other field contributes one argument, as before.+--+-- Crucially, each scoped-term field gets a __fresh__ inner scope: a constructor+-- with several scoped children (a recursive @let@, say) binds a separate name in+-- each of them, so sharing one scope variable between them is wrong. A+-- constructor with at most one scoped child keeps the inner scope named @i@,+-- so the generated code for such constructors is unchanged.+patternSynonymArgTypes :: FreeFoilConfig -> Type -> Type -> [Type] -> [Type]+patternSynonymArgTypes config@FreeFoilConfig{..} outerScope innerScope rawArgTypes =+    go (1 :: Int) rawArgTypes+  where+    -- Only when there are several scoped children do we need to number the+    -- scopes; with one child, @i@ keeps the generated code as it was.+    scopeCount = length (filter (isScopeField config) rawArgTypes)+    innerScopeFor k+      | scopeCount <= 1 = innerScope+      | otherwise       = VarT (mkName ("i" ++ show k))++    go _ [] = []+    go k (rawArgType : rest) = case rawArgType of+      PeelConT typeName _params+        -- The binder is an argument of the ScopedAST, not of the node.+        | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> go k rest+        -- A scoped child: its own binder, then its body, in its own scope.+        | Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs ->+            let inner = innerScopeFor k+                rawBindingType = PeelConT rawBindingName (typeParamsOf rawArgType)+             in toFreeFoilType SortTerm config outerScope inner rawBindingType+                  : toFreeFoilType SortTerm config outerScope inner rawArgType+                  : go (k + 1) rest+      _ -> toFreeFoilType SortTerm config outerScope innerScope rawArgType : go k rest++    -- A scoped type and its binding type are parametrised alike (both carry the+    -- annotation type, if any), so the binder type reuses the scope's parameters.+    typeParamsOf = \case+      PeelConT _ params -> params+      _                 -> []+ mkPatternSynonym :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [(Name, [Dec])] mkPatternSynonym rawTypeName config termConfig@FreeFoilTermConfig{..} rawRetType = go   where@@ -529,16 +625,18 @@       GadtC conNames rawArgTypes _rawRetType -> concat <$> do         forM (conNames \\ [rawVarConName]) $ \conName -> do           let patName = toConName config conName-              rawConType = foldr (\x y -> AppT (AppT ArrowT x) y) rawRetType (map snd rawArgTypes)               outerScope = VarT (mkName "o")               innerScope                 | rawTypeName `elem` rawSubScopeNames = outerScope                 | otherwise = VarT (mkName "i")+              synType = foldr (\x y -> AppT (AppT ArrowT x) y)+                (toFreeFoilType SortTerm config outerScope innerScope rawRetType)+                (patternSynonymArgTypes config outerScope innerScope (map snd rawArgTypes))           [(vars, pat, _, _)] <- termConToPat rawTypeName config termConfig (GadtC [conName] rawArgTypes rawRetType)    -- FIXME: unsafe matching!           addModFinalizer $ putDoc (DeclDoc patName)             ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Pattern synonym for an '" ++ show ''Foil.AST ++ "' node of type '" ++ show conName ++ "'.")           return [(patName,-            [ PatSynSigD patName (toFreeFoilType SortTerm config outerScope innerScope rawConType)+            [ PatSynSigD patName synType             , PatSynD patName (PrefixPatSyn vars) ImplBidir pat             ])] @@ -1187,6 +1285,19 @@ sigConToClause :: Sort -> Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause] sigConToClause sort rawRetType config@FreeFoilConfig{..} FreeFoilTermConfig{..} = go   where+    -- Matching a raw constructor, we must bind exactly one variable per raw+    -- field. The binding (pattern) field binds @theBinder@, and each scoped+    -- field binds only a body -- and then every scoped child of the free foil+    -- node is given /the same/ @theBinder@, since the raw syntax names one+    -- binder and a constructor binding several scopes binds it in each of them.+    fromRawArgType :: Bool -> Name -> Name -> Type -> Q ([Pat], [Exp])+    fromRawArgType isVarCon theIdent theBinder rawArgType+      | isBindingField config rawArgType = return ([VarP theBinder], [])+      | isScopeField config rawArgType = do+          body <- newName "body"+          return ([VarP body], [TupE [Just (VarE theBinder), Just (VarE body)]])+      | otherwise = fromArgType isVarCon theIdent rawArgType+     fromArgType :: Bool -> Name -> Type -> Q ([Pat], [Exp])     fromArgType isVarCon theIdent = \case       PeelConT typeName _params@@ -1227,11 +1338,12 @@     go = \case       GadtC conNames rawArgTypes _rawRetType -> concat <$> do         theIdent <- newName "_theRawIdent"+        theBinder <- newName "binder"         forM conNames $ \conName -> do           let newConName = toSignatureName config conName               isVarCon = conName == rawVarConName           (concat -> pats, concat -> exps) <- unzip <$>-            mapM (fromArgType isVarCon theIdent . snd) rawArgTypes+            mapM (fromRawArgType isVarCon theIdent theBinder . snd) rawArgTypes           case sort of             SortTerm               | isVarCon -> return

@@ -0,0 +1,53 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs     #-}++-- | Helpers for 'Foil.NameMap' and 'Foil.NameBinderList'.+module Control.Monad.Foil.NameMapSpec (spec) where++import           Data.Foldable      (toList)+import           Test.Hspec++import qualified Control.Monad.Foil as Foil++-- | The raw names bound by a list of binders, outermost first.+binderIds :: Foil.NameBinderList n l -> [Int]+binderIds Foil.NameBinderListEmpty = []+binderIds (Foil.NameBinderListCons binder binders) =+  Foil.nameId (Foil.nameOf binder) : binderIds binders++spec :: Spec+spec = do+  describe "withFreshNameBinderList" $ do+    it "binds each value to a fresh binder, in order" $+      Foil.withFreshNameBinderList "abc" Foil.emptyScope Foil.emptyNameMap $+        \_scope binders nameMap -> do+          binderIds binders `shouldBe` [0, 1, 2]   -- a fresh name is max scope + 1+          toList nameMap `shouldBe` "abc"++    it "binds nothing when there is nothing to bind" $+      Foil.withFreshNameBinderList ([] :: [Int]) Foil.emptyScope Foil.emptyNameMap $+        \_scope binders nameMap -> do+          binderIds binders `shouldBe` []+          toList nameMap `shouldBe` []++  describe "popNameBinder" $+    it "undoes addNameBinder" $+      Foil.withFresh Foil.emptyScope $ \binder ->+        let nameMap = Foil.addNameBinder binder 'x' Foil.emptyNameMap+         in toList (Foil.popNameBinder binder nameMap) `shouldBe` ""++  describe "snocNameBinderList" $+    it "adds a binder to the innermost position" $+      Foil.withFreshNameBinderList "ab" Foil.emptyScope Foil.emptyNameMap $+        \scope binders _nameMap ->+          Foil.withFresh scope $ \binder ->+            binderIds (Foil.snocNameBinderList binders binder) `shouldBe` [0, 1, 2]++  describe "concatNameBinderLists" $+    it "agrees with snocNameBinderList on a singleton" $+      Foil.withFreshNameBinderList "ab" Foil.emptyScope Foil.emptyNameMap $+        \scope binders _nameMap ->+          Foil.withFresh scope $ \binder ->+            let singleton = Foil.NameBinderListCons binder Foil.NameBinderListEmpty+             in binderIds (Foil.concatNameBinderLists binders singleton)+                  `shouldBe` binderIds (Foil.snocNameBinderList binders binder)

@@ -0,0 +1,68 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE PatternSynonyms     #-}+{-# LANGUAGE ScopedTypeVariables #-}++-- | 'Foil.unifyNameBinders' renames the binder with the /larger/ name towards the+-- one with the smaller name. This module pins that down, because the choice looks+-- arbitrary and is not: it is safe, but only because the renaming it asks for is+-- applied by a capture-avoiding substitution.+--+-- A fresh name is @max scope + 1@, so binder names normally grow as one goes+-- deeper into a term. They do not have to: 'Foil.sink' is a coercion, so a term+-- built in a small scope keeps its (small) binder names when it is placed inside+-- a larger one. A term whose /outer/ binder is named after its /inner/ one is+-- therefore reachable, and it is the term that makes the direction of the+-- renaming observable.+module Control.Monad.Foil.UnifyNameBindersSpec (spec) where++import           Data.Maybe                                       (fromJust)+import           Test.Hspec++import qualified Control.Monad.Foil                               as Foil+import           Control.Monad.Free.Foil++import           Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax++-- | @\\x. x@, with the binder named @max scope + 1@.+identityIn :: Foil.Distinct n => Foil.Scope n -> FFTerm n+identityIn scope = Foil.withFresh scope $ \binder ->+  case Foil.assertDistinct binder of+    Foil.Distinct -> FFFun (FFPatternVar binder) (Var (Foil.nameOf binder))++-- | @\\x. \\y. y@, built outside-in: the outer binder is named 0, the inner 1.+nestedNormal :: FFTerm Foil.VoidS+nestedNormal = Foil.withFresh Foil.emptyScope $ \outer ->+  case Foil.assertDistinct outer of+    Foil.Distinct ->+      FFFun (FFPatternVar outer) (identityIn (Foil.extendScope outer Foil.emptyScope))++-- | The same term, @\\x. \\y. y@, built inside-out: the outer binder is named 1+-- and the inner one 0, so the names run backwards.+nestedInverted :: FFTerm Foil.VoidS+nestedInverted = fromJust $+  Foil.withFresh Foil.emptyScope $ \(binder0 :: Foil.NameBinder Foil.VoidS n1) ->+    case Foil.assertDistinct binder0 of+      Foil.Distinct ->+        let scope1 = Foil.extendScope binder0 Foil.emptyScope+            inner  = Foil.sink (identityIn Foil.emptyScope) :: FFTerm n1  -- binder named 0+         in Foil.withFresh scope1 $ \outer ->                             -- named 1+              case Foil.assertDistinct outer of+                Foil.Distinct ->+                  unsinkAST Foil.emptyScope+                    (FFFun (FFPatternVar outer) (Foil.sink inner))++spec :: Spec+spec = describe "unifyNameBinders (via alphaEquiv)" $ do+  it "identifies two spellings of the same term whose binder names run opposite ways" $+    -- Unifying the two outer binders renames the right one (1) down to the left+    -- one (0) -- onto a name a binder /inside that very body/ already uses. The+    -- renaming is applied with 'liftRM', which refreshes on a clash, so it does+    -- not capture. Renaming towards the smaller name is therefore safe, and this+    -- is the example that says so.+    alphaEquiv Foil.emptyScope nestedNormal nestedInverted `shouldBe` True++  it "is symmetric on that pair" $+    alphaEquiv Foil.emptyScope nestedInverted nestedNormal `shouldBe` True++  it "still tells genuinely different terms apart" $+    alphaEquiv Foil.emptyScope nestedNormal (identityIn Foil.emptyScope) `shouldBe` False

@@ -0,0 +1,73 @@+{-# LANGUAGE DataKinds       #-}+{-# LANGUAGE PatternSynonyms #-}++-- | Regression tests for 'mkFreeFoil' and 'mkFreeFoilConversions' on raw+-- constructors whose shape does not line up with the free foil node they become.+--+-- That "Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax" compiles at all is half+-- the test: the generated pattern synonyms and conversions used to be ill-typed+-- for @Let@ and @LetRec@. These examples are the other half — they check that a+-- raw binder still binds what it used to.+module Control.Monad.Free.Foil.TH.MkFreeFoilSpec (spec) where++import qualified Control.Monad.Foil                               as Foil+import qualified Data.Map                                         as Map+import           Test.Hspec++import           Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config+import           Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax++-- | Convert a closed raw term into the scope-safe representation and back.+--+-- Binders come back renamed (that is what 'intToVarIdent' is for), so the+-- examples below check how names /relate/, not what they are called.+roundtrip :: Term -> Term+roundtrip = fromTerm . toTerm Foil.emptyScope Map.empty++x, y :: VarIdent+x = VarIdent "x"+y = VarIdent "y"++-- | A closed term, to use where a term must not mention the surrounding binder.+identity :: Term+identity = Fun (PatternVar y) (ScopedTerm (Var y))++spec :: Spec+spec = do+  describe "a pattern adjacent to its scope (Fun)" $+    it "round-trips, and the body still refers to the binder" $+      case roundtrip (Fun (PatternVar x) (ScopedTerm (Var x))) of+        Fun (PatternVar binder) (ScopedTerm (Var v)) -> v `shouldBe` binder+        other -> expectationFailure ("unexpected shape: " <> show other)++  describe "a pattern separated from its scope (Let)" $ do+    it "puts the binder in the binding position, not the bound term's" $+      -- The generated conversions used to hand the raw constructor its arguments+      -- in the free foil node's order rather than the raw one, which put the+      -- bound term where the pattern belongs.+      case roundtrip (Let (PatternVar x) identity (ScopedTerm (Var x))) of+        Let (PatternVar binder) bound (ScopedTerm (Var v)) -> do+          v `shouldBe` binder                 -- the body refers to the binder+          bound `shouldSatisfy` isFun         -- the bound term is still a term+        other -> expectationFailure ("unexpected shape: " <> show other)++  describe "one pattern binding two scopes (LetRec)" $ do+    it "binds the same name in both scopes" $+      -- Each scoped child of a free foil node carries its own binder, so the two+      -- scopes get two distinct foil names. The raw syntax has only one pattern,+      -- so converting back must give both scopes the same name again.+      case roundtrip (LetRec (PatternVar x) (ScopedTerm (Var x)) (ScopedTerm (Var x))) of+        LetRec (PatternVar binder) (ScopedTerm (Var v1)) (ScopedTerm (Var v2)) -> do+          v1 `shouldBe` binder+          v2 `shouldBe` binder+        other -> expectationFailure ("unexpected shape: " <> show other)++    it "keeps the two scopes apart" $+      case roundtrip (LetRec (PatternVar x) (ScopedTerm identity) (ScopedTerm (Var x))) of+        LetRec (PatternVar binder) (ScopedTerm first) (ScopedTerm (Var v)) -> do+          first `shouldSatisfy` isFun   -- the first scope does not mention the binder+          v `shouldBe` binder           -- the second one does+        other -> expectationFailure ("unexpected shape: " <> show other)+  where+    isFun Fun{} = True+    isFun _     = False

@@ -0,0 +1,73 @@+{-# LANGUAGE TemplateHaskell #-}++-- | A raw syntax in the shape BNFC produces, used to test 'mkFreeFoil'.+--+-- The interesting constructors are the ones whose /raw/ shape does not line up+-- with the free foil node they become:+--+-- * @Let@ has a pattern, a term, and one scoped term (so the pattern is not+--   adjacent to the scope it binds);+-- * @LetRec@ has a pattern and __two__ scoped terms (so one raw binder binds+--   two separate scopes).+--+-- Both used to generate ill-typed code. See the spec.+--+-- The config lives in its own module because Template Haskell may not splice a+-- value defined in the same module.+module Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config where++import           Control.Monad.Free.Foil.TH.MkFreeFoil++newtype VarIdent = VarIdent String+  deriving (Eq, Ord, Show)++newtype Pattern = PatternVar VarIdent+  deriving (Eq, Show)++newtype ScopedTerm = ScopedTerm Term+  deriving (Eq, Show)++data Term+  = Var VarIdent+  | App Term Term+  | Fun Pattern ScopedTerm                -- ^ pattern, then its scope (this always worked)+  | Let Pattern Term ScopedTerm           -- ^ a term between the pattern and its scope+  | LetRec Pattern ScopedTerm ScopedTerm  -- ^ one pattern binding two scopes+  deriving (Eq, Show)++rawVar :: VarIdent -> Term+rawVar = Var++intToVarIdent :: Int -> VarIdent+intToVarIdent i = VarIdent ("x" <> show i)++rawScopedTerm :: Term -> ScopedTerm+rawScopedTerm = ScopedTerm++rawScopeToTerm :: ScopedTerm -> Term+rawScopeToTerm (ScopedTerm t) = t++config :: FreeFoilConfig+config = FreeFoilConfig+  { rawQuantifiedNames = []+  , freeFoilTermConfigs =+      [ FreeFoilTermConfig+          { rawIdentName = ''VarIdent+          , rawTermName = ''Term+          , rawBindingName = ''Pattern+          , rawScopeName = ''ScopedTerm+          , rawVarConName = 'Var+          , rawSubTermNames = []+          , rawSubScopeNames = []+          , intToRawIdentName = 'intToVarIdent+          , rawVarIdentToTermName = 'rawVar+          , rawTermToScopeName = 'rawScopedTerm+          , rawScopeToTermName = 'rawScopeToTerm+          } ]+  , freeFoilNameModifier = ("FF" ++)+  , freeFoilScopeNameModifier = ("FFScoped" ++)+  , freeFoilConNameModifier = ("FF" ++)+  , freeFoilConvertFromName = ("from" ++)+  , freeFoilConvertToName = ("to" ++)+  , signatureNameModifier = (++ "Sig")+  }

@@ -0,0 +1,52 @@+{-# LANGUAGE DataKinds         #-}+{-# LANGUAGE DeriveGeneric     #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleContexts  #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs             #-}+{-# LANGUAGE KindSignatures    #-}+{-# LANGUAGE LambdaCase        #-}+{-# LANGUAGE PatternSynonyms   #-}+{-# LANGUAGE RankNTypes        #-}+{-# LANGUAGE TemplateHaskell   #-}+{-# LANGUAGE TypeFamilies      #-}+-- Generated conversions carry a redundant @Ord@ constraint; 'soas' silences the+-- same warning in its generated module, as it does the orphan 'ZipMatchK'+-- instance for the raw identifier type.+{-# OPTIONS_GHC -Wno-missing-signatures -Wno-redundant-constraints -Wno-orphans #-}++-- | The scope-safe syntax generated from+-- "Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config".+--+-- That this module /compiles at all/ is the regression test: before the fix,+-- 'mkFreeFoil' and 'mkFreeFoilConversions' generated ill-typed code for @Let@+-- and @LetRec@ (a pattern synonym whose signature disagreed with its arguments,+-- and conversions that gave the raw constructor the wrong number of arguments in+-- the wrong order).+module Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax where++import qualified Control.Monad.Foil                              as Foil+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.Config++mkFreeFoil config++deriveGenericK ''FFPattern+instance Foil.SinkableK FFPattern+instance Foil.HasNameBinders FFPattern+instance Foil.CoSinkable FFPattern+instance Foil.UnifiablePattern FFPattern++deriveBifunctor ''TermSig+deriveBifoldable ''TermSig+deriveBitraversable ''TermSig++deriveGenericK ''TermSig+instance ZipMatchK VarIdent where zipMatchWithK = zipMatchViaEq+instance ZipMatchK TermSig++mkFreeFoilConversions config

@@ -1,2 +1,1 @@-main :: IO ()-main = putStrLn "Test suite not yet implemented"+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}