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
```

- Comparing lists in Haskell
- Is there a non-identity monad morphism M ~> M that is monadically natural in M?
- Problem with loading module ‘Distribution.Simple’
- Improving efficiency in Stirling numbers calculation
- Does sequencing an infinite list of IO actions by definition result in a never-ending action? Or is there a way to bail out?
- How to call pgQuery from postgresql-query?
- How to avoid whitespace after a tag (link) in Hamlet templates?
- Understanding type-directed resolution in Haskell with existential types
- Why is seq bad?
- Understanding bind function in Haskell
- How to create route that will trigger on any path in Servant?
- How do I use a global state in WAI middleware?
- nixos 23.11 cabal install mysql-simple problem - "Missing (or bad) C libraries"
- Is there a way to kill all forked threads in a GHCi session without restarting it?
- Why can an invalid list expression such as 2:1 be assigned to a variable, but not printed?
- Iterate over a type level list and call a function based on each type in the list
- How does this solution of Project Euler Problem 27 in the Haskell Wiki work?
- Why `Monad` is required to use `pure`?
- Can't do partial function definitions in GHCi
- recommended way to convert Double -> Float in Haskell
- Haskell profiling understanding cost centre summary for anonymous lambda
- Why is Haskell fully declarative?
- GHC Generating Redundant Core Operations
- Question about Event firing in reflex-frp
- Using Haskell's "Maybe", type declarations
- How can I elegantly invert a Map's keys and values?
- Why there is no output for wrapped IO in Haskell?
- What are the definitions of Weather and Memory in xmobar repo?
- Serializing a Data.Text value to a ByteString without unnecessary \NUL bytes
- Using Haskell with VS Code