Add Generic instance for SinkableK

[fizruk]

• Generic implementations for
  • Sinkable
  • CoSinkable
  • UnifiablePattern
• SinkableK generalizes both Sinkable and CoSinkable (except withPattern)
  • ℹ️ f n1 n2 .. nK is treated as a generalized binder with variables/terms in scopes n1, n2, ... nK
• Kind-polymorphic generic instances for SinkableK (covering sinkabilityProof and coSinkabilityProof)
• HasNameBinders generalizes access to nested NameBinders, which makes generic withPattern possible!
  • ✅ UPDATE: we now have a separate check via GValidNameBinders that prevents misuse mentioned below and (sometimes) provides nice error messages. In particular, the following example shows good vs bad constructors in a user-defined pattern:

  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 :: forall b n i' i unused l a. b -> Foil.NameBinder n i' -> Test a i' i -> Test a i l -> Test a n l
    Good6 :: forall a n i l. Term' a n -> Test a n i -> Term' a i -> Test a i l -> Term' a l -> Test a n l
    -- deriving HasNameBinders for any of the constructors below will result in a type error
    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)

  • Current implementation is "slightly" unsafe, but should be fine in practice 🤞
    

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

    Lines 1215 to 1234 in 02a8d1b

    	-- | FIXME: this is, perhaps, the most "unsafe" place for the user
    	-- since it does not reject "parallel" binders:
    	--
    	-- data BadPattern n l = BadPattern (NameBinder n l) (NameBinder n l)
    	--
    	-- This instance will treat both binders in the same way as "nested":
    	--
    	-- data GoodPattern n l = forall i. GoodPattern (NameBinder n i) (NameBinder i l)
    	--
    	-- However, Template Haskell code at the moment will never generate "parallel" binders,
    	-- and the very user is unlikely to misuse this instance, since "parallel" binders
    	-- require extra effort to support it.
    	--
    	-- Still, it would be better to detect and reject any "parallel" or otherwise improper binders.
    	instance (GHasNameBinders f, GHasNameBinders g) => GHasNameBinders (f :*: g) where
    	ggetNameBindersRaw (x :*: y) = ggetNameBindersRaw x <> ggetNameBindersRaw y
    	greallyUnsafeSetNameBindersRaw (x :*: y) names =
    	let (x', names') = greallyUnsafeSetNameBindersRaw x names
    	(y', names'') = greallyUnsafeSetNameBindersRaw y names'
    	in (x' :*: y', names'')

• Use generic instance in examples

Obsolete plan:

• Add an internal GSinkable class and use it for default sinkabilityProof implementation
• Make GSinkable work for GADTs
  • ⚠️ it works for some important examples, but is ad hoc is some places and will easily not work for your definition, in that case you will get a, likely horrific, type error, and will have to resort to manually implementing the instance

[fizruk]

Despite 20+ uses of unsafeCoerce and otherwise ugly generic and type-level stuff in this PR, I do believe, that it provides safer and more general capabilities for the end users.

I am NOT removing Sinkable, CoSinkable, and UnifiablePattern or any of the older Template Haskell just yet to not break too many things at once.

Also I have a feeling that the code will become way simple with another step or two in the generalization direction. In particular, the fact that patterns rely on two type parameters for inner and outer scopes is super annoying to deal with. Also the separation between terms and patterns feels too artificial: patterns may have terms in them!