Ensure only injectivity if not named
commit631816842018e74485845a7ab508fa59b2dae275
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateWed 8 Nov 2017, 15:30 (9 years ago)
parent683be9b
src/Idris/Elab/Implementation.hs+2−1
@@ -77,7 +77,8 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
7777 _ -> addImplementation intImpl False n iname
7878
7979 ist <- getIState
80− checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
80+ when (isNothing expn) $
81+ checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
8182
8283 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do
8384 -- Add the parent implementation names to the privileged set