git.iko.soy/Idris-dev
on master help sign in
Fix implementation argument check
cf5ab6bEdwin Brady
src/Idris/Elab/Implementation.hs+6−5
compare with master
unifiedsplit
@@ -99,6 +99,10 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
99 (map fst $ interface_implementations ci)
99 (map fst $ interface_implementations ci)
100 addImplementation intImpl True n iname
100 addImplementation intImpl True n iname
101 _ -> addImplementation intImpl False n iname
101 _ -> addImplementation intImpl False n iname
102+
103+ ist <- getIState
104+ checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
105+
102 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do
106 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do
103 -- Add the parent implementation names to the privileged set
107 -- Add the parent implementation names to the privileged set
104 oldOpen <- addOpenImpl parents
108 oldOpen <- addOpenImpl parents
@@ -212,7 +216,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
212 setOpenImpl oldOpen
216 setOpenImpl oldOpen
213-- totalityCheckBlock
217-- totalityCheckBlock
214
218
215− checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
216 addIBC (IBCImplementation intImpl (isNothing expn) n iname)
219 addIBC (IBCImplementation intImpl (isNothing expn) n iname)
217
220
218 where
221 where
@@ -243,9 +246,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
243 (_:_) -> return True
246 (_:_) -> return True
244 _ -> return False -- couldn't find interface, just let elabImplementation fail later
247 _ -> return False -- couldn't find interface, just let elabImplementation fail later
245
248
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
249 elabFindOverlapping i ci iname syn t
249 elabFindOverlapping i ci iname syn t
250 = do ty' <- addUsingConstraints syn fc t
250 = do ty' <- addUsingConstraints syn fc t
251 -- TODO think: something more in info?
251 -- TODO think: something more in info?
@@ -506,7 +506,8 @@ checkInjectiveArgs fc n ds (Just ty)
506 isInj i (P _ n _) = isConName n (tt_ctxt i)
506 isInj i (P _ n _) = isConName n (tt_ctxt i)
507 isInj i (App _ f a) = isInj i f && isInj i a
507 isInj i (App _ f a) = isInj i f && isInj i a
508 isInj i (V _) = True
508 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
510 isInj _ _ = True
511 isInj _ _ = True
511
512
512 instantiateRetTy (Bind n (Pi _ _ _ _) sc)
513 instantiateRetTy (Bind n (Pi _ _ _ _) sc)
test/reg027/expected−1
@@ -1,3 +1,2 @@
1<<int fn>>
1<<int fn>>
2−6
3reg027a.idr:9:16:Overlapping implementation: Show (Int -> a) already defined
2reg027a.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
9IntFn : Type -> Type
9IntFn : Type -> Type
10IntFn = \x => Int -> x
10IntFn = \x => Int -> x
11
11
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−
22dbl : IntFn Int
12dbl : IntFn Int
23dbl x = x * 2
13dbl x = x * 2
24
14
25−foo : Int -> String
26−foo = do val <- dbl
27− \x => show val
28−
29main : IO ()
15main : IO ()
30−main = do printLn dbl
16+main = printLn dbl
31− putStrLn (foo 3)
32
17