Re: Exhaustive pattern match warning and GADTs

Brilliant, thank you Brent!

Now that you've given me the solution, I think I recall that I had a
top-level STRICT pragma on my old project, which would explain why I didn't
run into this confusion.

Will

On Sat, Jun 1, 2024 at 2:11 PM Brent Yorgey <[email protected]> wrote:

> 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 <[email protected]>
> 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.
>
>

_______________________________________________
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.