How to constrain kinds in a type family

Question

In a recent question of mine I found an answer using a type class of kinds. NB that in HasNProxyK k, k is the kind of the second NProxyK parameter.

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}

import GHC.TypeLits hiding ( (*) )
import Data.Kind

class HasNProxyK j where
  data NProxyK (n :: Nat) (a::j) :: k
instance HasNProxyK Type where
  data NProxyK n a = NProxyK0
instance HasNProxyK k => HasNProxyK (j -> k) where
  data NProxyK n f = NProxyKSuc -- or NProxyKS (ProxyK n (f a))

type family ToNProxyK (n :: Nat) (a :: k) :: k where
  ToNProxyK n (a :: Type) = NProxyK n a
  ToNProxyK n (a :: j -> k) = NProxyK n a

I'm unsatisfied with the above in at least one way. I would have liked to declare the type family with a constraint in its kind, something like:

type family ToNProxyK (n :: Nat) (a :: HasNProxyK k => k) :: k where
   ToNProxyK n (a::Type) = Type
   ToNProxyK n (a :: j -> k) = NProxyK n a

My intent being that I'm constraining the kind of a to belong to HasNProxyK. And in order to use the type family i must know that the class instance is satisfied--hopefully catching declarations like ToNProxyK 3 True at compilation. However, when I try the above ghc tells me:

src/Traversal.hs:359:15: error:
    • Expected kind ‘HasNProxyK k0 => k0’,
        but ‘(a :: Type)’ has kind ‘*’
    • In the second argument of ‘ToNProxyK’, namely ‘(a :: Type)’
      In the type family declaration for ‘ToNProxyK’
    |
359 |   ToNProxyK n (a :: Type) = NProxyK n a
    |               ^^^^^^^^^^^

What I get from this is that I'm not actually declaring what I think I'm declaring. That I've specified a new kind, not just restricted the kinds which are accepted. I've also tried including the constraint in the member types (HasNProxyK Type => Type) but that just leads to other problems.

So, what am I actually declaring in my constrained kind family? Is there a way to constrain k in this type family to disallow types such as ToNProxyK n True?

chi chi · Accepted Answer · 2019-05-20T16:01:45

I can't find a perfect way to achieve a constrained closed type family, which is what you want, as far as I can understand.

However, for your specific case, it might be enough to use a type family declared inside a type class, which allows to constrain k as you wish.

class HasNProxyK k => C k (n :: Nat) (a :: k) where
    type ToNProxyK k n a :: k

instance C Type n a where
    type ToNProxyK Type n a = NProxyK n a

instance HasNProxyK k => C (j -> k) n a where
    type ToNProxyK (j -> k) n a = NProxyK n a

By doing that, we lose the "top-down" handling of closed type families. In your case, there is no overlap between Type and j -> k, so it should not be an issue.

Simpler variant:

class HasNProxyK k => C k where
    type ToNProxyK k (n :: Nat) (a :: k) :: k

instance C Type where
    type ToNProxyK Type n a = NProxyK n a

instance HasNProxyK k => C (j -> k) where
    type ToNProxyK (j -> k) n a = NProxyK n a

How to constrain kinds in a type family

1 Answers