[SOLVED] Can type families evaluate to qualified types such as `C a => T`?

Can type families evaluate to qualified types such as `C a => T`?

Is there any way to write a type family that sometimes evaluates to a constrained type such as C a => T?

This question arose when I was writing the following type family:

type family Function (cs :: [Constraint]) (as :: [Type]) (r :: Type) :: Type where
  Function (c ': cs) as        r = c => Function cs  as r
  Function '[]       (a ': as) r = a -> Function '[] as r
  Function '[]       '[]       r = r

The goal was that Function '[Integral a, Show b] '[String, b, a] (IO ()) would evaluate to Integral a => Show b => String -> b -> a -> IO (). However, instead, I get the error

    • Illegal qualified type: c => Function cs as r
    • In the equations for closed type family ‘Function’
      In the type family declaration for ‘Function’

I tried using Show c => Function cs as r to see if the issue was with the bare c, but that didn't seem to make a difference. I've tried this with GHC2021 plus the extensions ConstraintKinds, DataKinds, RankNTypes, TypeFamilies, and UndecidableInstances, but I'm happy to add any other language extensions as well if they'll make a difference.

Is there any way to do this? If not, why isn't it possible?

Solution

This compiles. The trick is splitting the constraint part and the type part.

{-# LANGUAGE TypeFamilies, DataKinds #-}

import Data.Kind

-- Handle the list of constraints.
type family Context (cs :: [Constraint]) :: Constraint where
  Context (c ': cs) = (c, Context cs)
  Context '[]       = ()    

-- Handle the list of argument types.
type family Fun (as :: [Type]) (r :: Type) :: Type where
  Fun (a ': as) r = a -> Fun as r
  Fun '[]       r = r

-- Combine both.
type Function (cs :: [Constraint]) (as :: [Type]) (r :: Type)
  = (Context cs) => Fun as r