@@ -451,10 +451,9 @@ Bracketed' ::=
451451 ')'
452452 | Expr ')'
453453 | ExprList ')'
454− | Expr '**' Expr ')'
454+ | DependentPair ')'
455455 | Operator Expr ')'
456456 | Expr Operator ')'
457− | Name ':' Expr '**' Expr ')'
458457 ;
459458@
460459-}
@@ -486,16 +485,17 @@ bracketed' open syn =
486485
487486
488487
488+{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}
489489dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm
490490dependentPair pun prev openFC syn =
491491 case pun of
492− IsType -> nametypePart <|> namePart
493− IsTerm -> exprPart
492+ IsType -> nametypePart <|> namePart <|> exprPart True
493+ IsTerm -> exprPart False
494494 TypeOrTerm ->
495495 if prev /= [] then -- To avoid ambiguity with later parsing
496496 nametypePart <|> namePart
497497 else
498− nametypePart <|> namePart <|> exprPart
498+ nametypePart <|> namePart <|> exprPart False
499499 where nametypePart = do
500500 (ln, lnfc, colonFC) <- try $ do
501501 (ln, lnfc) <- name
@@ -508,9 +508,12 @@ dependentPair pun prev openFC syn =
508508 (ln, lnfc) <- name
509509 starsFC <- reservedOpFC "**"
510510 dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn
511− exprPart = do
511+ exprPart isEnd = do
512512 e <- expr syn
513− sepFCE <- (Left <$> reservedOpFC "**") <|> (Right <$> lcharFC ')')
513+ sepFCE <-
514+ let stars = (Left <$> reservedOpFC "**")
515+ ending = (Right <$> lcharFC ')')
516+ in if isEnd then ending else stars <|> ending
514517 case sepFCE of
515518 Left starsFC -> dependentPair IsTerm ((e, Nothing, starsFC):prev) openFC syn
516519 Right closeFC ->