How can I combine this closed type family with a dependent type class

Question

My issue

I have the following type family that splits arguments off of a function:

type family
  SeparateArgs
    ( a :: Type )
      :: ( Type, [Type] )
  where
    SeparateArgs (a -> b) =
      SndCons2 a (SeparateArgs b)
    SeparateArgs a =
      '(a, '[])

I also have this typeclass to do the reverse:

class Refunct args goal newSig | args goal -> newSig where
  refunct :: (HList args -> goal) -> newSig
instance Refunct '[] goal goal where
  refunct makeA = makeA HNil
instance
  ( Refunct tailArgs goal c
  )
    => Refunct (headArg ': tailArgs) goal (headArg -> c)
  where
    refunct hFunct x = refunct $ hFunct . (x :>)

Now pretty much every time I use these two, I use them together like the following:

instance
  ( SeparateArgs a ~ '(goal, args)
  , Refunct goal args a
  , ...
  )
    => ...

This is so I can break off the arguments, do some processing to create a function of the type HList args -> goal and then turn it back into a regular function.

This works but it is pretty frustrating since I know that Separate a ~ '(goal, args) => Refunct args goal a, meaning that only one of these statements is needed. However the compiler can't tell that so I need to inform it.

It is of course not critical, since my code currently works, but I would like to roll it into one statement. Ideally by adding a second functional dependency to Refunct like so:

class
  ( SeparateArgs newSig ~ '(goal, args)
  )
    => Refunct args goal newSig
  | args goal -> newSig
  , newSig -> args goal
  where
    refunct :: (HList args -> goal) -> newSig

(Of course this does not work on it's own)

Is there a way to reduce the two (the type family SeparateArgs and the type class Refunct) into a single constraint? I am still willing to define additional constructs I would just like to have non-redundant constraints in the result. I will still need the refunct function.

If it is needed here is my implementation of HList:

data HList (a :: [ Type ]) where
  HNil :: HList '[]
  (:>) :: a -> HList b -> HList (a ': b)

hHead :: HList (a ': b) -> a
hHead (a :> _) = a

hTail :: HList (a ': b) -> HList b
hTail (_ :> b) = b

What I have tried

After discussing this elsewhere it was suggested I try:

type family
  IsAtomic
    ( a :: Type )
      :: Bool
  where
    IsAtomic (a -> b) = 'False
    IsAtomic a = 'True

class
  Refunct args goal newSig
  | args goal -> newSig
  , newSig -> args goal
  where
    refunct :: (HList args -> goal) -> newSig
instance
  ( IsAtomic goal ~ 'True
  )
    =>  Refunct '[] goal goal
  where
  refunct makeA = makeA HNil
instance
  ( Refunct tailArgs goal c
  , IsAtomic (headArg -> c) ~ 'False
  )
    => Refunct (headArg ': tailArgs) goal (headArg -> c)
  where
    refunct hFunct x = refunct $ hFunct . (x :>)

Here we add an additional constrain that the first instance only works if IsAtomic goal ~ 'True and the second only if IsAtomic goal ~ 'False where IsAtomic is a type family I've defined which is 'False on functions and 'True on everything else.

Here the compiler seems to be unable to confirm that the two instances do not violate the functional dependency. The exact error is:

    Functional dependencies conflict between instance declarations:
      instance (IsAtomic goal ~ 'True) => Refunct '[] goal goal
      instance (Refunct tailArgs goal c, IsAtomic goal ~ 'False) =>
               Refunct (headArg : tailArgs) goal (headArg -> c)
    |
XXX |   ( IsAtomic goal ~ 'True
    |   ^^^^^^^^^^^^^^^^^^^^^^^...

(ok it's not exact since I have removed all identifying info).

My intuition here is that it is not aware that IsAtomic goal ~ 'True and IsAtomic goal ~ 'False cannot both be true at the same time. This is reasonable since without inspection, we cannot know IsAtomic is not forall a. a which does satisfy both constraints.

Answer 1

What do we want?

In order to solve this we can first break down what it is that we want.

We want the "falling through" of behavior of a closed type family (so that functions and non-functions will match different instances) but we also want to construct data like a type class (so we can get refunct).

That is we want a type class with the logic of a close type family. So in order to do that we can just separate the two parts and implement them separately; the logic as a closed type family and the rest as a type class.

Now to do that we take our type family and we add another paramenter

class
  Foo
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)

becomes

class
  Foo'
    (flag :: Flag)
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)

This parameter will act as a flag to tell us which instance to use. Since it is of kind Flag we need to make that datatype. It should have a constructor for every instance (we can be a little loose with this in some cases but in general you would want one to one)

data Flag = Instance1 | Instance2 | Instance3 ...

^{(In the case of my issue since there are only two instances we use Bool)}

Now we build a closed type family which calculates which instance to match. It should take the relevant arguments from the parameters of Foo and produce a Flag

type family
  FooInstance
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)
      :: Flag
  where
    FooInstance ... = Instance1
    FooInstance ... = Instance2
    FooInstance ... = Instance3
    ...

^{In the case of the question at hand we call this IsAtomic since that name is descriptive as to what it does.}

Now we modify our instances to match the correct Flags. This is pretty simple we just add the instance flag to the declaration:

instance
  ( Foo newBar newBaz newBax
  ...
  )
    => Foo' 'Instance3 foo bar baz bax
  where
    ...

Importantly we do not change recursive calls to Foo to calls to Foo'. We are about to build Foo as a wrapper around Foo' that manages our closed type family (FooInstance in this case) so we want to call the Foo to avoid envoking the same logic every time.

That is built like this:

class
  Foo
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)
  where
    ...
instance
  ( Foo' (FooInstance bar baz bax) bar baz bax
  )
    => Foo bar baz bax
  where
    ...

If we want to be extra safe we can add a line to each Foo' instance to check that it is being called correctly:

instance
  ( Foo newBar newBaz newBax
  , FooInstance bar baz baz ~ 'Instance3
  ...
  )
    => Foo' 'Instance3 bar baz bax
  where
    ...

My solution

So now we use this strategy on the specific question at hand. Here is the code in full. The relevant class is SeparateArgs:

type family
  IsAtomic
    ( a :: Type )
      :: Bool
  where
    IsAtomic (a -> b) = 'False
    IsAtomic a = 'True

class
  SeparateArgs
    (args :: [Type])
    (goal :: Type)
    (newSig :: Type)
  | args goal -> newSig
  , newSig -> args goal
  where
    refunct :: (HList args -> goal) -> newSig

instance
  ( IsAtomic newSig ~ isAtomic -- For (possible? compilation time) speedup
  , SeparateArgs' isAtomic args goal newSig
  )
    => SeparateArgs args goal newSig
  where
    refunct = refunct' @isAtomic

class
  SeparateArgs'
    (isAtomic :: Bool)
    (args :: [Type])
    (goal :: Type)
    (newSig :: Type)
  | args goal -> newSig isAtomic
  , newSig isAtomic -> args goal
  where
    refunct' :: (HList args -> goal) -> newSig
instance
  ( IsAtomic goal ~ 'True -- Only exists to ensure we are not invoking this in an illegal manner
  )
    => SeparateArgs' 'True '[] goal goal
  where
    refunct' makeA = makeA HNil
instance
  ( IsAtomic (headArg -> c) ~ 'False -- Only exists to ensure we are not invoking this in an illegal manner
  , SeparateArgs tailArgs goal c
  )
    => SeparateArgs' 'False (headArg ': tailArgs) goal (headArg -> c)
  where
    refunct' hFunct x = refunct $ hFunct . (x :>)