Dependent type synonym in recursive type family causes GHC to panic
Background
I had written the following code in Haskell (GHC):
{-# LANGUAGE
NoImplicitPrelude,
TypeInType, PolyKinds, DataKinds,
ScopedTypeVariables,
TypeFamilies,
UndecidableInstances
#-}
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 GetKind (pt :: Type) :: Type where
GetKind (PolyType k t) = k
type family GetType (pt :: Type) :: k where
GetType (PolyType k t) = t
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 wanted to define a function that would recursively operate on a composite type like so:
data Composite :: a -> b -> Type
type family RecursiveWrap expr where
RecursiveWrap (Composite a b) =
Wrap (Composite (Unwrap (RecursiveWrap a)) (Unwrap (RecursiveWrap b)))
RecursiveWrap x = Wrap x
However, the above definition causes GHC to panic:
ghc.exe: panic! (the 'impossible' happened)
(GHC version 8.4.3 for x86_64-unknown-mingw32):
cyclic evaluation in fixIO
Ideas
If we inline the the Unwrap
synoynm into the defintion of the type family
above like so:
type family RecursiveWrap expr where
RecursiveWrap (Composite a b) =
Wrap (Composite
(GetType (RecursiveWrap a) :: GetKind (RecursiveWrap a))
(GetType (RecursiveWrap a) :: GetKind (RecursiveWrap a))
)
RecursiveWrap x = Wrap x
GHC instead simply produces an error:
* Type constructor `RecursiveWrap' cannot be used here
(it is defined and used in the same recursive group)
* In the first argument of `GetKind', namely `(RecursiveWrap a)'
In the kind `GetKind (RecursiveWrap a)'
In the first argument of `Composite', namely
`(GetType (RecursiveWrap a) :: GetKind (RecursiveWrap a))'
As such, I suspect this has to do with the recursive type family appearing in
the kind signature when the Unwrap
type synonym is expanded.
However, it strikes me as odd that even the above code errors. Since with the
UndecidableInstances
extension turned on, I think that I should be able to
write recursive type families like the above. Especially given that the above
family would not loop indefinitely and thus be reducible.