#11699: Type families mistakingly report kind variables as unbound type variables -------------------------------------+------------------------------------- Reporter: mniip | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1-rc2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | 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: {{{#!hs {-# 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?) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11699 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler