@@ -409,7 +409,7 @@ pFunDecl' syn = try (do push_indent
409409 opts' <- pFnOpts
410410 n_in <- pfName
411411 let n = expandNS syn n_in
412− ty <- pTSig syn
412+ ty <- pTSig (impOK syn)
413413 fc <- pfc
414414 pTerminator
415415-- ty' <- implicit syn n ty
@@ -656,7 +656,7 @@ pSimpleExpr syn =
656656 <|> try (pList syn)
657657 <|> try (pAlt syn)
658658 <|> try (pIdiom syn)
659− <|> try (do lchar '('; bracketed syn)
659+ <|> try (do lchar '('; bracketed (noImp syn))
660660 <|> try (do c <- pConstant; fc <- pfc
661661 return (modifyConst syn fc (PConstant c)))
662662 <|> do reserved "Set"; return PSet
@@ -793,9 +793,12 @@ mkSet (UN n) = UN ("set_" ++ n)
793793mkSet (MN 0 n) = MN 0 ("set_" ++ n)
794794mkSet (NS n s) = NS (mkSet n) s
795795
796+noImp syn = syn { implicitAllowed = False }
797+impOK syn = syn { implicitAllowed = True }
798+
796799pTSig syn = do lchar ':'
797− cs <- pConstList syn
798− sc <- pExpr syn
800+ cs <- if implicitAllowed syn then pConstList syn else return []
801+ sc <- pExpr syn
799802 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
800803
801804pLambda syn = do lchar '\\'
@@ -832,12 +835,14 @@ pPi syn =
832835 symbol "->"
833836 sc <- pExpr syn
834837 return (bindList (PPi (Exp lazy st)) xt sc))
835− <|> try (do lazy <- option False (do lchar '|'; return True)
836− st <- pStatic
837− lchar '{'; xt <- tyDeclList syn; lchar '}'
838− symbol "->"
839− sc <- pExpr syn
840− return (bindList (PPi (Imp lazy st)) xt sc))
838+ <|> try (if implicitAllowed syn then
839+ do lazy <- option False (do lchar '|'; return True)
840+ st <- pStatic
841+ lchar '{'; xt <- tyDeclList syn; lchar '}'
842+ symbol "->"
843+ sc <- pExpr syn
844+ return (bindList (PPi (Imp lazy st)) xt sc)
845+ else fail "No implicit arguments allowed here")
841846 <|> try (do lchar '{'; reserved "auto"
842847 xt <- tyDeclList syn; lchar '}'
843848 symbol "->"
@@ -858,19 +863,19 @@ pPi syn =
858863
859864pConstList :: SyntaxInfo -> IParser [PTerm]
860865pConstList syn = try (do lchar '('
861− tys <- sepBy1 (pExpr' syn) (lchar ',')
866+ tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')
862867 lchar ')'
863868 reservedOp "=>"
864869 return tys)
865− <|> try (do t <- pExpr syn
870+ <|> try (do t <- pExpr (noImp syn)
866871 reservedOp "=>"
867872 return [t])
868873 <|> return []
869874
870−tyDeclList syn = try (sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))
875+tyDeclList syn = try (sepBy1 (do x <- pfName; t <- pTSig (noImp syn); return (x,t))
871876 (lchar ','))
872877 <|> do ns <- sepBy1 pName (lchar ',')
873− t <- pTSig syn
878+ t <- pTSig (noImp syn)
874879 return (map (\x -> (x, t)) ns)
875880
876881tyOptDeclList syn = sepBy1 (do x <- pfName;
@@ -978,7 +983,7 @@ accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns
978983pRecord :: SyntaxInfo -> IParser PDecl
979984pRecord syn = do acc <- pAccessibility
980985 reserved "record"; fc <- pfc
981− tyn_in <- pfName; ty <- pTSig syn
986+ tyn_in <- pfName; ty <- pTSig (impOK syn)
982987 let tyn = expandNS syn tyn_in
983988 reserved "where"
984989 open_block
@@ -1004,7 +1009,7 @@ pRecord syn = do acc <- pAccessibility
10041009pData :: SyntaxInfo -> IParser PDecl
10051010pData syn = try (do acc <- pAccessibility
10061011 reserved "data"; fc <- pfc
1007− tyn_in <- pfName; ty <- pTSig syn
1012+ tyn_in <- pfName; ty <- pTSig (impOK syn)
10081013 let tyn = expandNS syn tyn_in
10091014 reserved "where"
10101015 open_block
@@ -1044,7 +1049,7 @@ pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
10441049pConstructor syn
10451050 = do cn_in <- pfName; fc <- pfc
10461051 let cn = expandNS syn cn_in
1047− ty <- pTSig syn
1052+ ty <- pTSig (impOK syn)
10481053-- ty' <- implicit syn cn ty
10491054 return (cn, ty, fc)
10501055