[GHC] #11699: Type families mistakingly report kind variables as unbound type variables
#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
#11699: Type families mistakingly report kind variables as unbound type variables -------------------------------------+------------------------------------- Reporter: mniip | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 8.0.1-rc2 Resolution: | Keywords: TypeInType 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: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: => goldfire * keywords: => TypeInType * milestone: => 8.0.1 Comment: Richard, this doesn't look hard. I think the program itself is fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11699#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11699: Type families mistakingly report kind variables as unbound type variables -------------------------------------+------------------------------------- Reporter: mniip | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 8.0.1-rc2 Resolution: | Keywords: TypeInType 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: | -------------------------------------+------------------------------------- Comment (by goldfire): This one is actually already fixed in HEAD. I'll add the test case. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11699#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11699: Type families mistakingly report kind variables as unbound type variables -------------------------------------+------------------------------------- Reporter: mniip | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 8.0.1-rc2 Resolution: | Keywords: TypeInType 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: | -------------------------------------+------------------------------------- Comment (by mniip): Replying to [comment:1 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?
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11699#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11699: Type families mistakingly report kind variables as unbound type variables -------------------------------------+------------------------------------- Reporter: mniip | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 8.0.1-rc2 Resolution: | Keywords: TypeInType 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: | -------------------------------------+------------------------------------- Comment (by goldfire): No issues. This was just a straightforward bug, as you pointed out. If you update to HEAD, your program should work fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11699#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11699: Type families mistakingly report kind variables as unbound type variables
-------------------------------------+-------------------------------------
Reporter: mniip | Owner: goldfire
Type: bug | Status: new
Priority: normal | Milestone: 8.0.1
Component: Compiler | Version: 8.0.1-rc2
Resolution: | Keywords: TypeInType
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: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#11699: Type families mistakingly report kind variables as unbound type variables -------------------------------------+------------------------------------- Reporter: mniip | Owner: goldfire Type: bug | Status: merge Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 8.0.1-rc2 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compiler/T11699 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * testcase: => typecheck/should_compiler/T11699 * status: new => merge Comment: The only thing to merge here is the test cases, I believe. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11699#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11699: Type families mistakingly report kind variables as unbound type variables -------------------------------------+------------------------------------- Reporter: mniip | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 8.0.1-rc2 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compiler/T11699 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged as 397362e6eaee30e0650dd8f8681160eaf5227407. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11699#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC