#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 simonpj): Aha. But there is a real difference between the two: {{{ MkT :: forall (u:*). forall (k:BOX), (b:k). (u ~ Proxy k b) => Proxy k b -> T u SNil :: forall (k:BOX) (xs:[k]). (xs ~ '[] k) => Sing22 k xs }}} (I've used `Sing22` for the data type for `Sing (xs:[k])`.) In `SNil` the `k` is univerally quantified over the whole thing. In `MkT` the `k` is existentially quantified, ''and'' involved in an equality constraint. So I rephrase my proposal: '''reject any data constructor with an existentially quantified kind variable that is mentioned in an equality constraint'''. Of course "mentioned in an equality constraint" is itself not too obvious (think superclasses and constraint kinds). But is the direction of travel right? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8566#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler