@@ -55,6 +55,9 @@ strlit = PTok.stringLiteral lexer
5555chlit = PTok.charLiteral lexer
5656lchar = lexeme.char
5757
58+fixErrorMsg :: String -> [String] -> String
59+fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
60+
5861-- Loading modules
5962
6063loadModule :: FilePath -> Idris String
@@ -1193,7 +1196,18 @@ pData syn = try (do doc <- option "" (pDocComment '|')
11931196 let ty = bindArgs (map (const PSet) args) PSet
11941197 let tyn = expandNS syn tyn_in
11951198 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1196− 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+
11971211 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
11981212 pTerminator
11991213 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)