Opened 6 months ago

Closed 4 months ago

#13680 closed bug (fixed)

Can't use TypeApplications with [] data constructor

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeApplications Cc: goldfire, mpickering
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D3733
Wiki Page:

Description

Why can't I do this?

{-# 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:

data [] a = [] | a : [a]

I suspect that []'s tyvar binder visibility is not wired into GHC correctly.

Change History (15)

comment:1 Changed 6 months ago by Iceland_jack

I wish type application worked with a more things, see #11409

comment:2 Changed 6 months ago 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.

comment:3 Changed 6 months ago by Iceland_jack

Yes for lists it's more of a no-brainer, as you say [] is conceptually a constructor.

comment:4 Changed 6 months ago by RyanGlScott

A have a (very slight) hunch what might be happening here. [] is wired in to GHC here:

nilDataCon :: DataCon
nilDataCon  = pcDataCon nilDataConName alpha_tyvar [] listTyCon

And if you follow the definition of pcDataCon deep enough, you'll discover it eventually calls this code:

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...

comment:5 Changed 5 months ago by RyanGlScott

Actually, this limitation applies to more than just empty lists:

$ ~/Software/ghc-8.2.0.20170507/bin/ghci -fprint-explicit-foralls -XTypeApplications
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:1: error:
    • Cannot apply expression of type ‘[a0]’
      to a visible type argument ‘Int’
    • In the expression: [1] @Int

So perhaps I was barking up the wrong tree in my investigation in comment:4.

Last edited 5 months ago by RyanGlScott (previous) (diff)

comment:6 Changed 5 months ago by RyanGlScott

Summary: Can't use TypeApplications with empty list expressionCan't use TypeApplications with list expressions

comment:7 Changed 5 months ago by RyanGlScott

Summary: Can't use TypeApplications with list expressionsCan't use TypeApplications with [] data constructor

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, this case:

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:

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.

comment:8 Changed 5 months ago by simonpj

Cc: goldfire added

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.

comment:9 Changed 4 months ago 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.

comment:10 in reply to:  9 Changed 4 months ago by RyanGlScott

Replying to goldfire:

Happy to take a look at your code if you like.

Well, that's the thing... the line:

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.

comment:11 Changed 4 months ago 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.

comment:12 Changed 4 months ago by RyanGlScott

Cc: mpickering added

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.

comment:13 Changed 4 months ago by RyanGlScott

Differential Rev(s): Phab:D3733
Status: newpatch

comment:14 Changed 4 months ago by Ben Gamari <ben@…>

In c9e4c861/ghc:

Allow visible type application for []

This amounts to a one-line change in `tcExpr`. I've added a Note to
explain what is going on.

This requires a separate change in the pattern-match checker to
account for the fact that typechecked `[]` expressions become
`ConLikeOut`s, not `ExplicitList`s.

Test Plan: make test TEST=T13680

Reviewers: goldfire, mpickering, austin, bgamari

Reviewed By: mpickering, bgamari

Subscribers: rwbarton, thomie, goldfire

GHC Trac Issues: #13680

Differential Revision: https://phabricator.haskell.org/D3733

comment:15 Changed 4 months ago by bgamari

Milestone: 8.4.1
Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.