haskelltype-familiestype-level-computation

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