Compiled program throws ‘Non-exhaustive patterns in case’

Summary

It's hard to say what exactly causes this bug; it's very fragile and requires a lot of newer GHC type features. But, with the below combination of unlifted data types, type data, type families, GADTs, and less interesting circumstantial details, GHC produces a program that crashes with Non-exhaustive patterns in case.

This crash is incorrect, as the case expression in question is exhaustive given the types of the GADT constructors. Furthermore, GHC doesn't warn about this at compile time with -Wincomplete-patterns. Changing minor details, like inlining the contents of the BugLib module into Main or replacing the $ in the definition of shouldBeExhaustive with parentheses, results in a program that doesn't crash.

Steps to reproduce

{-# LANGUAGE GADTs, UnliftedDatatypes #-}
module BugLib where

import GHC.Exts (UnliftedType)
import GHC.Types (Type)

data UnliftedGADTProxy :: Type -> UnliftedType where
  UGPInt :: UnliftedGADTProxy Int
  UGPBool :: UnliftedGADTProxy Bool

{-# LANGUAGE GADTs, TypeData, TypeFamilies #-}
{-# OPTIONS_GHC -Wincomplete-patterns -Werror #-}
module Main where

import GHC.Types (Type)

import BugLib

type data TDWrapper = TDWrapperCon Type

type family UnwrapTDW tdw where
  UnwrapTDW (TDWrapperCon a) = a

data ProxyBox tdw = ProxyBox (UnliftedGADTProxy (UnwrapTDW tdw))

shouldBeExhaustive :: ProxyBox (TDWrapperCon Int) -> ()
shouldBeExhaustive pb = id $ case pb of ProxyBox UGPInt -> ()

main :: IO ()
main = let
  pb :: ProxyBox (TDWrapperCon Int)
  pb = ProxyBox UGPInt
  !_ = shouldBeExhaustive pb
  in putStrLn "works"

Expected behavior

It should compile to a program that prints works.

Environment

• GHC version used: 9.6.2

Optional:

• Operating System: Linux (NixOS)
• System Architecture: x86_64