[GHC] #16410: Order of declarations matters
GHC
ghc-devs at haskell.org
Fri Mar 8 21:00:12 UTC 2019
#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>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list