319582e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Elaborate lhs of pattern clause properly in implicit arguments

319582eEdwin Brady14 years ago

src/Idris/ElabTerm.hs+5−2

@@ -151,8 +151,11 @@ elab ist info pattern tcgen fn tm

151 showHd x = show x

152 elab' ina (PAlternative False as)

153 = trySeq as

154− where trySeq [] = fail "All alternatives fail to elaborate"

154+ where -- if none work, take the error from the first

155+ trySeq (x : xs) = let e1 = elab' ina x in

156+ try e1 (trySeq' e1 xs)

157+ trySeq' deferr [] = deferr

155− trySeq (x : xs) = try (elab' ina x) (trySeq xs)

158+ trySeq' deferr (x : xs) = try (elab' ina x) (trySeq' deferr xs)

156 elab' ina (PPatvar fc n) | pattern = patvar n

159 elab' ina (PPatvar fc n) | pattern = patvar n

157 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

160 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

158 = do ctxt <- get_context

161 = do ctxt <- get_context

src/Idris/Parser.hs+2−2

@@ -1259,7 +1259,7 @@ pClause syn

1259 = try (do pushIndent

1260 n_in <- pfName; let n = expandNS syn n_in

1261 cargs <- many (pConstraintArg syn)

1262− iargs <- many (pImplicitArg syn)

1262+ iargs <- many (pImplicitArg (syn { inPattern = True } ))

1263 fc <- pfc

1264 args <- many (pArgExpr syn)

1265 wargs <- many (pWExpr syn)

@@ -1297,7 +1297,7 @@ pClause syn

1297 <|> try (do pushIndent

1298 n_in <- pfName; let n = expandNS syn n_in

1299 cargs <- many (pConstraintArg syn)

1300− iargs <- many (pImplicitArg syn)

1300+ iargs <- many (pImplicitArg (syn { inPattern = True } ))

1301 fc <- pfc

1302 args <- many (pArgExpr syn)

1303 wargs <- many (pWExpr syn)