Allow more types (terms) in user-defined binders/patterns

fizruk · Oct 29, 2024 · 770de72 · 770de72
1 parent c95abf9
commit 770de72
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 11 deletions.
diff --git a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs
@@ -1086,10 +1086,11 @@ instance GSinkableK (Field (Var a)) where
   gsinkabilityProofK irename (Field x) cont =
     cont irename (Field (unsafeCoerce x)) -- FIXME: unsafeCoerce?
 
-instance SinkableK f => GSinkableK (Field (Kon f :@: Var0)) where
-  gsinkabilityProofK irename@(RCons _ RNil) (Field x) cont =
-    sinkabilityProofK irename x $ \rename' x' ->
-      cont rename' (Field x')
+instance (SinkableK f, ExtractRenamingK i) => GSinkableK (Field (Kon f :@: Var i)) where
+  gsinkabilityProofK irename (Field x) cont =
+    sinkabilityProofK (RCons (extractRenamingK @_ @i irename) RNil) x $ \case
+      RCons rename' RNil -> \x' ->
+        cont (putBackRenamingK @_ @i rename' irename) (Field (unsafeCoerce x')) -- unsafeCoerce?
 
 instance SinkableK (f a) => GSinkableK (Field (Kon f :@: Kon a :@: Var0)) where
   gsinkabilityProofK irename@(RCons _ RNil) (Field x) cont =
@@ -1307,6 +1308,10 @@ instance GHasNameBinders (Field (Var x)) where
   ggetNameBindersRaw (Field _x) = []
   greallyUnsafeSetNameBindersRaw (Field x) names = (Field (unsafeCoerce x), names)  -- FIXME: unsafeCoerce?
 
+instance GHasNameBinders (Field (Kon f :@: Var i)) where
+  ggetNameBindersRaw (Field _x) = []
+  greallyUnsafeSetNameBindersRaw (Field x) names = (Field (unsafeCoerce x), names) -- FIXME: unsafeCoerce?
+
 instance HasNameBinders f => GHasNameBinders (Field (Kon f :@: Var i :@: Var j)) where
   ggetNameBindersRaw (Field x) = getNameBindersRaw x
   greallyUnsafeSetNameBindersRaw (Field x) names =

diff --git a/haskell/free-foil/src/Control/Monad/Foil/Internal/ValidNameBinders.hs b/haskell/free-foil/src/Control/Monad/Foil/Internal/ValidNameBinders.hs
@@ -62,8 +62,6 @@ type ShowSaturatedPatternType pattern oo n l ll =
 
 type GInnerScopeOfAtom :: ErrorMessage -> Nat -> Nat -> (s -> s -> Type) -> Atom d Type -> Atom d s -> Atom d s -> Atom d s -> Atom d s
 type family GInnerScopeOfAtom msg icon ifield pattern atom oo n ll where
-  GInnerScopeOfAtom msg icon ifield pattern (Var x) oo n ll = n
-  GInnerScopeOfAtom msg icon ifield pattern (Kon a) oo n ll = n
   GInnerScopeOfAtom msg icon ifield pattern (Kon f :@: n :@: l) oo n ll = l
   GInnerScopeOfAtom msg icon ifield pattern (Kon f :@: o :@: i) oo n ll =
     TypeError
@@ -77,11 +75,7 @@ type family GInnerScopeOfAtom msg icon ifield pattern atom oo n ll where
       :$$: 'Text "  " :<>: ShowKindedScope oo n ll
       :$$: ShowLocalizeError msg icon ifield pattern oo ll
       )
-  GInnerScopeOfAtom msg icon ifield pattern atom oo n ll =
-    TypeError
-      ('Text "Unexpected atom in a Foil binder/pattern"
-      :$$: 'Text "  " :<>: 'ShowType atom
-      :$$: ShowLocalizeError msg icon ifield pattern oo ll)
+  GInnerScopeOfAtom msg icon ifield pattern atom oo n ll = n
 
 type SameInnerScope :: ErrorMessage -> Nat -> (s -> s -> Type) -> Atom k s -> Atom k s -> Atom k s
 type family SameInnerScope msg icon pattern n l where