[GHC] #13680: Can't use TypeApplications with empty list expression
#13680: Can't use TypeApplications with empty list expression -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Why can't I do this? {{{#!hs {-# LANGUAGE TypeApplications #-} module Bug where foo :: [Int] foo = [] @Int }}} Compiling this with GHC 8.0.1, 8.0.2, 8.2.1, or HEAD gives me: {{{ $ /opt/ghc/head/bin/ghci Bug2.hs GHCi, version 8.3.20170509: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug2.hs, interpreted ) Bug2.hs:5:7: error: • Cannot apply expression of type ‘[a0]’ to a visible type argument ‘Int’ • In the expression: [] @Int In an equation for ‘foo’: foo = [] @Int | 5 | foo = [] @Int | ^^^^^^^ }}} This seems really strange, since I can use `TypeApplications` with expressions like `Nothing @Int` without issues. According to GHCi: {{{ $ /opt/ghc/head/bin/ghci GHCi, version 8.3.20170509: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci λ> :set -XTypeApplications -fprint-explicit-foralls λ> :type +v [] [] :: forall {a}. [a] λ> :type +v Nothing Nothing :: forall a. Maybe a }}} The type variable for `[]` isn't visible! But I don't see any reason why it shouldn't be, especially since, conceptually, the data type declaration for lists is: {{{#!hs data [] a = [] | a : [a] }}} I suspect that `[]`'s tyvar binder visibility is not wired into GHC correctly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with empty list expression -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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 Iceland_jack): I wish type application worked with a more things, see #11409 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with empty list expression -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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): Indeed. However, I think #11409 is unrelated to the issue at hand here. Using `TypeApplications` with numeric literals is tricky due to the desugaring down to `fromInteger` that has to take place, whereas there's no such obstacle here, as far as I understand. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with empty list expression -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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 Iceland_jack): Yes for lists it's more of a no-brainer, as you say `[]` is conceptually a constructor. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with empty list expression -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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): A have a (very slight) hunch what might be happening here. `[]` is wired in to GHC [http://git.haskell.org/ghc.git/blob/4d9167b087abd2f4dad4ccfaba7bbde177fd2797... here]: {{{#!hs nilDataCon :: DataCon nilDataCon = pcDataCon nilDataConName alpha_tyvar [] listTyCon }}} And if you follow the definition of `pcDataCon` deep enough, you'll discover it eventually calls [http://git.haskell.org/ghc.git/blob/4d9167b087abd2f4dad4ccfaba7bbde177fd2797... this code]: {{{#!hs pcDataConWithFixity' :: Bool -> Name -> Unique -> RuntimeRepInfo -> [TyVar] -> [TyVar] -> [Type] -> TyCon -> DataCon -- The Name should be in the DataName name space; it's the name -- of the DataCon itself. pcDataConWithFixity' declared_infix dc_name wrk_key rri tyvars ex_tyvars arg_tys tycon = data_con where data_con = mkDataCon dc_name declared_infix prom_info (map (const no_bang) arg_tys) [] -- No labelled fields (mkTyVarBinders Specified tyvars) (mkTyVarBinders Specified ex_tyvars) [] -- No equality spec [] -- No theta arg_tys (mkTyConApp tycon (mkTyVarTys tyvars)) rri tycon [] -- No stupid theta (mkDataConWorkId wrk_name data_con) NoDataConRep -- Wired-in types are too simple to need wrappers no_bang = HsSrcBang NoSourceText NoSrcUnpack NoSrcStrict wrk_name = mkDataConWorkerName data_con wrk_key prom_info = mkPrelTyConRepName dc_name }}} The use of `Specified` is a tad suspicious. I tried changing it to `Required`, but unfortunately, the bug still persists after this. So there must be something else that explains this behavior, but it eludes me for now... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with empty list expression -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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): Actually, this limitation applies to more than just empty lists: {{{ $ ~/Software/ghc-8.2.0.20170507/bin/ghci -fprint-explicit-foralls GHCi, version 8.2.0.20170507: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /Users/rscott/.ghci λ> :type +v [1] [1] :: forall {a}. Num a => [a] λ> :type +v [1] @Int <interactive>:1:5: error: parse error on input ‘@’ }}} So perhaps I was barking up the wrong tree in my investigation in comment:4. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with list expressions -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with [] data constructor -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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): Please ignore what I wrote in comment:5. That is expected behavior, since the type variables for that expression's type would have to be inferred (i.e., invisible). I now suspect the culprit here is `tcExpr`. Specifically, [http://git.haskell.org/ghc.git/blob/76769bdf9e423d89518eae4a5a441ae172c54e96... this case]: {{{#!hs tcExpr (ExplicitList _ witness exprs) res_ty = case witness of Nothing -> do { res_ty <- expTypeToType res_ty ; (coi, elt_ty) <- matchExpectedListTy res_ty ; exprs' <- mapM (tc_elt elt_ty) exprs ; return $ mkHsWrapCo coi $ ExplicitList elt_ty Nothing exprs' } Just fln -> do { ... } where tc_elt elt_ty expr = tcPolyExpr expr elt_ty }}} Notice that we're calling `matchExpectedListTy` here. This causes the inferred type _not_ to be `forall a. [a]`, but instead something of a coercion type `p[a:tau]`. This means we have to fish out the `a` afterwards, which causes it to have inferred visibility. Blegh. I was hoping that we could just special-case `[]` like so: {{{#!hs tcExpr (ExplicitList _ Nothing []) res_ty = tcCheckId nilDataConName res_ty }}} And while that does achieve what I'd hoped for, it has the unfortunate effect of messing with the pattern-match exhaustivity checker, as the `T12957` test starts failing with this change. So for the time being, I'm out of ideas. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with [] data constructor -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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 simonpj): * cc: goldfire (added) Comment: Richard is the king of visible type application, but he's on holiday for a fortnight. But I think you are right that the empty-list case of `ExplicitList` probably needs to be special-case. Should not be too hard to do that. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with [] data constructor -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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): Agreed with comment:8 and, subsequently, the approach in comment:7. I'm not sure about the pattern-match checker, but perhaps that problem can be solved. Happy to take a look at your code if you like. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with [] data constructor -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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): Replying to [comment:9 goldfire]:
Happy to take a look at your code if you like.
Well, that's the thing... the line: {{{#!hs tcExpr (ExplicitList _ Nothing []) res_ty = tcCheckId nilDataConName res_ty }}} is literally the only change I had to make to make `[] @Int` work. So that's nice. But now exactly one GHC test fails: `T12957`. {{{ =====> T12957(normal) 1 of 1 [0, 0, 0] cd "./pmcheck/should_compile/T12957.run" && "/home/rgscott/Software/ghc4/inplace/test spaces/ghc-stage2" -c T12957.hs -dcore-lint -dcmm-lint -no-user-package-db -rtsopts -fno-warn- missed-specialisations -fshow-warning-groups -fdiagnostics-color=never -fno-diagnostics-show-caret -dno-debug-output -fwarn-overlapping-patterns Actual stderr output differs from expected: diff -uw "./pmcheck/should_compile/T12957.run/T12957.stderr.normalised" "./pmcheck/should_compile/T12957.run/T12957.comp.stderr.normalised" --- ./pmcheck/should_compile/T12957.run/T12957.stderr.normalised 2017-07-10 17:44:06.341225345 -0400 +++ ./pmcheck/should_compile/T12957.run/T12957.comp.stderr.normalised 2017-07-10 17:44:06.341225345 -0400 @@ -1,4 +0,0 @@ - -T12957.hs:4:16: warning: [-Woverlapping-patterns (in -Wdefault)] - Pattern match is redundant - In a case alternative: (_ : _) -> ... *** unexpected failure for T12957(normal) }}} And that's where I'm stuck. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with [] data constructor -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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): Then just accept the new output. :) The test case for #12957 is not testing to see if GHC can report a redundant pattern match -- it's checking to make sure GHC avoids a panic. This change would bring the behavior around lists in line with that for other datatypes. Note that `case Nothing of Just _ -> ...` does not report a redundant match. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with [] data constructor -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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: mpickering (added) Comment: Huh, I certainly didn't realize that lists were unique in this regard. In fact, the warning even goes away if you replace `[]` with an empty string literal! {{{ λ> case [] of (_:_) -> case () of a -> undefined <interactive>:5:12: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: (_ : _) -> ... *** Exception: <interactive>:5:1-45: Non-exhaustive patterns in case λ> case "" of (_:_) -> case () of a -> undefined *** Exception: <interactive>:6:1-45: Non-exhaustive patterns in case }}} In that case, I'm slightly more comfortable with making this change. But just in case, I'll cc mpickering, the author of the `T12957` test, to make sure he's comfortable with this idea. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with [] data constructor -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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): Phab:D3733 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D3733 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13680: Can't use TypeApplications with [] data constructor
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.0.1
checker) | Keywords:
Resolution: | 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): Phab:D3733
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
#13680: Can't use TypeApplications with [] data constructor -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: fixed | 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): Phab:D3733 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: patch => closed * resolution: => fixed * milestone: => 8.4.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13680#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC