@@ -451,10 +451,9 @@ Bracketed' ::=
452 | Expr ')'
452 | Expr ')'
453 | ExprList ')'
453 | ExprList ')'
454− | Expr '**' Expr ')'
454+ | DependentPair ')'
455 | Operator Expr ')'
455 | Operator Expr ')'
456 | Expr Operator ')'
456 | Expr Operator ')'
457− | Name ':' Expr '**' Expr ')'
@@ -486,16 +485,17 @@ bracketed' open syn =
488+{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}
489dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm
489dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm
490dependentPair pun prev openFC syn =
490dependentPair pun prev openFC syn =
491 case pun of
491 case pun of
492− IsType -> nametypePart <|> namePart
492+ IsType -> nametypePart <|> namePart <|> exprPart True
493− IsTerm -> exprPart
493+ IsTerm -> exprPart False
494 TypeOrTerm ->
494 TypeOrTerm ->
495 if prev /= [] then -- To avoid ambiguity with later parsing
495 if prev /= [] then -- To avoid ambiguity with later parsing
496 nametypePart <|> namePart
496 nametypePart <|> namePart
498− nametypePart <|> namePart <|> exprPart
498+ nametypePart <|> namePart <|> exprPart False
499 where nametypePart = do
499 where nametypePart = do
500 (ln, lnfc, colonFC) <- try $ do
500 (ln, lnfc, colonFC) <- try $ do
501 (ln, lnfc) <- name
501 (ln, lnfc) <- name
@@ -508,9 +508,12 @@ dependentPair pun prev openFC syn =
508 (ln, lnfc) <- name
508 (ln, lnfc) <- name
509 starsFC <- reservedOpFC "**"
509 starsFC <- reservedOpFC "**"
510 dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn
510 dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn
511− exprPart = do
511+ exprPart isEnd = do
512 e <- expr syn
512 e <- expr syn
513− sepFCE <- (Left <$> reservedOpFC "**") <|> (Right <$> lcharFC ')')
514+ let stars = (Left <$> reservedOpFC "**")
515+ ending = (Right <$> lcharFC ')')
516+ in if isEnd then ending else stars <|> ending
514 case sepFCE of
517 case sepFCE of
515 Left starsFC -> dependentPair IsTerm ((e, Nothing, starsFC):prev) openFC syn
518 Left starsFC -> dependentPair IsTerm ((e, Nothing, starsFC):prev) openFC syn
516 Right closeFC ->
519 Right closeFC ->