on master help sign in
possible fixes for missing type signature in data decls
441f51draichoo
src/Idris/Parser.hs+12−1
@@ -1196,7 +1196,18 @@ pData syn = try (do doc <- option "" (pDocComment '|')
1196 let ty = bindArgs (map (const PSet) args) PSet
1196 let ty = bindArgs (map (const PSet) args) PSet
1197 let tyn = expandNS syn tyn_in
1197 let tyn = expandNS syn tyn_in
1198 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1198 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1199− lchar '='
1199+ try (lchar '=') <|> do reserved "where"
1200+ let kw = (if co then "co" else "") ++ "data "
1201+ let n = show tyn_in ++ " "
1202+ let s = kw ++ n
1203+ let as = concat (intersperse " " $ map show args) ++ " "
1204+ let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Set)") . show) args)
1205+ let ss = concat (intersperse " -> " $ map (const "Set") args)
1206+ let fix1 = s ++ as ++ " = ..."
1207+ let fix2 = s ++ ": " ++ ns ++ " -> Set where\n ..."
1208+ let fix3 = s ++ ": " ++ ss ++ " -> Set where\n ..."
1209+ fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1210+
1200 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1211 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1201 pTerminator
1212 pTerminator
1202 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1213 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)