Singling partiality in `do`-notation is troublesome

[RyanGlScott]

Even with https://github.com/goldfirere/th-desugar/pull/82, I'm not sure that we can properly single partial pattern matches in do-notation. For example, consider:

f :: [()]
f = do
  Just () <- [Nothing]
  return ()

This will desugar (after https://github.com/goldfirere/th-desugar/pull/82) to something like:

f :: [()]
f = [Nothing] >>= \arg ->
  case arg of
    Just () -> return ()
    _ -> fail "Partial pattern match in do notation"

f singles to this:

sF :: Sing (FSym0 :: [()])
sF
      = (applySing
           ((applySing ((singFun2 @(>>=@#@$)) (%>>=)))
              ((applySing ((applySing ((singFun2 @(:@#@$)) SCons)) SNothing))
                 SNil)))
          ((singFun1 @Lambda_6989586621679165469Sym0)
             (\ sArg
                -> case sArg of {
                     _ :: Sing arg_aEuX
                       -> case sArg of
                            SJust STuple0
                              -> (applySing ((singFun1 @ReturnSym0) sReturn)) STuple0
                            _ -> (applySing ((singFun1 @FailSym0) sFail))
                                   (sing :: Sing "Partial pattern match in do notation") ::
                            Sing (Case_6989586621679165472_aEuZ arg_aEuX arg_aEuX) }))

Which, annoyingly, does not typecheck:

../Bug2.hs:13:3: error:
    • Couldn't match type ‘Case_6989586621679165472 t t’ with ‘'[]’
      Expected type: Sing (Case_6989586621679165472 t t)
        Actual type: Sing
                       (FailSym0 @@ "Partial pattern match in do notation")
    • In the expression:
        (applySing ((singFun1 @FailSym0) sFail))
          (sing :: Sing "Partial pattern match in do notation")
      In a case alternative:
          _ -> (applySing ((singFun1 @FailSym0) sFail))
                 (sing :: Sing "Partial pattern match in do notation")
      In the expression:
          case sArg of
            SJust STuple0
              -> (applySing ((singFun1 @ReturnSym0) sReturn)) STuple0
            _ -> (applySing ((singFun1 @FailSym0) sFail))
                   (sing :: Sing "Partial pattern match in do notation") ::
            Sing (Case_6989586621679165472 arg_aEuX arg_aEuX)
    • Relevant bindings include
        sArg :: Sing t (bound at ../Bug2.hs:13:3)

The issue is that we have a wildcard pattern, which means that the Case_6989586621679165472_aEuZ type family cannot reduce. If we had matched on SNothing, then it would typecheck, although this is a trick we couldn't apply in the general case (since the monad we're using might have more than one constructor that could be matched in the catch-all case).

I'm not sure what to do here. We could:

1. Admit this as a deficiency in the Known bugs section of the README.
2. Wire in the type signature of sFail to be Sing (t :: Symbol) -> a. We currently employ a similar trick for sError :: Sing (t :: Symbol) -> a, which allows sError to be used in catch-all cases like the one above. The downside is that the type of sFail would be far more general than it ought to be (since its term-level equivalent has the type String -> m a).

[goldfirere]

Sounds like a case for #113. Once we have #113 in hand, then several other blocked bugs will be opened up. And I think we could solve this one, too, as match-flattening removes overlapping patterns.