TypeInType: Type error conditioned on ordering of GADT and type family definitions

Consider this code which successfully compiles:

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

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture