kindFunResult panic in the

[ChrisN]

This code:

f  = b  (l  () )

l :: b a -> c b
l = undefined

b :: (a -> b) -> c
b = undefined

Produces the following panic:

/tmp/Test.hs:4:10:
    Couldn't match kind `* -> *' with `*'
    Expected type: a0 -> b0
      Actual type: a0 -> b0
    Kind incompatibility when matching types:
      b_k :: * -> *
      b0 :: *
    In the return type of a call of `l'
    In the first argument of `b', namely `(l ())'

/tmp/Test.hs:4:13:ghc: panic! (the 'impossible' happened)
  (GHC version 7.7.20120909 for x86_64-unknown-linux):
	kindFunResult ghc-prim:GHC.Prim.*{(w) tc 34d}

I don't think this is the same as #6039 since that test code produces a parse error when I try to compile it (and it is listed as fixed).

[simonpj]

Good bug. Yes 7.6.1 fails, thus

T7368.hs:3:10:
    Couldn't match kind `* -> *' with `*'
    Expected type: a0 -> b0
      Actual type: a0 -> b0
    Kind incompatibility when matching types:
      b_w :: * -> *
      b0 :: *
    In the return type of a call of `l'
    In the first argument of `b', namely `(l ())'

T7368.hs:3:13:ghc-stage1: panic! (the 'impossible' happened)
  (GHC version 7.6.1.20121011 for x86_64-unknown-linux):
	kindFunResult ghc-prim:GHC.Prim.*{(w) tc 34d}

However HEAD (will be 7.8) is (happily) ok:

T7368.hs:3:10:
    Couldn't match kind `* -> *' with `*'
    When matching types
      c0 :: (* -> *) -> *
      (->) a0 :: * -> *
    Expected type: a0 -> b0
      Actual type: c0 b1
    In the return type of a call of `l'
    Probable cause: `l' is applied to too many arguments
    In the first argument of `b', namely `(l ())'
    In the expression: b (l ())

T7368.hs:3:13:
    Couldn't match type `()' with `b0 a1'
    Expected type: b1 a1
      Actual type: ()
    In the first argument of `l', namely `()'
    In the first argument of `b', namely `(l ())'
    In the expression: b (l ())

I don't know where exactly the problem lies in 7.6, and I'm very swamped, so I'm going to leave this open and unfixed. If it turns out to bite some mission-critical package I can look into fixing it in 7.6, I'd prefer not to have to do that.

I have added a regression test though.

Simon

[ChrisN]

Fine, I don't think it's a big deal anyway since I can only get it to crop up in programs with kind errors.

[arkeet]

I don't know if this should be a separate bug, but the following (ill-typed) code produces the same error, both on 7.6.1 and on HEAD:

{-# LANGUAGE Rank2Types #-}
newtype Bad f = Bad (forall a. (f a -> a))
fun :: f (Bad f) -> Bad f
fun (Bad x) = Bad x

[1 of 1] Compiling Main             ( bad.hs, bad.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 7.7.20121127 for x86_64-unknown-linux):
	kindFunResult ghc-prim:GHC.Prim.*{(w) tc 34d}

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

[simonpj]

Ugh. So it does. I'll investigate.

[simonpj@…]

commit be5cc2e33aa8e54299527af9b91e659d54c4cde5

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Dec 19 23:49:47 2012 +0000

    Fix TcUnify.matchExpectedTyConApp so that it returns types of compatible kinds
    
    This fixes Trac #7368. The problem was that we were matching
       Bad w ~ f (Bad f)
    where (f :: * -> *).  Thta leads to (w ~ Bad f), which is
    ill-kinded, but matchExpectedTyConApp was returning the (Bad f)
    as the argument type, and that was being used to instanatiate
    w in the data constructor type, which is very bad.
    
    The code also becomes simpler and easier to understand, which is
    an excellent thing.

 compiler/typecheck/TcUnify.lhs |   81 ++++++++++++++++++++--------------------
 1 files changed, 40 insertions(+), 41 deletions(-)

[simonpj]

Fixed! New test case added. Thanks for reporting this.

Simon

[igloo]

Merged as c4b2ac3775323948b7a6abdb241a4ad02afa7141