Opened 4 years ago

Closed 4 years ago

#11699 closed bug (fixed)

Type families mistakingly report kind variables as unbound type variables

Reported by: mniip Owned by: goldfire
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 8.0.1-rc2
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compiler/T11699
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


GHC verifies that if some equation of a type family binds a type variable, that this type variable actually exists and doesn't disappear through type synonym/family application (#7536). However this also mistakingly catches kind variables that aren't present in the type family head.

Simplest test case:

{-# LANGUAGE TypeFamilies, PolyKinds #-}
type family F a where F (f a) = f a

As seen on 8.0.1-rc2 and 7.10.2:

    Family instance purports to bind type variable ‘k1’
      but the real LHS (expanding synonyms) is: F (f a) = ...
    In the equations for closed type family ‘F’
    In the type family declaration for ‘F’

The culprit seems to be in exactTyCoVarsOfType, which doesn't grab kind variables from a type variable's kind, even though tyCoVarsOfType does.

Now, I'm not too sure whether this is a "GHC rejects valid program", or "Incorrect warning at compile time", as I'm not sure if type families like the aforementioned F are actually okay. (Are they?)

Change History (7)

comment:1 Changed 4 years ago by simonpj

Keywords: TypeInType added
Milestone: 8.0.1
Owner: set to goldfire

Richard, this doesn't look hard.

I think the program itself is fine.

comment:2 Changed 4 years ago by goldfire

This one is actually already fixed in HEAD. I'll add the test case.

comment:3 in reply to:  1 Changed 4 years ago by mniip

Replying to simonpj:

Richard, this doesn't look hard.

I think the program itself is fine.

So there are no issues with type family equations introducing new kind variables?

comment:4 Changed 4 years ago by goldfire

No issues. This was just a straightforward bug, as you pointed out. If you update to HEAD, your program should work fine.

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

In 693b38c/ghc:

Test case for #11699 in typecheck/should_compile

[skip ci]

comment:6 Changed 4 years ago by goldfire

Status: newmerge
Test Case: typecheck/should_compiler/T11699

The only thing to merge here is the test cases, I believe.

comment:7 Changed 4 years ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.