Re: type level function with different return kinds

Glad you've found your answer :) By the way this is a technique I've 
used in the package fcf-family: 
https://hackage.haskell.org/package/fcf-family

The idea is that given a Name which uniquely identifies a type family, 
it should be possible to map it to, well, the type family it names. You 
will then also need a type family to map to its type, so you get 
essentially this:

type family TypeOf (n :: Name) :: Type
type family Eval (n :: Name) :: TypeOf n

I've used fcf-family to extend kind-generics to enable Generic instances 
for data types that involve type families.

Cheers,
Li-yao

On 2025-04-06 2:43 PM, Tom Smeding wrote:
> I played around a little, and it seems that GHC has some support for 
> dependent quantification here:
>
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE TypeFamilies #-}
> module M where
>
> import GHC.TypeLits
>
> data A = A1 | A2
> data B = B1 | B2
>
> type family K (n :: Nat) where
>   K 0 = A
>   K 1 = A
>   K 2 = B
>   K 3 = B
>
> type F :: forall (n :: Nat) -> K n
> type family F n where
>      F 0 = 'A1
>      F 1 = 'A2
>      F 2 = 'B1
>      F 3 = 'B2
>
> I put it online in a playground paste here: 
> https://play.haskell.org/saved/Pcx912j0
>
> It typechecks, but I didn't test if it indeed works in practice.
>
> On 06-04-2025 00:27, Zoran Bošnjak wrote:
>> Dear haskellers,
>> is it possible to write a type/kind level function that returns types 
>> of different kinds for different inputs. Either by using open/closed 
>> type families, a typeclass, extensions or any other type level magic. 
>> Something like this:
>>
>> {-# LANGUAGE DataKinds #-}
>> {-# LANGUAGE TypeFamilies #-}
>>
>> import GHC.TypeLits
>>
>> data A = A1 | A2
>> data B = B1 | B2
>>
>> type family F (n :: Nat) where
>>     F 0 = 'A1
>>     F 1 = 'A2
>>     F 2 = 'B1
>>     F 3 = 'B2
>>
>> The problem with this approach is that (F 0) and (F 1) are ok, but 
>> not in combination with (F 2). The error says:
>>     • Expected kind ‘A’, but ‘'B1’ has kind ‘B’
>>
>> If I instead write:
>> type family F (n :: Nat) :: k where
>> ... I get compile error already on the (F 0) line
>>     • Expected kind ‘k’, but ‘'A1’ has kind ‘A’
>>
>> Any ideas how to remove the "same kind" restriction or how to 
>> workaround it?
>>
>> I am using ghc 9.6.6.
>>
>> regards,
>> Zoran
>> _______________________________________________
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> Only members subscribed via the mailman list are allowed to post.
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.