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