Support GSinkableK for binders with arbitrary variables

haskell/free-foil/src/Control/Monad/Foil/Internal.hs

@@ -1088,19 +1088,46 @@ instance SinkableK (f a b) => GSinkableK (Field (Kon f :@: Kon a :@: Kon b :@: V
     sinkabilityProofK irename x $ \rename' x' ->
       cont rename' (Field x')
 
--- FIXME: generalize to arbitary variables
-instance SinkableK f => GSinkableK (Field (Kon f :@: Var0 :@: Var1)) where
-  gsinkabilityProofK irename@(RCons _ (RCons _ RNil)) (Field x) cont =
-    sinkabilityProofK irename x $ \irename' x' ->
-      cont irename' (Field x')
-instance SinkableK f => GSinkableK (Field (Kon f :@: Var1 :@: Var0)) where
-  gsinkabilityProofK (RCons f (RCons g RNil)) (Field x) cont =
-    sinkabilityProofK (RCons g (RCons f RNil)) x $ \(RCons g' (RCons f' RNil)) x' ->
-      cont ((RCons f' (RCons g' RNil))) (Field x')
-instance SinkableK f => GSinkableK (Field (Kon f :@: Var0 :@: Var2)) where
-  gsinkabilityProofK (RCons f (RCons g (RCons h RNil))) (Field x) cont =
-    sinkabilityProofK (RCons f (RCons h RNil)) x $ \(RCons f' (RCons h' RNil)) x' ->
-      cont (RCons f' (RCons g (RCons h' RNil))) (Field x')
+class ExtractRenamingK (i :: TyVar k S) where
+  extractRenamingK :: forall (as :: LoT k) (bs :: LoT k).
+    RenamingsK as bs -> Name (Interpret (Var i) as) -> Name (Interpret (Var i) bs)
+  putBackRenamingK :: forall c (as :: LoT k) (bs :: LoT k).
+       (Name (Interpret (Var i) as) -> Name c)
+    -> RenamingsK as bs
+    -> RenamingsK as (PutBackLoT i c bs)
+
+instance ExtractRenamingK VZ where
+  extractRenamingK (RCons f _fs) = f
+  putBackRenamingK f (RCons _ gs) = RCons f gs
+
+instance ExtractRenamingK x => ExtractRenamingK (VS x) where
+  extractRenamingK (RCons _f fs) = extractRenamingK @_ @x fs
+  putBackRenamingK f (RCons g gs) = RCons g (putBackRenamingK @_ @x f gs)
+
+extractTwoRenamingsK :: forall k (i :: TyVar k S) (j :: TyVar k S) (as :: LoT k) (bs :: LoT k).
+    (ExtractRenamingK i, ExtractRenamingK j)
+  => RenamingsK as bs
+  -> RenamingsK
+      (Interpret (Var i) as :&&: Interpret (Var j) as :&&: LoT0)
+      (Interpret (Var i) bs :&&: Interpret (Var j) bs :&&: LoT0)
+extractTwoRenamingsK irename =
+  (RCons (extractRenamingK @_ @i irename) (RCons (extractRenamingK @_ @j irename) RNil))
+
+putBackTwoRenamingsK :: forall k (i :: TyVar k S) (j :: TyVar k S) c1 c2 (as :: LoT k) (bs :: LoT k).
+    (ExtractRenamingK i, ExtractRenamingK j)
+  => RenamingsK
+      (Interpret (Var i) as :&&: Interpret (Var j) as :&&: LoT0)
+      (c1 :&&: c2 :&&: LoT0)
+  -> RenamingsK as bs
+  -> RenamingsK as (PutBackLoT j c2 (PutBackLoT i c1 bs))
+putBackTwoRenamingsK (RCons f1 (RCons f2 RNil)) rename
+  = putBackRenamingK @_ @j f2 (putBackRenamingK @_ @i f1 rename)
+
+instance (SinkableK f, ExtractRenamingK i, ExtractRenamingK j) => GSinkableK (Field (Kon f :@: Var (i :: TyVar k S) :@: Var (j :: TyVar k S))) where
+  gsinkabilityProofK irename (Field x) cont =
+    sinkabilityProofK (extractTwoRenamingsK @_ @i @j irename) x $ \rename'@(RCons _ (RCons _ RNil)) x' ->
+      cont (putBackTwoRenamingsK @_ @i @j rename' irename)
+           (Field (unsafeCoerce x'))  -- FIXME: can we do better than unsafeCoerce?
 
 instance (Functor f, GSinkableK (Field x)) => GSinkableK (Field (Kon f :@: x)) where
   gsinkabilityProofK irename (Field x) cont =

haskell/free-foil/src/Control/Monad/Foil/Internal/ValidNameBinders.hs

@@ -176,3 +176,8 @@ type family GInnerScopeOfRepK msg icon ifield pattern f o n l where
       ('Text "Unsupported structure in a binder/pattern"
       :$$: 'Text "  " :<>: 'ShowType f
       :$$: ShowLocalizeError msg icon 0 pattern n l)
+
+type PutBackLoT :: TyVar d s -> s -> LoT k -> LoT k
+type family PutBackLoT i c bs where
+  PutBackLoT VZ c (b :&&: bs) = c :&&: bs
+  PutBackLoT (VS x) c (b :&&: bs) = b :&&: PutBackLoT x c bs

haskell/soas/src/Language/SOAS/Impl/Generated.hs

@@ -63,14 +63,31 @@ instance Foil.Sinkable (OpTyping' a)
 instance Foil.SinkableK (Binders' a)
 instance Foil.SinkableK (TypeBinders' a)
 
--- FIXME: derive via GenericK
 instance Foil.HasNameBinders (Binders' a)
 instance Foil.CoSinkable (Binders' a)
 
--- FIXME: derive via GenericK
 instance Foil.HasNameBinders (TypeBinders' a)
 instance Foil.CoSinkable (TypeBinders' a)
 
+data Test a (n :: Foil.S) (l :: Foil.S) where
+  Good1 :: Foil.NameBinder n l -> Test a n l
+  Good2 :: Foil.NameBinder n n -> Test a n n
+  Good3 :: Test a n n
+  Good4 :: Foil.NameBinder n i -> Test a i l -> Test a n l
+  Good5 :: Foil.NameBinder n i' -> Test a i' i -> Test a i l -> Test a n l
+  -- Bad1 :: Test a n l                           -- not enough binders
+  -- Bad2 :: Foil.NameBinder n i -> Test a n l    -- intermediate scope escapes (not enough binders?)
+  -- Bad3 :: Int -> Int -> Int -> Foil.NameBinder i n -> Int -> Test a n l    -- unexpected scope extension
+  -- Bad4 :: Foil.NameBinder l n -> Test a n l    -- unexpected scope extension
+  -- Bad5 :: Foil.NameBinder n i -> Foil.NameBinder i l -> Foil.NameBinder l i -> Test a n l -- intermediate scope escapes (not enough binders?)
+  -- Bad6 :: Foil.NameBinder n l -> Foil.NameBinder n l -> Test a n l -- unexpected scope extension
+  -- Bad7 :: [Foil.NameBinder n l] -> Test a n l -- no GHasNameBinders (unreadable error message)
+deriveGenericK ''Test
+instance Foil.HasNameBinders (Test a)
+instance Foil.SinkableK (Test a)
+instance Foil.CoSinkable (Test a)
+
+
 mkFreeFoilConversions soasConfig
 
 -- | Ignore 'Raw.BNFC'Position' when matching terms.