[GHC] #15561: TypeInType: Type error conditioned on ordering of GADT and type family definitions

23 Aug 2018

      #15561: TypeInType: Type error conditioned on ordering of GADT and type family
definitions
-------------------------------------+-------------------------------------
           Reporter:  Bj0rn          |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
           Keywords:  TypeInType,    |  Operating System:  Unknown/Multiple
  TypeFamilies, GADTs                |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider this code which successfully compiles:
 {{{#!hs
 {-# LANGUAGE TypeInType, TypeFamilies, GADTs #-}

 module Bug where

 class HasIndex a where
     type Index a
     emptyIndex :: IndexWrapper a
 instance HasIndex [a] where
     type Index [a] = Int
     emptyIndex = Wrap 0

 data IndexWrapper a where
     Wrap :: Index a -> IndexWrapper a

 type family UnwrapAnyWrapperLikeThing (a :: t) :: k

 type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
 }}}

 The mere act of moving the definition of `IndexWrapper` anywhere below the
 definition of `UnwrapAnyWrapperLikeThing` makes the type family instance
 at the bottom of the example fail compilation, with this error:
 {{{
 Bug.hs:17:15: error:
     • Illegal type synonym family application in instance: Index [b]
     • In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’
    |
 17 | type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b])
 = a
    |
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 This is the smallest example that I could come up with; my real scenario
 of course has more things going on, but I can share if it would help.

 The problem for me (other than that I'm pretty sure reordering definitions
 in Haskell should never affect anything) is that I would like just the
 definition of the type family (`UnwrapAnyWrapperLikeThing` in this
 example) in module `A` and all of the other definitions in module `B` that
 imports `A`.

 Ideally, I would have liked to add a `HasIndex a` constraint to the `Wrap`
 constructor, but that disqualifies use of `'Wrap` on the type level. This
 does make me feel like I'm on shaky ground to begin with.

 I have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I
 should note that 8.0.2 rejects even the code that I pasted here.

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