Weird Error When Defining a Type Synonym of a Type Synonym (GHC)

Question

Background

I have written the following code in Haskell (GHC):

{-# LANGUAGE 
  NoImplicitPrelude,
  TypeInType, PolyKinds, DataKinds,
  ScopedTypeVariables,
  TypeFamilies
#-}

import Data.Kind(Type)

data PolyType k (t :: k)

type Wrap (t :: k) = PolyType k t
type Unwrap pt = (GetType pt :: GetKind pt)

type family GetType (pt :: Type) :: k where
  GetType (PolyType k t) = t

type family GetKind (pt :: Type) :: Type where
  GetKind (PolyType k t) = k

The intention of this code is to allow me to wrap a type of an arbitrary kind into a type (namely PolyType) of a single kind (namely Type) and then reverse the process (i.e. unwrap it) later.

Problem

I would like to define a type synonym for Unwrap akin to the following:

type UnwrapSynonym pt = Unwrap pt

However, the above definition produces the following error (GHC 8.4.3):

* Invalid declaration for `UnwrapSynonym'; you must explicitly
  declare which variables are dependent on which others.
  Inferred variable kinds: pt :: *
* In the type synonym declaration for `UnwrapSynonym'

What does this error mean? Is there a way I can get around it in order to define UnwrapSynonym?

What I Have Been Doing

My approach to this problem thus far is to essentially manually inline Uwrap in any high-order type synonyms I wish to define, but that feels icky, and I am hoping there is a better way.

Unfortunately, I am not experienced enough with the inner workings of GHC even understand exactly what the problem is much less figure out how to fix it.

I believe I have a decent understanding of how the extensions I'm using (ex. TypeInType and PolyKinds) work, but it is apparently not deep enough to understand this error. Furthermore, I have not been able to find an resources that address a similar problem. This is partly because I don't know how to succinctly describe it, which also made it hard to come up with a good title for this question.

Answer 1

The error is quite obtuse, but what I think it's trying to say is that GHC has noticed that the kind of UnwrapSynonym is dependent, forall (pt :: Type) -> GetKind pt, and it wants you to explicitly annotate the dependency:

type UnwrapSynonym pt = (Unwrap pt :: GetKind pt)

The reason it's talking about telling it "which variables are dependent on which others" is because this error can also pop up in e.g. this situation:

data Nat = Z | S Nat
data Fin :: Nat -> Type where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

type family ToNat (n :: Nat) (x :: Fin n) :: Nat where
  ToNat (S n) FZ = Z
  ToNat (S n) (FS x) = S (ToNat n x)

type ToNatAgain n x = ToNat n x -- similar error

ToNatAgain should have kind forall (n :: Nat) -> Fin n -> Nat, but the type of the variable x depends on the type of the variable n. GHC wants that explicitly annotated, so it tells me to tell it which variables depend on which other variables, and it gives me what it inferred as their kinds to help do that.

type ToNatAgain (n :: Nat) (x :: Fin n) = ToNat n x

In your case, the dependency is between the return kind and the argument kind. The underlying reason is the same, but the error message was apparently not designed with your case in mind and doesn't fit. You should submit a bug report.

As an aside, do you really need separate Unwrap and GetType? Why not make GetType dependent?

type family GetType (pt :: Type) :: GetKind pt where
  GetType (PolyType k t) = t