[GHC] #15220: ScopedTypeVariables binds a non-existent variable
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 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: -------------------------------------+------------------------------------- GHC accepts this definition: {{{#!hs f :: (forall a. a -> a) -> () f (x :: b -> b) = x (undefined :: b) `seq` () }}} If a scoped type variable is bound always to a variable, then what variable is `b` bound to? In the desugared Core, it looks like `b` is bound to `Any`. Note that I couldn't find any valid argument for `x` here other than `undefined`. I think this definition should be rejected. In terms of implementation, the `zonkTcTypeToType` function should never encounter a unfilled-in `SigTv`. If it does, error. I don't like putting the error there, but I'm not sure I know another place to do it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 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: | -------------------------------------+------------------------------------- Comment (by simonpj): I suspect we'll end up saying that a type variable can be bound to an arbitrary type, in which case this will become moot. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 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: | -------------------------------------+------------------------------------- Comment (by goldfire): Yes, I suppose so. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 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: | -------------------------------------+------------------------------------- Comment (by goldfire): But I still think it would be very strange if `zonkTcTypeToType` ever zonked a `SigTv` to `Any`. Could that happen another way? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 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: | -------------------------------------+------------------------------------- Comment (by simonpj):
But I still think it would be very strange if zonkTcTypeToType ever zonked a SigTv to Any.
I don't understand the question. In the example, `b` will not stand for a `SigTv` any more -- it'll stand for a `TauTv`, which can get unified with anything. I suppose we'll have to look at any remaining uses of `SigTv`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 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: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:4 simonpj]:
I suppose we'll have to look at any remaining uses of `SigTv`.
Yes, that's what I meant. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 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: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): What is the status of this ticket post-commit 4d91cabcd5e3c603997d9876f6d30204a9b029c6 (`Allow scoped type variables refer to types`)? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 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: | -------------------------------------+------------------------------------- Comment (by goldfire): We should still make sure we never zonk a `SigTv` to `Any`, so we can't close quite yet. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 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: | -------------------------------------+------------------------------------- Comment (by simonpj):
We should still make sure we never zonk a SigTv to Any, so we can't close quite yet.
Why should we make sure of that? We allow `length []` to elaborate to `length @Any ([] @Any)`. I don't see what `SigTv` has to do with it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 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: | -------------------------------------+------------------------------------- Comment (by goldfire): The semantics of `TyVarTv` (né `SigTv`) state that a `TyVarTv` unifies only with another variable. `Any` is not a variable, and so a `TyVarTv` should not unify to it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 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: | -------------------------------------+------------------------------------- Comment (by simonpj): Hmm. What should happen to an unbound `TyVarTv` unification variable then? The presenting problem was with the old `SigTv`, when a scoped type variable could only be bound to a variable. But we've changed that now - they are `TauTv`s. I'm unsure about exactly how the remaining uses of `TyVarTv` work and whether this issue will arise at all. I suspect that it will not. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 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: | -------------------------------------+------------------------------------- Comment (by goldfire): I agree with your suspicion -- all I'm saying is that we should check. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 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: | -------------------------------------+------------------------------------- Comment (by nomeata): As a side node, there is need for `undefined` to trigger this: {{{ f :: (forall a. (a -> (), a)) -> () f (p :: (b -> (), b)) = fst p (snd p) }}} also has `p` instantiated with `Any`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15220: ScopedTypeVariables binds a non-existent variable -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 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: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm no longer sure what the bug (if any) is here. It all looks fine to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15220#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC