[GHC] #9151: Recursive default associated types don't kind-generalize properly
#9151: Recursive default associated types don't kind-generalize properly ------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- When I say {{{ {-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, UndecidableInstances #-} module Bug where import Data.Proxy class PEnum (kproxy :: KProxy a) where type ToEnum (x :: a) :: Bool type ToEnum x = TEHelper type TEHelper = ToEnum Int }}} I get {{{ /Users/rae/temp/Bug.hs:11:24: The first argument of ‘ToEnum’ should have kind ‘a’, but ‘Int’ has kind ‘*’ In the type ‘ToEnum Int’ In the type declaration for ‘TEHelper’ }}} I believe my original code should kind-check, as `ToEnum` should be applicable to any kind. My guess is that this sort of recursion isn't properly accounted for in the kind-checking algorithm in !TcTyClsDecls, and that we kind-check `TEHelper` before `ToEnum` is kind-generalized. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by archblob): I have played with the test case a little to see if I can reduce it, and to see when exactly the error happens. Here is what I have: {{{#!haskell {-# LANGUAGE PolyKinds, TypeFamilies, UndecidableInstances #-} module Bug where class PEnum (k :: a) where type ToEnum (x :: a) :: * type ToEnum x = TEHelper type TEHelper = ToEnum Int }}} That fails as the test case in the ticket, and this one passes: {{{#!haskell {-# LANGUAGE PolyKinds, TypeFamilies, UndecidableInstances #-} module Bug where class PEnum (k :: a) where type ToEnum (x :: b) :: * type ToEnum x = TEHelper type TEHelper = ToEnum Int }}} Also this is the output from {{{-ddump-tc-trace}}} : {{{ rn12 rn13 Tc2 (src) Tc3 kcTyClGroup module Bug class PEnum (k :: a) where type family ToEnum (x :: a) :: * type instance ToEnum x = TEHelper type TEHelper = ToEnum Int env2 [(a, Type variable ‘a’ = a)] env2 [] kcTyClGroup: initial kinds [(PEnum, AThing a -> Constraint), (ToEnum, AThing a -> *)] env2 [] kcd1 TEHelper [] tc_lhs_type: ToEnum Int Expected kind ‘k_av5’ tc_lhs_type: ToEnum Expected kind ‘k_av6’ lk1 ToEnum lk2 ToEnum AThing a -> * writeMetaTyVar k_av6 := a -> * tc_lhs_type: Int The first argument of ‘ToEnum’ should have kind ‘a’ lk1 Int lk2 Int Type constructor ‘Int’ checkExpectedKind Int * a checkExpectedKind 1 Int * a ([(k0, 1)], [(av4, a)]) ([(k0, 1)], [(av4, a)]) Adding error: Bug.hs:9:24: The first argument of ‘ToEnum’ should have kind ‘a’, but ‘Int’ has kind ‘*’ In the type ‘ToEnum Int’ In the type declaration for ‘TEHelper’ tryTc/recoverM recovering from IOEnv failure Bug.hs:9:24: The first argument of ‘ToEnum’ should have kind ‘a’, but ‘Int’ has kind ‘*’ In the type ‘ToEnum Int’ In the type declaration for ‘TEHelper’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): That second example is somewhat alarming -- the associated type family does not mention any class parameters. I'm surprised that's accepted! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by archblob): It really is. By playing with the kind checking strategy when default instances are defined I've managed to get the initial program to typecheck and get the correct type and kinds. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by archblob):
That second example is somewhat alarming -- the associated type family does not mention > any class parameters. I'm surprised that's accepted!
@goldfire, wasn't this introduced in #7939 ? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Created #9167 about the malformed associated type issue. @archblob: Do you have a patch about the original issue? Thanks for looking into it! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Replying to [comment:4 archblob]:
That second example is somewhat alarming -- the associated type family does not mention > any class parameters. I'm surprised that's accepted!
@goldfire, wasn't this introduced in #7939 ?
Perhaps, but if so, it was certainly not intentional. That work should make `b` poly-kinded, but it shouldn't necessarily make `F` accepted. I'm actually surprised that kind-checking strategies have much to do with this bug, but I haven't looked into it. When you change strategies, how does that affect other programs? As outlined in the very long comment explaining them and in #7939, kind-checking strategies are fiddly and subtle, a dangerous combination. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by archblob): The patch for the original issue still needs validating, I'm working on it now. I was interested in tracking down when the other problem happened first. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by archblob): Although my patch fixed this specific problem, it failed validation by causing others. My initial idea was to infer a more general {{{forall (a :: BOX). a -> *}}} kind when the associated type is mentioned in the rhs of the synonym, works for this case but causes breakages. Anyway, I'll be looking more into how to do it because I'm having a good time, but I'm not really sure anything will come of it so if someone else wants to work on this, don't mind me, go ahead. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Looking at the code for a bit, I don't think this is a trivial fix, after all. The problem is that associated type defaults are type-checked in the same group as the enclosing class. This means that GHC thinks that `TEHelper` and `PEnum` are mutually recursive. Thus, polymorphic recursion is not allowed between them, which is what we're asking for here. Instead, GHC should type check associated type defaults with other instances (in `tcInstDecls1`, likely), ''after'' all !TyClGroups are done being checked. With that line-up, `TEHelper` depends on `ToEnum` (part of the group with `PEnum`), but not the other way around. Unfortunately, this requires some moving plumbing around, and is not something I have time for at the moment. This all is not unlike how default method declarations have to be checked quite separately from the rest of a class. Anyway, archblob, if you want to keep playing, perhaps my comments above are helpful. I don't think this is ''hard'', but I originally thought the problem was due to a small oversight in the dependency analysis in the renamer. That's not the case, but it shouldn't be more than an hour or two of work. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by archblob): I think you original assumption still stands, as the current failure happens when we try to type-check the type synonym, we don't even get to the associated defaults, thus only postponing the type checking of atdefs will do no good I think. The failure will still happen at this stage. I think the synonym would have to be type checked in a different group, after the class declaration and before the atdefs, which will have to be checked with other instances as you suggested. Maybe someone else can chime in with some ideas about the strategy. Please tell me if my assumptions are wrong. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by archblob): * cc: simonpj (added) Comment: I'm adding simonpj, maybe he can chime in. I'm writing again as documentation. I've been looking into the result of the dependency analysis done in `depAnalTyClDecls` and we have : {{{ REC type TEHelper = ToEnum Int class PEnum (k :: a) where type family ToEnum (x :: a) :: * type instance ToEnum x = TEHelper }}} which means we will try to check `TEHelper` before we generalize `ToEnum` and hence the kind check error. Braking the cycle and having: {{{ REC class PEnum (k :: a) where type family ToEnum (x :: a) :: * type instance ToEnum x = TEHelper NOREC type TEHelper = ToEnum Int }}} will only work if we defer default type instance checking as you suggested. These modifications have to go together. But they really fell hackish. One other thing that I don't know if we can do is somehow accommodate for this by tweaking the four steps in `kcTyClGroup` , I'll be looking into how to do that as an alternative and compare the two. Am I making sense ? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): archblob, you are digging into one of the darkest corners of the type inference engine. I don't have time to page all this in right now. My suggestion would be to tackle something easier for now. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm reluctant to change the way that associated type defaults are kind- checked; but solving #9200 will also allow this program to be kind- checked. `ToEnum` will be treated as having a CUSK, and hence will support polymorphic recursion. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Confirmed that the original program is accepted in HEAD. Adding a test case soon. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9151: Recursive default associated types don't kind-generalize properly
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.2
Resolution: | Keywords:
Operating System: | Architecture: Unknown/Multiple
Unknown/Multiple | Difficulty: Unknown
Type of failure: | Blocked By:
None/Unknown | Related Tickets:
Test Case: |
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#9151: Recursive default associated types don't kind-generalize properly -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | typecheck/should_compile/T9151 | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * testcase: => typecheck/should_compile/T9151 * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9151#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC