3dc90d3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix for implicits in records

3dc90d3Edwin Brady10 years ago

src/Idris/Parser/Data.hs+2−1

@@ -106,7 +106,8 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

106 <|> (symbol "_" >> return Nothing)

107 ns <- commaSeparated oneName

108 lchar ':'

109+ -- Implicits are scoped in fields (fields aren't top level)

109− t <- typeExpr (allowImp syn)

110+ t <- typeExpr (scopedImp syn)

110 p <- endPlicity c

111 p <- endPlicity c

111 ist <- get

112 ist <- get

112 let doc' = case doc of -- Temp: Throws away any possible arg docs

113 let doc' = case doc of -- Temp: Throws away any possible arg docs

src/Idris/Parser/Expr.hs+6−2

@@ -46,8 +46,12 @@ allowImp syn = syn { implicitAllowed = True,

47-- | Disallow implicit type declarations

48disallowImp :: SyntaxInfo -> SyntaxInfo

49+disallowImp = scopedImp

50+

51+-- | Implicits hare are scoped rather than top level

52+scopedImp :: SyntaxInfo -> SyntaxInfo

49−disallowImp syn = syn { implicitAllowed = False,

53+scopedImp syn = syn { implicitAllowed = False,

50− constraintAllowed = False }

54+ constraintAllowed = False }

52-- | Allow scoped constraint arguments

56-- | Allow scoped constraint arguments

53allowConstr :: SyntaxInfo -> SyntaxInfo

57allowConstr :: SyntaxInfo -> SyntaxInfo