[GHC] #14515: "Same" higher-rank kind synonyms behave differently

23 Nov 2017

      #14515: "Same" higher-rank kind synonyms behave differently
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           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:
-------------------------------------+-------------------------------------
 As you know type-level `forall`s don't float, so we may want to write
 `HRefl`'s kind

 {{{#!hs
 -- Different from
 --   HREFL :: forall k1 k2. k1 -> k2 -> Type
 --
 data HREFL :: forall k1. k1 -> (forall k2. k2 -> Type) where
   HREFL :: HREFL a a
 }}}

 Let us capture `forall k2. k2 -> ..` with a kind synonym

 {{{#!hs
 type HRank2 ty = forall k2. k2 -> ty

 data HREFL :: forall k. k -> HRank2 Type where
   HREFL :: HREFL a a
 }}}

 Works fine. Phew. Let's do the same for `forall k1. k1 -> ..`

 {{{#!hs
 type HRank1 ty = forall k1. k1 -> ty
 type HRank2 ty = forall k2. k2 -> ty

 data HREFL :: HRank1 (HRank2 Type) where
   HREFL :: HREFL a a
 }}}

 Works fine. Phew.

 “Didn't you just define the same kind synonym twice?” The funny thing is
 that this fails to compile when they coincide!

 {{{#!hs
 data HREFL :: HRank1 (HRank1 Type) -- FAILS
 data HREFL :: HRank1 (HRank2 Type) -- OK
 data HREFL :: HRank2 (HRank1 Type) -- OK
 data HREFL :: HRank2 (HRank2 Type) -- FAILS
 }}}

 {{{
 $ ghci -ignore-dot-ghci /tmp/Weird.hs
 GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( /tmp/Weird.hs, interpreted )

 /tmp/Weird.hs:8:1: error:
     • These kind and type variables: (b :: k2) k2 (d :: k2)
       are out of dependency order. Perhaps try this ordering:
         k2 (b :: k2) (d :: k2)
     • In the data type declaration for ‘HREFL’
   |
 8 | data HREFL :: HRank2 (HRank2 Type)
   | ^^^^^^^^^^
 Failed, 0 modules loaded.
 Prelude>
 }}}

 Same happens defining `HRank2` in terms of `HRank1`

 {{{#!hs
 type HRank1 ty = forall k1. k1 -> ty
 type HRank2 ty = HRank1 ty
 }}}

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