@@ -77,7 +77,8 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
77 _ -> addImplementation intImpl False n iname
77 _ -> addImplementation intImpl False n iname
79 ist <- getIState
79 ist <- getIState
80+ when (isNothing expn) $
80− checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
81+ checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
82 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do
83 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do
83 -- Add the parent implementation names to the privileged set
84 -- Add the parent implementation names to the privileged set