264b67f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

More restrictive automated addition of implicit arguments

Only added automatically if they begin with a lower case letter, or appear in a using block. Apologies for breaking code: however, this catches a common class of error which causes confusing (but correct) typechecker behaviour.

commit264b67ffd739e32772208a2bb8d6d96166dba228 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 30 Oct 2012, 20:20 (14 years ago) parent895b323

1 file changed+6−2

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+6−2

src/Idris/AbsSyntax.hs+6−2

@@ -621,7 +621,8 @@ implicit' syn ignore n ptm

621621implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])

622622implicitise syn ignore ist tm

623623 = let (declimps, ns') = execState (imps True [] tm) ([], [])

624− ns = ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in

624+ ns = filter (\n -> implicitable n || elem n (map fst uvars)) $

625+ ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in

625626 if null ns

626627 then (tm, reverse declimps)

627628 else implicitise syn ignore ist (pibind uvars ns tm)

@@ -700,7 +701,10 @@ implicitise syn ignore ist tm

700701 pibind using (n:ns) sc

701702 = case lookup n using of

702703 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)

703− Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)

704+ Nothing -> if (implicitable n)

705+ then PPi (Imp False Dynamic) n Placeholder

706+ (pibind using ns sc)

707+ else pibind using ns sc

704708

705709-- Add implicit arguments in function calls

706710addImplPat :: IState -> PTerm -> PTerm