[GHC] #10109: Kinds aren't checked in the coverage condition

#10109: Kinds aren't checked in the coverage condition -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1-rc2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Following on from the debate in #9103 (but you don't need to read that ticket), I found a curiosity. The following module fails to compile, complaining about the unsatisfied coverage condition: {{{ {-# LANGUAGE PolyKinds, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-} module Bug where data Succ a class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab, a ab -> b instance (Add a b ab) => Add (Succ a) b (Succ ab) }}} With `-fprint-explicit-kinds`, I get {{{ Bug.hs:9:10: Illegal instance declaration for ‘Add * k * (Succ k a) b (Succ k ab)’ The liberal coverage condition fails in class ‘Add’ for functional dependency: ‘a b -> ab’ Reason: lhs types ‘Succ k a’, ‘b’ do not jointly determine rhs type ‘Succ k ab’ In the instance declaration for ‘Add (Succ a) b (Succ ab)’ }}} But, when I add `k3` to the right-hand side of the first functional dependency (viz. {{{ {-# LANGUAGE PolyKinds, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-} module Bug where data Succ a class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab k3, a ab -> b instance (Add a b ab) => Add (Succ a) b (Succ ab) }}} ) I get {{{ [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Ok, modules loaded: Bug. }}} I always assumed that fixing a type in a fundep also fixed its kind. I get the same behavior in 7.8 as in 7.10.1RC2. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10109 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10109: Kinds aren't checked in the coverage condition -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1-rc2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): As a further curiosity, both versions of the program above fail without `UndecidableInstances`. How does `UndecidableInstances` affect the coverage condition check? Is this documented? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10109#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10109: Kinds aren't checked in the coverage condition -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1-rc2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by jstolarek): * cc: jan.stolarek@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10109#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10109: Kinds aren't checked in the coverage condition
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.10.1-rc2
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: None/Unknown | Unknown/Multiple
Blocked By: | Test Case:
Related Tickets: | Blocking:
| Differential Revisions:
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones

#10109: Kinds aren't checked in the coverage condition -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 7.10.1-rc2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | typecheck/should_compile/T10109 | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge * testcase: => typecheck/should_compile/T10109 Comment: Sorry for the slightly garbled commit message, but the main payload is right! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10109#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10109: Kinds aren't checked in the coverage condition -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: closed Priority: normal | Milestone: 7.10.2 Component: Compiler | Version: 7.10.1-rc2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | typecheck/should_compile/T10109 | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by thoughtpolice): * status: merge => closed * resolution: => fixed * milestone: => 7.10.2 Comment: This was actually merged a while back; just not closed (see d5c089208735014a09d43b1ee757f52ddbfc92bf). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10109#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10109: Kinds aren't checked in the coverage condition -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 7.10.2 Component: Compiler | Version: 7.10.1-rc2 Resolution: fixed | Keywords: FunDeps Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_compile/T10109 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => FunDeps -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10109#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC