Exhaustive pattern match warning and GADTs

Hello cafe,

I'm writing a bit of code with state machines that are only allowed to make
certain types of transitions between certain classes of states (e.g.
"ready" and "unready"). The state types have some type parameters
describing which class of state it's currently in. The step functions look
vaguely  like `step :: state a -> input b -> state c`, with various
constraints on `a`, `b`, and `c`. When `state` and `input` are GADTs, you
can enforce interesting invariants about the output state, given the input
state and event.

This all seems to work fine, and seems to be getting me in the direction I
want to go. However, I'm running into a roadblock (possibly a bug?). Take
the following minimal example:

{-# LANGUAGE DataKinds, GADTs #-}
module Lib () where

data State2 s a where
  State2T :: s True -> State2 s True
  State2F :: s False -> State2 s False

data OnlyTrue s where
  TrueState :: OnlyTrue True

example :: State2 OnlyTrue s -> ()
example (State2T TrueState) = ()
-- Comment this and get non-exhaustive pattern warning
-- Uncomment this and get "Inaccessible code" warning
-- example (State2F TrueState) = ()

There is only one possible pattern on the LHS of the equation. If I don't
put the (impossible) pattern, GHC gives me a warning about missing a
pattern. If I do put the impossible pattern, GHC warns me that the pattern
is impossible. Indeed! So why is GHC complaining about it in the first
place?

I'm using GHC 9.6.5.

Around 7-8 years ago, I wrote some similar code, using typeclasses to
constraint GADTs, and I remember being very impressed that the completeness
checker was smart enough to figure out not to complain about impossible
patterns (cf the paper "GADTs meet their match"). This seems like a simpler
use case than what I recall doing in the past, but the completeness checker
is giving me bad warnings here.

Any ideas what might be going wrong?

Thanks,
Will

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.