c5be396 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Another scoped implicit fix

When checking that an implicit argument exists, we need to do this after inserting scoped implicits, not before, in case more arise by expanding types.

commitc5be396e272fb88c9bea570942d13a0f3602f08f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 16 Mar 2017, 11:31 (10 years ago) parentc37ab25

2 files changed+32−18

compare with master

unifiedsplit

src/Idris/Elab/Term.hs+31−17 test/interactive010/expected+1−1

src/Idris/Elab/Term.hs+31−17

@@ -853,8 +853,10 @@ elab ist info emode opts fn tm

853853 ctxt <- get_context

854854 let dataCon = isDConName f ctxt

855855 annot <- findHighlight f

856− mapM_ checkKnownImplicit args_in

857− let args = insertScopedImps fc (normalise ctxt env fty) args_in

856+ knowns_m <- mapM getKnownImplicit args_in

857+ let knowns = mapMaybe id knowns_m

858+ args <- insertScopedImps fc f knowns (normalise ctxt env fty) args_in

859+

858860 let unmatchableArgs = if pattern

859861 then getUnmatchable (tt_ctxt ist) f

860862 else []

@@ -959,10 +961,10 @@ elab ist info emode opts fn tm

959961 es -> do put s

960962 elab' ina topfc (PAppImpl tm es)

961963

962− checkKnownImplicit imp

964+ getKnownImplicit imp

963965 | UnknownImp `elem` argopts imp

964− = lift $ tfail $ UnknownImplicit (pname imp) f

965− checkKnownImplicit _ = return ()

966+ = return Nothing -- lift $ tfail $ UnknownImplicit (pname imp) f

967+ | otherwise = return (Just (pname imp))

966968

967969 getReqImps (Bind x (Pi _ (Just i) ty _) sc)

968970 = i : getReqImps sc

@@ -1519,17 +1521,29 @@ elab ist info emode opts fn tm

15191521 findImplicit n (x : xs) = let (arg, rest) = findImplicit n xs in

15201522 (arg, x : rest)

15211523

1522− insertScopedImps fc ty@(Bind n (Pi _ im@(Just i) _ _) sc) xs

1523− | (Just arg, xs') <- findImplicit n xs,

1524− not (toplevel_imp i)

1525− = arg : insertScopedImps fc sc xs'

1526− | tcimplementation i && not (toplevel_imp i)

1527− = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs

1528− | not (toplevel_imp i)

1529− = pimp n Placeholder True : insertScopedImps fc sc xs

1530− insertScopedImps fc (Bind n (Pi _ _ _ _) sc) (x : xs)

1531− = x : insertScopedImps fc sc xs

1532− insertScopedImps _ ty xs = xs

1524+ insertScopedImps :: FC -> Name -> [Name] -> Type -> [PArg] -> ElabD [PArg]

1525+ insertScopedImps fc f knowns ty xs =

1526+ do mapM_ (checkKnownImplicit (map fst (getArgTys ty) ++ knowns)) xs

1527+ doInsert ty xs

1528+ where

1529+ doInsert ty@(Bind n (Pi _ im@(Just i) _ _) sc) xs

1530+ | (Just arg, xs') <- findImplicit n xs,

1531+ not (toplevel_imp i)

1532+ = liftM (arg :) (doInsert sc xs')

1533+ | tcimplementation i && not (toplevel_imp i)

1534+ = liftM (pimp n (PResolveTC fc) True :) (doInsert sc xs)

1535+ | not (toplevel_imp i)

1536+ = liftM (pimp n Placeholder True :) (doInsert sc xs)

1537+ doInsert (Bind n (Pi _ _ _ _) sc) (x : xs)

1538+ = liftM (x :) (doInsert sc xs)

1539+ doInsert ty xs = return xs

1540+

1541+ -- Any implicit in the application needs to have the name of a

1542+ -- scoped implicit or a top level implicit, otherwise report an error

1543+ checkKnownImplicit ns imp@(PImp{})

1544+ | pname imp `elem` ns = return ()

1545+ | otherwise = lift $ tfail $ At fc $ UnknownImplicit (pname imp) f

1546+ checkKnownImplicit ns _ = return ()

15331547

15341548 insertImpLam ina t =

15351549 do ty <- goal

@@ -1570,7 +1584,7 @@ elab ist info emode opts fn tm

15701584 do fty <- get_type (Var n) -- check for implicits

15711585 ctxt <- get_context

15721586 env <- get_env

1573− let a' = insertScopedImps fc (normalise ctxt env fty) []

1587+ a' <- insertScopedImps fc n [] (normalise ctxt env fty) []

15741588 if null a'

15751589 then erun fc $

15761590 do apply (Var n) []

test/interactive010/expected+1−1

@@ -1,6 +1,6 @@

11Prelude.List.(++) : List a -> List a -> List a

22Prelude.Strings.(++) : String -> String -> String

3−a is not an implicit argument of Prelude.Interfaces./

3+(input):1:11:a is not an implicit argument of Prelude.Interfaces./

44Usage is :doc <functionname>

55Usage is :wc <functionname>

66Usage is :printdef <functionname>