[GHC] #15142: GHC HEAD regression: tcTyVarDetails

[GHC]

#15142: GHC HEAD regression: tcTyVarDetails
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  closed
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |             Keywords:  TypeInType,
      Resolution:  fixed             |  TypeFamilies, CUSKs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Compile-time      |            Test Case:  indexed-
  crash or panic                     |  types/should_compile/T15142
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 comment:21 is quite debatable as Richard and I agreed on the phone
 today.  It's easier to understand at the term level.  Suppose you
 write
 {{{
 f :: forall a b. a b -> Int
 f x = let y :: b; y = undefined in 5
 }}}
 With `-XPolyKinds` the type signature is generalised to
 {{{
 f :: forall k. (a :: k->*) (b :: k). a b -> Int
 }}}
 But then the definition of `f` is less polymorphic than that!
 The use of `y::b` forces `b::*`; but the signature says `b::k`, so
 the definition is rejected.

 By omitting a `forall` in the final item of the CUSK comment above,
 the curren system says "not a CUSK", so inference can do its magic.
 But we can't currently do that in terms.  Except perhaps by making
 a partial type signature like
 {{{
 f :: forall a b. a b -> _
 }}}
 for which inference takes place.

 The final bullet in the Note, about data types, amounts to a very
 ad-hoc way of signaling "don't use a CUSK". Ugh.

 We decided to leave it as-is for now, because we'll end up
 revisiting all this when we introduce separate kind signatures for
 type constructors.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15142#comment:22>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler