[GHC] #15666: Dependent type synonym in recursive type family causes GHC to panic

[GHC]

#15666: Dependent type synonym in recursive type family causes GHC to panic
-------------------------------------+-------------------------------------
        Reporter:  tydeu             |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:  newcomer
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Old description:

> = Background
>
> I had written the following code in Haskell (GHC):
>
> {{{#!hs
> {-# 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:
>
> {{{#!hs
> data Composite :: a -> b -> Type
>
> type family RecursiveWrap (expr :: exprK) 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:
>
> {{{#!hs
> 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.

New description:

 = Background

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

 {{{#!hs
 {-# 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:

 {{{#!hs
 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:

 {{{#!hs
 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.

--

Comment (by tydeu):

 Realized I accidentally broke my example while trying to clean it up for
 this ticket. Fixed it.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15666#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler