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

22 Sep 2018

      #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
           Keywords:                 |  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:
-------------------------------------+-------------------------------------
 = 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.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15666
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler