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

git.iko.soy/Idris-dev

Fix for implicits in records

Since we have this annoying distinction between top level implicits and scoped implicits, we need to make sure that things are marked appropriately. So when we parse record fields, they become scoped implicits. (I don't think there is really a need for this distinction, but because implicits were top level only at first, it's hard to unify everything. One for the next rewrite, should it ever happen, I suppose...) Fixes #2266

commit3dc90d3e14a0682d0a9ecd04eb1d93cfbaddbc24 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 13 Mar 2017, 17:14 (10 years ago) parent060c734

2 files changed+8−3

compare with master

unifiedsplit

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

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

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

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

107107 ns <- commaSeparated oneName

108108 lchar ':'

109− t <- typeExpr (allowImp syn)

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

110+ t <- typeExpr (scopedImp syn)

110111 p <- endPlicity c

111112 ist <- get

112113 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,

4646

4747-- | Disallow implicit type declarations

4848disallowImp :: SyntaxInfo -> SyntaxInfo

49−disallowImp syn = syn { implicitAllowed = False,

50− constraintAllowed = False }

49+disallowImp = scopedImp

50+

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

52+scopedImp :: SyntaxInfo -> SyntaxInfo

53+scopedImp syn = syn { implicitAllowed = False,

54+ constraintAllowed = False }

5155

5256-- | Allow scoped constraint arguments

5357allowConstr :: SyntaxInfo -> SyntaxInfo