Typed hole panic on GHC 8.6 (tcTyVarDetails)

The following program panics on GHC 8.6 and HEAD:

{-# 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 (closed), as this is still reproducible on HEAD, even after commit 030211d2.

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	high
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture