<div dir="ltr"><div>Hi Will,</div><div><br></div>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).<div><br></div><div>One way around this is to add strictness annotations in the definition of State2:</div><div><br></div><div><span style="font-family:monospace">data State2 s a where</span><br style="font-family:monospace"><span style="font-family:monospace">  State2T :: !(s True) -> State2 s True</span><br style="font-family:monospace"><span style="font-family:monospace">  State2F :: !(s False) -> State2 s False</span><br style="font-family:monospace"></div><div><span style="font-family:monospace"><br></span></div><div><font face="arial, sans-serif">Now (</font><font face="monospace">State2F undefined</font><font face="arial, sans-serif">) is no longer a valid inhabitant of </font><font face="monospace">State2 OnlyTrue s</font><font face="arial, sans-serif">, and the warning goes away.</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">-Brent</font></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Jun 1, 2024 at 12:25 PM William Yager <<a href="mailto:will.yager@gmail.com">will.yager@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Hello cafe,<div><br></div><div>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.</div><div><br></div><div>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:</div><div><br></div><div><font face="monospace">{-# LANGUAGE DataKinds, GADTs #-}<br>module Lib () where<br><br>data State2 s a where<br>  State2T :: s True -> State2 s True<br>  State2F :: s False -> State2 s False<br><br>data OnlyTrue s where<br>  TrueState :: OnlyTrue True<br><br>example :: State2 OnlyTrue s -> ()<br>example (State2T TrueState) = ()<br>-- Comment this and get non-exhaustive pattern warning<br>-- Uncomment this and get "Inaccessible code" warning<br>-- example (State2F TrueState) = ()</font><br></div><div><br></div><div>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?</div><div><br></div><div>I'm using GHC 9.6.5.</div><div><br></div><div>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. </div><div><br></div><div>Any ideas what might be going wrong?</div><div><br></div><div>Thanks,</div><div>Will</div></div>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>