I have a class:
class C (g :: [a] -> Type) where
type ExtractType g :: a -> Type
But I am not sure how to write the type family instance
instance C X where
type ExtractType X = ???
Type is * from GHC.Types.
For example, lets say I have an named NHList (ts::[(Symbol,Type)]), then ExtractType NHList should return (Symbol,Type) -> Type and be equivalent to Snd.
Contrast the two signatures:
type ExtractType g :: a -> Type
type ExtractType g (x :: a) :: Type
It may seem like merely a syntactic difference, but there's more to it than that.
Both definitions yield the same kind signature:
ghci> :kind ExtractType
ExtractType :: ([a] -> *) -> a -> *
So what's the difference?
The first definition declares that ExtractType is a type family (type function) that takes a single argument, and returns something of kind a -> Type.
The second one says that ExtractType is a type family of two arguments, returning something of kind Type. Using our intuition from the term-level, these two may sound equivalent, but that equivalence relies on partial application: the ability to pass around functions without fully saturating their arguments first. However, this is not allowed for type families: they must always be fully saturated.
More concretely, your example would look like
type family Snd (t :: (a, b)) :: b where
Snd '(_, b) = b
...
instance C NHList where
type ExtractType NHList = Snd
^^^
Here, Snd is unsaturated, because it takes one argument, but it is given none.
The solution is simple: saturate Snd. To do this, we adopt the second version:
class C (g :: [a] -> Type) where
type ExtractType g (x :: a) :: Type
instance C NHList where
type ExtractType NHList a = Snd a
^^^^^
Now, I said that type families must always be fully saturated - but why is this? There are a few reasons, here's one of them.
The constraint solver used in GHC's type system makes the following assumption:
Given a known equality f a ~ g b, we can deduce that f ~ g and a ~ b.
fancyId :: f a ~ g b => a -> b
fancyId = id -- `a` must be the same as `b`
A type can be in the form f a when f is a type constructor, like Maybe, like Maybe Int. What if f could be a type family?
type family Dumb a b where
Dumb _ b = b
With partial application, we could have something like Dumb Int ~ Dumb String, and GHC would readily derive Int ~ String. With the restriction that type families must be fully saturated, we can't even write down that equality, getting us away from the problem. Instead, Dumb Int String ~ Dumb String a now relates two fully saturated families, so they can first be reduced to String ~ a, and we're good.
Type constructors, like Maybe or Either are allowed to be partially applied, however. That's because they have certain properties (namely generativity and injectivity) that allow us to deduce the equalities above.
Given Either Int ~ Either a, we can learn that Int ~ a, because Either is injective. Snd is not injective: Snd '(Int, String) ~ Snd '(Char, String) holds, but that doesn't mean '(Int, String) ~ '(Char, String).
Summarising the above, the signature
type ExtractType g :: a -> Type
really means that ExtractType takes a single argument, and return a type constructor. A valid definition, albeit not a very useful one, would be
data Proxy (a :: k) = Proxy
...
type ExtractType g = Proxy
So what would happen if this restriction was lifted? As @pigworker mentioned, this would allow us to have type-level lambdas (well, not necessarily lambdas for us to use, but it would bring about the same problems as if we had lambdas):
Currently, if we know that for some g and h, ExtractType g and ExtractType h are the same, it must mean that they return the same type constructor, such as Proxy above (this is using the first definition). The equational theory here is pretty straightforward because we can easily decide when two type constructors are definitionally equal. Things get more complicated when ExtractType g is allowed to return any old type function: when are two type functions equal?
We could use definitional equality for the lambda terms, that is reducing them to their normal forms, and then using alpha-equivalence, but short of a strong normalisation property, this notion equality is undecidable. That's not necessarily a problem, but this is not something GHC does (yet).