Opened 6 years ago

Closed 5 years ago

#9201 closed bug (fixed)

GHC unexpectedly refines explicit kind signatures

Reported by: ekmett Owned by:
Priority: normal Milestone: 7.10.1
Component: Compiler (Type checker) Version: 7.8.2
Keywords: Cc: ekmett@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case: typecheck/should_fail/T9201
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


The following program should be rejected by the type checker:

{-# LANGUAGE PolyKinds, FunctionalDependencies, MultiParamTypeClasses #-}

class MonoidalCCC (f :: x -> y) (d :: y -> y -> *) | f -> d where
  ret :: d a (f a)

Instead it is accepted, but the kind variables specified above are 'corrected' during typechecking to:

>>> :browse
class MonoidalCCC (f :: x -> x) (d :: x -> x -> *) | f -> d where
  ret :: d a (f a)

This may be similar in root cause to issue #9200, but there a valid program is rejected, and here an invalid program is accepted, so the fixes may be quite different.

It seems these kind variables are just being allowed to unify rather than being checked for subsumption.

Change History (5)

comment:1 Changed 6 years ago by ekmett

Cc: ekmett@… added; ekmett removed

comment:2 Changed 6 years ago by goldfire

The underlying cause of this is directly related to what's causing #9200. The ParametricKinds strategy makes kind variables into SigTvs, which are allowed to unify with other SigTvs. The intent is that the SigTvs are in different signatures, like this:

class C (a :: k1) where
  foo :: D a => a -> a
class C a => D (a :: k2) where ...

Here, C and D are mutually recursive, and we would want these to type-check. However, according to the ParametricKinds strategy, we do not want to generalize over k while kind-checking the group. The only way to get this to work, then, is to unify k1 and k2. This is sensible enough, but it fails utterly in Edward's example, where the SigTvs are in the same signature.

The fix here is the same as the fix for #9200: change classes to use NonParametricKinds, which does not have this behavior.

I should note why ParametricKinds does what it does: when I added closed type families last summer, I needed to dig somewhat deep into all of this, to get kind inference for closed families to work. At that point, there were two strategies: the "normal" one and the one used in the presence of a "complete user-supplied kind signature" ("cusk"). See section 7.8.3 of the manual. Closed type families didn't fit into either of these categories cleanly. Instead of just adding a few ad-hoc conditionals, I invented the idea of "kind-checking strategies" where each of the (now, 3) approaches could be tracked a little more transparently. ParametricKinds was intended to behave exactly as kind inference did without a cusk. In retrospect, I had the opportunity to perhaps clean this all up a bit, but I didn't want to challenge the status quo without a concrete reason.

comment:3 Changed 5 years ago by thomie

Milestone: 7.10.1

With HEAD, the program from the description now shows the following error message:

$ ghc-7.9.20141113 T9201.hs 
[1 of 1] Compiling T9201            ( T9201.hs, T9201.o )

    The first argument of ‘f’ should have kind ‘x1’,
      but ‘a’ has kind ‘y1’
    In the type ‘d a (f a)’
    In the class declaration for ‘MonoidalCCC’

I think this ticket can be closed, once a regression test is added.

comment:4 Changed 5 years ago by Richard Eisenberg <eir@…>

In 8fea2acde696f9960ffcf84f512235bbf4b481d6/ghc:

Test #9201 in typecheck/should_fail/T9201

comment:5 Changed 5 years ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_fail/T9201
Note: See TracTickets for help on using tickets.