[GHC] #8566: Panic with kindFunResult

[GHC]

#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