[GHC] #15370: Typed hole panic on GHC 8.6 (tcTyVarDetails)

[GHC]

#15370: Typed hole panic on GHC 8.6 (tcTyVarDetails)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  Tritlo
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.4.3
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypedHoles
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 RyanGlScott):

 Tritlo, what commit are you on? I just tried compiling the program in
 comment:1 using commit f0d27f515ffbc476144d1d1dd1a71bf9fa93c94b, and to my
 surprise, it no longer panics!

 {{{
 $ inplace/bin/ghc-stage2 ../Bug.hs
 [1 of 1] Compiling Bug              ( ../Bug.hs, ../Bug.o )

 ../Bug.hs:14:10: error:
     • Couldn't match type ‘n’ with ‘j’
       ‘n’ is a rigid type variable bound by
         the type signature for:
           mkRefl :: forall k (n :: k) (j :: k). n :~: j
         at ../Bug.hs:13:1-17
       ‘j’ is a rigid type variable bound by
         the type signature for:
           mkRefl :: forall k (n :: k) (j :: k). n :~: j
         at ../Bug.hs:13:1-17
       Expected type: n :~: j
         Actual type: n :~: n
     • In the expression: Refl
       In an equation for ‘mkRefl’: mkRefl = Refl
     • Relevant bindings include
         mkRefl :: n :~: j (bound at ../Bug.hs:14:1)
    |
 14 | mkRefl = Refl
    |          ^^^^

 ../Bug.hs:20:13: error:
     • Couldn't match type ‘S r’ with ‘()’
       Expected type: ()
         Actual type: S r
     • In the expression: no + _
       In a case alternative: Refl -> no + _
       In the expression: case mkRefl @x @y of { Refl -> no + _ }
     • Relevant bindings include
         no :: S r (bound at ../Bug.hs:18:7)
         right :: S r -> () (bound at ../Bug.hs:18:1)
    |
 20 |     Refl -> no + _
    |             ^^^^^^

 ../Bug.hs:20:18: error:
     • Found hole: _ :: S r
       Where: ‘r’, ‘y’, ‘x’ are rigid type variables bound by
                the type signature for:
                  right :: forall x y (r :: Either x y). S r -> ()
                at ../Bug.hs:(16,1)-(17,18)
     • In the second argument of ‘(+)’, namely ‘_’
       In the expression: no + _
       In a case alternative: Refl -> no + _
     • Relevant bindings include
         no :: S r (bound at ../Bug.hs:18:7)
         right :: S r -> () (bound at ../Bug.hs:18:1)
       Constraints include y ~ x (from ../Bug.hs:20:5-8)
    |
 20 |     Refl -> no + _
    |                  ^
 }}}

 Which seems positive, although I'm not sure which commit would have fixed
 this.

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