Skip to content

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.

Edited by tydeu
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information