git.iko.soy/Idris-dev
on master help sign in
Fix implementation argument check

We weren't rejecting lambdas, which meant that implementations were being accepted that had no chance of working. Fixes #3700

commitcf5ab6b3aa719a8674c0535dba76a25eb97080b5 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 31 Mar 2017, 15:31 (10 years ago) parent3e4752f
3 files changed+7−22
compare with master
unifiedsplit
src/Idris/Elab/Implementation.hs+6−5 test/reg027/expected−1 test/reg027/reg027.idr+1−16
src/Idris/Elab/Implementation.hs+6−5
@@ -99,6 +99,10 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
9999 (map fst $ interface_implementations ci)
100100 addImplementation intImpl True n iname
101101 _ -> addImplementation intImpl False n iname
102+
103+ ist <- getIState
104+ checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
105+
102106 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do
103107 -- Add the parent implementation names to the privileged set
104108 oldOpen <- addOpenImpl parents
@@ -212,7 +216,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
212216 setOpenImpl oldOpen
213217-- totalityCheckBlock
214218
215− checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
216219 addIBC (IBCImplementation intImpl (isNothing expn) n iname)
217220
218221 where
@@ -243,9 +246,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
243246 (_:_) -> return True
244247 _ -> return False -- couldn't find interface, just let elabImplementation fail later
245248
246− -- TODO: largely based upon elabType' - should try to abstract
247− -- Issue #1614 in the issue tracker:
248− -- https://github.com/idris-lang/Idris-dev/issues/1614
249249 elabFindOverlapping i ci iname syn t
250250 = do ty' <- addUsingConstraints syn fc t
251251 -- TODO think: something more in info?
@@ -506,7 +506,8 @@ checkInjectiveArgs fc n ds (Just ty)
506506 isInj i (P _ n _) = isConName n (tt_ctxt i)
507507 isInj i (App _ f a) = isInj i f && isInj i a
508508 isInj i (V _) = True
509− isInj i (Bind n b sc) = isInj i sc
509+ isInj i (Bind n b@(Pi{}) sc) = isInj i (binderTy b) && isInj i sc
510+ isInj i (Bind n b sc) = False
510511 isInj _ _ = True
511512
512513 instantiateRetTy (Bind n (Pi _ _ _ _) sc)
test/reg027/expected−1
@@ -1,3 +1,2 @@
11<<int fn>>
2−6
32reg027a.idr:9:16:Overlapping implementation: Show (Int -> a) already defined
test/reg027/reg027.idr+1−16
@@ -9,24 +9,9 @@ implementation Show (Char -> b) where
99IntFn : Type -> Type
1010IntFn = \x => Int -> x
1111
12−implementation Functor IntFn where -- (\x => Int -> x) where
13− map f intf = \x => f (intf x)
14−
15−implementation Applicative (\x => Int -> x) where
16− pure v = \x => v
17− (<*>) f a = \x => f x (a x)
18−
19−implementation Monad IntFn where
20− f >>= k = \x => k (f x) x
21−
2212dbl : IntFn Int
2313dbl x = x * 2
2414
25−foo : Int -> String
26−foo = do val <- dbl
27− \x => show val
28−
2915main : IO ()
30−main = do printLn dbl
31− putStrLn (foo 3)
16+main = printLn dbl
3217