[GHC] #15343: Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind)

[GHC]

#15343: Implicitly quantifying a kind variable causes GHC 8.6 to panic
(coercionKind)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Simon Peyton Jones <simonpj@…>):

 In [changeset:"5067b205a8abb5a9f98335d3a929f647c88c0aa2/ghc" 5067b20/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="5067b205a8abb5a9f98335d3a929f647c88c0aa2"
 Add nakedSubstTy and use it in TcHsType.tcInferApps

 This was a tricky one.

 During type checking we maintain TcType:
    Note [The well-kinded type invariant]
 That is, types are well-kinded /without/ zonking.

 But in tcInferApps we were destroying that invariant by calling
 substTy, which in turn uses smart constructors, which eliminate
 apparently-redundant Refl casts.

 This is horribly hard to debug beause they really are Refls and
 so it "ought" to be OK to discard them. But it isn't, as the
 above Note describes in some detail.

 Maybe we should review the invariant?  But for now I just followed
 it, tricky thought it is.

 This popped up because (for some reason) when I fixed Trac #15343,
 that exposed this bug by making test polykinds/T14174a fail (in
 Trac #14174 which indeed has the same origin).

 So this patch fixes a long standing and very subtle bug.

 One interesting point: I defined nakedSubstTy in a few lines by
 using the generic mapType stuff.  I note that the "normal"
 TyCoRep.substTy does /not/ use mapType.  But perhaps it should:
 substTy has lots of $! strict applications in it, and they could
 all be eliminated just by useing the StrictIdentity monad.  And
 that'd make it much easier to experiment with switching between
 strict and lazy versions.
 }}}

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