[GHC] #13524: GHC does not preserve order of forall'd vars with TypeApplications

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 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: -------------------------------------+------------------------------------- The following code compiles with 8.0.2. Note that the order of variables on `pt1` is `a :: *` and `expr :: * -> *`, and this is the order of the type application in `main`. {{{ {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -fno-warn-partial-type-signatures #-} type Empty a = () foo :: expr a -> expr a -> expr (Empty a) foo = undefined newtype Expr a = SPT {run :: String} pt1 :: forall a ptexpr . ptexpr a -> ptexpr (Empty a) --pt1 :: forall a ptexpr . ptexpr a -> ptexpr _ pt1 a = foo a a main :: IO () main = putStrLn $ run $ pt1 @Int @Expr undefined }}} If I use partial type signatures with the alternate signature for `pt1` (which has the same order of the `forall`), I get these errors: {{{ Bug.hs:19:25: error: • Couldn't match type ‘Int’ with ‘Expr’ Expected type: Expr (Empty Expr) Actual type: Int (Empty Expr) • In the second argument of ‘($)’, namely ‘pt1 @Int @Expr undefined’ In the second argument of ‘($)’, namely ‘run $ pt1 @Int @Expr undefined’ In the expression: putStrLn $ run $ pt1 @Int @Expr undefined Bug.hs:19:30: error: • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’ • In the type ‘Int’ In the second argument of ‘($)’, namely ‘pt1 @Int @Expr undefined’ In the second argument of ‘($)’, namely ‘run $ pt1 @Int @Expr undefined’ Bug.hs:19:35: error: • Expecting one more argument to ‘Expr’ Expected a type, but ‘Expr’ has kind ‘* -> *’ • In the type ‘Expr’ In the second argument of ‘($)’, namely ‘pt1 @Int @Expr undefined’ In the second argument of ‘($)’, namely ‘run $ pt1 @Int @Expr undefined’ }}} The errors are saying that the kinds of the type applications are incorrect, but nothing in the order of `pt1`s `forall` nor the order of application has changed. However, if I then change the order of the type applications in `main` to `main = putStrLn $ run $ pt1 @Expr @Int undefined`, GHC accepts the program, even though the kinds of types in the application are incorrect with respect to the order listed in `pt1` (so it should reject the program). Somehow GHC has swapped the order of `a` and `ptexpr` in the variable list for `pt1`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: | TypeApplications 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 RyanGlScott): * keywords: => TypeApplications Comment: Even spookier, this actually //works// on GHC 8.0.1—it's only in GHC 8.0.2 (and HEAD) that I can reproduce the incorrect type variable order when using the partial type signature. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: | TypeApplications 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 RyanGlScott): * cc: niteria (added) Comment: This regression first popped up in c9bcaf3165586ac214fa694e61c55eb45eb131ab (Kill varSetElemsWellScoped in quantifyTyVars). You can also reproduce the same error in GHC 8.0.1 by compiling with `-dunique-increment=-1` (after uncommenting the partial type signature, of course). cc'ing niteria, in case he has an idea of what might be happening here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: | TypeApplications 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 niteria): Hmm, I would have expected 7e96526ac2ef5987ecb03217d3d616b6281c1441 to fix it and #13371 to be related. But you tested with HEAD, so that's a bit odd. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: | TypeApplications 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): Hmm. When the user gives a partial type signature, a whole new code path is used when checking the function. It seems this code path does not respect the order of specified type variables. @niteria's patch likely just exposed the underlying fragility; I don't think investigating that patch will yield any tasty fruit. I'm afraid I'm unable to address this right now, unfortunately. We could advertise this as an infelicity (I'm fairly confident the problem will happen only with a partial type signature). Perhaps even better, we could label variables in partial type signatures as "inferred", meaning that GHC will prevent them from being available for type application. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: | TypeApplications 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 simonpj):
Perhaps even better, we could label variables in partial type signatures as "inferred", meaning that GHC will prevent them from being available for type application.
Yes! After all, if you write {{{ f :: forall a. _ -> a -> a f = ... }}} you might end up with more type variables; e.g. f's signature might really be {{{ f :: forall a b c. (b,c) -> a -> a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: | TypeApplications 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 crockeea): I'm confused here: are you suggesting that you would be able to apply `f` to `a`, but not to `b` or `c`, or are you saying you would disallow type applications completely on functions that have partial type signatures? In the former case, new variables aren't causing my issue; GHC is reordering explicitly listed variables. In the latter case, this really weakens these two features! I'd rather guess the right order through trial and (compile) error than be disallowed completely. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: | TypeApplications 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 RyanGlScott): I think there's a bit of confusion here. The issue is not that wildcards are being treated as visible type variables, as evidenced in this GHCi session: {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive GHCi, version 8.3.20170329: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci λ> :set -fprint-explicit-foralls -XPartialTypeSignatures λ> let foo :: _ -> b; foo _ = undefined <interactive>:2:12: warning: [-Wpartial-type-signatures] • Found type wildcard ‘_’ standing for ‘w’ Where: ‘w’ is a rigid type variable bound by the inferred type of foo :: w -> b at <interactive>:2:20-36 • In the type signature: foo :: _ -> b λ> :type +v foo foo :: forall {w} b. w -> b }}} The fresh type variable that gets used in place of `_` is implicitly quantified and unspecified, so it is not available for visible type application in the first place: {{{ λ> :set -XTypeApplications λ> :type +v foo @Int foo @Int :: forall {w}. w -> Int λ> :type +v foo @Int @Char <interactive>:1:1: error: • Cannot apply expression of type ‘w0 -> Int’ to a visible type argument ‘Char’ • In the expression: foo @Int @Char }}} This part is working as expected. The issue is the order in which the //explicitly// quantified type variables are being returned in the presence of `PartialTypeSignatures`. If you take this code {{{#!hs {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -fno-warn-partial-type-signatures #-} type Empty a = () foo :: expr a -> expr a -> expr (Empty a) foo = undefined newtype Expr a = SPT {run :: String} pt1 :: forall a ptexpr . ptexpr a -> ptexpr _ pt1 a = foo a a }}} and load it into GHCi, you can see for yourself the exact (incorrect) order in which `pt1`'s type variables are appearing: {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.3.20170329: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Ok, modules loaded: Main. λ> :set -fprint-explicit-foralls λ> :type +v pt1 pt1 :: forall (ptexpr :: * -> *) a. ptexpr a -> ptexpr (Empty a) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: | TypeApplications 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 RyanGlScott): I heartily agree with crockeea that we should not disable VTA altogther for things with partial type signatures. I think that would be even more confusing than the current behavior, in fact! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: | TypeApplications 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 crockeea): @RyanGlScott Thank you for helping to clear up the question; you nailed it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13524: GHC does not preserve order of forall'd vars with TypeApplications
-------------------------------------+-------------------------------------
Reporter: crockeea | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.0.2
Resolution: | Keywords:
| TypeApplications
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 Ben Gamari

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: | TypeApplications 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): My comment:4 says:
Perhaps even better, we could label variables in partial type signatures as "inferred", meaning that GHC will prevent them from being available for type application.
This was always meant to be a stopgap solution, in case the status quo is unacceptable for 8.2. I've already put this bug in my queue for my summer bug roundup. But I simply can't get to it in the next month. "Even better" is suggesting that reliable, explainable behavior is better than capricious behavior, but @crockeea's comment:6 disagrees with this suggestion. I certainly don't feel strongly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13524: GHC does not preserve order of forall'd vars with TypeApplications
-------------------------------------+-------------------------------------
Reporter: crockeea | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.0.2
Resolution: | Keywords:
| TypeApplications
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 Simon Peyton Jones

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: fixed | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T13524 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => typecheck/should_compile/T13524 * resolution: => fixed Comment: I fixed this, somewhat by accident. The key code is in `TcSimplify.decideQuantifiedTyVars`, where there is a comment to explain. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: fixed | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T13524 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by crockeea): Will this make 8.2.1, or even 8.2 rc2? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13524: GHC does not preserve order of forall'd vars with TypeApplications -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.2 Resolution: fixed | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T13524 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: => 8.2.1 Comment: Yes, I've merged this to `ghc-8.2` as ace3117924133b69e9be78d1b1ed76a2f9956d47. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13524#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC