[Haskell-cafe] Exhaustive pattern match warning and GADTs

[Brent Yorgey]

Hi Will,

Sure, State2F TrueState is impossible, but there is actually another
possible pattern on the LHS of the equation, namely, (State2F _)  (this is
exactly what the warning says).  The reason this is a possible pattern is
that it would match on (State2F undefined).

One way around this is to add strictness annotations in the definition of
State2:

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

Now (State2F undefined) is no longer a valid inhabitant of State2 OnlyTrue s,
and the warning goes away.

-Brent

On Sat, Jun 1, 2024 at 12:25 PM William Yager <will.yager at gmail.com> wrote:

> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20240601/79f6e459/attachment.html>