#8566: Given kind equalities are discarded -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: polykinds/T8566 | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): I think that would be bad. For example, take the singleton for lists: {{{ data instance Sing (xs :: [k]) where SNil :: Sing '[] SCons :: Sing h -> Sing t -> Sing (h ': t) }}} The constructors expand to {{{ SNil :: forall (k :: BOX) (xs :: [k]). (xs ~ '[] k) => Sing [k] xs SCons :: forall (k :: BOX) (xs :: [k]). forall (h :: k) (t :: [k]). (xs ~ ((':) k h t)) => Sing k h -> Sing [k] t -> Sing [k] xs }}} (If you get suspicious of the `[k]` in the return type, it's because I didn't unfold the `data instance` piece of it. With that unfolded, the return type's indices are indeed variables.) These equalities mention kind variables, and yet I would be quite sad without them. Or did I miss something here? PS: I take back my claim about `k` being existential and `unA` being ill- typed. Simon is right. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8566#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler