[GHC] #8566: Panic with kindFunResult
GHC
ghc-devs at haskell.org
Sat Dec 28 13:09:51 UTC 2013
#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
More information about the ghc-tickets
mailing list