Re: #16410: Order of declarations matters

--===============1972936115726076851==
Content-Type: multipart/related;
 boundary="===============7488846783084194561=="

--===============7488846783084194561==
MIME-Version: 1.0
Content-Type: text/plain; charset="utf-8"
Content-Transfer-Encoding: 8bit

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

Comment (by Iceland_jack):

 I get similar behavior for

 {{{#!hs
 {-# Language DataKinds              #-}
 {-# Language GADTs                  #-}
 {-# Language PolyKinds              #-}
 {-# Language TypeFamilyDependencies #-}
 {-# Language TypeOperators          #-}
 {-# Language UndecidableInstances   #-}

 import Data.Kind
 -- import Data.Type.Equality

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

 class Category tag => Stripped tag where
  type Hom tag = (res::Strip tag -> Strip tag -> Type) | res -> tag

 data REFL (k :: Type) :: Type
 data a :~: b where
  Refl :: a :~: a

 instance Category (REFL k) where
  type Strip (REFL k) = k
 instance Stripped (REFL k) where
  type Hom (REFL k) = (:~:)
 }}}

 This works.

 Moving `(:~:)` above `REFL` fails

 {{{
     Type family equation violates injectivity annotation.
     Type variable ‘k’ cannot be inferred from the right-hand side.
     In the type family equation:
       Hom (REFL k) = (:~:) -- Defined at 1154_bug.hs:24:7
    |
 24 |  type Hom (REFL k) = (:~:)
    |       ^^^
 Failed, no modules loaded.
 }}}

 Similarly removing the `(:~:)` declaration and importing it from
 `Data.Type.Equality` yields the same.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16410#comment:2>