[GHC] #11698: GHC's tct_closed flag is not being set correctly
#11698: GHC's tct_closed flag is not being set correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The `Note [Bindings with closed types]` in `TcEnv` describes when a binding is "closed", which in turn affects generalisation. (See the Note for details.) But the implementation doesn't follow the Note. Instead it uses this function in `TcEnv`: {{{ isClosedLetBndr :: Id -> TopLevelFlag -- See Note [Bindings with closed types] in TcRnTypes -- Note that we decided if a let-bound variable is closed by -- looking at its type, which is slightly more liberal, and a whole -- lot easier to implement, than looking at its free variables isClosedLetBndr id | isEmptyVarSet (tyCoVarsOfType (idType id)) = TopLevel | otherwise = NotTopLevel }}} It may be easier but it's also wrong. Consider {{{ f x = ( let g y = x+y in ... , x::Int) }}} Is `g` closed (which affects how definitions in `...` are generalised)? Well if we typecheck the second element of the tuple first, we may "know" that `x::Int` by the time we are inferring a type for `g`, conclude that `g` has no free type variables, and say that it is closed. But if we do the `x::Int` part second, so while type checking the `let` we think that `x::alpha`, then we'll say that `g` is open. This looks nasty. I think we should do it the way the `Note` says. Thanks to Facundo for pointing this out. Not urgent, but plainly wrong. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11698 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11698: GHC's tct_closed flag is not being set correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mboes): * cc: mboes (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11698#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11698: GHC's tct_closed flag is not being set correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 11656 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by facundo.dominguez): The definition reads {{{ Definition: A variable is "closed", and has tct_closed set to TopLevel, iff a) all its free variables are imported, or are let-bound with closed types b) generalisation is not restricted by the monomorphism restriction }}} I suppose that (a) should read instead: {{{ a) all its free variables are imported, or are let-bound and closed. }}} i.e. not only the type must be closed, the defining term should be as well. If closed types are required for a binding to be closed, then a new item (c) should be added asking for it, unless (a) implies that somehow: {{{ Definition: A variable is "closed", and has tct_closed set to TopLevel, iff a) all its free variables are imported, or are let-bound and closed b) generalisation is not restricted by the monomorphism restriction c) it has a closed type }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11698#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11698: GHC's tct_closed flag is not being set correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 11656 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes for (a). And (c) is implied by (a) and (b). Why? Assume (induction hypothesis) that closed variables have closed types, and that we have a new binding f = e, satisfying (a) and (b). Then since monomorphism restriction does not apply, and there are no free type variables, we can fully generalise, so its type will be closed. We should state that in the Note though -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11698#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11698: GHC's tct_closed flag is not being set correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 11656 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by facundo.dominguez): I can think of two ways to compute closedness. 1. Attach the free variables computed during the renaming pass to each binding. During type-checking, use these and the type of the binding to determine if it is closed. 2. Compute the free variables during type-checking and determine closedness from these alone. Is it (1) ok? Maybe it is more convenient than (2)? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11698#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11698: GHC's tct_closed flag is not being set correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 11656 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes, (1) already happens. The annoying thing is plumbing the info to `tcExtendLetEnv`. Note that `TcBinds.decideGeneralisationPlan` already computes the closed- ness flag, at least for the `InferGen` case; it would be annoying to compute it twice. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11698#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11698: GHC's tct_closed flag is not being set correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 11656 Related Tickets: | Differential Rev(s): Phab:D2016 Wiki Page: | -------------------------------------+------------------------------------- Changes (by facundo.dominguez): * status: new => patch * differential: => Phab:D2016 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11698#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11698: GHC's tct_closed flag is not being set correctly
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: patch
Priority: normal | Milestone:
Component: Compiler | Version: 7.10.3
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking: 11656
Related Tickets: | Differential Rev(s): Phab:D2016
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Facundo Domínguez
#11698: GHC's tct_closed flag is not being set correctly -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 11656 Related Tickets: | Differential Rev(s): Phab:D2016 Wiki Page: | -------------------------------------+------------------------------------- Changes (by facundo.dominguez): * status: patch => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11698#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC