Partial type family application-CodePudding

This recursive definition of T fails to type-check.

class C a where
  type T a :: Type

newtype Compose (f :: Type -> Type) (g :: Type -> Type) (a :: Type) = Compose {getCompose :: f (g a)}

instance C (Maybe a) where
  type T (Maybe a) = NP (Compose T Identity) '[a]

Specific error:

    • The associated type family ‘T’ should have 1 argument, but has been given none
    • In the type instance declaration for ‘T’
      In the instance declaration for ‘C (Maybe a)’
   |
32 |   type T (Maybe a) = NP (Compose T Identity) '[a]
   |        ^

Why is GHC unable to do this?
Is there a workaround?

The real class/instance looks like this:

instance Ema (MultiSite models) where
  type RouteFor (MultiSite models) = NP (Compose RouteFor Site) models

This says that "the route for a multisite is an n-ary product of the routes for the individual sites", hence RouteFor has to be defined recursively.

CodePudding user response：

Type families are unmatchable and must be fully saturated. This means they can not be passed partially applied as an argument. This is basically what the error message says

• The associated type family ‘T’ should have 1 argument, but has been given none

At the present time this is not distinguished at the kind level (see Unsaturated type families proposal) but there is a very clear distinction within GHC.

According to :kind both T and Identity have the same kind while in reality Identity is Matchable and T is Unmatchable:

Identity :: Type -> @M Type
T        :: Type -> @U Type

Because the arguments of Compose are Type -> @M Type you cannot pass an unmatchable type family. The type language is first order! (Higher-Order Type-Level Programming in Haskell) and there is no way to define Compose that accepts an unmatchable function at the moment.

If you compare the kind of the slightly modified T1 and T2, the first one is unmatchable in both arguments while the second is matchable in its second argument

type  C1 :: Type -> @M Constraint
class C1 a where
  --   T1 :: Type -> @U Type -> @U Type
  type T1 a (b :: Type) :: Type

type  C2 :: Type -> @M Contraint
class C2 a where
  --   T2 :: Type -> @U Type -> @M Type
  type T2 a :: Type -> Type

A possibility is to wrap it in a (matchable) newtype

type    Wrapp'T :: Type -> @M Type
newtype Wrapp'T a = Wrapp'd (T a)

instance C (Maybe a) where
  type T (Maybe a) = NP (Compose Wrapp'T Identity) '[a]