title: Failable match on a seemingly irrefutable GADT pattern
body: <p>Continuing <a href="https://stackoverflow.com/q/59537969/12274">my crusade</a> against <code>MonadFail</code> being a constraint in my monad, I'm now faced with the following:</p>
  
  <pre><code>data Thing :: Bool -&gt; Type where
    TrueThing :: Thing 'True
    FalseThing :: Thing 'False
  
  myFunc :: Monad m =&gt; m ()
  myFunc = do
    TrueThing &lt;- return TrueThing
    return ()
  </code></pre>
  
  <p>Which won't compile because, you guessed it:</p>
  
  <pre><code>• Could not deduce (MonadFail m)
      arising from a do statement
      with the failable pattern ‘TrueThing’
  </code></pre>
  
  <p>Indeed, if I read whatever<sup>1</sup> documentation I could find on the subject, it's not quite clear how the matching should work on a GADT.  I would obviously have thought this case fell under the “matches unconditionally” umbrella.  But I'll concede it doesn't qualify as a “single constructor <code>data</code> type”<sup>2</sup>.  Even though avoiding that sort of ambiguity was the point of using a GADT in the first place.</p>
  
  <p>Sure <code>~lazyPattern</code> works, but that's just band-aid.  I've desugared the match:</p>
  
  <pre><code>myFunc' :: Monad m =&gt; m ()
  myFunc' = let f :: _
                f TrueThing = return ()
            in return TrueThing &gt;&gt;= f
  </code></pre>
  
  <p>And now, while the error message isn't that explicit (<code>Couldn't match expected type ‘p’ with actual type ‘m0 ()</code>), the type wildcard is more telling:</p>
  
  <pre><code>• Found type wildcard ‘_’ standing for ‘Thing a -&gt; p’
  </code></pre>
  
  <p>…and guides me towards a “solution”:</p>
  
  <pre><code>myFunc' :: forall m. Monad m =&gt; m ()
  myFunc' = let f :: Thing 'True -&gt; m ()
                f TrueThing = return ()
            in return TrueThing &gt;&gt;= f
  </code></pre>
  
  <p>Well, that works.  Can I sugar it back?  <code>f</code> doesn't occur in the initial expression, but there are two spots I can annotate with a type: the monadic expression and the pattern.  I've tried both separately as well as together, and it's all “could not deduce <code>MonadFail</code>”.</p>
  
  <p>I suppose my expectations were too high, but I'd like to understand why.  Is it some type inference limitation?  A GADT one?  Am I not using the right machinery in the first place?  How could this pattern fail <em>at all</em>?</p>
  
  <hr>
  
  <p>(1) It's hard to find an authority on the subject.  The GHC manual <a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html?highlight=inline#extension-MonadFailDesugaring" rel="noreferrer">mentions MonadFail</a>, but links to the <a href="https://prime.haskell.org/wiki/Libraries/Proposals/MonadFail" rel="noreferrer">HaskellPrime wiki</a>, which seems to be an older revision of the same page on the <a href="https://wiki.haskell.org/MonadFail_Proposal" rel="noreferrer">Haskell wiki</a></p>
  
  <p>(2) Replacing <code>Bool</code> with <code>()</code> works too.  But that's too much simplification with regard to my actual problem.</p>