git.iko.soy/Idris-dev
on master help sign in
Check for unbound expression before checking for a constraint list. (#3217)
55230b7Niklas Larsson
src/Idris/Parser/Expr.hs+13−2
compare with master
unifiedsplit
@@ -1130,6 +1130,17 @@ unboundPi opts st syn = do
1130 return (PPi binder (sUN "__pi_arg") NoFC x sc))
1130 return (PPi binder (sUN "__pi_arg") NoFC x sc))
1131 <|> return x
1131 <|> return x
1132
1132
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+
1133pi :: SyntaxInfo -> IdrisParser PTerm
1144pi :: SyntaxInfo -> IdrisParser PTerm
1134pi syn =
1145pi syn =
1135 do opts <- piOpts syn
1146 do opts <- piOpts syn
@@ -1137,8 +1148,8 @@ pi syn =
1137 explicitPi opts st syn
1148 explicitPi opts st syn
1138 <|> try (do lchar '{'; implicitPi opts st syn)
1149 <|> try (do lchar '{'; implicitPi opts st syn)
1139 <|> if constraintAllowed syn
1150 <|> if constraintAllowed syn
1140− then try (constraintPi opts st syn)
1151+ then try (unboundPiNoConstraint opts st syn)
1141− <|> unboundPi opts st syn
1152+ <|> constraintPi opts st syn
1142 else unboundPi opts st syn
1153 else unboundPi opts st syn
1143 <?> "dependent type signature"
1154 <?> "dependent type signature"
1144
1155