Opened 3 years ago

Closed 3 years ago

#7230 closed bug (fixed)

GHC states the same kind mismatched

Reported by: konn Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.7
Keywords: Cc:
Operating System: MacOS X Architecture: x86_64 (amd64)
Type of failure: Incorrect warning at compile-time Test Case: T7230
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


The attached code fails to compile with following rather strange kind error:

    Couldn't match kind `Nat' with `Nat'
    Expected type: (':) Nat x1 xs2
      Actual type: xs1
    Kind incompatibility when matching types:
      xs1 :: [Nat]
      (':) Nat x1 xs2 :: [Nat]
    In the pattern: SCons y xs
    In the pattern: SCons x (SCons y xs)
Failed, modules loaded: none.

The code, on the other hand, is expected not to compile because current GHC can't infer that Increasing (x ': y ': xs) implies x :<<= y, and the code attached compiles successfully if we rewrite the function crash as follows:

crash :: (Increasing xs) ~ True => SList xs -> SBool (Increasing xs)
crash (SCons x (SCons y xs)) =
  case x %:<<= y of
    STrue -> x %:<<= y
    _     -> error "impossible"
crash _                      = STrue

I think it is strange and rather confusing that GHC says "Nat kind doesn't match with Nat!" and GHC should throws more appropriate compile error. (Furthermore, it would be more convenient if GHC could infer x :<<= y from Increasing (x ': y ': xs), but it should be argued in another place, not here.)

I confirmed that this strange error message is genrated in 7.7.20120906.

Attachments (1)

kind-mismatch-error.hs (1.4 KB) - added by konn 3 years ago.
The code that generates strange kind error

Download all attachments as: .zip

Change History (5)

Changed 3 years ago by konn

The code that generates strange kind error

comment:1 Changed 3 years ago by konn

Oops, I attached the wrong source code. Re-uploaded.

comment:2 Changed 3 years ago by simonpj@…

commit c32bb5d0c09a7e55197191f152c6875b398717cf

Author: Simon Peyton Jones <[email protected]>
Date:   Sun Sep 9 07:07:39 2012 +0100

    Remember to zonk the skolems of an implication
    Their kinds may contain kind unification variables!
    This patch fixes Trac #7230.

 compiler/typecheck/TcMType.lhs |   25 ++++++++++++++++++-------
 1 files changed, 18 insertions(+), 7 deletions(-)

comment:3 Changed 3 years ago by simonpj

  • difficulty set to Unknown
  • Status changed from new to merge
  • Test Case set to T7230

Thanks for the example, now fixed.


comment:4 Changed 3 years ago by igloo

  • Resolution set to fixed
  • Status changed from merge to closed
Note: See TracTickets for help on using tickets.