#8566: Panic with kindFunResult -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: fixed | 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): I had a look at this. I don't agree with Richard: it should typecheck. This `unT` is well typed, despite the GADT: {{{ type family F (a :: *) :: * data T a where MkT :: F a -> T [a] unT :: T [b] -> F b unT (MkT x) = x }}} Here we see that {{{ MkT :: forall u. forall a. (u ~ [a]) => F a -> T u }}} So the 'a' is existential. But from the pattern match we get a Given constraint `[b] ~ [a]`, and we can decompose that to, in effect, determine the existential via a Given equality `b~a`. However that doesn't work in the poly-kinded case of this ticket because the constraint we get is something like `APP k1 (b:k1) ~ APP k2 (a:k2)`. The trouble is that we don't have kind equalities (yet!), so GHC currently decomposes the Given APP constraint, but then silently discards new Given constraint `k1~k2` (since we don't have kind equalities) and `b~a` (because they have incompatible kinds). See `Note [Do not create Given kind equalities]` in `TcSMonad`. The net result is that we can't prove an equality that we "ought" to be able to prove, giving a confusing error message. I do agree with Richard that (until we get kind equalities) it would be better to treat it like an existential record selector, rather than produce the opaque error message. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8566#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler