@@ -1130,6 +1130,17 @@ unboundPi opts st syn = do
11301130 return (PPi binder (sUN "__pi_arg") NoFC x sc))
11311131 <|> return x
11321132
1133+-- This is used when we need to disambiguate from a constraint list
1134+unboundPiNoConstraint opts st syn = do
1135+ x <- opExpr syn
1136+ (do binder <- bindsymbol opts st syn
1137+ sc <- expr syn
1138+ notFollowedBy $ reservedOp "=>"
1139+ return (PPi binder (sUN "__pi_arg") NoFC x sc))
1140+ <|> do notFollowedBy $ reservedOp "=>"
1141+ return x
1142+
1143+
11331144pi :: SyntaxInfo -> IdrisParser PTerm
11341145pi syn =
11351146 do opts <- piOpts syn
@@ -1137,8 +1148,8 @@ pi syn =
11371148 explicitPi opts st syn
11381149 <|> try (do lchar '{'; implicitPi opts st syn)
11391150 <|> if constraintAllowed syn
1140− then try (constraintPi opts st syn)
1141− <|> unboundPi opts st syn
1151+ then try (unboundPiNoConstraint opts st syn)
1152+ <|> constraintPi opts st syn
11421153 else unboundPi opts st syn
11431154 <?> "dependent type signature"
11441155