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

Question

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?

Solifluction

One possible operational consideration: I guess it's probably pretty hard to generate code for a value that must accept a statically-unknown number of typeclass dictionaries as arguments. That's my reading of what something with a type like Function cs '[] () would need to do. – Biofeedback

@DanielWagner: Oh, that makes sense. It also explains why constraint tuples don’t reduce – similar attempts would generate (C1 a, (C2 b, C3 c)) => … and that’s distinct from (C1 a, C2 b, C3 c), to what was my surprise. – Solifluction

Answer 1

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

Kisor

Oh nice! This definitely works for that specific case, but I'm also wondering about the more general one – is there any way to generate constrained functions at all? – Solifluction

@AntalSpector-Zabusky I'm not sure about why your code fails, to be honest. I don't fully understand how general constrained types like T -> (c => U) -> V exactly work. A long time ago, I thought that constraints could be used only after quantifiers e.g. forall a . C a => .... but nowadays more forms seem to be accepted. – Kisor

I think they go where quantifiers go, so you need RankNTypes, but there don't need to be any quantified variables. Anyway, thanks for the answer! Some mysteries of GHC must remain mysterious :-) – Solifluction