[GHC] #16410: Order of declarations matters

8 Mar 2019

      #16410: Order of declarations matters
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.7
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This piece of code works.

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

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

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

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