[GHC] #13680: Can't use TypeApplications with [] data constructor (was: Can't use TypeApplications with list expressions)

[GHC]

#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:/compiler/typecheck/TcExpr.hs#l511
 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