Core Lint error in ill-typed GADT code

Consider the following program:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

module T3651 where

data Z a where
  U :: Z ()
  B :: Z Bool


unsafe2 :: a ~ b => Z b -> Z a -> a
unsafe2 B U = ()

On current GHC HEAD, this fails with an "Inaccessible branch" error. However, if we turn this error into a warning, e.g. using the following patch:

--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -708,7 +708,7 @@ mkGivenErrorReporter implic ctxt cts
                              Nothing ty1 ty2
 
        ; traceTc "mkGivenErrorReporter" (ppr ct)
-       ; maybeReportError ctxt err }
+       ; reportWarning NoReason err }
   where
     (ct : _ )  = cts    -- Never empty
     (ty1, ty2) = getEqPredTys (ctPred ct)

1. ..and then compile with -dcore-lint -Werror, the program gets rejected with a core lint error:

[1 of 1] Compiling T3651            ( minimal.hs, minimal.o )
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
    In a case alternative: (U co_a1ri :: (a_a1rd :: *) ~# (() :: *))
    Unfilled coercion hole: {co_a1rw}
<no location info>: warning:
    In a case alternative: (U co_a1ri :: (a_a1rd :: *) ~# (() :: *))
    co_a1rw :: (() :: *) ~# (Bool :: *)
    [LclId[CoVarId]] is out of scope
*** Offending Program ***
Rec {
$tcZ :: TyCon
[LclIdX]
$tcZ
  = TyCon
      5287023927886307113##
      7998054209879401454##
      $trModule
      (TrNameS "Z"#)
      0#
      krep$*Arr*

$tc'U :: TyCon
[LclIdX]
$tc'U
  = TyCon
      5625905484817226555##
      8662083060712566586##
      $trModule
      (TrNameS "'U"#)
      0#
      $krep_a1sr

$tc'B :: TyCon
[LclIdX]
$tc'B
  = TyCon
      477146386442824276##
      11145321492051770584##
      $trModule
      (TrNameS "'B"#)
      0#
      $krep_a1st

$krep_a1sr [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_a1sr
  = KindRepTyConApp $tcZ (: @ KindRep $krep_a1ss ([] @ KindRep))

$krep_a1st [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_a1st
  = KindRepTyConApp $tcZ (: @ KindRep $krep_a1su ([] @ KindRep))

$krep_a1ss [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_a1ss = KindRepTyConApp $tc() ([] @ KindRep)

$krep_a1su [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_a1su = KindRepTyConApp $tcBool ([] @ KindRep)

$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "T3651"#)

unsafe2 :: forall a b. ((a :: *) ~ (b :: *)) => Z b -> Z a -> a
[LclIdX]
unsafe2
  = \ (@ a_a1rd)
      (@ b_a1re)
      ($d~_a1rg :: (a_a1rd :: *) ~ (b_a1re :: *)) ->
      let {
        $d~~_a1ro :: (a_a1rd :: *) ~~ (b_a1re :: *)
        [LclId]
        $d~~_a1ro = $p1~ @ * @ a_a1rd @ b_a1re $d~_a1rg } in
      case heq_sel @ * @ * @ a_a1rd @ b_a1re $d~~_a1ro of co_a1rp
      { __DEFAULT ->
      \ (ds_d1sv :: Z b_a1re) (ds_d1sw :: Z a_a1rd) ->
        let {
          fail_d1tc :: Void# -> a_a1rd
          [LclId]
          fail_d1tc
            = \ (ds_d1td [OS=OneShot] :: Void#) ->
                patError
                  @ 'LiftedRep @ a_a1rd "minimal.hs:12:1-16|function unsafe2"# } in
        case ds_d1sv of wild_00 {
          __DEFAULT -> fail_d1tc void#;
          B co_a1rh ->
            let {
              co_a1ru :: (a_a1rd :: *) ~# (Bool :: *)
              [LclId[CoVarId]]
              co_a1ru = CO: co_a1rp ; co_a1rh } in
            case ds_d1sw of wild_00 {
              __DEFAULT -> fail_d1tc void#;
              U co_a1ri ->
                ()
                `cast` (Sub ({co_a1rw} ; Sym co_a1ru)
                        :: (() :: *) ~R# (a_a1rd[sk:2] :: *))
            }
        }
      }
end Rec }

*** End of Offense ***


<no location info>: error: 
Compilation had errors

However, without core linting, the correct errors appear:

[1 of 1] Compiling T3651            ( minimal.hs, minimal.o )

minimal.hs:12:1: error: [-Woverlapping-patterns, -Werror=overlapping-patterns]
    Pattern match has inaccessible right hand side
    In an equation for ‘unsafe2’: unsafe2 B U = ...
   |
12 | unsafe2 B U = ()
   | ^^^^^^^^^^^^^^^^

minimal.hs:12:11: error: [-Werror]
    • Couldn't match type ‘Bool’ with ‘()’
      Inaccessible code in
        a pattern with constructor: U :: Z (), in an equation for ‘unsafe2’
    • In the pattern: U
      In an equation for ‘unsafe2’: unsafe2 B U = ()
   |
12 | unsafe2 B U = ()
   |           ^

Without either core linting or -Werror, GHC just emits the warnings, and then falls into a hole:

[1 of 1] Compiling T3651            ( minimal.hs, minimal.o )

minimal.hs:12:1: warning: [-Woverlapping-patterns]
    Pattern match has inaccessible right hand side
    In an equation for ‘unsafe2’: unsafe2 B U = ...
   |
12 | unsafe2 B U = ()
   | ^^^^^^^^^^^^^^^^

minimal.hs:12:11: warning:
    • Couldn't match type ‘Bool’ with ‘()’
      Inaccessible code in
        a pattern with constructor: U :: Z (), in an equation for ‘unsafe2’
    • In the pattern: U
      In an equation for ‘unsafe2’: unsafe2 B U = ()
   |
12 | unsafe2 B U = ()
   |           ^
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.5.20180508 for x86_64-unknown-linux):
	opt_univ fell into a hole
  {co_a1rw}
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
        pprPanic, called at compiler/types/OptCoercion.hs:242:5 in ghc:OptCoercion

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

This behavior also appears in the following test cases from the GHC test suite:

• gadt/T3651
• gadt/T7558