Order of declarations matters

This piece of code works.

{-# Language DataKinds    #-}
{-# Language GADTs        #-}
{-# Language InstanceSigs #-}
{-# Language PolyKinds    #-}
{-# Language TypeFamilies #-}

import Data.Kind

class Category (tag::Type) where
 type Strip tag :: Type

class Category tag => Stripped tag where
 type Hom tag::Strip tag -> Strip tag -> Type

instance Category () where
 type Strip () = ()
instance Stripped () where
 type Hom () = Unit1

data Unit1 :: () -> () -> Type where U1 :: Unit1 '() '()
data Tag
data Unit2 :: () -> () -> Type where U2 :: Unit2 '() '()

instance Category Tag where
 type Strip Tag = ()
instance Stripped Tag where
 type Hom Tag = Unit2

Note that Unit1 and Unit2 are declared identically, separated by data Tag. The order is important.

If we change the last line to Hom Tag = Unit1 (same as Hom ()) we get

$ ghc -ignore-dot-ghci 1152_bug.hs
GHCi, version 8.7.20190115: https://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 1152_bug.hs, interpreted )

1152_bug.hs:28:18: error:
    • Expected kind ‘Strip Tag -> Strip Tag -> *’,
        but ‘Unit1’ has kind ‘() -> () -> *’
    • In the type ‘Unit1’
      In the type instance declaration for ‘Hom’
      In the instance declaration for ‘Stripped Tag’
   |
28 |  type Hom Tag = Unit1
   |                  ^^^^^
Failed, no modules loaded.
Prelude>

even though Strip Tag is defined to equal (). Here comes the weird part.

If I move Unit1 decl beneath data Tag

data Tag
data Unit1 :: () -> () -> Type where U1 :: Unit1 '() '()
data Unit2 :: () -> () -> Type where U2 :: Unit2 '() '()

then type Hom Tag = Unit1 and type Hom Tag = Unit2 both work well.

If I move Unit2 decl above data Tag then both Hom Tag = Unit1 and Hom Tag = Unit2 fail!

data Unit1 :: () -> () -> Type where U1 :: Unit1 '() '()
data Unit2 :: () -> () -> Type where U2 :: Unit2 '() '()
data Tag

If I replace all occurrences of Tag with Bool it succeeds.

Trac metadata

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