#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: -------------------------------------+------------------------------------ Changes (by simonpj): * status: closed => new * resolution: fixed => Comment: Hmm. It occurs to me that with these GADTs it isn't just record selectors that are going to bad on us. Consider {{{ -- Proxy :: forall k. k -> * data T a where MkT :: Proxy b -> T (Proxy b) }}} So the real type of `MkT` is (putting in the kinds) {{{ MkT :: forall u. forall k, b:k. (u ~ Proxy k b) => Proxy k b -> T u }}} Now that `k` is existential. So pattern-matching is going to be problematic. For example, if we write {{{ f :: forall kc, c:kc. T (Proxy kc c) -> Proxy kc c f (MkT x) = x }}} we'll get a Given equality `Proxy kc c ~ Proxy k b`, where the 'k' and 'b' are existentially bound; since we can't make use of such Given equalities, we'll get obscure failures. I rather think that we should '''reject any type signature (including GADT ones) with an equality constraint that mentions a kind variable'''. That would be more restrictive, but it is at least clear. How bad would that be? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8566#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler