1054d7d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add UnknownImplicit error

Reports whether a given implicit is not an implicit argument of the function. Fixes #2279.

commit1054d7d9914ab7b8c8deb1e8e1e5c2c23aea35d6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 19 May 2015, 21:05 (11 years ago) parent309189c

11 files changed+49−10

compare with master

unifiedsplit

libs/base/Language/Reflection/Utils.idr+1 libs/prelude/Language/Reflection/Errors.idr+1 src/Idris/AbsSyntax.hs+24−7 src/Idris/AbsSyntaxTree.hs+3−2 src/Idris/Core/Binary.hs+5 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/TT.hs+2 src/Idris/Delaborate.hs+1 src/Idris/Elab/Term.hs+8−1 src/Idris/IBC.hs+2 src/Idris/Reflection.hs+1

libs/base/Language/Reflection/Utils.idr+1

@@ -291,6 +291,7 @@ instance Show Err where

291291 show UniverseError = "UniverseError"

292292 show ProgramLineComment = "ProgramLineComment"

293293 show (Inaccessible n) = "Inaccessible " ++ show n

294+ show (UnknownImplicit n f) = "UnknownImplicit " ++ show n ++ " " ++ show f

294295 show (NonCollapsiblePostulate n) = "NonCollapsiblePostulate " ++ show n

295296 show (AlreadyDefined n) = "AlreadyDefined " ++ show n

296297 show (ProofSearchFail err) = "ProofSearchFail " ++ show err

libs/prelude/Language/Reflection/Errors.idr+1

@@ -36,6 +36,7 @@ data Err = Msg String

3636 | UniverseError

3737 | ProgramLineComment

3838 | Inaccessible TTName

39+ | UnknownImplicit TTName TTName

3940 | NonCollapsiblePostulate TTName

4041 | AlreadyDefined TTName

4142 | ProofSearchFail Err

src/Idris/AbsSyntax.hs+24−7

@@ -1622,7 +1622,13 @@ addImpl' inpat env infns imp_meths ist ptm

16221622-- if in a pattern, and there are no arguments, and there's no possible

16231623-- names with zero explicit arguments, don't add implicits.

16241624

1625−aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> FC -> [[T.Text]] -> [PArg] -> Either Err PTerm

1625+aiFn :: Bool -> Bool -> Bool

1626+ -> [Name]

1627+ -> IState -> FC

1628+ -> Name -- ^ function being applied

1629+ -> FC -> [[T.Text]]

1630+ -> [PArg] -> -- ^ initial arguments

1631+ Either Err PTerm

16261632aiFn inpat True qq imp_meths ist fc f ffc ds []

16271633 = case lookupDef f (tt_ctxt ist) of

16281634 [] -> Right $ PPatvar ffc f

@@ -1685,8 +1691,20 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as

16851691 Just (n,t) -> t

16861692 _ -> Public

16871693

1688− insertImpl :: [PArg] -> [PArg] -> [PArg]

1689− insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not . exp) as)

1694+ insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)

1695+ -> [PArg] -- ^ given arguments

1696+ -> [PArg]

1697+ insertImpl ps as

1698+ = let (as', badimpls) = partition (impIn ps) as in

1699+ map addUnknownImp badimpls ++

1700+ insImpAcc M.empty ps (filter exp as') (filter (not . exp) as')

1701+

1702+ -- return True if the second argument is an implicit argument which is

1703+ -- expected in the implicits, or if it's not an implicit

1704+ impIn :: [PArg] -> PArg -> Bool

1705+ impIn ps (PExp _ _ _ _) = True

1706+ impIn ps (PConstraint _ _ _ _) = True

1707+ impIn ps arg = any (\p -> pname arg == pname p) ps

16901708

16911709 exp (PExp _ _ _ _) = True

16921710 exp (PConstraint _ _ _ _) = True

@@ -1723,12 +1741,11 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as

17231741 insImpAcc (M.insert n Placeholder pnas) ps given imps

17241742 else PTacImplicit p l n sc sc :

17251743 insImpAcc (M.insert n sc pnas) ps given imps

1726− insImpAcc _ expected [] imps = imps -- so that unused implicits give error

1727− -- TODO: report here, and prune alternatives

1728− -- Issue #1740 in the Issue Tracker

1729−-- https://github.com/idris-lang/Idris-dev/issues/1740

1744+ insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error

17301745 insImpAcc _ _ given imps = given ++ imps

17311746

1747+ addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }

1748+

17321749 find n [] acc = Nothing

17331750 find n (PImp _ _ _ n' t : gs) acc

17341751 | n == n' = Just (t, reverse acc ++ gs)

src/Idris/AbsSyntaxTree.hs+3−2

@@ -987,7 +987,8 @@ type PDo = PDo' PTerm

987987data PArg' t = PImp { priority :: Int,

988988 machine_inf :: Bool, -- true if the machine inferred it

989989 argopts :: [ArgOpt],

990− pname :: Name, getTm :: t }

990+ pname :: Name,

991+ getTm :: t }

991992 | PExp { priority :: Int,

992993 argopts :: [ArgOpt],

993994 pname :: Name,

@@ -1003,7 +1004,7 @@ data PArg' t = PImp { priority :: Int,

10031004 getTm :: t }

10041005 deriving (Show, Eq, Functor, Data, Typeable)

10051006

1006−data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg

1007+data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp

10071008 deriving (Show, Eq, Data, Typeable)

10081009

10091010instance Sized a => Sized (PArg' a) where

src/Idris/Core/Binary.hs+5

@@ -179,6 +179,9 @@ instance Binary a => Binary (Err' a) where

179179 put t

180180 put (ElabScriptStuck x1) = do putWord8 39

181181 put x1

182+ put (UnknownImplicit n f) = do putWord8 40

183+ put n

184+ put f

182185

183186 get = do i <- getWord8

184187 case i of

@@ -246,6 +249,8 @@ instance Binary a => Binary (Err' a) where

246249 return (InvalidTCArg x1 x2)

247250 39 -> do x1 <- get

248251 return (ElabScriptStuck x1)

252+ 40 -> do x <- get ; y <- get

253+ return $ UnknownImplicit x y

249254 _ -> error "Corrupted binary data for Err'"

250255----- Generated by 'derive'

251256

src/Idris/Core/DeepSeq.hs+1

@@ -98,6 +98,7 @@ instance NFData Err where

9898 rnf (UniverseError x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

9999 rnf ProgramLineComment = ()

100100 rnf (Inaccessible x1) = rnf x1 `seq` ()

101+ rnf (UnknownImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

101102 rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()

102103 rnf (AlreadyDefined x1) = rnf x1 `seq` ()

103104 rnf (ProofSearchFail x1) = rnf x1 `seq` ()

src/Idris/Core/TT.hs+2

@@ -231,6 +231,7 @@ data Err' t

231231 | UniqueKindError Universe Name

232232 | ProgramLineComment

233233 | Inaccessible Name

234+ | UnknownImplicit Name Name

234235 | CantMatch t

235236 | NonCollapsiblePostulate Name

236237 | AlreadyDefined Name

@@ -332,6 +333,7 @@ instance Show Err where

332333 show e ++ " in " ++ show sc ++ " " ++ show i

333334 show (CantSolveGoal g _) = "CantSolve " ++ show g

334335 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

336+ show (UnknownImplicit n f) = show n ++ " is not an implicit argument of " ++ show f

335337 show (ProviderError msg) = "Type provider error: " ++ msg

336338 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e

337339 show ProgramLineComment = "Program line next to comment"

src/Idris/Delaborate.hs+1

@@ -338,6 +338,7 @@ pprintErr' i (UniqueKindError k n) = text "Constructor" <+> annName' n (showbasi

338338 <+> text "but the data type does not"

339339pprintErr' i ProgramLineComment = text "Program line next to comment"

340340pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"

341+pprintErr' i (UnknownImplicit n f) = annName n <+> text "is not an implicit argument of" <+> annName f

341342pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>

342343 annName n <+> text "is not collapsible"

343344pprintErr' i (AlreadyDefined n) = annName n<+>

src/Idris/Elab/Term.hs+8−1

@@ -708,6 +708,7 @@ elab ist info emode opts fn tm

708708 ctxt <- get_context

709709 annot <- findHighlight f

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

711+ mapM_ checkKnownImplicit args

711712 let unmatchableArgs = if pattern

712713 then getUnmatchable (tt_ctxt ist) f

713714 else []

@@ -715,6 +716,7 @@ elab ist info emode opts fn tm

715716 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

716717 && isTConName f (tt_ctxt ist)) $

717718 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

719+-- trace (show (f, args_in, args)) $

718720 if (f `elem` map fst env && length args == 1 && length args_in == 1)

719721 then -- simple app, as below

720722 do simple_app False

@@ -805,7 +807,12 @@ elab ist info emode opts fn tm

805807 [] -> return ()

806808 es -> do put s

807809 elab' ina topfc (PAppImpl tm es)

808−

810+

811+ checkKnownImplicit imp

812+ | UnknownImp `elem` argopts imp

813+ = lift $ tfail $ UnknownImplicit (pname imp) f

814+ checkKnownImplicit _ = return ()

815+

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

810817 = i : getReqImps sc

811818 getReqImps _ = []

src/Idris/IBC.hs+2

@@ -1071,12 +1071,14 @@ instance Binary ArgOpt where

10711071 HideDisplay -> putWord8 0

10721072 InaccessibleArg -> putWord8 1

10731073 AlwaysShow -> putWord8 2

1074+ UnknownImp -> putWord8 3

10741075 get

10751076 = do i <- getWord8

10761077 case i of

10771078 0 -> return HideDisplay

10781079 1 -> return InaccessibleArg

10791080 2 -> return AlwaysShow

1081+ 3 -> return UnknownImp

10801082 _ -> error "Corrupted binary data for Static"

10811083

10821084instance Binary Static where

src/Idris/Reflection.hs+1

@@ -853,6 +853,7 @@ reflectErr (UniverseError fc ue old new tys) =

853853 Var $ reflErrName "UniverseError"

854854reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

855855reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

856+reflectErr (UnknownImplicit n f) = raw_apply (Var $ reflErrName "UnknownImplicit") [reflectName n, reflectName f]

856857reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]

857858reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]

858859reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]