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

[GHC]

#15370: Typed hole panic on GHC 8.6 (tcTyVarDetails)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
  (Type checker)                     |
           Keywords:  TypeInType,    |  Operating System:  Unknown/Multiple
  TypedHoles                         |
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following program panics on GHC 8.6 and HEAD:

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind
 import Data.Type.Equality
 import Data.Void

 data family Sing :: forall k. k -> Type

 data (~>) :: Type -> Type -> Type
 infixr 0 ~>
 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

 newtype instance Sing (f :: k1 ~> k2) =
   SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }

 mkRefl :: n :~: j
 mkRefl = Refl

 right :: forall (r :: (x :~: y) ~> z).
          Sing r -> ()
 right no =
   case mkRefl @x @y of
     Refl -> applySing no _
 }}}
 {{{
 $ /opt/ghc/8.6.1/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
 ghc: panic! (the 'impossible' happened)
   (GHC version 8.6.0.20180627 for x86_64-unknown-linux):
         tcTyVarDetails
   co_a1BG :: y_a1Bz[sk:1] ~# x_a1By[sk:1]
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in
 ghc:Outputable
         pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var
 }}}

 On GHC 8.4, this simply errors:

 {{{
 $ /opt/ghc/8.4.3/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:23:10: error:
     • Couldn't match type ‘n’ with ‘j’
       ‘n’ is a rigid type variable bound by
         the type signature for:
           mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j
         at Bug.hs:22:1-17
       ‘j’ is a rigid type variable bound by
         the type signature for:
           mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j
         at Bug.hs:22: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:23:1)
    |
 23 | mkRefl = Refl
    |          ^^^^

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

 Bug.hs:29:26: error:
     • Found hole: _ :: Sing t0
       Where: ‘t0’ is an ambiguous type variable
              ‘y’, ‘x’, ‘k’ are rigid type variables bound by
                the type signature for:
                  right :: forall k1 (x1 :: k1) (y1 :: k1) z (r :: (x1 :~:
 y1) ~> z).
                           Sing r -> ()
                at Bug.hs:(25,1)-(26,21)
     • In the second argument of ‘applySing’, namely ‘_’
       In the expression: applySing no _
       In a case alternative: Refl -> applySing no _
     • Relevant bindings include
         no :: Sing r (bound at Bug.hs:27:7)
         right :: Sing r -> () (bound at Bug.hs:27:1)
       Valid substitutions include
         undefined :: forall (a :: TYPE r).
                      GHC.Stack.Types.HasCallStack =>
                      a
           (imported from ‘Prelude’ at Bug.hs:7:8-10
            (and originally defined in ‘GHC.Err’))
    |
 29 |     Refl -> applySing no _
    |                          ^
 }}}

 Note that this is distinct from #15142, as this is still reproducible on
 HEAD, even after commit 030211d21207dabb7a4bf21cc9af6fa5eb066db1.

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