More liberal with alternatives in with blocks

Only need to match one possibility (it's essentially impossible to match
more than one after all!). Fixes #297.

src/TTImp/WithClause.idr

@@ -57,9 +57,9 @@ mutual
   -- implicit in the parent
   getMatch lhs f (IImplicitApp fc f' n a)
       = matchFail fc
-  -- Alternatives are okay as long as all corresponding alternatives are okay
-  getMatch lhs (IAlternative _ _ as) (IAlternative _ _ as')
-      = matchAll lhs (zip as as')
+  -- Alternatives are okay as long as one of the alternatives is okay
+  getMatch lhs (IAlternative fc _ as) (IAlternative _ _ as')
+      = matchAny fc lhs (zip as as')
   getMatch lhs (IAs _ _ (UN n) p) (IAs fc _ (UN n') p')
       = do ms <- getMatch lhs p p'
            mergeMatches lhs ((n, IBindVar fc n') :: ms)
@@ -75,6 +75,13 @@ mutual
     else matchFail fc
   getMatch lhs pat spec = matchFail (getFC pat)
 
+  matchAny : FC -> (lhs : Bool) -> List (RawImp, RawImp) ->
+             Core (List (String, RawImp))
+  matchAny fc lhs [] = matchFail fc
+  matchAny fc lhs ((x, y) :: ms)
+      = catch (getMatch lhs x y)
+              (\err => matchAny fc lhs ms)
+
   matchAll : (lhs : Bool) -> List (RawImp, RawImp) ->
              Core (List (String, RawImp))
   matchAll lhs [] = pure []

tests/Main.idr

@@ -99,7 +99,7 @@ idrisTests
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
        "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
        "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
-       "reg029", "reg030",
+       "reg029", "reg030", "reg031",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008", "total009",

tests/idris2/reg031/dpair.idr

@@ -0,0 +1,10 @@
+data Foobar : String -> Type where
+  MkBar : (s : String) -> Foobar s
+
+test : (foobar : (x ** Foobar x)) -> String
+test (MkDPair fst snd) with (snd)
+  test (MkDPair fst snd) | (MkBar fst) = ?test_rhs__rhs_
+
+test' : (foobar : (x ** Foobar x)) -> String
+test' (s ** foobar) with (foobar)
+  test' (s ** foobar) | with_pat = ?test'_rhs_rhs

tests/idris2/reg031/expected

@@ -0,0 +1 @@
+1/1: Building dpair (dpair.idr)

tests/idris2/reg031/run

@@ -0,0 +1,3 @@
+$1 --check dpair.idr
+
+rm -rf build