Type families mistakingly report kind variables as unbound type variables
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 (closed)). 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:
../File.hs:3:23:
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?)
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1-rc2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |